Loogle!

Result

Found 145 declarations mentioning CategoryTheory.Functor.Initial.

• CategoryTheory.Functor.Initial 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Prop
• CategoryTheory.Functor.initial_fromPUnit_of_isInitial 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {c : C} (hc : CategoryTheory.Limits.IsInitial c) : (CategoryTheory.Functor.fromPUnit c).Initial
• CategoryTheory.Functor.Initial.lift 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] (d : D) : C
• CategoryTheory.Functor.initial_of_isLeftAdjoint 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsLeftAdjoint] : F.Initial
• CategoryTheory.IsCofiltered.of_initial 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] [CategoryTheory.IsCofiltered C] : CategoryTheory.IsCofiltered D
• CategoryTheory.IsCofilteredOrEmpty.of_initial 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] [CategoryTheory.IsCofilteredOrEmpty C] : CategoryTheory.IsCofilteredOrEmpty D
• CategoryTheory.Functor.Initial.instNonemptyCostructuredArrow 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] (d : D) : Nonempty (CategoryTheory.CostructuredArrow F d)
• CategoryTheory.Functor.initial_of_adjunction 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (adj : L ⊣ R) : L.Initial
• CategoryTheory.Functor.Initial.hasLimitsOfShape_of_initial 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.Limits.HasLimitsOfShape C E] : CategoryTheory.Limits.HasLimitsOfShape D E
• CategoryTheory.Functor.instInitialOfHasInitialOfPreservesColimitDiscretePEmptyEmpty 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) F] : F.Initial
• CategoryTheory.Functor.Initial.mk 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (out : ∀ (d : D), CategoryTheory.IsConnected (CategoryTheory.CostructuredArrow F d)) : F.Initial
• CategoryTheory.Functor.Initial.out 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {F : CategoryTheory.Functor C D} [self : F.Initial] (d : D) : CategoryTheory.IsConnected (CategoryTheory.CostructuredArrow F d)
• CategoryTheory.Functor.final_of_initial_op 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.op.Initial] : F.Final
• CategoryTheory.Functor.final_op_of_initial 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] : F.op.Final
• CategoryTheory.Functor.initial_of_final_op 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.op.Final] : F.Initial
• CategoryTheory.Functor.initial_op_of_final 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Final] : F.op.Initial
• CategoryTheory.Functor.instFinalOppositeLeftOpOfInitial 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C Dᵒᵖ) [F.Initial] : F.leftOp.Final
• CategoryTheory.Functor.instFinalOppositeRightOpOfInitial 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor Cᵒᵖ D) [F.Initial] : F.rightOp.Final
• CategoryTheory.Functor.instInitialOppositeLeftOpOfFinal 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C Dᵒᵖ) [F.Final] : F.leftOp.Initial
• CategoryTheory.Functor.instInitialOppositeRightOpOfFinal 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor Cᵒᵖ D) [F.Final] : F.rightOp.Initial
• CategoryTheory.Functor.Initial.homToLift 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] (d : D) : F.obj (CategoryTheory.Functor.Initial.lift F d) ⟶ d
• CategoryTheory.Functor.initial_of_natIso 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F F' : CategoryTheory.Functor C D} [F.Initial] (i : F ≅ F') : F'.Initial
• CategoryTheory.Functor.initial_natIso_iff 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F F' : CategoryTheory.Functor C D} (i : F ≅ F') : F.Initial ↔ F'.Initial
• CategoryTheory.Functor.Initial.createsLimitsOfShapeOfInitial 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (H : CategoryTheory.Functor E B) [CategoryTheory.CreatesLimitsOfShape C H] : CategoryTheory.CreatesLimitsOfShape D H
• CategoryTheory.Functor.Initial.preservesLimitsOfShape_of_initial 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (H : CategoryTheory.Functor E B) [CategoryTheory.Limits.PreservesLimitsOfShape C H] : CategoryTheory.Limits.PreservesLimitsOfShape D H
• CategoryTheory.Functor.Initial.reflectsLimitsOfShape_of_initial 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (H : CategoryTheory.Functor E B) [CategoryTheory.Limits.ReflectsLimitsOfShape C H] : CategoryTheory.Limits.ReflectsLimitsOfShape D H
• CategoryTheory.Functor.initial_comp 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.Initial] [G.Initial] : (F.comp G).Initial
• CategoryTheory.Functor.initial_comp_equivalence 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.Initial] [G.IsEquivalence] : (F.comp G).Initial
• CategoryTheory.Functor.initial_equivalence_comp 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.IsEquivalence] [G.Initial] : (F.comp G).Initial
• CategoryTheory.Functor.initial_of_equivalence_comp 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.IsEquivalence] [(F.comp G).Initial] : G.Initial
• CategoryTheory.Functor.initial_of_initial_comp 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.Initial] [(F.comp G).Initial] : G.Initial
• CategoryTheory.Functor.Initial.comp_hasLimit 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} [CategoryTheory.Limits.HasLimit G] : CategoryTheory.Limits.HasLimit (F.comp G)
• CategoryTheory.Functor.Initial.hasLimit_of_comp 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} [CategoryTheory.Limits.HasLimit (F.comp G)] : CategoryTheory.Limits.HasLimit G
• CategoryTheory.Functor.Initial.limitConeComp 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.LimitCone G) : CategoryTheory.Limits.LimitCone (F.comp G)
• CategoryTheory.Functor.Initial.limitConeOfComp 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.LimitCone (F.comp G)) : CategoryTheory.Limits.LimitCone G
• CategoryTheory.Functor.initial_iff_comp_equivalence 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [G.IsEquivalence] : F.Initial ↔ (F.comp G).Initial
• CategoryTheory.Functor.initial_iff_equivalence_comp 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.IsEquivalence] : G.Initial ↔ (F.comp G).Initial
• CategoryTheory.Functor.initial_iff_initial_comp 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.Initial] : G.Initial ↔ (F.comp G).Initial
• CategoryTheory.Functor.Initial.hasLimit_comp_iff 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} : CategoryTheory.Limits.HasLimit (F.comp G) ↔ CategoryTheory.Limits.HasLimit G
• CategoryTheory.instInitialCostructuredArrowOverToOver 📋 Mathlib.CategoryTheory.Limits.Final
  {C₀ : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} C₀] [CategoryTheory.Category.{v_2, u_2} C] (F : CategoryTheory.Functor C₀ C) (X : C) [F.Initial] : (CategoryTheory.CostructuredArrow.toOver F X).Initial
