Loogle!

Result

Found 100 declarations mentioning CategoryTheory.Limits.Fan.

• CategoryTheory.Limits.Fan 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (f : β → C) : Type (max (max w u) v)
• CategoryTheory.Limits.Fan.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → P ⟶ f b) : CategoryTheory.Limits.Fan f
• CategoryTheory.Limits.hasProducts_of_limit_fans 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (lf : {J : Type w} → (f : J → C) → CategoryTheory.Limits.Fan f) (lf_isLimit : {J : Type w} → (f : J → C) → CategoryTheory.Limits.IsLimit (lf f)) : CategoryTheory.Limits.HasProducts C
• CategoryTheory.Limits.Fan.proj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (p : CategoryTheory.Limits.Fan f) (j : β) : p.pt ⟶ f j
• CategoryTheory.Limits.Fan.IsLimit.lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Fan F} (hc : CategoryTheory.Limits.IsLimit c) {A : C} (f : (i : β) → A ⟶ F i) : A ⟶ c.pt
• CategoryTheory.Limits.Fan.isLimitOfIsIsoPiLift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasProduct f] (c : CategoryTheory.Limits.Fan f) [hc : CategoryTheory.IsIso (CategoryTheory.Limits.Pi.lift c.proj)] : CategoryTheory.Limits.IsLimit c
• CategoryTheory.Limits.Fan.nonempty_isLimit_iff_isIso_piLift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasProduct f] (c : CategoryTheory.Limits.Fan f) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ CategoryTheory.IsIso (CategoryTheory.Limits.Pi.lift c.proj)
• CategoryTheory.Limits.Fan.IsLimit.fac 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Fan F} (hc : CategoryTheory.Limits.IsLimit c) {A : C} (f : (i : β) → A ⟶ F i) (i : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc f) (c.proj i) = f i
• CategoryTheory.Limits.Fan.IsLimit.lift_proj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Fan X} (d : CategoryTheory.Limits.Fan X) (hc : CategoryTheory.Limits.IsLimit c) (i : β) : CategoryTheory.CategoryStruct.comp (hc.lift d) (c.proj i) = d.proj i
• CategoryTheory.Limits.Fan.isLimitEquivOfEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) {f : γ → C} (c : CategoryTheory.Limits.Fan f) : CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk c.pt fun i => c.proj (ε i))
• CategoryTheory.Limits.Fan.IsLimit.fac_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Fan F} (hc : CategoryTheory.Limits.IsLimit c) {A : C} (f : (i : β) → A ⟶ F i) (i : β) {Z : C} (h : F i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc f) (CategoryTheory.CategoryStruct.comp (c.proj i) h) = CategoryTheory.CategoryStruct.comp (f i) h
• CategoryTheory.Limits.Fan.isLimitMapConeEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {ι : Type u_1} (X : ι → C) (c : CategoryTheory.Limits.Fan X) : CategoryTheory.Limits.IsLimit (F.mapCone c) ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (F.obj c.pt) fun i => F.map (c.proj i))
• CategoryTheory.Limits.Fan.IsLimit.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type u_1} {F : I → C} {c : CategoryTheory.Limits.Fan F} (hc : CategoryTheory.Limits.IsLimit c) {A : C} (f g : A ⟶ c.pt) (h : ∀ (i : I), CategoryTheory.CategoryStruct.comp f (c.proj i) = CategoryTheory.CategoryStruct.comp g (c.proj i)) : f = g
• CategoryTheory.Limits.Fan.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} {c₁ c₂ : CategoryTheory.Limits.Fan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), c₁.proj b = CategoryTheory.CategoryStruct.comp e.hom (c₂.proj b) := by cat_disch) : c₁ ≅ c₂
• CategoryTheory.Limits.Fan.IsLimit.lift_proj_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Fan X} (d : CategoryTheory.Limits.Fan X) (hc : CategoryTheory.Limits.IsLimit c) (i : β) {Z : C} (h : X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (hc.lift d) (CategoryTheory.CategoryStruct.comp (c.proj i) h) = CategoryTheory.CategoryStruct.comp (d.proj i) h
• CategoryTheory.Limits.Fan.ext_hom_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} {c₁ c₂ : CategoryTheory.Limits.Fan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), c₁.proj b = CategoryTheory.CategoryStruct.comp e.hom (c₂.proj b) := by cat_disch) : (CategoryTheory.Limits.Fan.ext e w).hom.hom = e.hom
• CategoryTheory.Limits.Fan.ext_inv_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} {c₁ c₂ : CategoryTheory.Limits.Fan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), c₁.proj b = CategoryTheory.CategoryStruct.comp e.hom (c₂.proj b) := by cat_disch) : (CategoryTheory.Limits.Fan.ext e w).inv.hom = e.inv
• CategoryTheory.Limits.Fan.IsLimit.prod 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {ι' : Type u_2} {X : ι → ι' → C} (c : (i : ι) → CategoryTheory.Limits.Fan fun j => X i j) (hc : (i : ι) → CategoryTheory.Limits.IsLimit (c i)) (c' : CategoryTheory.Limits.Fan fun i => (c i).pt) (hc' : CategoryTheory.Limits.IsLimit c') : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk c'.pt fun p => CategoryTheory.CategoryStruct.comp (c'.proj p.1) ((c p.1).proj p.2))
• CategoryTheory.Limits.mkFanLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (t : CategoryTheory.Limits.Fan f) (lift : (s : CategoryTheory.Limits.Fan f) → s.pt ⟶ t.pt) (fac : ∀ (s : CategoryTheory.Limits.Fan f) (j : β), CategoryTheory.CategoryStruct.comp (lift s) (t.proj j) = s.proj j := by cat_disch) (uniq : ∀ (s : CategoryTheory.Limits.Fan f) (m : s.pt ⟶ t.pt), (∀ (j : β), CategoryTheory.CategoryStruct.comp m (t.proj j) = s.proj j) → m = lift s := by cat_disch) : CategoryTheory.Limits.IsLimit t
• CategoryTheory.Limits.Fan.IsLimit.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (t : CategoryTheory.Limits.Fan f) (lift : (s : CategoryTheory.Limits.Fan f) → s.pt ⟶ t.pt) (fac : ∀ (s : CategoryTheory.Limits.Fan f) (j : β), CategoryTheory.CategoryStruct.comp (lift s) (t.proj j) = s.proj j := by cat_disch) (uniq : ∀ (s : CategoryTheory.Limits.Fan f) (m : s.pt ⟶ t.pt), (∀ (j : β), CategoryTheory.CategoryStruct.comp m (t.proj j) = s.proj j) → m = lift s := by cat_disch) : CategoryTheory.Limits.IsLimit t
• CategoryTheory.Limits.Fan.IsLimit.mk_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (t : CategoryTheory.Limits.Fan f) (lift : (s : CategoryTheory.Limits.Fan f) → s.pt ⟶ t.pt) (fac : ∀ (s : CategoryTheory.Limits.Fan f) (j : β), CategoryTheory.CategoryStruct.comp (lift s) (t.proj j) = s.proj j := by cat_disch) (uniq : ∀ (s : CategoryTheory.Limits.Fan f) (m : s.pt ⟶ t.pt), (∀ (j : β), CategoryTheory.CategoryStruct.comp m (t.proj j) = s.proj j) → m = lift s := by cat_disch) (s : CategoryTheory.Limits.Fan f) : (CategoryTheory.Limits.Fan.IsLimit.mk t lift fac uniq).lift s = lift s
• CommRingCat.piFan 📋 Mathlib.Algebra.Category.Ring.Constructions
  {ι : Type u} (R : ι → CommRingCat) : CategoryTheory.Limits.Fan R
• CategoryTheory.extendFan 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Fan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) : CategoryTheory.Limits.Fan f
• CategoryTheory.extendFan_pt 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Fan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) : (CategoryTheory.extendFan c₁ c₂).pt = c₂.pt
• CategoryTheory.extendFanIsLimit 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} (f : Fin (n + 1) → C) {c₁ : CategoryTheory.Limits.Fan fun i => f i.succ} {c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt} (t₁ : CategoryTheory.Limits.IsLimit c₁) (t₂ : CategoryTheory.Limits.IsLimit c₂) : CategoryTheory.Limits.IsLimit (CategoryTheory.extendFan c₁ c₂)
• CategoryTheory.extendFan_π_app 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Fan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) (X : CategoryTheory.Discrete (Fin (n + 1))) : (CategoryTheory.extendFan c₁ c₂).π.app X = Fin.cases c₂.fst (fun i => CategoryTheory.CategoryStruct.comp c₂.snd (c₁.π.app { as := i })) X.as
• ModuleCat.productCone 📋 Mathlib.Algebra.Category.ModuleCat.Products
  {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) : CategoryTheory.Limits.Fan Z
• CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2} (s t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) (i : CategoryTheory.Limits.Fork s t) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_pt 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2} (s t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) (i : CategoryTheory.Limits.Fork s t) : (CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit s t hs ht i).pt = i.pt
• CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildIsLimit 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2} (s t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) {i : CategoryTheory.Limits.Fork s t} (t₁ : CategoryTheory.Limits.IsLimit c₁) (t₂ : CategoryTheory.Limits.IsLimit c₂) (hi : CategoryTheory.Limits.IsLimit i) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit s t hs ht i)
• CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_π_app 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2} (s t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) (i : CategoryTheory.Limits.Fork s t) (x✝ : J) : (CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit s t hs ht i).π.app x✝ = CategoryTheory.CategoryStruct.comp i.ι (c₁.π.app { as := x✝ })
• AddCommGrpCat.HasLimit.lift 📋 Mathlib.Algebra.Category.Grp.Biproducts
  {J : Type w} (f : J → AddCommGrpCat) (s : CategoryTheory.Limits.Fan f) : s.pt ⟶ AddCommGrpCat.of ((j : J) → ↑(f j))
• AddCommGrpCat.HasLimit.productLimitCone_isLimit_lift 📋 Mathlib.Algebra.Category.Grp.Biproducts
  {J : Type w} (f : J → AddCommGrpCat) (s : CategoryTheory.Limits.Fan f) : (AddCommGrpCat.HasLimit.productLimitCone f).isLimit.lift s = AddCommGrpCat.HasLimit.lift f s
