Loogle!

Result

Found 97 declarations mentioning CategoryTheory.Limits.HasProductsOfShape.

• CategoryTheory.Limits.HasProductsOfShape 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (β : Type v) (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : Prop
• CategoryTheory.Limits.hasProductsOfShape_of_hasProducts 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] (J : Type w) : CategoryTheory.Limits.HasProductsOfShape J C
• CategoryTheory.Limits.Pi.functor 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] : CategoryTheory.Functor (α → C) C
• CategoryTheory.Limits.Pi.functor_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] (f : α → C) : (CategoryTheory.Limits.Pi.functor α).obj f = ∏ᶜ f
• CategoryTheory.Limits.Pi.mapIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ≅ g b) : ∏ᶜ f ≅ ∏ᶜ g
• CategoryTheory.Limits.Pi.functorπ 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] (a : α) : CategoryTheory.Limits.Pi.functor α ⟶ CategoryTheory.Pi.eval (fun x => C) a
• CategoryTheory.Limits.Pi.functorπ_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] (a : α) (f : α → C) : (CategoryTheory.Limits.Pi.functorπ a).app f = CategoryTheory.Limits.Pi.π f a
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] : (CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.comp CategoryTheory.Limits.lim ≅ CategoryTheory.Limits.Pi.functor α
• CategoryTheory.Limits.Pi.functor_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] {f g : α → C} (t : f ⟶ g) : (CategoryTheory.Limits.Pi.functor α).map t = CategoryTheory.Limits.Pi.map t
• CategoryTheory.Limits.Pi.map_isIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ⟶ g b) [∀ (b : β), CategoryTheory.IsIso (p b)] : CategoryTheory.IsIso (CategoryTheory.Limits.Pi.map p)
• CategoryTheory.Limits.Pi.constCompPiIsoConst 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] {I : α → Type u_1} [(i : α) → CategoryTheory.Category.{v_1, u_1} (I i)] (X : α → C) : (CategoryTheory.Functor.pi fun i => (CategoryTheory.Functor.const (I i)).obj (X i)).comp (CategoryTheory.Limits.Pi.functor α) ≅ (CategoryTheory.Functor.const ((i : α) → I i)).obj (∏ᶜ X)
• CategoryTheory.Limits.Pi.mapIso_hom_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.mapIso p).hom (CategoryTheory.Limits.Pi.π g b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) (p b).hom
• CategoryTheory.Limits.Pi.mapIso_inv_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.mapIso p).inv (CategoryTheory.Limits.Pi.π f b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π g b) (p b).inv
• CategoryTheory.Limits.Pi.mapIso_hom_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) {Z : C} (h : g b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.mapIso p).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π g b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) (CategoryTheory.CategoryStruct.comp (p b).hom h)
• CategoryTheory.Limits.Pi.mapIso_inv_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) {Z : C} (h : f b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.mapIso p).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π g b) (CategoryTheory.CategoryStruct.comp (p b).inv h)
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] (X : α → C) : (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim α).hom.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit (CategoryTheory.Discrete.functor X))
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] (X : α → C) : (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim α).inv.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit (CategoryTheory.Discrete.functor X))
• CategoryTheory.Limits.Pi.constCompPiIsoConst_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] {I : α → Type u_1} [(i : α) → CategoryTheory.Category.{v_1, u_1} (I i)] (X : α → C) (X✝ : (i : α) → I i) : (CategoryTheory.Limits.Pi.constCompPiIsoConst X).hom.app X✝ = CategoryTheory.CategoryStruct.id (∏ᶜ fun i => X i)
• CategoryTheory.Limits.Pi.constCompPiIsoConst_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] {I : α → Type u_1} [(i : α) → CategoryTheory.Category.{v_1, u_1} (I i)] (X : α → C) (X✝ : (i : α) → I i) : (CategoryTheory.Limits.Pi.constCompPiIsoConst X).inv.app X✝ = CategoryTheory.CategoryStruct.id (∏ᶜ fun i => X i)
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim_comp_functorπ 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] (a : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim α).hom (CategoryTheory.Limits.Pi.functorπ a) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.whiskerLeft (CategoryTheory.Limits.lim.π { as := a })) (CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso C a).hom
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim_comp_functorπ_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] (a : α) {Z : CategoryTheory.Functor (α → C) C} (h : CategoryTheory.Pi.eval (fun x => C) a ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim α).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.functorπ a) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.whiskerLeft (CategoryTheory.Limits.lim.π { as := a })) (CategoryTheory.CategoryStruct.comp (CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso C a).hom h)
• CategoryTheory.Limits.hasProductsOfShape_of_hasBiproductsOfShape 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} (C : Type uC) [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBiproductsOfShape J C] : CategoryTheory.Limits.HasProductsOfShape J C
• CategoryTheory.Limits.hasCoproductsOfShape_of_opposite 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : Type v₂) [CategoryTheory.Limits.HasProductsOfShape X Cᵒᵖ] : CategoryTheory.Limits.HasCoproductsOfShape X C
• CategoryTheory.Limits.hasCoproductsOfShape_opposite 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : Type v₂) [CategoryTheory.Limits.HasProductsOfShape X C] : CategoryTheory.Limits.HasCoproductsOfShape X Cᵒᵖ
• CategoryTheory.Limits.hasProductsOfShape_of_opposite 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : Type v₂) [CategoryTheory.Limits.HasCoproductsOfShape X Cᵒᵖ] : CategoryTheory.Limits.HasProductsOfShape X C
• CategoryTheory.Limits.hasProductsOfShape_opposite 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : Type v₂) [CategoryTheory.Limits.HasCoproductsOfShape X C] : CategoryTheory.Limits.HasProductsOfShape X Cᵒᵖ
• CategoryTheory.Limits.instHasProductsOfShapeOfHasCountableProductsOfCountable 📋 Mathlib.CategoryTheory.Limits.Shapes.Countable
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCountableProducts C] (J : Type u_3) [Countable J] : CategoryTheory.Limits.HasProductsOfShape J C
• CategoryTheory.Limits.HasCountableProducts.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Countable
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (out : ∀ (J : Type) [Countable J], CategoryTheory.Limits.HasProductsOfShape J C) : CategoryTheory.Limits.HasCountableProducts C
• CategoryTheory.Limits.HasCountableProducts.out 📋 Mathlib.CategoryTheory.Limits.Shapes.Countable
  {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.Limits.HasCountableProducts C] (J : Type) [Countable J] : CategoryTheory.Limits.HasProductsOfShape J C