• CategoryTheory.Functor.initial_of_comp_full_faithful 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [G.Full] [G.Faithful] [(F.comp G).Initial] : F.Initial
• CategoryTheory.Functor.initial_of_comp_full_faithful' 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [G.Full] [G.Faithful] [(F.comp G).Initial] : G.Initial
• CategoryTheory.Functor.initial_iff_comp_initial_full_faithful 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [G.Initial] [G.Full] [G.Faithful] : F.Initial ↔ (F.comp G).Initial
• CategoryTheory.Functor.Initial.compCreatesLimit 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {H : CategoryTheory.Functor E B} [CategoryTheory.CreatesLimit G H] : CategoryTheory.CreatesLimit (F.comp G) H
• CategoryTheory.Functor.Initial.comp_preservesLimit 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {H : CategoryTheory.Functor E B} [CategoryTheory.Limits.PreservesLimit G H] : CategoryTheory.Limits.PreservesLimit (F.comp G) H
• CategoryTheory.Functor.Initial.comp_reflectsLimit 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {H : CategoryTheory.Functor E B} [CategoryTheory.Limits.ReflectsLimit G H] : CategoryTheory.Limits.ReflectsLimit (F.comp G) H
• CategoryTheory.Functor.Initial.createsLimitOfComp 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {H : CategoryTheory.Functor E B} [CategoryTheory.CreatesLimit (F.comp G) H] : CategoryTheory.CreatesLimit G H
• CategoryTheory.Functor.Initial.preservesLimit_of_comp 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {H : CategoryTheory.Functor E B} [CategoryTheory.Limits.PreservesLimit (F.comp G) H] : CategoryTheory.Limits.PreservesLimit G H
• CategoryTheory.Functor.Initial.reflectsLimit_of_comp 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {H : CategoryTheory.Functor E B} [CategoryTheory.Limits.ReflectsLimit (F.comp G) H] : CategoryTheory.Limits.ReflectsLimit G H
• CategoryTheory.ObjectProperty.initial_ι 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty C) (h : ∀ (d : C), ¬P d → CategoryTheory.IsConnected (CategoryTheory.CostructuredArrow P.ι d)) : P.ι.Initial
• CategoryTheory.Functor.Initial.preservesLimit_comp_iff 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {H : CategoryTheory.Functor E B} : CategoryTheory.Limits.PreservesLimit (F.comp G) H ↔ CategoryTheory.Limits.PreservesLimit G H
• CategoryTheory.instInitialProdProd 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C' : Type u₃} [CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C' D') [F.Initial] [G.Initial] : (F.prod G).Initial
• CategoryTheory.Functor.Initial.isLimitWhiskerEquiv 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.Cone G) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Cone.whisker F t) ≃ CategoryTheory.Limits.IsLimit t
• CategoryTheory.Functor.Initial.conesEquiv 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor D E) : CategoryTheory.Limits.Cone (F.comp G) ≌ CategoryTheory.Limits.Cone G
• CategoryTheory.Functor.Initial.extendCone 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} : CategoryTheory.Functor (CategoryTheory.Limits.Cone (F.comp G)) (CategoryTheory.Limits.Cone G)
• CategoryTheory.Functor.Initial.limitIso 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.HasLimit G] : CategoryTheory.Limits.limit (F.comp G) ≅ CategoryTheory.Limits.limit G
• CategoryTheory.CostructuredArrow.initial_pre 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (T : CategoryTheory.Functor C D) [T.Initial] (S : CategoryTheory.Functor D E) (X : E) : (CategoryTheory.CostructuredArrow.pre T S X).Initial
• CategoryTheory.Limits.IsLimit.overPost 📋 Mathlib.CategoryTheory.Limits.Final
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] {D : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone D} (hc : CategoryTheory.Limits.IsLimit c) (j : J) [(CategoryTheory.Over.forget j).Initial] : CategoryTheory.Limits.IsLimit (c.overPost j)
• CategoryTheory.Functor.Initial.limitConeComp_cone 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.LimitCone G) : (CategoryTheory.Functor.Initial.limitConeComp F t).cone = CategoryTheory.Limits.Cone.whisker F t.cone
• CategoryTheory.Functor.Initial.limit_pre_isIso 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} [CategoryTheory.Limits.HasLimit G] : CategoryTheory.IsIso (CategoryTheory.Limits.limit.pre G F)
• CategoryTheory.Functor.Initial.isLimitExtendConeEquiv 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.Cone (F.comp G)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.Initial.extendCone.obj t) ≃ CategoryTheory.Limits.IsLimit t
• CategoryTheory.Functor.Initial.extendCone_obj_pt 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cone (F.comp G)) : (CategoryTheory.Functor.Initial.extendCone.obj c).pt = c.pt
• CategoryTheory.Functor.Initial.conesEquiv_inverse 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor D E) : (CategoryTheory.Functor.Initial.conesEquiv F G).inverse = CategoryTheory.Limits.Cone.whiskering F
• CategoryTheory.Functor.Initial.conesEquiv_functor 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor D E) : (CategoryTheory.Functor.Initial.conesEquiv F G).functor = CategoryTheory.Functor.Initial.extendCone
• CategoryTheory.Functor.Initial.limitConeOfComp_cone 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.LimitCone (F.comp G)) : (CategoryTheory.Functor.Initial.limitConeOfComp F t).cone = CategoryTheory.Functor.Initial.extendCone.obj t.cone
• CategoryTheory.Functor.Initial.limitIso_inv 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.HasLimit G] : (CategoryTheory.Functor.Initial.limitIso F G).inv = CategoryTheory.Limits.limit.pre G F
• CategoryTheory.Functor.Initial.limIso 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.Limits.HasLimitsOfShape D E] [CategoryTheory.Limits.HasLimitsOfShape C E] : ((CategoryTheory.Functor.whiskeringLeft C D E).obj F).comp CategoryTheory.Limits.lim ≅ CategoryTheory.Limits.lim
• CategoryTheory.Functor.Initial.limitIso_hom 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.HasLimit G] : (CategoryTheory.Functor.Initial.limitIso F G).hom = CategoryTheory.inv (CategoryTheory.Limits.limit.pre G F)
• CategoryTheory.Functor.Initial.induction 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {d : D} (Z : (X : C) → (F.obj X ⟶ d) → Sort u_1) (h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → CategoryTheory.CategoryStruct.comp (F.map f) k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂) (h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → CategoryTheory.CategoryStruct.comp (F.map f) k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁) {X₀ : C} {k₀ : F.obj X₀ ⟶ d} (z : Z X₀ k₀) : Z (CategoryTheory.Functor.Initial.lift F d) (CategoryTheory.Functor.Initial.homToLift F d)
• CategoryTheory.Functor.Initial.extendCone_obj_π_app 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cone (F.comp G)) (d : D) : (CategoryTheory.Functor.Initial.extendCone.obj c).π.app d = CategoryTheory.CategoryStruct.comp (c.π.app (CategoryTheory.Functor.Initial.lift F d)) (G.map (CategoryTheory.Functor.Initial.homToLift F d))
• CategoryTheory.Functor.Initial.limitConeComp_isLimit 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.LimitCone G) : (CategoryTheory.Functor.Initial.limitConeComp F t).isLimit = (CategoryTheory.Functor.Initial.isLimitWhiskerEquiv F t.cone).symm t.isLimit
• CategoryTheory.Functor.Initial.limit_cone_comp_aux 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (s : CategoryTheory.Limits.Cone (F.comp G)) (j : C) : CategoryTheory.CategoryStruct.comp (s.π.app (CategoryTheory.Functor.Initial.lift F (F.obj j))) (G.map (CategoryTheory.Functor.Initial.homToLift F (F.obj j))) = s.π.app j
• CategoryTheory.Functor.Initial.extendCone_obj_π_app' 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cone (F.comp G)) {X : C} {Y : D} (f : F.obj X ⟶ Y) : (CategoryTheory.Functor.Initial.extendCone.obj c).π.app Y = CategoryTheory.CategoryStruct.comp (c.π.app X) (G.map f)
• CategoryTheory.Functor.Initial.conesEquiv_counitIso 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor D E) : (CategoryTheory.Functor.Initial.conesEquiv F G).counitIso = CategoryTheory.NatIso.ofComponents (fun c => CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl (((CategoryTheory.Limits.Cone.whiskering F).comp CategoryTheory.Functor.Initial.extendCone).obj c).pt) ⋯) ⋯
• CategoryTheory.Functor.Initial.extendCone_map_hom 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} {X✝ Y✝ : CategoryTheory.Limits.Cone (F.comp G)} (f : X✝ ⟶ Y✝) : (CategoryTheory.Functor.Initial.extendCone.map f).hom = f.hom
• CategoryTheory.Functor.Initial.limitConeOfComp_isLimit 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.LimitCone (F.comp G)) : (CategoryTheory.Functor.Initial.limitConeOfComp F t).isLimit = (CategoryTheory.Functor.Initial.isLimitExtendConeEquiv F t.cone).symm t.isLimit
• CategoryTheory.Functor.Initial.conesEquiv_unitIso 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor D E) : (CategoryTheory.Functor.Initial.conesEquiv F G).unitIso = CategoryTheory.NatIso.ofComponents (fun c => CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone (F.comp G))).obj c).pt) ⋯) ⋯
• CategoryTheory.Limits.LimitPresentation.reindex 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (P : CategoryTheory.Limits.LimitPresentation J X) {J' : Type u_1} [CategoryTheory.Category.{v_1, u_1} J'] (F : CategoryTheory.Functor J' J) [F.Initial] : CategoryTheory.Limits.LimitPresentation J' X
• CategoryTheory.Limits.LimitPresentation.reindex_diag 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (P : CategoryTheory.Limits.LimitPresentation J X) {J' : Type u_1} [CategoryTheory.Category.{v_1, u_1} J'] (F : CategoryTheory.Functor J' J) [F.Initial] : (P.reindex F).diag = F.comp P.diag
• CategoryTheory.Limits.LimitPresentation.reindex_π 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (P : CategoryTheory.Limits.LimitPresentation J X) {J' : Type u_1} [CategoryTheory.Category.{v_1, u_1} J'] (F : CategoryTheory.Functor J' J) [F.Initial] : (P.reindex F).π = F.whiskerLeft P.π
• CategoryTheory.ObjectProperty.LimitOfShape.reindex 📋 Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'} [CategoryTheory.Category.{v', u'} J] {J' : Type u''} [CategoryTheory.Category.{v'', u''} J'] {X : C} (h : P.LimitOfShape J X) (G : CategoryTheory.Functor J' J) [G.Initial] : P.LimitOfShape J' X
• CategoryTheory.ObjectProperty.limitsOfShape_le_of_initial 📋 Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {J : Type u'} [CategoryTheory.Category.{v', u'} J] {J' : Type u''} [CategoryTheory.Category.{v'', u''} J'] (G : CategoryTheory.Functor J J') [G.Initial] : P.limitsOfShape J' ≤ P.limitsOfShape J
• CategoryTheory.ObjectProperty.LimitOfShape.reindex_toLimitPresentation 📋 Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'} [CategoryTheory.Category.{v', u'} J] {J' : Type u''} [CategoryTheory.Category.{v'', u''} J'] {X : C} (h : P.LimitOfShape J X) (G : CategoryTheory.Functor J' J) [G.Initial] : (h.reindex G).toLimitPresentation = h.reindex G
• CategoryTheory.Limits.IsCofiltered.sequentialFunctor_initial 📋 Mathlib.CategoryTheory.Limits.Shapes.Countable
  (J : Type u_2) [Countable J] [Preorder J] [CategoryTheory.IsCofiltered J] : (CategoryTheory.Limits.IsCofiltered.sequentialFunctor J).Initial
• CategoryTheory.hasExactLimitsOfShape_of_initial 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C] {J : Type u_1} {J' : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} J'] (F : CategoryTheory.Functor J J') [F.Initial] [CategoryTheory.Limits.HasLimitsOfShape J' C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.HasExactLimitsOfShape J C] : CategoryTheory.HasExactLimitsOfShape J' C
• CategoryTheory.instInitialDiscreteOfIsConnected 📋 Mathlib.CategoryTheory.Limits.Final.Connected
  {C : Type u} [CategoryTheory.Category.{v, u} C] {T : Type w} [Unique T] (F : CategoryTheory.Functor C (CategoryTheory.Discrete T)) [CategoryTheory.IsConnected C] : F.Initial