• AddCommGrpCat.HasLimit.lift_hom_apply 📋 Mathlib.Algebra.Category.Grp.Biproducts
  {J : Type w} (f : J → AddCommGrpCat) (s : CategoryTheory.Limits.Fan f) (x : ↑s.1) (j : J) : (AddCommGrpCat.Hom.hom (AddCommGrpCat.HasLimit.lift f s)) x j = (CategoryTheory.ConcreteCategory.hom (s.π.app { as := j })) x
• CategoryTheory.Limits.Cofan.op 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} (c : CategoryTheory.Limits.Cofan Z) : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)
• CategoryTheory.Limits.Fan.op 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} (f : CategoryTheory.Limits.Fan Z) : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)
• CategoryTheory.Limits.Fan.IsLimit.op 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : CategoryTheory.Limits.Fan Z} (hf : CategoryTheory.Limits.IsLimit f) : CategoryTheory.Limits.IsColimit f.op
• CategoryTheory.Limits.opCoproductIsoProduct' 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)} (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.IsLimit f) : Opposite.op c.pt ≅ f.pt
• CategoryTheory.Limits.opProductIsoCoproduct' 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : CategoryTheory.Limits.Fan Z} {c : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)} (hf : CategoryTheory.Limits.IsLimit f) (hc : CategoryTheory.Limits.IsColimit c) : Opposite.op f.pt ≅ c.pt
• CategoryTheory.Limits.opCoproductIsoProduct'_hom_comp_proj 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)} (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.IsLimit f) (i : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).hom (f.proj i) = (c.inj i).op
• CategoryTheory.Limits.opCoproductIsoProduct'_inv_comp_inj 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)} (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.IsLimit f) (b : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).inv (c.inj b).op = f.proj b
• CategoryTheory.Limits.proj_comp_opProductIsoCoproduct'_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : CategoryTheory.Limits.Fan Z} {c : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)} (hf : CategoryTheory.Limits.IsLimit f) (hc : CategoryTheory.Limits.IsColimit c) (b : α) : CategoryTheory.CategoryStruct.comp (f.proj b).op (CategoryTheory.Limits.opProductIsoCoproduct' hf hc).hom = c.inj b
• CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)} (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.IsLimit f) (c' : CategoryTheory.Limits.Cofan Z) : CategoryTheory.CategoryStruct.comp (hc.desc c').op (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).hom = hf.lift c'.op
• CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : CategoryTheory.Limits.Fan Z} {c : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)} (hf : CategoryTheory.Limits.IsLimit f) (hc : CategoryTheory.Limits.IsColimit c) (f' : CategoryTheory.Limits.Fan Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProductIsoCoproduct' hf hc).inv (hf.lift f').op = hc.desc f'.op
• CategoryTheory.Limits.opCoproductIsoProduct'_hom_comp_proj_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)} (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.IsLimit f) (i : α) {Z✝ : Cᵒᵖ} (h : Opposite.op (Z i) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).hom (CategoryTheory.CategoryStruct.comp (f.proj i) h) = CategoryTheory.CategoryStruct.comp (c.inj i).op h
• CategoryTheory.Limits.opCoproductIsoProduct'_comp_self 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c c' : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)} (hc : CategoryTheory.Limits.IsColimit c) (hc' : CategoryTheory.Limits.IsColimit c') (hf : CategoryTheory.Limits.IsLimit f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).hom (CategoryTheory.Limits.opCoproductIsoProduct' hc' hf).inv = (hc.coconePointUniqueUpToIso hc').op.inv
• CategoryTheory.Limits.opProductIsoCoproduct'_comp_self 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f f' : CategoryTheory.Limits.Fan Z} {c : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)} (hf : CategoryTheory.Limits.IsLimit f) (hf' : CategoryTheory.Limits.IsLimit f') (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProductIsoCoproduct' hf hc).hom (CategoryTheory.Limits.opProductIsoCoproduct' hf' hc).inv = (hf.conePointUniqueUpToIso hf').op.inv
• CategoryTheory.isCoseparator_of_isLimit_fan 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} {f : β → C} (hf : (CategoryTheory.ObjectProperty.ofObj f).IsCoseparating) {c : CategoryTheory.Limits.Fan f} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.IsCoseparator c.pt
• CategoryTheory.isCoseparator_iff_of_isLimit_fan 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} {f : β → C} {c : CategoryTheory.Limits.Fan f} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.IsCoseparator c.pt ↔ (CategoryTheory.ObjectProperty.ofObj f).IsCoseparating
• CategoryTheory.ObjectProperty.IsCoseparating.mk_of_exists_mono 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C} (hP : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x j, CategoryTheory.Mono j) : P.IsCoseparating
• CategoryTheory.Limits.MulticospanIndex.parallelPairDiagramOfIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C
• CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : c.pt ⟶ d.pt
• CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : c.pt ⟶ d.pt
• CategoryTheory.Limits.MulticospanIndex.parallelPairDiagramOfIsLimit_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (x : CategoryTheory.Limits.WalkingParallelPair) : (I.parallelPairDiagramOfIsLimit c hd).obj x = CategoryTheory.Limits.parallelPair.parallelPairObj c.pt d.pt x
• CategoryTheory.Limits.Multifork.ofPiFork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} {hd : CategoryTheory.Limits.IsLimit d} (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) : CategoryTheory.Limits.Multifork I
• CategoryTheory.Limits.Multifork.toPiFork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (K : CategoryTheory.Limits.Multifork I) : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
• CategoryTheory.Limits.Multifork.toPiFork_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (K : CategoryTheory.Limits.Multifork I) : (CategoryTheory.Limits.Multifork.toPiFork hc hd K).pt = K.pt
• CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : CategoryTheory.Functor (CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) (CategoryTheory.Limits.Multifork I)
• CategoryTheory.Limits.Multifork.ofPiFork_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} {hd : CategoryTheory.Limits.IsLimit d} (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) : (CategoryTheory.Limits.Multifork.ofPiFork a).pt = a.pt
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : CategoryTheory.Limits.Multifork I ≌ CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
• CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : CategoryTheory.Functor (CategoryTheory.Limits.Multifork I) (CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd))
• CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit_proj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (i : J.R) : CategoryTheory.CategoryStruct.comp (I.fstPiMapOfIsLimit c hd) (d.proj i) = CategoryTheory.CategoryStruct.comp (c.proj (J.fst i)) (I.fst i)
• CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit_proj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (i : J.R) : CategoryTheory.CategoryStruct.comp (I.sndPiMapOfIsLimit c hd) (d.proj i) = CategoryTheory.CategoryStruct.comp (c.proj (J.snd i)) (I.snd i)
• CategoryTheory.Limits.MulticospanIndex.parallelPairDiagramOfIsLimit_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) {X✝ Y✝ : CategoryTheory.Limits.WalkingParallelPair} (h : X✝ ⟶ Y✝) : (I.parallelPairDiagramOfIsLimit c hd).map h = CategoryTheory.Limits.parallelPair.parallelPairHom (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd) h
• CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit_proj_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (i : J.R) {Z : C} (h : I.right i ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.fstPiMapOfIsLimit c hd) (CategoryTheory.CategoryStruct.comp (d.proj i) h) = CategoryTheory.CategoryStruct.comp (c.proj (J.fst i)) (CategoryTheory.CategoryStruct.comp (I.fst i) h)
• CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit_proj_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (i : J.R) {Z : C} (h : I.right i ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.sndPiMapOfIsLimit c hd) (CategoryTheory.CategoryStruct.comp (d.proj i) h) = CategoryTheory.CategoryStruct.comp (c.proj (J.snd i)) (CategoryTheory.CategoryStruct.comp (I.snd i) h)
• CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) : (I.ofPiForkFunctor hd).obj a = CategoryTheory.Limits.Multifork.ofPiFork a
• CategoryTheory.Limits.Multifork.toPiFork_π_app_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (CategoryTheory.Limits.Multifork.toPiFork hc hd K).ι = CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι
• CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (K : CategoryTheory.Limits.Multifork I) : (I.toPiForkFunctor hc hd).obj K = CategoryTheory.Limits.Multifork.toPiFork hc hd K
• CategoryTheory.Limits.Multifork.pi_condition 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (I.fstPiMapOfIsLimit c hd) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (I.sndPiMapOfIsLimit c hd)
• CategoryTheory.Limits.Multifork.ofPiFork_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) (i : J.L) : (CategoryTheory.Limits.Multifork.ofPiFork a).ι i = CategoryTheory.CategoryStruct.comp a.ι (c.proj i)
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_inverse 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).inverse = I.ofPiForkFunctor hd
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_functor 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).functor = I.toPiForkFunctor hc hd
• CategoryTheory.Limits.Multifork.pi_condition_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) {Z : C} (h : d.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (CategoryTheory.CategoryStruct.comp (I.fstPiMapOfIsLimit c hd) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (CategoryTheory.CategoryStruct.comp (I.sndPiMapOfIsLimit c hd) h)
• CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) {K₁ K₂ : CategoryTheory.Limits.Multifork I} (f : K₁ ⟶ K₂) : ((I.toPiForkFunctor hc hd).map f).hom = f.hom
• CategoryTheory.Limits.Multifork.ofPiFork_π_app_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) (i : J.R) : (CategoryTheory.Limits.Multifork.ofPiFork a).π.app (CategoryTheory.Limits.WalkingMulticospan.right i) = CategoryTheory.CategoryStruct.comp a.ι (CategoryTheory.CategoryStruct.comp (I.fstPiMapOfIsLimit c hd) (d.proj i))
• CategoryTheory.Limits.Multifork.toPiFork_π_app_one 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (CategoryTheory.Limits.Multifork.toPiFork hc hd K).π.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (I.fstPiMapOfIsLimit c hd)
• CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) {K₁ K₂ : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)} (f : K₁ ⟶ K₂) : ((I.ofPiForkFunctor hd).map f).hom = f.hom
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_unitIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).unitIso = CategoryTheory.NatIso.ofComponents (fun K => CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Multifork I)).obj K).pt) ⋯) ⋯
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_counitIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).counitIso = CategoryTheory.NatIso.ofComponents (fun K => CategoryTheory.Limits.Fork.ext (CategoryTheory.Iso.refl (((I.ofPiForkFunctor hd).comp (I.toPiForkFunctor hc hd)).obj K).pt) ⋯) ⋯
• ModuleCat.HasLimit.lift 📋 Mathlib.Algebra.Category.ModuleCat.Biproducts
  {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) (s : CategoryTheory.Limits.Fan f) : s.pt ⟶ ModuleCat.of R ((j : J) → ↑(f j))