• CategoryTheory.Limits.hasProductsOfShape_of_small 📋 Mathlib.CategoryTheory.Limits.EssentiallySmall
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (β : Type w₂) [Small.{w₁, w₂} β] [CategoryTheory.Limits.HasProducts C] : CategoryTheory.Limits.HasProductsOfShape β C
• CategoryTheory.Limits.IsIPCOfShape 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  (ι : Type u_3) (C : Type u_4) [CategoryTheory.Category.{v_2, u_4} C] [CategoryTheory.Limits.HasProductsOfShape ι C] : Prop
• CategoryTheory.Limits.instIsIPCOfShapeOfIsIPCOfSmall 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasProducts C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v_1, u_1} C] [CategoryTheory.Limits.IsIPC C] (ι : Type u_3) [Small.{w, u_3} ι] [CategoryTheory.Limits.HasProductsOfShape ι C] : CategoryTheory.Limits.IsIPCOfShape.{w, u_3, v_1, u_1} ι C
• CategoryTheory.Limits.IsIPCOfShape.of_equiv 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} [CategoryTheory.Limits.HasProductsOfShape ι C] {ι' : Type u_3} [CategoryTheory.Limits.HasProductsOfShape ι' C] [CategoryTheory.Limits.IsIPCOfShape.{w, u_2, v_1, u_1} ι C] (e : ι ≃ ι') : CategoryTheory.Limits.IsIPCOfShape.{w, u_3, v_1, u_1} ι' C
• CategoryTheory.Limits.pointwiseProduct 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] [CategoryTheory.Limits.HasProductsOfShape α C] (F : (i : α) → CategoryTheory.Functor (I i) C) : CategoryTheory.Functor ((i : α) → I i) C
• CategoryTheory.Limits.instIsIPCOfShapeFunctorOfHasFilteredColimitsOfSize 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] (ι : Type u_1) [CategoryTheory.Limits.HasProductsOfShape ι C] [CategoryTheory.Limits.IsIPCOfShape.{w, u_1, v, u} ι C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] : CategoryTheory.Limits.IsIPCOfShape.{w, u_1, max u₁ v, max (max (max u u₁) v) v₁} ι (CategoryTheory.Functor D C)
• CategoryTheory.Limits.coconePointwiseProduct 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] [CategoryTheory.Limits.HasProductsOfShape α C] {F : (i : α) → CategoryTheory.Functor (I i) C} (c : (i : α) → CategoryTheory.Limits.Cocone (F i)) : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pointwiseProduct F)
• CategoryTheory.Limits.IsIPCOfShape.mk 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {ι : Type u_3} {C : Type u_4} [CategoryTheory.Category.{v_2, u_4} C] [CategoryTheory.Limits.HasProductsOfShape ι C] (nonempty_isColimit : ∀ ⦃J : ι → Type w⦄ [inst : (i : ι) → CategoryTheory.SmallCategory (J i)] [∀ (i : ι), CategoryTheory.IsFiltered (J i)] ⦃F : (i : ι) → CategoryTheory.Functor (J i) C⦄ ⦃c : (i : ι) → CategoryTheory.Limits.Cocone (F i)⦄ (a : (i : ι) → CategoryTheory.Limits.IsColimit (c i)), Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconePointwiseProduct c))) : CategoryTheory.Limits.IsIPCOfShape.{w, u_3, v_2, u_4} ι C
• CategoryTheory.Limits.IsIPCOfShape.nonempty_isColimit 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {ι : Type u_3} {C : Type u_4} {inst✝ : CategoryTheory.Category.{v_2, u_4} C} {inst✝¹ : CategoryTheory.Limits.HasProductsOfShape ι C} [self : CategoryTheory.Limits.IsIPCOfShape.{w, u_3, v_2, u_4} ι C] ⦃J : ι → Type w⦄ [(i : ι) → CategoryTheory.SmallCategory (J i)] [∀ (i : ι), CategoryTheory.IsFiltered (J i)] ⦃F : (i : ι) → CategoryTheory.Functor (J i) C⦄ ⦃c : (i : ι) → CategoryTheory.Limits.Cocone (F i)⦄ : ∀ (a : (i : ι) → CategoryTheory.Limits.IsColimit (c i)), Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconePointwiseProduct c))
• CategoryTheory.Limits.coconePointwiseProduct_pt 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] [CategoryTheory.Limits.HasProductsOfShape α C] {F : (i : α) → CategoryTheory.Functor (I i) C} (c : (i : α) → CategoryTheory.Limits.Cocone (F i)) : (CategoryTheory.Limits.coconePointwiseProduct c).pt = ∏ᶜ fun i => (c i).pt
• CategoryTheory.Limits.IsIPCOfShape.of_forall_exists 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} [CategoryTheory.Limits.HasProductsOfShape ι C] (H : ∀ ⦃J : ι → Type w⦄ [inst : (i : ι) → CategoryTheory.SmallCategory (J i)] [∀ (i : ι), CategoryTheory.IsFiltered (J i)] (F : (i : ι) → CategoryTheory.Functor (J i) C) [∀ (i : ι), CategoryTheory.Limits.HasColimit (F i)], ∃ c x, Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconePointwiseProduct c))) : CategoryTheory.Limits.IsIPCOfShape.{w, u_2, v_1, u_1} ι C
• CategoryTheory.Limits.coconePointwiseProductIso 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] [CategoryTheory.Limits.HasProductsOfShape α C] (F : (i : α) → CategoryTheory.Functor (I i) C) {c c' : (i : α) → CategoryTheory.Limits.Cocone (F i)} (e : (i : α) → c i ≅ c' i) : CategoryTheory.Limits.coconePointwiseProduct c ≅ CategoryTheory.Limits.coconePointwiseProduct c'
• CategoryTheory.Limits.instIsIsoColimitPointwiseProductToProductColimitOfIsIPCOfShapeOfIsFiltered 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} [CategoryTheory.Limits.HasProductsOfShape ι C] [CategoryTheory.Limits.IsIPCOfShape.{w, u_2, v_1, u_1} ι C] {J : ι → Type w} [(i : ι) → CategoryTheory.SmallCategory (J i)] [∀ (i : ι), CategoryTheory.IsFiltered (J i)] (F : (i : ι) → CategoryTheory.Functor (J i) C) [∀ (i : ι), CategoryTheory.Limits.HasColimit (F i)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pointwiseProduct F)] : CategoryTheory.IsIso (CategoryTheory.Limits.colimitPointwiseProductToProductColimit F)
• CategoryTheory.Limits.colimitPointwiseProductToProductColimit 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] [CategoryTheory.Limits.HasProductsOfShape α C] (F : (i : α) → CategoryTheory.Functor (I i) C) [∀ (i : α), CategoryTheory.Limits.HasColimit (F i)] [CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.pi F).comp (CategoryTheory.Limits.Pi.functor α))] : CategoryTheory.Limits.colimit (CategoryTheory.Limits.pointwiseProduct F) ⟶ ∏ᶜ fun s => CategoryTheory.Limits.colimit (F s)
• CategoryTheory.Limits.IsIPCOfShape.of_isIso 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} [CategoryTheory.Limits.HasProductsOfShape ι C] (H : ∀ (J : ι → Type w) [inst : (i : ι) → CategoryTheory.SmallCategory (J i)] [∀ (i : ι), CategoryTheory.IsFiltered (J i)] (F : (i : ι) → CategoryTheory.Functor (J i) C) [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasColimit (F i)], ∃ (x : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pointwiseProduct F)), CategoryTheory.IsIso (CategoryTheory.Limits.colimitPointwiseProductToProductColimit F)) : CategoryTheory.Limits.IsIPCOfShape.{w, u_2, v_1, u_1} ι C
• CategoryTheory.Limits.Pi.equivalenceOfEquivCompPointwiseProduct 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] [CategoryTheory.Limits.HasProductsOfShape α C] (F : (i : α) → CategoryTheory.Functor (I i) C) {β : Type u_3} (f : β ≃ α) [CategoryTheory.Limits.HasProductsOfShape β C] : (CategoryTheory.Pi.equivalenceOfEquiv I f).inverse.comp (CategoryTheory.Limits.pointwiseProduct fun i => F (f i)) ≅ CategoryTheory.Limits.pointwiseProduct F
• CategoryTheory.Limits.ι_colimitPointwiseProductToProductColimit_π 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] [CategoryTheory.Limits.HasProductsOfShape α C] (F : (i : α) → CategoryTheory.Functor (I i) C) [∀ (i : α), CategoryTheory.Limits.HasColimit (F i)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pointwiseProduct F)] (k : (i : α) → I i) (s : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.pointwiseProduct F) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitPointwiseProductToProductColimit F) (CategoryTheory.Limits.Pi.π (fun s => CategoryTheory.Limits.colimit (F s)) s)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π ((CategoryTheory.Functor.pi F).obj k) s) (CategoryTheory.Limits.colimit.ι (F s) (k s))
• CategoryTheory.Limits.ι_colimitPointwiseProductToProductColimit_π_assoc 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] [CategoryTheory.Limits.HasProductsOfShape α C] (F : (i : α) → CategoryTheory.Functor (I i) C) [∀ (i : α), CategoryTheory.Limits.HasColimit (F i)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pointwiseProduct F)] (k : (i : α) → I i) (s : α) {Z : C} (h : CategoryTheory.Limits.colimit (F s) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.pointwiseProduct F) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitPointwiseProductToProductColimit F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun s => CategoryTheory.Limits.colimit (F s)) s) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π ((CategoryTheory.Functor.pi F).obj k) s) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F s) (k s)) h)
• CategoryTheory.Limits.coconePointwiseProduct_ι 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] [CategoryTheory.Limits.HasProductsOfShape α C] {F : (i : α) → CategoryTheory.Functor (I i) C} (c : (i : α) → CategoryTheory.Limits.Cocone (F i)) : (CategoryTheory.Limits.coconePointwiseProduct c).ι = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.pi fun i => (c i).ι) (CategoryTheory.Limits.Pi.functor α)) (CategoryTheory.Limits.Pi.constCompPiIsoConst fun i => (c i).pt).hom
• CategoryTheory.Limits.Pi.equivalenceOfEquivCompPointwiseProduct_inv_app 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] [CategoryTheory.Limits.HasProductsOfShape α C] (F : (i : α) → CategoryTheory.Functor (I i) C) {β : Type u_3} (f : β ≃ α) [CategoryTheory.Limits.HasProductsOfShape β C] (X : (i : α) → I i) : (CategoryTheory.Limits.Pi.equivalenceOfEquivCompPointwiseProduct F f).inv.app X = CategoryTheory.Limits.Pi.map' ⇑f fun j => CategoryTheory.CategoryStruct.id ((F (f j)).obj (X (f j)))
• CategoryTheory.Limits.Pi.equivalenceOfEquivCompPointwiseProduct_hom_app 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type u_1} {I : α → Type u_2} [(i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] [CategoryTheory.Limits.HasProductsOfShape α C] (F : (i : α) → CategoryTheory.Functor (I i) C) {β : Type u_3} (f : β ≃ α) [CategoryTheory.Limits.HasProductsOfShape β C] (X : (i : α) → I i) : (CategoryTheory.Limits.Pi.equivalenceOfEquivCompPointwiseProduct F f).hom.app X = CategoryTheory.Limits.Pi.map' ⇑f.symm fun k => CategoryTheory.eqToHom ⋯
• CategoryTheory.evaluationRightAdjoint 📋 Mathlib.CategoryTheory.Adjunction.Evaluation
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] (c : C) : CategoryTheory.Functor D (CategoryTheory.Functor C D)
• CategoryTheory.evaluationIsLeftAdjoint 📋 Mathlib.CategoryTheory.Adjunction.Evaluation
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] (c : C) : ((CategoryTheory.evaluation C D).obj c).IsLeftAdjoint
• CategoryTheory.evaluationAdjunctionLeft 📋 Mathlib.CategoryTheory.Adjunction.Evaluation
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] (c : C) : (CategoryTheory.evaluation C D).obj c ⊣ CategoryTheory.evaluationRightAdjoint D c
• CategoryTheory.evaluationRightAdjoint_obj_obj 📋 Mathlib.CategoryTheory.Adjunction.Evaluation
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] (c : C) (d : D) (t : C) : ((CategoryTheory.evaluationRightAdjoint D c).obj d).obj t = ∏ᶜ fun x => d
• CategoryTheory.NatTrans.epi_iff_epi_app' 📋 Mathlib.CategoryTheory.Adjunction.Evaluation
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] {F G : CategoryTheory.Functor C D} (η : F ⟶ G) : CategoryTheory.Epi η ↔ ∀ (c : C), CategoryTheory.Epi (η.app c)
• CategoryTheory.evaluationRightAdjoint_obj_map 📋 Mathlib.CategoryTheory.Adjunction.Evaluation
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] (c : C) (d : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.evaluationRightAdjoint D c).obj d).map f = CategoryTheory.Limits.Pi.lift fun g => CategoryTheory.Limits.Pi.π (fun x => d) (CategoryTheory.CategoryStruct.comp f g)
• CategoryTheory.evaluationAdjunctionLeft_counit_app 📋 Mathlib.CategoryTheory.Adjunction.Evaluation
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] (c : C) (Y : D) : (CategoryTheory.evaluationAdjunctionLeft D c).counit.app Y = CategoryTheory.Limits.Pi.π (fun x => Y) (CategoryTheory.CategoryStruct.id c)
• CategoryTheory.evaluationAdjunctionLeft_unit_app_app 📋 Mathlib.CategoryTheory.Adjunction.Evaluation
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] (c : C) (X : CategoryTheory.Functor C D) (x✝ : C) : ((CategoryTheory.evaluationAdjunctionLeft D c).unit.app X).app x✝ = CategoryTheory.Limits.Pi.lift fun g => X.map g
• CategoryTheory.evaluationRightAdjoint_map_app 📋 Mathlib.CategoryTheory.Adjunction.Evaluation
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] (c : C) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (x✝ : C) : ((CategoryTheory.evaluationRightAdjoint D c).map f).app x✝ = CategoryTheory.Limits.Pi.lift fun g => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => X✝) g) f
• CategoryTheory.Limits.FormalCoproduct.power 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) (α : Type t) [CategoryTheory.Limits.HasProductsOfShape α C] : CategoryTheory.Limits.FormalCoproduct C
• CategoryTheory.Limits.FormalCoproduct.powerFan 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) (α : Type) [CategoryTheory.Limits.HasProductsOfShape α C] : CategoryTheory.Limits.Fan fun x => U
• CategoryTheory.Limits.FormalCoproduct.powerFunctor 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (α : Type t) [CategoryTheory.Limits.HasProductsOfShape α C] : CategoryTheory.Functor (CategoryTheory.Limits.FormalCoproduct C) (CategoryTheory.Limits.FormalCoproduct C)
• CategoryTheory.Limits.FormalCoproduct.power_I 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) (α : Type t) [CategoryTheory.Limits.HasProductsOfShape α C] : (U.power α).I = (α → U.I)
• CategoryTheory.Limits.FormalCoproduct.powerπ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α : Type} [CategoryTheory.Limits.HasProductsOfShape α C] (a : α) : U.power α ⟶ U
• CategoryTheory.Limits.FormalCoproduct.isLimitPowerFan 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) (α : Type) [CategoryTheory.Limits.HasProductsOfShape α C] : CategoryTheory.Limits.IsLimit (U.powerFan α)
• CategoryTheory.Limits.FormalCoproduct.powerFunctor_obj 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (α : Type t) [CategoryTheory.Limits.HasProductsOfShape α C] (U : CategoryTheory.Limits.FormalCoproduct C) : (CategoryTheory.Limits.FormalCoproduct.powerFunctor α).obj U = U.power α
• CategoryTheory.Limits.FormalCoproduct.mapPower 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α β : Type t} [CategoryTheory.Limits.HasProductsOfShape α C] [CategoryTheory.Limits.HasProductsOfShape β C] (f : α → β) : U.power β ⟶ U.power α
• CategoryTheory.Limits.FormalCoproduct.powerπ_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α : Type} [CategoryTheory.Limits.HasProductsOfShape α C] (a : α) (i : (U.power α).I) : (U.powerπ a).f i = i a
• CategoryTheory.Limits.FormalCoproduct.power_obj 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) (α : Type t) [CategoryTheory.Limits.HasProductsOfShape α C] (i : α → U.I) : (U.power α).obj i = ∏ᶜ U.obj ∘ i
• CategoryTheory.Limits.FormalCoproduct.powerMap 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {U V : CategoryTheory.Limits.FormalCoproduct C} (f : U ⟶ V) (α : Type t) [CategoryTheory.Limits.HasProductsOfShape α C] : U.power α ⟶ V.power α
• CategoryTheory.Limits.FormalCoproduct.mapPower_id 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) (α : Type t) [CategoryTheory.Limits.HasProductsOfShape α C] : U.mapPower id = CategoryTheory.CategoryStruct.id (U.power α)
• CategoryTheory.Limits.FormalCoproduct.powerMap_id 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) (α : Type t) [CategoryTheory.Limits.HasProductsOfShape α C] : CategoryTheory.Limits.FormalCoproduct.powerMap (CategoryTheory.CategoryStruct.id U) α = CategoryTheory.CategoryStruct.id (U.power α)
• CategoryTheory.Limits.FormalCoproduct.mapPower_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α β : Type t} [CategoryTheory.Limits.HasProductsOfShape α C] [CategoryTheory.Limits.HasProductsOfShape β C] (f : α → β) : (U.mapPower f).f = fun i => i ∘ f
• CategoryTheory.Limits.FormalCoproduct.powerFunctor_map 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (α : Type t) [CategoryTheory.Limits.HasProductsOfShape α C] {X✝ Y✝ : CategoryTheory.Limits.FormalCoproduct C} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.FormalCoproduct.powerFunctor α).map f = CategoryTheory.Limits.FormalCoproduct.powerMap f α
• CategoryTheory.Limits.FormalCoproduct.mapPower_π 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α β : Type} [CategoryTheory.Limits.HasProductsOfShape α C] [CategoryTheory.Limits.HasProductsOfShape β C] (f : α → β) (a : α) : CategoryTheory.CategoryStruct.comp (U.mapPower f) (U.powerπ a) = U.powerπ (f a)
• CategoryTheory.Limits.FormalCoproduct.powerMap_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {U V : CategoryTheory.Limits.FormalCoproduct C} (f : U ⟶ V) (α : Type t) [CategoryTheory.Limits.HasProductsOfShape α C] : (CategoryTheory.Limits.FormalCoproduct.powerMap f α).f = fun i => f.f ∘ i
• CategoryTheory.Limits.FormalCoproduct.powerπ_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α : Type} [CategoryTheory.Limits.HasProductsOfShape α C] (a : α) (x✝ : (U.power α).I) : (U.powerπ a).φ x✝ = CategoryTheory.Limits.Pi.π (U.obj ∘ x✝) a
• CategoryTheory.Limits.FormalCoproduct.mapPower_comp 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α β γ : Type t} [CategoryTheory.Limits.HasProductsOfShape α C] [CategoryTheory.Limits.HasProductsOfShape β C] [CategoryTheory.Limits.HasProductsOfShape γ C] (f : α → β) (g : β → γ) : U.mapPower (g ∘ f) = CategoryTheory.CategoryStruct.comp (U.mapPower g) (U.mapPower f)
• CategoryTheory.Limits.FormalCoproduct.powerMap_comp 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {U V W : CategoryTheory.Limits.FormalCoproduct C} (f : U ⟶ V) (g : V ⟶ W) (α : Type t) [CategoryTheory.Limits.HasProductsOfShape α C] : CategoryTheory.Limits.FormalCoproduct.powerMap (CategoryTheory.CategoryStruct.comp f g) α = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.powerMap f α) (CategoryTheory.Limits.FormalCoproduct.powerMap g α)
• CategoryTheory.Limits.FormalCoproduct.mapPower_π_assoc 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α β : Type} [CategoryTheory.Limits.HasProductsOfShape α C] [CategoryTheory.Limits.HasProductsOfShape β C] (f : α → β) (a : α) {Z : CategoryTheory.Limits.FormalCoproduct C} (h : U ⟶ Z) : CategoryTheory.CategoryStruct.comp (U.mapPower f) (CategoryTheory.CategoryStruct.comp (U.powerπ a) h) = CategoryTheory.CategoryStruct.comp (U.powerπ (f a)) h
• CategoryTheory.Limits.FormalCoproduct.mapPower_powerMap 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {U V : CategoryTheory.Limits.FormalCoproduct C} (f : U ⟶ V) {α β : Type t} [CategoryTheory.Limits.HasProductsOfShape α C] [CategoryTheory.Limits.HasProductsOfShape β C] (g : α → β) : CategoryTheory.CategoryStruct.comp (U.mapPower g) (CategoryTheory.Limits.FormalCoproduct.powerMap f α) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.powerMap f β) (V.mapPower g)
• CategoryTheory.Limits.FormalCoproduct.mapPower_comp_assoc 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α β γ : Type t} [CategoryTheory.Limits.HasProductsOfShape α C] [CategoryTheory.Limits.HasProductsOfShape β C] [CategoryTheory.Limits.HasProductsOfShape γ C] (f : α → β) (g : β → γ) {Z : CategoryTheory.Limits.FormalCoproduct C} (h : U.power α ⟶ Z) : CategoryTheory.CategoryStruct.comp (U.mapPower (g ∘ f)) h = CategoryTheory.CategoryStruct.comp (U.mapPower g) (CategoryTheory.CategoryStruct.comp (U.mapPower f) h)
• CategoryTheory.Limits.FormalCoproduct.mapPower_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α β : Type t} [CategoryTheory.Limits.HasProductsOfShape α C] [CategoryTheory.Limits.HasProductsOfShape β C] (f : α → β) : (U.mapPower f).φ = fun x => CategoryTheory.Limits.Pi.lift fun x_1 => CategoryTheory.Limits.Pi.π (U.obj ∘ x) (f x_1)
• CategoryTheory.Limits.FormalCoproduct.powerMap_comp_assoc 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {U V W : CategoryTheory.Limits.FormalCoproduct C} (f : U ⟶ V) (g : V ⟶ W) (α : Type t) [CategoryTheory.Limits.HasProductsOfShape α C] {Z : CategoryTheory.Limits.FormalCoproduct C} (h : W.power α ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.powerMap (CategoryTheory.CategoryStruct.comp f g) α) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.powerMap f α) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.powerMap g α) h)
• CategoryTheory.Limits.FormalCoproduct.powerMap_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {U V : CategoryTheory.Limits.FormalCoproduct C} (f : U ⟶ V) (α : Type t) [CategoryTheory.Limits.HasProductsOfShape α C] : (CategoryTheory.Limits.FormalCoproduct.powerMap f α).φ = fun i => CategoryTheory.Limits.Pi.map fun a => f.φ (i a)
• CategoryTheory.Limits.FormalCoproduct.mapPower_powerMap_assoc 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {U V : CategoryTheory.Limits.FormalCoproduct C} (f : U ⟶ V) {α β : Type t} [CategoryTheory.Limits.HasProductsOfShape α C] [CategoryTheory.Limits.HasProductsOfShape β C] (g : α → β) {Z : CategoryTheory.Limits.FormalCoproduct C} (h : V.power α ⟶ Z) : CategoryTheory.CategoryStruct.comp (U.mapPower g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.powerMap f α) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.powerMap f β) (CategoryTheory.CategoryStruct.comp (V.mapPower g) h)
• CategoryTheory.NatTrans.instIsClosedUnderColimitsOfShapeUnderFunctorCoequifiberedHomOfHasProductsOfShapeHom 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
  {J : Type u_1} {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Category.{v_3, u_3} D] (F : CategoryTheory.Functor C D) [∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] : CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape (fun f => CategoryTheory.NatTrans.Coequifibered f.hom) J