• CategoryTheory.initial_fst 📋 Mathlib.CategoryTheory.Limits.Final.Connected
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.IsConnected D] : (CategoryTheory.Prod.fst C D).Initial
• CategoryTheory.initial_snd 📋 Mathlib.CategoryTheory.Limits.Final.Connected
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.IsConnected C] : (CategoryTheory.Prod.snd C D).Initial
• CategoryTheory.isConnected_iff_initial_of_unique 📋 Mathlib.CategoryTheory.Limits.Final.Connected
  {C : Type u} [CategoryTheory.Category.{v, u} C] {T : Type w} [Unique T] (F : CategoryTheory.Functor C (CategoryTheory.Discrete T)) : CategoryTheory.IsConnected C ↔ F.Initial
• CategoryTheory.Functor.isConnected_iff_of_initial 📋 Mathlib.CategoryTheory.Limits.IsConnected
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] : CategoryTheory.IsConnected C ↔ CategoryTheory.IsConnected D
• CategoryTheory.Functor.initial_diag_of_isFiltered 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsCofilteredOrEmpty C] : (CategoryTheory.Functor.diag C).Initial
• CategoryTheory.Functor.initial_of_isCofiltered_pUnit 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsCofiltered C] (F : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{u_1 + 1})) : F.Initial
• CategoryTheory.Over.initial_forget 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsCofilteredOrEmpty C] (c : C) : (CategoryTheory.Over.forget c).Initial
• CategoryTheory.IsFiltered.initial_fst 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.IsCofiltered D] : (CategoryTheory.Prod.fst C D).Initial
• CategoryTheory.IsFiltered.initial_snd 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.IsCofiltered C] : (CategoryTheory.Prod.snd C D).Initial
• CategoryTheory.initial_eval 📋 Mathlib.CategoryTheory.Filtered.Final
  {α : Type u₁} {I : α → Type u₂} [(s : α) → CategoryTheory.Category.{v₂, u₂} (I s)] [∀ (s : α), CategoryTheory.IsCofiltered (I s)] (s : α) : (CategoryTheory.Pi.eval I s).Initial