• ModuleCat.HasLimit.productLimitCone_isLimit_lift 📋 Mathlib.Algebra.Category.ModuleCat.Biproducts
  {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) (s : CategoryTheory.Limits.Fan f) : (ModuleCat.HasLimit.productLimitCone f).isLimit.lift s = ModuleCat.HasLimit.lift f s
• ModuleCat.HasLimit.lift_hom_apply 📋 Mathlib.Algebra.Category.ModuleCat.Biproducts
  {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) (s : CategoryTheory.Limits.Fan f) (x : ↑s.1) (j : J) : (ModuleCat.Hom.hom (ModuleCat.HasLimit.lift f s)) x j = (CategoryTheory.ConcreteCategory.hom (s.π.app { as := j })) x
• CategoryTheory.Pretriangulated.productTriangle.fan 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] : CategoryTheory.Limits.Fan T
• CategoryTheory.ObjectProperty.prop_of_isLimit_fan 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderFiniteProducts] {J : Type u_2} [Finite J] {f : J → C} {F : CategoryTheory.Limits.Fan f} (hF : CategoryTheory.Limits.IsLimit F) (h : ∀ (j : J), P (f j)) : P F.pt
• TopCat.piFan 📋 Mathlib.Topology.Category.TopCat.Limits.Products
  {ι : Type v} (α : ι → TopCat) : CategoryTheory.Limits.Fan α