• CategoryTheory.Localization.hasProductsOfShape 📋 Mathlib.CategoryTheory.Localization.FiniteProducts
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.ContainsIdentities] (J : Type) [Finite J] [CategoryTheory.Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] : CategoryTheory.Limits.HasProductsOfShape J D
• CategoryTheory.Localization.preservesProductsOfShape 📋 Mathlib.CategoryTheory.Localization.FiniteProducts
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.ContainsIdentities] (J : Type) [Finite J] [CategoryTheory.Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) L
• CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctor 📋 Mathlib.CategoryTheory.Localization.FiniteProducts
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] (J : Type) [CategoryTheory.Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] [W.ContainsIdentities] [Finite J] : CategoryTheory.Functor (CategoryTheory.Functor (CategoryTheory.Discrete J) D) D
• CategoryTheory.Localization.HasProductsOfShapeAux.adj 📋 Mathlib.CategoryTheory.Localization.FiniteProducts
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] (J : Type) [CategoryTheory.Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] [W.ContainsIdentities] [Finite J] : CategoryTheory.Functor.const (CategoryTheory.Discrete J) ⊣ CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctor L W J
• CategoryTheory.Localization.HasProductsOfShapeAux.inverts 📋 Mathlib.CategoryTheory.Localization.FiniteProducts
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] (J : Type) [CategoryTheory.Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] : (W.functorCategory (CategoryTheory.Discrete J)).IsInvertedBy (CategoryTheory.Limits.lim.comp L)
• CategoryTheory.Localization.HasProductsOfShapeAux.isLimitMapCone 📋 Mathlib.CategoryTheory.Localization.FiniteProducts
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] (J : Type) [CategoryTheory.Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] [W.ContainsIdentities] [Finite J] (F : CategoryTheory.Functor (CategoryTheory.Discrete J) C) : CategoryTheory.Limits.IsLimit (L.mapCone (CategoryTheory.Limits.limit.cone F))
• CategoryTheory.Localization.HasProductsOfShapeAux.instCatCommSqFunctorDiscreteLimObjWhiskeringRightLimitFunctor 📋 Mathlib.CategoryTheory.Localization.FiniteProducts
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] (J : Type) [CategoryTheory.Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] [W.ContainsIdentities] [Finite J] : CategoryTheory.CatCommSq CategoryTheory.Limits.lim ((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Discrete J) C D).obj L) L (CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctor L W J)
• CategoryTheory.Localization.HasProductsOfShapeAux.compLimitFunctorIso 📋 Mathlib.CategoryTheory.Localization.FiniteProducts
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] (J : Type) [CategoryTheory.Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] [W.ContainsIdentities] [Finite J] : ((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Discrete J) C D).obj L).comp (CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctor L W J) ≅ CategoryTheory.Limits.lim.comp L
• CategoryTheory.Localization.HasProductsOfShapeAux.adj_counit_app 📋 Mathlib.CategoryTheory.Localization.FiniteProducts
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] (J : Type) [CategoryTheory.Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] [W.ContainsIdentities] [Finite J] (F : CategoryTheory.Functor (CategoryTheory.Discrete J) C) : (CategoryTheory.Localization.HasProductsOfShapeAux.adj L W J).counit.app (F.comp L) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const (CategoryTheory.Discrete J)).map ((CategoryTheory.Localization.HasProductsOfShapeAux.compLimitFunctorIso L W J).hom.app F)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.compConstIso (CategoryTheory.Discrete J) L).hom.app (CategoryTheory.Limits.lim.obj F)) (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.constLimAdj.counit.app F) L))
• CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_ind_discrete 📋 Mathlib.CategoryTheory.ObjectProperty.Ind
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {ι : Type u_1} [Small.{w, u_1} ι] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete ι)] [CategoryTheory.Limits.HasProductsOfShape ι C] [CategoryTheory.Limits.IsIPCOfShape.{w, u_1, v, u} ι C] : P.ind.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete ι)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c