• CategoryTheory.Functor.initial_of_isCofiltered_costructuredArrow 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [∀ (d : D), CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow F d)] : F.Initial
• CategoryTheory.Functor.initial_iff_isCofiltered_costructuredArrow 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C] : F.Initial ↔ ∀ (d : D), CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow F d)
• CategoryTheory.Functor.initial_const_of_isInitial 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.IsCofiltered C] {X : D} (hX : CategoryTheory.Limits.IsInitial X) : ((CategoryTheory.Functor.const C).obj X).Initial
• CategoryTheory.Functor.initial_const_initial 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.IsCofiltered C] [CategoryTheory.Limits.HasInitial D] : ((CategoryTheory.Functor.const C).obj (⊥_ D)).Initial
• CategoryTheory.CostructuredArrow.initial_proj_of_isCofiltered 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.IsCofilteredOrEmpty C] (T : CategoryTheory.Functor C D) [T.Initial] (Y : D) : (CategoryTheory.CostructuredArrow.proj T Y).Initial
• Monotone.initial_functor_iff 📋 Mathlib.CategoryTheory.Filtered.Final
  {J₁ : Type u_1} {J₂ : Type u_2} [Preorder J₁] [Preorder J₂] [IsCodirectedOrder J₁] {f : J₁ → J₂} (hf : Monotone f) : hf.functor.Initial ↔ ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁
• CategoryTheory.Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty D] [F.Full] [F.Faithful] (h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) : F.Initial
• CategoryTheory.CostructuredArrow.initial_post 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.IsCofiltered C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (X : D) (T : CategoryTheory.Functor C D) [T.Initial] (S : CategoryTheory.Functor D E) [S.Initial] : (CategoryTheory.CostructuredArrow.post T S X).Initial
• CategoryTheory.CostructuredArrow.initial_map₂_id 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.IsCofiltered C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (T : CategoryTheory.Functor C D) [T.Initial] (S : CategoryTheory.Functor D E) [S.Initial] (d : D) (e : E) (u : S.obj d ⟶ e) : (CategoryTheory.CostructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (T.comp S)) u).Initial
• CategoryTheory.Functor.Initial.exists_eq 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C] [F.Initial] {d : D} {c : C} (s s' : F.obj c ⟶ d) : ∃ c' t, CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s'
• CategoryTheory.Functor.initial_of_exists_of_isCofiltered 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C] (h₁ : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) (h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s') : F.Initial
• CategoryTheory.Functor.initial_iff_of_isCofiltered 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C] : F.Initial ↔ (∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) ∧ ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s'
• CategoryTheory.InitiallySmall.mk' 📋 Mathlib.CategoryTheory.Limits.FinallySmall
  {J : Type u} [CategoryTheory.Category.{v, u} J] {S : Type w} [CategoryTheory.SmallCategory S] (F : CategoryTheory.Functor S J) [F.Initial] : CategoryTheory.InitiallySmall J