• CommRingCat.Under.piFan 📋 Mathlib.Algebra.Category.Ring.Under.Limits
  {R : CommRingCat} {ι : Type u} (P : ι → CategoryTheory.Under R) : CategoryTheory.Limits.Fan P
• CommRingCat.Under.tensorProductFan 📋 Mathlib.Algebra.Category.Ring.Under.Limits
  {R : CommRingCat} (S : CommRingCat) [Algebra ↑R ↑S] {ι : Type u} (P : ι → CategoryTheory.Under R) : CategoryTheory.Limits.Fan fun i => S.mkUnder (TensorProduct ↑R ↑S ↑(P i).right)
• CommRingCat.Under.tensorProductFan' 📋 Mathlib.Algebra.Category.Ring.Under.Limits
  {R : CommRingCat} (S : CommRingCat) [Algebra ↑R ↑S] {ι : Type u} (P : ι → CategoryTheory.Under R) : CategoryTheory.Limits.Fan fun i => S.mkUnder (TensorProduct ↑R ↑S ↑(P i).right)
• CommRingCat.Under.tensorProductFanIso 📋 Mathlib.Algebra.Category.Ring.Under.Limits
  {R S : CommRingCat} [Algebra ↑R ↑S] {ι : Type u} (P : ι → CategoryTheory.Under R) [Fintype ι] [DecidableEq ι] : CommRingCat.Under.tensorProductFan S P ≅ CommRingCat.Under.tensorProductFan' S P