• CategoryTheory.initial_fromInitialModel 📋 Mathlib.CategoryTheory.Limits.FinallySmall
  (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.InitiallySmall J] : (CategoryTheory.fromInitialModel J).Initial
• CategoryTheory.initiallySmall_of_initial_of_essentiallySmall 📋 Mathlib.CategoryTheory.Limits.FinallySmall
  {J : Type u} [CategoryTheory.Category.{v, u} J] {K : Type u₁} [CategoryTheory.Category.{v₁, u₁} K] [CategoryTheory.EssentiallySmall.{w, v₁, u₁} K] (F : CategoryTheory.Functor K J) [F.Initial] : CategoryTheory.InitiallySmall J
• CategoryTheory.initiallySmall_of_initial_of_initiallySmall 📋 Mathlib.CategoryTheory.Limits.FinallySmall
  {J : Type u} [CategoryTheory.Category.{v, u} J] {K : Type u₁} [CategoryTheory.Category.{v₁, u₁} K] [CategoryTheory.InitiallySmall K] (F : CategoryTheory.Functor K J) [F.Initial] : CategoryTheory.InitiallySmall J
• CategoryTheory.InitiallySmall.initial_smallCategory 📋 Mathlib.CategoryTheory.Limits.FinallySmall
  {J : Type u} {inst✝ : CategoryTheory.Category.{v, u} J} [self : CategoryTheory.InitiallySmall J] : ∃ S x F, F.Initial
• CategoryTheory.InitiallySmall.mk 📋 Mathlib.CategoryTheory.Limits.FinallySmall
  {J : Type u} [CategoryTheory.Category.{v, u} J] (initial_smallCategory : ∃ S x F, F.Initial) : CategoryTheory.InitiallySmall J
• CategoryTheory.InitiallySmall.instInitialCofilteredInitialModelFromCofilteredInitialModel 📋 Mathlib.CategoryTheory.Filtered.FinallySmall
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.InitiallySmall C] : (CategoryTheory.InitiallySmall.fromCofilteredInitialModel C).Initial
• CategoryTheory.InitiallySmall.exists_of_isCofiltered 📋 Mathlib.CategoryTheory.Filtered.FinallySmall
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.InitiallySmall C] : ∃ D x, ∃ (_ : CategoryTheory.IsCofiltered D), ∃ F, F.Initial
• CategoryTheory.initial_of_representablyCoflat 📋 Mathlib.CategoryTheory.Functor.Flat
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [h : CategoryTheory.RepresentablyCoflat F] : F.Initial
• CategoryTheory.instInitialCostructuredArrowCompPreOfRepresentablyCoflat 📋 Mathlib.CategoryTheory.Functor.Flat
  {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : E) [CategoryTheory.RepresentablyCoflat F] : (CategoryTheory.CostructuredArrow.pre F G X).Initial
• CategoryTheory.Functor.bijective_sectionsPrecomp 📋 Mathlib.CategoryTheory.Limits.Final.Type
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (P : CategoryTheory.Functor D (Type w)) [F.Initial] : Function.Bijective F.sectionsPrecomp
• SimplexCategory.Truncated.initial_inclusion 📋 Mathlib.AlgebraicTopology.SimplexCategory.Truncated
  {n : ℕ} [NeZero n] : (SimplexCategory.Truncated.inclusion n).Initial
• SimplexCategory.Truncated.initial_incl 📋 Mathlib.AlgebraicTopology.SimplexCategory.Truncated
  {n m : ℕ} [NeZero n] (hm : n ≤ m) : (SimplexCategory.Truncated.incl n m ⋯).Initial
• CategoryTheory.TwoSquare.instInitialStructuredArrowObjStructuredArrowDownwardsOfGuitartExact 📋 Mathlib.CategoryTheory.GuitartExact.Basic
  {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₃, u₃} C₃] [CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) [hw : w.GuitartExact] (X₂ : C₂) : (w.structuredArrowDownwards X₂).Initial
• CategoryTheory.TwoSquare.guitartExact_iff_initial 📋 Mathlib.CategoryTheory.GuitartExact.Basic
  {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₃, u₃} C₃] [CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) : w.GuitartExact ↔ ∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial
• CategoryTheory.TwoSquare.structuredArrowDownwards_initial_iff_of_iso 📋 Mathlib.CategoryTheory.GuitartExact.Basic
  {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₃, u₃} C₃] [CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) {X₂ X₂' : C₂} (e : X₂ ≅ X₂') : (w.structuredArrowDownwards X₂).Initial ↔ (w.structuredArrowDownwards X₂').Initial
• CategoryTheory.TwoSquare.hasPointwiseRightKanExtensionAt_iff 📋 Mathlib.CategoryTheory.GuitartExact.KanExtension
  {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} {D : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₃, u₃} C₃] [CategoryTheory.Category.{v₄, u₄} C₄] [CategoryTheory.Category.{v₅, u₅} D] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) (F : CategoryTheory.Functor C₃ D) (X₂ : C₂) [(w.structuredArrowDownwards X₂).Initial] : T.HasPointwiseRightKanExtensionAt (L.comp F) X₂ ↔ B.HasPointwiseRightKanExtensionAt F (R.obj X₂)
• CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionAtCompTwoSquareEquiv 📋 Mathlib.CategoryTheory.GuitartExact.KanExtension
  {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} {D : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₃, u₃} C₃] [CategoryTheory.Category.{v₄, u₄} C₄] [CategoryTheory.Category.{v₅, u₅} D] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} {F : CategoryTheory.Functor C₃ D} (E : B.RightExtension F) (w : CategoryTheory.TwoSquare T L R B) (X₂ : C₂) [(w.structuredArrowDownwards X₂).Initial] : (E.compTwoSquare w).IsPointwiseRightKanExtensionAt X₂ ≃ E.IsPointwiseRightKanExtensionAt (R.obj X₂)
• CategoryTheory.Functor.RightExtension.nonempty_isPointwiseRightKanExtensionAt_compTwoSquare_iff 📋 Mathlib.CategoryTheory.GuitartExact.KanExtension
  {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} {D : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₃, u₃} C₃] [CategoryTheory.Category.{v₄, u₄} C₄] [CategoryTheory.Category.{v₅, u₅} D] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} {F : CategoryTheory.Functor C₃ D} (E : B.RightExtension F) (w : CategoryTheory.TwoSquare T L R B) (X₂ : C₂) [(w.structuredArrowDownwards X₂).Initial] : Nonempty ((E.compTwoSquare w).IsPointwiseRightKanExtensionAt X₂) ↔ Nonempty (E.IsPointwiseRightKanExtensionAt (R.obj X₂))
• localCohomology.ideal_powers_initial 📋 Mathlib.Algebra.Homology.LocalCohomology
  {R : Type u} [CommRing R] {J : Ideal R} [hR : IsNoetherian R R] : (localCohomology.idealPowersToSelfLERadical J).Initial
• localCohomology.isoOfFinal 📋 Mathlib.Algebra.Homology.LocalCohomology
  {R : Type u} [CommRing R] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] (I' : CategoryTheory.Functor E D) (I : CategoryTheory.Functor D (Ideal R)) [I'.Initial] (i : ℕ) [CategoryTheory.Limits.HasColimit (localCohomology.diagram (I'.comp I) i)] [CategoryTheory.Limits.HasColimit (localCohomology.diagram I i)] : localCohomology.ofDiagram (I'.comp I) i ≅ localCohomology.ofDiagram I i
• CategoryTheory.Comma.isConnected_comma_of_initial 📋 Mathlib.CategoryTheory.Comma.Final
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [CategoryTheory.IsConnected B] [L.Initial] : CategoryTheory.IsConnected (CategoryTheory.Comma L R)
• CategoryTheory.Comma.isCofiltered_of_initial 📋 Mathlib.CategoryTheory.Comma.Final
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [CategoryTheory.IsCofiltered A] [CategoryTheory.IsCofiltered B] [L.Initial] : CategoryTheory.IsCofiltered (CategoryTheory.Comma L R)
• CategoryTheory.Comma.initial_snd 📋 Mathlib.CategoryTheory.Comma.Final
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [L.Initial] : (CategoryTheory.Comma.snd L R).Initial
• CategoryTheory.Comma.initial_fst 📋 Mathlib.CategoryTheory.Comma.Final
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [CategoryTheory.IsCofiltered A] [CategoryTheory.IsCofiltered B] [L.Initial] : (CategoryTheory.Comma.fst L R).Initial
• CategoryTheory.Comma.initial_snd_of_isConnected_costructuredArrow 📋 Mathlib.CategoryTheory.Comma.Final
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [∀ (b : B), CategoryTheory.IsConnected (CategoryTheory.CostructuredArrow L (R.obj b))] : (CategoryTheory.Comma.snd L R).Initial
• CategoryTheory.Comma.initial_fst_of_isCofiltered_costructuredArrow 📋 Mathlib.CategoryTheory.Comma.Final
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [CategoryTheory.IsCofiltered A] [CategoryTheory.IsCofiltered B] [∀ (b : B), CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow L (R.obj b))] : (CategoryTheory.Comma.fst L R).Initial
• CategoryTheory.Join.instInitialInclLeftOfIsConnected 📋 Mathlib.CategoryTheory.Join.Final
  (C : Type u_1) (D : Type u_2) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.IsConnected C] : (CategoryTheory.Join.inclLeft C D).Initial
• CategoryTheory.Limits.exists_eq_isLimitMap_of_preservesColimit_yoneda 📋 Mathlib.CategoryTheory.Limits.ConstructLimitMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u₂} [CategoryTheory.Category.{v₂, u₂} I] {I' : Type u₃} [CategoryTheory.Category.{v₃, u₃} I'] {D : CategoryTheory.Functor I C} {D' : CategoryTheory.Functor I' C} {c : CategoryTheory.Limits.Cone D} {c' : CategoryTheory.Limits.Cone D'} (hc : CategoryTheory.Limits.IsLimit c) (hc' : CategoryTheory.Limits.IsLimit c') (f : c.pt ⟶ c'.pt) [CategoryTheory.IsCofiltered I] [CategoryTheory.IsCofiltered I'] [∀ (i : I'), CategoryTheory.Limits.PreservesColimit D.op (CategoryTheory.yoneda.obj (D'.obj i))] : ∃ J x, ∃ (_ : CategoryTheory.IsCofiltered J), ∃ G G', ∃ (_ : G.Initial) (x_3 : G'.Initial), ∃ g, f = CategoryTheory.Limits.IsLimit.map (CategoryTheory.Limits.Cone.whisker G c) ((CategoryTheory.Functor.Initial.isLimitWhiskerEquiv G' c').symm hc') g
• CategoryTheory.Limits.parallelPair_initial_mk' 📋 Mathlib.CategoryTheory.Limits.Final.ParallelPair
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y) (h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)) (h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), CategoryTheory.Zigzag (CategoryTheory.CostructuredArrow.mk i) (CategoryTheory.CostructuredArrow.mk j)) : (CategoryTheory.Limits.parallelPair f g).Initial
• CategoryTheory.Limits.parallelPair_initial_mk 📋 Mathlib.CategoryTheory.Limits.Final.ParallelPair
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y) (h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)) (h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ a, i = CategoryTheory.CategoryStruct.comp f a ∧ j = CategoryTheory.CategoryStruct.comp g a) : (CategoryTheory.Limits.parallelPair f g).Initial
• CategoryTheory.regularTopology.parallelPair_pullback_initial 📋 Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X B : C} (π : X ⟶ B) (c : CategoryTheory.Limits.PullbackCone π π) (hc : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.Limits.parallelPair (CategoryTheory.ObjectProperty.homMk (CategoryTheory.Over.homMk c.fst ⋯)).op (CategoryTheory.ObjectProperty.homMk (CategoryTheory.Over.homMk c.snd ⋯)).op).Initial
• CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.instInitialElementsFiberFunctorOfIsCofiltered 📋 Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {N : Type u'} [CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C) [CategoryTheory.InitiallySmall N] [CategoryTheory.IsCofiltered N] : (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor p).Initial
• Profinite.Extend.functor_initial 📋 Mathlib.Topology.Category.Profinite.Extend
  {I : Type u} [CategoryTheory.SmallCategory I] [CategoryTheory.IsCofiltered I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : I), CategoryTheory.Epi (c.π.app i)] : (Profinite.Extend.functor c).Initial
• LightProfinite.Extend.functor_initial 📋 Mathlib.Topology.Category.LightProfinite.Extend
  {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)] : (LightProfinite.Extend.functor c).Initial
• TopologicalSpace.Compacts.instInitialElemOpensOpenRcNhdsCompactNhdsFunctorOfT2Space 📋 Mathlib.Topology.Sets.BaseChangeNhds
  {α : Type u_1} [TopologicalSpace α] {K : TopologicalSpace.Compacts α} [T2Space α] : ⋯.functor.Initial
• TopologicalSpace.Compacts.instInitialElemOpensOpenRcNhdsOpenNhdsFunctorOfT2SpaceOfLocallyCompactSpace 📋 Mathlib.Topology.Sets.BaseChangeNhds
  {α : Type u_1} [TopologicalSpace α] {K : TopologicalSpace.Compacts α} [T2Space α] [LocallyCompactSpace α] : ⋯.functor.Initial

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