• CategoryTheory.Grpd.piLimitFan 📋 Mathlib.CategoryTheory.Groupoid.Grpd.Basic
  ⦃J : Type u⦄ (F : J → CategoryTheory.Grpd) : CategoryTheory.Limits.Fan F
• FundamentalGroupoidFunctor.instIsIsoFanGrpdObjTopCatFundamentalGroupoidFunctorPiTopToPiCone 📋 Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
  {I : Type u} (X : I → TopCat) : CategoryTheory.IsIso (FundamentalGroupoidFunctor.piTopToPiCone X)
• FundamentalGroupoidFunctor.piTopToPiCone 📋 Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
  {I : Type u} (X : I → TopCat) : CategoryTheory.Limits.Fan.mk (FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ((i : I) → ↑(X i)))) (FundamentalGroupoidFunctor.proj X) ⟶ CategoryTheory.Grpd.piLimitFan fun i => FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i)
• CategoryTheory.Limits.Fan.combPairHoms 📋 Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {ι₁ : Type u_1} {ι₂ : Type u_2} {f₁ : ι₁ → C} {f₂ : ι₂ → C} (c₁ : CategoryTheory.Limits.Fan f₁) (c₂ : CategoryTheory.Limits.Fan f₂) (bc : CategoryTheory.Limits.BinaryFan c₁.pt c₂.pt) (i : ι₁ ⊕ ι₂) : bc.pt ⟶ Sum.elim f₁ f₂ i
• CategoryTheory.Limits.Fan.combPairIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {ι₁ : Type u_1} {ι₂ : Type u_2} {f₁ : ι₁ → C} {f₂ : ι₂ → C} {c₁ : CategoryTheory.Limits.Fan f₁} {c₂ : CategoryTheory.Limits.Fan f₂} {bc : CategoryTheory.Limits.BinaryFan c₁.pt c₂.pt} (h₁ : CategoryTheory.Limits.IsLimit c₁) (h₂ : CategoryTheory.Limits.IsLimit c₂) (h : CategoryTheory.Limits.IsLimit bc) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk bc.pt (c₁.combPairHoms c₂ bc))
• CategoryTheory.Limits.WidePullbackCone.toFan 📋 Mathlib.CategoryTheory.Limits.Constructions.WidePullbackOfTerminal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type w} {B : C} {objs : ι → C} (arrows : (j : ι) → objs j ⟶ B) (s : CategoryTheory.Limits.WidePullbackCone arrows) : CategoryTheory.Limits.Fan objs
• CategoryTheory.Limits.WidePullbackCone.ofFan 📋 Mathlib.CategoryTheory.Limits.Constructions.WidePullbackOfTerminal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type w} {B : C} {objs : ι → C} (arrows : (j : ι) → objs j ⟶ B) (c : CategoryTheory.Limits.Fan objs) (hB : CategoryTheory.Limits.IsTerminal B) : CategoryTheory.Limits.WidePullbackCone arrows
• CategoryTheory.Limits.WidePullbackCone.isLimitOfFan 📋 Mathlib.CategoryTheory.Limits.Constructions.WidePullbackOfTerminal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type w} {B : C} {objs : ι → C} (arrows : (j : ι) → objs j ⟶ B) {c : CategoryTheory.Limits.Fan objs} (hc : CategoryTheory.Limits.IsLimit c) (hB : CategoryTheory.Limits.IsTerminal B) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.WidePullbackCone.ofFan arrows c hB)
• 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
• ωCPO.HasProducts.product 📋 Mathlib.Order.Category.OmegaCompletePartialOrder
  {J : Type v} (f : J → ωCPO) : CategoryTheory.Limits.Fan f

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