Loogle!

Result

Found 263 declarations mentioning CategoryTheory.Limits.IsInitial. Of these, only the first 200 are shown.

• CategoryTheory.Limits.IsInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) : Type (max u₁ v₁)
• CategoryTheory.Limits.initialOpOfTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (t : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.IsInitial (Opposite.op X)
• CategoryTheory.Limits.terminalOpOfInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (t : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Limits.IsTerminal (Opposite.op X)
• CategoryTheory.Limits.IsInitial.op 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X : C} (hX : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Limits.IsTerminal (Opposite.op X)
• CategoryTheory.Limits.IsTerminal.op 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X : C} (hX : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.IsInitial (Opposite.op X)
• CategoryTheory.Limits.initialUnopOfTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} (t : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.IsInitial (Opposite.unop X)
• CategoryTheory.Limits.terminalUnopOfInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} (t : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Limits.IsTerminal (Opposite.unop X)
• CategoryTheory.Limits.IsInitial.ofIso 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y Z : C} (hY : CategoryTheory.Limits.IsInitial Y) (i : Y ≅ Z) : CategoryTheory.Limits.IsInitial Z
• CategoryTheory.Limits.IsInitial.to 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (t : CategoryTheory.Limits.IsInitial X) (Y : C) : X ⟶ Y
• CategoryTheory.Limits.IsInitial.uniqueUpToIso 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T T' : C} (hT : CategoryTheory.Limits.IsInitial T) (hT' : CategoryTheory.Limits.IsInitial T') : T ≅ T'
• CategoryTheory.Limits.IsInitial.unop 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} (hX : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Limits.IsTerminal (Opposite.unop X)
• CategoryTheory.Limits.IsTerminal.unop 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} (hX : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.IsInitial (Opposite.unop X)
• CategoryTheory.Limits.IsInitial.equivOfIso 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (e : X ≅ Y) : CategoryTheory.Limits.IsInitial X ≃ CategoryTheory.Limits.IsInitial Y
• CategoryTheory.Limits.IsInitial.ofUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) [h : (Y : C) → Unique (X ⟶ Y)] : CategoryTheory.Limits.IsInitial X
• CategoryTheory.Limits.isInitialBot 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {α : Type u_1} [Preorder α] [OrderBot α] : CategoryTheory.Limits.IsInitial ⊥
• CategoryTheory.Limits.coneOfDiagramInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (tX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.InitialMonoClass.isInitial_mono_from 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} [self : CategoryTheory.Limits.InitialMonoClass C] {I : C} (X : C) (hI : CategoryTheory.Limits.IsInitial I) : CategoryTheory.Mono (hI.to X)
• CategoryTheory.Limits.InitialMonoClass.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (isInitial_mono_from : ∀ {I : C} (X : C) (hI : CategoryTheory.Limits.IsInitial I), CategoryTheory.Mono (hI.to X)) : CategoryTheory.Limits.InitialMonoClass C
• CategoryTheory.Limits.InitialMonoClass.of_isInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : C} (hI : CategoryTheory.Limits.IsInitial I) (h : ∀ (X : C), CategoryTheory.Mono (hI.to X)) : CategoryTheory.Limits.InitialMonoClass C
• CategoryTheory.Limits.IsInitial.epi_to 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (t : CategoryTheory.Limits.IsInitial X) (f : Y ⟶ X) : CategoryTheory.Epi f
• CategoryTheory.Limits.IsInitial.isSplitEpi_to 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (t : CategoryTheory.Limits.IsInitial X) (f : Y ⟶ X) : CategoryTheory.IsSplitEpi f
• CategoryTheory.Limits.InitialMonoClass.of_isTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I T : C} (hI : CategoryTheory.Limits.IsInitial I) (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Mono (hI.to T) → CategoryTheory.Limits.InitialMonoClass C
• CategoryTheory.Limits.IsInitial.mono_from 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.InitialMonoClass C] {I X : C} (hI : CategoryTheory.Limits.IsInitial I) (f : I ⟶ X) : CategoryTheory.Mono f
• CategoryTheory.Limits.isIso_of_isInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (hY : CategoryTheory.Limits.IsInitial Y) (hX : CategoryTheory.Limits.IsInitial X) (f : Y ⟶ X) : CategoryTheory.IsIso f
• CategoryTheory.Limits.limitOfDiagramInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (tX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfDiagramInitial tX F)
• CategoryTheory.Limits.IsInitial.to_self 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (t : CategoryTheory.Limits.IsInitial X) : t.to X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.isColimitEquivIsInitialOfIsEmpty 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] [IsEmpty J] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.IsColimit c ≃ CategoryTheory.Limits.IsInitial c.pt
• CategoryTheory.Limits.coneOfDiagramInitial_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (tX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor J C) : (CategoryTheory.Limits.coneOfDiagramInitial tX F).pt = F.obj X
• CategoryTheory.Limits.IsInitial.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (t : CategoryTheory.Limits.IsInitial X) (f g : X ⟶ Y) : f = g
• CategoryTheory.Functor.isInitialConst 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {X : D} (hX : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Limits.IsInitial ((CategoryTheory.Functor.const C).obj X)
• CategoryTheory.Limits.IsInitial.ofUniqueHom 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (h : (Y : C) → X ⟶ Y) (uniq : ∀ (Y : C) (m : X ⟶ Y), m = h Y) : CategoryTheory.Limits.IsInitial X
• CategoryTheory.Limits.IsInitial.uniqueUpToIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T T' : C} (hT : CategoryTheory.Limits.IsInitial T) (hT' : CategoryTheory.Limits.IsInitial T') : (hT.uniqueUpToIso hT').hom = hT.to T'
• CategoryTheory.Limits.IsInitial.uniqueUpToIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T T' : C} (hT : CategoryTheory.Limits.IsInitial T) (hT' : CategoryTheory.Limits.IsInitial T') : (hT.uniqueUpToIso hT').inv = hT'.to T
• CategoryTheory.Limits.IsInitial.to_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z : C} (t : CategoryTheory.Limits.IsInitial Z) {X Y : C} (f : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (t.to Y) f = t.to X
• CategoryTheory.Limits.coconeOfDiagramInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (hX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor J C) [∀ (i j : J) (f : j ⟶ i), CategoryTheory.IsIso (F.map f)] : CategoryTheory.Limits.Cocone F
• CategoryTheory.Limits.colimitOfDiagramInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (hX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor J C) [∀ (i j : J) (f : j ⟶ i), CategoryTheory.IsIso (F.map f)] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfDiagramInitial hX F)
• CategoryTheory.Limits.coconeOfDiagramInitial_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (hX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor J C) [∀ (i j : J) (f : j ⟶ i), CategoryTheory.IsIso (F.map f)] : (CategoryTheory.Limits.coconeOfDiagramInitial hX F).pt = F.obj X
• CategoryTheory.Limits.coneOfDiagramInitial_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (tX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor J C) (j : J) : (CategoryTheory.Limits.coneOfDiagramInitial tX F).π.app j = F.map (tX.to j)
• CategoryTheory.Limits.IsLimit.isIso_π_app_of_isInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (X : J) (hX : CategoryTheory.Limits.IsInitial X) : CategoryTheory.IsIso (c.π.app X)
• CategoryTheory.Functor.isInitialConst_to_app 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {X : D} (hX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor C D) (Y : C) : ((CategoryTheory.Functor.isInitialConst C hX).to F).app Y = hX.to (F.obj Y)
• CategoryTheory.Limits.coconeOfDiagramInitial_ι_app 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (hX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor J C) [∀ (i j : J) (f : j ⟶ i), CategoryTheory.IsIso (F.map f)] (x✝ : J) : (CategoryTheory.Limits.coconeOfDiagramInitial hX F).ι.app x✝ = CategoryTheory.inv (F.map (hX.to x✝))
• CategoryTheory.StructuredArrow.mkIdInitial 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {Y : C} {T : CategoryTheory.Functor C D} [T.Full] [T.Faithful] : CategoryTheory.Limits.IsInitial (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.id (T.obj Y)))
• CategoryTheory.Under.equivalenceOfIsInitial 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Under X ≌ T
• CategoryTheory.Under.mkIdInitial 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} : CategoryTheory.Limits.IsInitial (CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.id X))
• CategoryTheory.Under.equivalenceOfIsInitial_functor 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.Under.equivalenceOfIsInitial hX).functor = CategoryTheory.Under.forget X
• CategoryTheory.Under.equivalenceOfIsInitial_inverse_obj 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) (Y : T) : (CategoryTheory.Under.equivalenceOfIsInitial hX).inverse.obj Y = CategoryTheory.Under.mk (hX.to Y)
• CategoryTheory.Under.equivalenceOfIsInitial_inverse_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) {X✝ Y✝ : T} (f : X✝ ⟶ Y✝) : (CategoryTheory.Under.equivalenceOfIsInitial hX).inverse.map f = CategoryTheory.Under.homMk f ⋯
• CategoryTheory.Under.equivalenceOfIsInitial_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.Under.equivalenceOfIsInitial hX).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl (({ obj := fun Y => CategoryTheory.Under.mk (hX.to Y), map := fun {X_1 Y} f => CategoryTheory.Under.homMk f ⋯, map_id := ⋯, map_comp := ⋯ }.comp (CategoryTheory.Under.forget X)).obj x)) ⋯
• CategoryTheory.Under.equivalenceOfIsInitial_unitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.Under.equivalenceOfIsInitial hX).unitIso = CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.Under.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Under X)).obj Y).right) ⋯) ⋯
• CategoryTheory.Limits.IsInitial.hasInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (h : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Limits.HasInitial C
• CategoryTheory.Limits.initialIsInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.IsInitial (⊥_ C)
• CategoryTheory.Limits.initialIsoIsInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] {P : C} (t : CategoryTheory.Limits.IsInitial P) : ⊥_ C ≅ P
• CategoryTheory.Limits.initialIsoIsInitial_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] {P : C} (t : CategoryTheory.Limits.IsInitial P) : (CategoryTheory.Limits.initialIsoIsInitial t).inv = t.to (⊥_ C)
• CategoryTheory.Limits.isIso_π_of_isInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {j : J} (I : CategoryTheory.Limits.IsInitial j) (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F] : CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F j)
• CategoryTheory.Limits.initialIsoIsInitial_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] {P : C} (t : CategoryTheory.Limits.IsInitial P) : (CategoryTheory.Limits.initialIsoIsInitial t).hom = CategoryTheory.Limits.initialIsInitial.to P
• CategoryTheory.Limits.isIso_ι_of_isInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {j : J} (I : CategoryTheory.Limits.IsInitial j) (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit F] [∀ (i j : J) (f : j ⟶ i), CategoryTheory.IsIso (F.map f)] : CategoryTheory.IsIso (CategoryTheory.Limits.colimit.ι F j)
• CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inl 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsInitial Y) (c : CategoryTheory.Limits.BinaryCofan X Y) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ CategoryTheory.IsIso c.inl
• CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inr 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsInitial X) (c : CategoryTheory.Limits.BinaryCofan X Y) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ CategoryTheory.IsIso c.inr
• CategoryTheory.Limits.IsZero.isInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (hX : CategoryTheory.Limits.IsZero X) : CategoryTheory.Limits.IsInitial X
• CategoryTheory.Limits.HasZeroObject.zeroIsInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.IsInitial 0
• CategoryTheory.Limits.IsZero.isoIsInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (hX : CategoryTheory.Limits.IsZero X) (hY : CategoryTheory.Limits.IsInitial Y) : X ≅ Y
• CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] {X : C} (t : CategoryTheory.Limits.IsInitial X) : 0 ≅ X
• CategoryTheory.Limits.IsInitial.isZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (hX : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Limits.IsZero X
• CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (t : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial t).hom = 0
• CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (t : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial t).inv = 0
• CategoryTheory.Limits.IsInitial.isInitialObj 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G] (l : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Limits.IsInitial (G.obj X)
• CategoryTheory.Limits.IsInitial.isInitialOfObj 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.empty C) G] (l : CategoryTheory.Limits.IsInitial (G.obj X)) : CategoryTheory.Limits.IsInitial X
• CategoryTheory.Limits.isColimitOfHasInitialOfPreservesColimit 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G] : CategoryTheory.Limits.IsInitial (G.obj (⊥_ C))
• CategoryTheory.Limits.IsInitial.isInitialIffObj 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G] [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.empty C) G] (X : C) : CategoryTheory.Limits.IsInitial X ≃ CategoryTheory.Limits.IsInitial (G.obj X)
• CategoryTheory.Limits.isColimitMapCoconeEmptyCoconeEquiv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) : CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.asEmptyCocone X)) ≃ CategoryTheory.Limits.IsInitial (G.obj X)
• CategoryTheory.IsCofiltered.of_isInitial 📋 Mathlib.CategoryTheory.Filtered.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] {X : C} (h : CategoryTheory.Limits.IsInitial X) : CategoryTheory.IsCofiltered C
• CommRingCat.forget₂Adj 📋 Mathlib.Algebra.Category.Ring.Adjunctions
  {R : CommRingCat} (hR : CategoryTheory.Limits.IsInitial R) : R.monoidAlgebra.comp (CategoryTheory.Under.forget R) ⊣ CategoryTheory.forget₂ CommRingCat CommMonCat
• CategoryTheory.Limits.IsInitial.subsingleton_to 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (hI : CategoryTheory.Limits.IsInitial I) {A : C} : Subsingleton (A ⟶ I)
• CategoryTheory.Limits.IsInitial.ofStrict 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {X Y : C} (f : X ⟶ Y) (hY : CategoryTheory.Limits.IsInitial Y) : CategoryTheory.Limits.IsInitial X
• CategoryTheory.Limits.isInitialMul 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (X : C) [CategoryTheory.Limits.HasBinaryProduct I X] (hI : CategoryTheory.Limits.IsInitial I) : I ⨯ X ≅ I
• CategoryTheory.Limits.mulIsInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (X : C) [CategoryTheory.Limits.HasBinaryProduct X I] (hI : CategoryTheory.Limits.IsInitial I) : X ⨯ I ≅ I
• CategoryTheory.Limits.HasStrictInitialObjects.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] (out : ∀ {I A : C} (f : A ⟶ I) (a : CategoryTheory.Limits.IsInitial I), CategoryTheory.IsIso f) : CategoryTheory.Limits.HasStrictInitialObjects C
• CategoryTheory.Limits.HasStrictInitialObjects.out 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasStrictInitialObjects C] {I A : C} (f : A ⟶ I) : ∀ (a : CategoryTheory.Limits.IsInitial I), CategoryTheory.IsIso f
• CategoryTheory.Limits.IsInitial.isIso_to 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (hI : CategoryTheory.Limits.IsInitial I) {A : C} (f : A ⟶ I) : CategoryTheory.IsIso f
• CategoryTheory.Limits.IsInitial.strict_hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (hI : CategoryTheory.Limits.IsInitial I) {A : C} (f g : A ⟶ I) : f = g
• CategoryTheory.Limits.isInitialMul_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (X : C) [CategoryTheory.Limits.HasBinaryProduct I X] (hI : CategoryTheory.Limits.IsInitial I) : (CategoryTheory.Limits.isInitialMul X hI).hom = CategoryTheory.Limits.prod.fst
• CategoryTheory.Limits.mulIsInitial_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (X : C) [CategoryTheory.Limits.HasBinaryProduct X I] (hI : CategoryTheory.Limits.IsInitial I) : (CategoryTheory.Limits.mulIsInitial X hI).hom = CategoryTheory.Limits.prod.snd
• CategoryTheory.Limits.isInitialMul_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (X : C) [CategoryTheory.Limits.HasBinaryProduct I X] (hI : CategoryTheory.Limits.IsInitial I) : (CategoryTheory.Limits.isInitialMul X hI).inv = hI.to (I ⨯ X)
• CategoryTheory.Limits.mulIsInitial_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (X : C) [CategoryTheory.Limits.HasBinaryProduct X I] (hI : CategoryTheory.Limits.IsInitial I) : (CategoryTheory.Limits.mulIsInitial X hI).inv = hI.to (X ⨯ I)
• isCoproductOfIsInitialIsPushout 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ X) (k : W ⟶ Y) (H₁ : CategoryTheory.Limits.IsInitial W) (H₂ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk f g ⋯)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk f g)
• isPushoutOfIsInitialIsCoproduct 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ X) (k : W ⟶ Y) (H₁ : CategoryTheory.Limits.IsInitial W) (H₂ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk f g)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk f g ⋯)
• isBinaryCoproductOfIsInitialIsPushout 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) (c : CategoryTheory.Limits.Cocone F) {X : C} (hX : CategoryTheory.Limits.IsInitial X) (f : X ⟶ F.obj { as := CategoryTheory.Limits.WalkingPair.left }) (g : X ⟶ F.obj { as := CategoryTheory.Limits.WalkingPair.right }) (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (c.ι.app { as := CategoryTheory.Limits.WalkingPair.left }) (c.ι.app { as := CategoryTheory.Limits.WalkingPair.right }) ⋯)) : CategoryTheory.Limits.IsColimit c
• CategoryTheory.IsPushout.of_is_coproduct' 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {inl : X ⟶ P} {inr : Y ⟶ P} (h : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk inl inr)) (t : CategoryTheory.Limits.IsInitial Z) : CategoryTheory.IsPushout (t.to X) (t.to Y) inl inr
• CategoryTheory.IsPushout.of_isColimit_binaryCofan_of_isInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) {I : C} (hI : CategoryTheory.Limits.IsInitial I) : CategoryTheory.IsPushout (hI.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right })) (hI.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) c.inr c.inl
• CategoryTheory.IsPushout.of_is_coproduct 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.Limits.IsColimit c) (t : CategoryTheory.Limits.IsInitial Z) : CategoryTheory.IsPushout (t.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (t.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right })) c.inl c.inr
• CommRingCat.zIsInitial 📋 Mathlib.Algebra.Category.Ring.Constructions
  : CategoryTheory.Limits.IsInitial (CommRingCat.of ℤ)
• CommRingCat.isInitial 📋 Mathlib.Algebra.Category.Ring.Constructions
  : CategoryTheory.Limits.IsInitial (CommRingCat.of (ULift.{u, 0} ℤ))
• CategoryTheory.Under.forgetMapInitial 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {I : C} (hI : CategoryTheory.Limits.IsInitial I) : CategoryTheory.Under.forget X ≅ (CategoryTheory.Under.map (hI.to X)).comp (CategoryTheory.Under.equivalenceOfIsInitial hI).functor
• CategoryTheory.Under.forgetMapInitial_hom_app 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {I : C} (hI : CategoryTheory.Limits.IsInitial I) (X✝ : CategoryTheory.Under X) : (CategoryTheory.Under.forgetMapInitial X hI).hom.app X✝ = CategoryTheory.CategoryStruct.id X✝.right
• CategoryTheory.Under.forgetMapInitial_inv_app 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {I : C} (hI : CategoryTheory.Limits.IsInitial I) (X✝ : CategoryTheory.Under X) : (CategoryTheory.Under.forgetMapInitial X hI).inv.app X✝ = CategoryTheory.CategoryStruct.id X✝.right
• CategoryTheory.mkInitialOfLeftAdjoint 📋 Mathlib.CategoryTheory.Adjunction.Comma
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor D C) {F : CategoryTheory.Functor C D} (h : F ⊣ G) (A : C) : CategoryTheory.Limits.IsInitial (CategoryTheory.StructuredArrow.mk (h.unit.app A))
• CategoryTheory.Limits.Cocone.isColimitEquivIsInitial 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.IsColimit c ≃ CategoryTheory.Limits.IsInitial c
• CategoryTheory.Limits.IsColimit.descCoconeMorphism_eq_isInitial_to 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cocone F) : hc.descCoconeMorphism s = (c.isColimitEquivIsInitial hc).to s
• CategoryTheory.Limits.IsInitial.to_eq_descCoconeMorphism 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsInitial c) (s : CategoryTheory.Limits.Cocone F) : hc.to s = (c.isColimitEquivIsInitial.symm hc).descCoconeMorphism s
• CategoryTheory.WithInitial.starInitial 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Limits.IsInitial CategoryTheory.WithInitial.star
• CategoryTheory.WithInitial.liftToInitial 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) : CategoryTheory.Functor (CategoryTheory.WithInitial C) D
• CategoryTheory.WithInitial.inclLiftToInitial 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) : CategoryTheory.WithInitial.incl.comp (CategoryTheory.WithInitial.liftToInitial F hZ) ≅ F
• CategoryTheory.WithInitial.liftToInitial_obj 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (X : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.liftToInitial F hZ).obj X = match X with | CategoryTheory.WithInitial.of x => F.obj x | CategoryTheory.WithInitial.star => Z
• CategoryTheory.WithInitial.liftToInitialUnique 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.WithInitial.incl.comp G ≅ F) (hG : G.obj CategoryTheory.WithInitial.star ≅ Z) : G ≅ CategoryTheory.WithInitial.liftToInitial F hZ
• CategoryTheory.WithInitial.inclLiftToInitial_inv_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (x✝ : C) : (CategoryTheory.WithInitial.inclLiftToInitial F hZ).inv.app x✝ = CategoryTheory.CategoryStruct.id (F.obj x✝)
• CategoryTheory.WithInitial.inclLiftToInitial_hom_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (x✝ : C) : (CategoryTheory.WithInitial.inclLiftToInitial F hZ).hom.app x✝ = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithInitial.incl.obj x✝ with | CategoryTheory.WithInitial.of x => F.obj x | CategoryTheory.WithInitial.star => Z)
• CategoryTheory.WithInitial.liftToInitial_map 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) {X Y : CategoryTheory.WithInitial C} (f : X ⟶ Y) : (CategoryTheory.WithInitial.liftToInitial F hZ).map f = match X, Y, f with | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f => F.map (CategoryTheory.WithInitial.down f) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => hZ.to (F.obj a) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => CategoryTheory.CategoryStruct.id Z
• CategoryTheory.WithInitial.liftToInitialUnique_hom_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.WithInitial.incl.comp G ≅ F) (hG : G.obj CategoryTheory.WithInitial.star ≅ Z) (X : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.liftToInitialUnique F hZ G h hG).hom.app X = (match X with | CategoryTheory.WithInitial.of x => h.app x | CategoryTheory.WithInitial.star => hG).hom
• CategoryTheory.WithInitial.liftToInitialUnique_inv_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.WithInitial.incl.comp G ≅ F) (hG : G.obj CategoryTheory.WithInitial.star ≅ Z) (X : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.liftToInitialUnique F hZ G h hG).inv.app X = (match X with | CategoryTheory.WithInitial.of x => h.app x | CategoryTheory.WithInitial.star => hG).inv
• CategoryTheory.Functor.Elements.isInitialOfCorepresentableBy 📋 Mathlib.CategoryTheory.Elements
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type u_1)} {X : C} (h : F.CorepresentableBy X) : CategoryTheory.Limits.IsInitial (CategoryTheory.Functor.Elements.initialOfCorepresentableBy h)
• CategoryTheory.Functor.Elements.isInitialOfRepresentableBy 📋 Mathlib.CategoryTheory.Elements
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)} {X : C} (h : F.RepresentableBy X) : CategoryTheory.Limits.IsInitial (CategoryTheory.Functor.Elements.initialOfRepresentableBy h)
• CategoryTheory.Functor.Elements.isInitial 📋 Mathlib.CategoryTheory.Elements
  {C : Type u} [CategoryTheory.Category.{v, u} C] (A : C) : CategoryTheory.Limits.IsInitial (CategoryTheory.Functor.Elements.initial A)
• 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.ObjectProperty.colimitsOfShape_isEmpty_iff 📋 Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u') [CategoryTheory.Category.{v', u'} J] [IsEmpty J] (X : C) : P.colimitsOfShape J X ↔ Nonempty (CategoryTheory.Limits.IsInitial X)
• CommAlgCat.isInitialSelf 📋 Mathlib.Algebra.Category.CommAlgCat.Monoidal
  {R : Type u} [CommRing R] : CategoryTheory.Limits.IsInitial (CommAlgCat.of R R)
• CategoryTheory.Subobject.subsingleton_of_isInitial 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (hX : CategoryTheory.Limits.IsInitial X) : Subsingleton (CategoryTheory.Subobject X)
• CategoryTheory.Functor.Elements.isInitialElementsMkShrinkYonedaObjObjEquivId 📋 Mathlib.CategoryTheory.Limits.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.LocallySmall.{w, v₁, u₁} C] (X : C) : CategoryTheory.Limits.IsInitial ((CategoryTheory.shrinkYoneda.{w, v₁, u₁}.flip.obj (Opposite.op X)).elementsMk X (CategoryTheory.shrinkYonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.id X)))
• CategoryTheory.Limits.Types.isInitialPEmpty 📋 Mathlib.CategoryTheory.Limits.Types.Coproducts
  : CategoryTheory.Limits.IsInitial PEmpty.{u + 1}
• CategoryTheory.Limits.Types.initial_iff_empty 📋 Mathlib.CategoryTheory.Limits.Types.Coproducts
  (X : Type u) : Nonempty (CategoryTheory.Limits.IsInitial X) ↔ IsEmpty X
• CategoryTheory.Limits.Concrete.empty_of_initial_of_preserves 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] (X : C) (h : Nonempty (CategoryTheory.Limits.IsInitial X)) : IsEmpty (CategoryTheory.ToType X)
• CategoryTheory.Limits.Concrete.initial_of_empty_of_reflects 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] (X : C) (h : IsEmpty (CategoryTheory.ToType X)) : Nonempty (CategoryTheory.Limits.IsInitial X)
• CategoryTheory.Limits.Concrete.initial_iff_empty_of_preserves_of_reflects 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] (X : C) : Nonempty (CategoryTheory.Limits.IsInitial X) ↔ IsEmpty (CategoryTheory.ToType X)
• PresheafOfModules.forgetToPresheafModuleCatObjObj 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) (Y : Cᵒᵖ) : ModuleCat ↑(R.obj X)
• PresheafOfModules.forgetToPresheafModuleCatObj 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) : CategoryTheory.Functor Cᵒᵖ (ModuleCat ↑(R.obj X))
• PresheafOfModules.forgetToPresheafModuleCatObjObj_coe 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) (Y : Cᵒᵖ) : ↑(PresheafOfModules.forgetToPresheafModuleCatObjObj X hX M Y) = ↑(M.obj Y)
• PresheafOfModules.forgetToPresheafModuleCatObj_obj 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) (Y : Cᵒᵖ) : (PresheafOfModules.forgetToPresheafModuleCatObj X hX M).obj Y = PresheafOfModules.forgetToPresheafModuleCatObjObj X hX M Y
• PresheafOfModules.forgetToPresheafModuleCat 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Functor (PresheafOfModules R) (CategoryTheory.Functor Cᵒᵖ (ModuleCat ↑(R.obj X)))
• PresheafOfModules.forgetToPresheafModuleCatObjMap 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) {Y Z : Cᵒᵖ} (f : Y ⟶ Z) : PresheafOfModules.forgetToPresheafModuleCatObjObj X hX M Y ⟶ PresheafOfModules.forgetToPresheafModuleCatObjObj X hX M Z
• PresheafOfModules.forgetToPresheafModuleCat_obj 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) : (PresheafOfModules.forgetToPresheafModuleCat X hX).obj M = PresheafOfModules.forgetToPresheafModuleCatObj X hX M
• PresheafOfModules.forgetToPresheafModuleCatObj_map 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : (PresheafOfModules.forgetToPresheafModuleCatObj X hX M).map f = PresheafOfModules.forgetToPresheafModuleCatObjMap X hX M f
• PresheafOfModules.forgetToPresheafModuleCatMap 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) {M N : PresheafOfModules R} (f : M ⟶ N) : PresheafOfModules.forgetToPresheafModuleCatObj X hX M ⟶ PresheafOfModules.forgetToPresheafModuleCatObj X hX N
• PresheafOfModules.forgetToPresheafModuleCat_map 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) {X✝ Y✝ : PresheafOfModules R} (f : X✝ ⟶ Y✝) : (PresheafOfModules.forgetToPresheafModuleCat X hX).map f = PresheafOfModules.forgetToPresheafModuleCatMap X hX f
• PresheafOfModules.forgetToPresheafModuleCatObjMap_apply 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) {Y Z : Cᵒᵖ} (f : Y ⟶ Z) (m : ↑(M.obj Y)) : (ModuleCat.Hom.hom (PresheafOfModules.forgetToPresheafModuleCatObjMap X hX M f)) m = (CategoryTheory.ConcreteCategory.hom (M.map f)) m
• CategoryTheory.ObjectProperty.prop_of_isInitial 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] (X : C) (hX : CategoryTheory.Limits.IsInitial X) : P X
• CategoryTheory.initial_mono 📋 Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {I : C} (B : C) (t : CategoryTheory.Limits.IsInitial I) [CategoryTheory.MonoidalClosed C] : CategoryTheory.Mono (t.to B)
• CategoryTheory.strict_initial 📋 Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {A : C} [CategoryTheory.Closed A] {I : C} (t : CategoryTheory.Limits.IsInitial I) (f : A ⟶ I) : CategoryTheory.IsIso f
• CategoryTheory.zeroMul 📋 Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {A : C} [CategoryTheory.Closed A] {I : C} (t : CategoryTheory.Limits.IsInitial I) : CategoryTheory.MonoidalCategoryStruct.tensorObj A I ≅ I
• CategoryTheory.mulZero 📋 Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {A : C} [CategoryTheory.Closed A] [CategoryTheory.BraidedCategory C] {I : C} (t : CategoryTheory.Limits.IsInitial I) : CategoryTheory.MonoidalCategoryStruct.tensorObj I A ≅ I
• CategoryTheory.powZero 📋 Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {B : C} [CategoryTheory.BraidedCategory C] {I : C} (t : CategoryTheory.Limits.IsInitial I) [CategoryTheory.MonoidalClosed C] : I ⟹ B ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit C
• CategoryTheory.zeroMul_hom 📋 Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {A : C} [CategoryTheory.Closed A] {I : C} (t : CategoryTheory.Limits.IsInitial I) : (CategoryTheory.zeroMul t).hom = CategoryTheory.SemiCartesianMonoidalCategory.snd A I
• CategoryTheory.zeroMul_inv 📋 Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {A : C} [CategoryTheory.Closed A] {I : C} (t : CategoryTheory.Limits.IsInitial I) : (CategoryTheory.zeroMul t).inv = t.to (CategoryTheory.MonoidalCategoryStruct.tensorObj A I)
• CategoryTheory.isConnected_of_isInitial 📋 Mathlib.CategoryTheory.Limits.IsConnected
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] {x : C} (h : CategoryTheory.Limits.IsInitial x) : CategoryTheory.IsConnected C
• 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.isInitial 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal
  {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} (hF : (X : C) → CategoryTheory.Limits.IsInitial (F.obj X)) : CategoryTheory.Limits.IsInitial F
• TopCat.isInitialPEmpty 📋 Mathlib.Topology.Category.TopCat.Limits.Basic
  : CategoryTheory.Limits.IsInitial (TopCat.of PEmpty.{u + 1})
• CategoryTheory.IsInitial.isVanKampenColimit 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {X : C} (h : CategoryTheory.Limits.IsInitial X) : CategoryTheory.IsVanKampenColimit (CategoryTheory.Limits.asEmptyCocone X)
• CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjoint 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.BinaryCoproductDisjoint X Y] [CategoryTheory.Limits.HasBinaryCoproduct X Y] [CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr] : CategoryTheory.Limits.IsInitial (CategoryTheory.Limits.pullback CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr)
• CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjointOfIsColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.BinaryCoproductDisjoint X Y] {Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [CategoryTheory.Limits.HasPullback f g] (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk f g)) : CategoryTheory.Limits.IsInitial (CategoryTheory.Limits.pullback f g)
• CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfIsColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} [CategoryTheory.Limits.CoproductDisjoint X] {i j : ι} (hij : i ≠ j) {Z : C} {f : (i : ι) → X i ⟶ Z} [CategoryTheory.Limits.HasPullback (f i) (f j)] (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk Z f)) : CategoryTheory.Limits.IsInitial (CategoryTheory.Limits.pullback (f i) (f j))
• CategoryTheory.Limits.IsInitial.ofCoproductDisjoint 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} [CategoryTheory.Limits.CoproductDisjoint X] {i j : ι} (hij : i ≠ j) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.Sigma.ι X i) (CategoryTheory.Limits.Sigma.ι X j)] : CategoryTheory.Limits.IsInitial (CategoryTheory.Limits.pullback (CategoryTheory.Limits.Sigma.ι X i) (CategoryTheory.Limits.Sigma.ι X j))
• CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjointOfIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.BinaryCoproductDisjoint X Y] [CategoryTheory.Limits.HasBinaryCoproduct X Y] (s : CategoryTheory.Limits.PullbackCone CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr) (hs : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Limits.IsInitial s.pt
• CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} [CategoryTheory.Limits.CoproductDisjoint X] {i j : ι} (hij : i ≠ j) [CategoryTheory.Limits.HasCoproduct X] {s : CategoryTheory.Limits.PullbackCone (CategoryTheory.Limits.Sigma.ι X i) (CategoryTheory.Limits.Sigma.ι X j)} (hs : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Limits.IsInitial s.pt
• CategoryTheory.Limits.CoproductDisjoint.isPullback_of_isInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} [CategoryTheory.Limits.CoproductDisjoint X] {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) {Y : C} (hY : CategoryTheory.Limits.IsInitial Y) {i j : ι} [CategoryTheory.Limits.HasPullback (c.inj i) (c.inj j)] (hij : i ≠ j) : CategoryTheory.IsPullback (hY.to (X i)) (hY.to (X j)) (c.inj i) (c.inj j)
• CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfIsColimitOfIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} [CategoryTheory.Limits.CoproductDisjoint X] {i j : ι} (hij : i ≠ j) {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) {s : CategoryTheory.Limits.PullbackCone (c.inj i) (c.inj j)} (hs : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Limits.IsInitial s.pt
• CategoryTheory.Limits.CoproductDisjoint.nonempty_isInitial_of_ne 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {ι : Type u_1} {X : ι → C} [self : CategoryTheory.Limits.CoproductDisjoint X] {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) {i j : ι} : i ≠ j → ∀ (s : CategoryTheory.Limits.PullbackCone (c.inj i) (c.inj j)) (a : CategoryTheory.Limits.IsLimit s), Nonempty (CategoryTheory.Limits.IsInitial s.pt)
• CategoryTheory.Limits.CoproductDisjoint.of_hasCoproduct 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} [CategoryTheory.Limits.HasCoproduct X] [∀ (i : ι), CategoryTheory.Mono (CategoryTheory.Limits.Sigma.ι X i)] (s : {i j : ι} → i ≠ j → CategoryTheory.Limits.PullbackCone (CategoryTheory.Limits.Sigma.ι X i) (CategoryTheory.Limits.Sigma.ι X j)) (hs : {i j : ι} → (hij : i ≠ j) → CategoryTheory.Limits.IsLimit (s hij)) (H : {i j : ι} → (hij : i ≠ j) → CategoryTheory.Limits.IsInitial (s hij).pt) : CategoryTheory.Limits.CoproductDisjoint X
• CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfCommSq 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} [CategoryTheory.Limits.CoproductDisjoint X] {i j : ι} (hij : i ≠ j) [CategoryTheory.Limits.HasStrictInitialObjects C] {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) {Z : C} (fst : Z ⟶ X i) (snd : Z ⟶ X j) (h : CategoryTheory.CategoryStruct.comp fst (c.inj i) = CategoryTheory.CategoryStruct.comp snd (c.inj j)) [CategoryTheory.Limits.HasPullback (c.inj i) (c.inj j)] : CategoryTheory.Limits.IsInitial Z
• CategoryTheory.Limits.CoproductDisjoint.of_cofan 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) [∀ (i : ι), CategoryTheory.Mono (c.inj i)] (s : {i j : ι} → i ≠ j → CategoryTheory.Limits.PullbackCone (c.inj i) (c.inj j)) (hs : {i j : ι} → (hij : i ≠ j) → CategoryTheory.Limits.IsLimit (s hij)) (H : {i j : ι} → (hij : i ≠ j) → CategoryTheory.Limits.IsInitial (s hij).pt) : CategoryTheory.Limits.CoproductDisjoint X
• CategoryTheory.Limits.CoproductDisjoint.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} (nonempty_isInitial_of_ne : ∀ {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) {i j : ι}, i ≠ j → ∀ (s : CategoryTheory.Limits.PullbackCone (c.inj i) (c.inj j)) (a : CategoryTheory.Limits.IsLimit s), Nonempty (CategoryTheory.Limits.IsInitial s.pt)) (mono_inj : ∀ {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) (i : ι), CategoryTheory.Mono (c.inj i)) : CategoryTheory.Limits.CoproductDisjoint X
• CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjointOfIsColimitOfIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.BinaryCoproductDisjoint X Y] {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) {s : CategoryTheory.Limits.PullbackCone c.inl c.inr} (hs : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Limits.IsInitial s.pt
• CategoryTheory.Limits.BinaryCoproductDisjoint.of_binaryCofan 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Mono c.inl] [CategoryTheory.Mono c.inr] {s : CategoryTheory.Limits.PullbackCone c.inl c.inr} (hs : CategoryTheory.Limits.IsLimit s) (H : CategoryTheory.Limits.IsInitial s.pt) : CategoryTheory.Limits.BinaryCoproductDisjoint X Y
• SheafOfModules.forgetToSheafModuleCat 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Functor (SheafOfModules R) (CategoryTheory.Sheaf J (ModuleCat ↑(R.obj.obj X)))
• SheafOfModules.forgetToSheafModuleCat_obj_obj 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : SheafOfModules R) : ((SheafOfModules.forgetToSheafModuleCat R X hX).obj M).obj = (PresheafOfModules.forgetToPresheafModuleCat X hX).obj M.val
• SheafOfModules.forgetToSheafModuleCat_map_hom 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) {X✝ Y✝ : SheafOfModules R} (f : X✝ ⟶ Y✝) : ((SheafOfModules.forgetToSheafModuleCat R X hX).map f).hom = (PresheafOfModules.forgetToPresheafModuleCat X hX).map f.val
• SheafOfModules.forgetToSheafModuleCatOfIso 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (X Y : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (hY : CategoryTheory.Limits.IsInitial Y) (φ : X ≅ Y) : SheafOfModules.forgetToSheafModuleCat R X hX ≅ (SheafOfModules.forgetToSheafModuleCat R Y hY).comp (CategoryTheory.sheafCompose J (ModuleCat.restrictScalars (RingCat.Hom.hom (R.obj.map φ.hom))))
• SheafOfModules.pushforwardCompForgetToSheafModuleCat 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (hX' : CategoryTheory.Limits.IsInitial (F.op.obj X)) : (SheafOfModules.pushforward φ).comp (SheafOfModules.forgetToSheafModuleCat S X hX) ≅ (SheafOfModules.forgetToSheafModuleCat R (F.op.obj X) hX').comp ((CategoryTheory.sheafCompose K (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app X)))).comp (F.sheafPushforwardContinuous (ModuleCat ↑(S.obj.obj X)) J K))
• CategoryTheory.Limits.IsInitial.orderBot 📋 Mathlib.CategoryTheory.Limits.Preorder
  {C : Type u} [Preorder C] {X : C} (t : CategoryTheory.Limits.IsInitial X) : OrderBot C
• Preorder.isInitialBot 📋 Mathlib.CategoryTheory.Limits.Preorder
  (C : Type u) [Preorder C] [OrderBot C] : CategoryTheory.Limits.IsInitial ⊥
• CategoryTheory.MorphismProperty.Under.mkIdInitial 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
  {T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T) [P.ContainsIdentities] : CategoryTheory.Limits.IsInitial (CategoryTheory.MorphismProperty.Under.mk ⊤ (CategoryTheory.CategoryStruct.id X) ⋯)
• CategoryTheory.CosimplicialObject.augmentOfIsInitial 📋 Mathlib.AlgebraicTopology.SimplicialObject.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {T : C} (hT : CategoryTheory.Limits.IsInitial T) : CategoryTheory.CosimplicialObject.Augmented C
• CategoryTheory.CosimplicialObject.augmentOfIsInitial_left 📋 Mathlib.AlgebraicTopology.SimplicialObject.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {T : C} (hT : CategoryTheory.Limits.IsInitial T) : (X.augmentOfIsInitial hT).left = T
• CategoryTheory.CosimplicialObject.augmentOfIsInitial_right 📋 Mathlib.AlgebraicTopology.SimplicialObject.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {T : C} (hT : CategoryTheory.Limits.IsInitial T) : (X.augmentOfIsInitial hT).right = X
• CategoryTheory.CosimplicialObject.augmentOfIsInitial_hom_app 📋 Mathlib.AlgebraicTopology.SimplicialObject.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {T : C} (hT : CategoryTheory.Limits.IsInitial T) (x✝ : SimplexCategory) : (X.augmentOfIsInitial hT).hom.app x✝ = hT.to (X.obj x✝)
• SSet.Subcomplex.isInitialBot 📋 Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
  {X : SSet} : CategoryTheory.Limits.IsInitial ⊥.toSSet
• HomotopicalAlgebra.isCofibrant_iff_of_isInitial 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [(HomotopicalAlgebra.cofibrations C).RespectsIso] {A X : C} (i : A ⟶ X) (hA : CategoryTheory.Limits.IsInitial A) : HomotopicalAlgebra.IsCofibrant X ↔ HomotopicalAlgebra.Cofibration i
• CategoryTheory.Factorisation.IsInitial_initial 📋 Mathlib.CategoryTheory.Category.Factorisation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} : CategoryTheory.Limits.IsInitial CategoryTheory.Factorisation.initial
• CategoryTheory.GradedObject.isInitialSingleObjApply 📋 Mathlib.CategoryTheory.GradedObject.Single
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) (i : J) (h : i ≠ j) : CategoryTheory.Limits.IsInitial ((CategoryTheory.GradedObject.single j).obj X i)
• CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀IsInitial 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C) [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] (X : CategoryTheory.GradedObject J D) (a : J × I) (ha : a.2 ≠ 0) : CategoryTheory.Limits.IsInitial (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y) a)
• CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIsInitial 📋 Mathlib.CategoryTheory.GradedObject.Unitor
  {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [Zero I] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C) [∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] (Y : CategoryTheory.GradedObject J D) (a : I × J) (ha : a.1 ≠ 0) : CategoryTheory.Limits.IsInitial (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y a)
• CategoryTheory.GradedObject.Monoidal.isInitialTensorUnitApply 📋 Mathlib.CategoryTheory.GradedObject.Monoidal
  {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] (i : I) (hi : i ≠ 0) : CategoryTheory.Limits.IsInitial (CategoryTheory.GradedObject.Monoidal.tensorUnit i)
• AlgebraicGeometry.LocallyRingedSpace.emptyIsInitial 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace
  : CategoryTheory.Limits.IsInitial ∅
• AlgebraicGeometry.emptyIsInitial 📋 Mathlib.AlgebraicGeometry.Limits
  : CategoryTheory.Limits.IsInitial ∅
• AlgebraicGeometry.specPUnitIsInitial 📋 Mathlib.AlgebraicGeometry.Limits
  : CategoryTheory.Limits.IsInitial (AlgebraicGeometry.Spec (CommRingCat.of PUnit.{u + 1}))
• AlgebraicGeometry.isInitialOfIsEmpty 📋 Mathlib.AlgebraicGeometry.Limits
  {X : AlgebraicGeometry.Scheme} [IsEmpty ↥X] : CategoryTheory.Limits.IsInitial X
• AlgebraicGeometry.isInitial_iff_isEmpty 📋 Mathlib.AlgebraicGeometry.Limits
  {X : AlgebraicGeometry.Scheme} : Nonempty (CategoryTheory.Limits.IsInitial X) ↔ IsEmpty ↥X
• CategoryTheory.Presieve.preservesTerminal_of_isSheaf_for_empty 📋 Mathlib.CategoryTheory.Sites.Preserves
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)) (hI : CategoryTheory.Limits.IsInitial I) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty Cᵒᵖ) F
• CategoryTheory.Presieve.preservesProduct_of_isSheafFor 📋 Mathlib.CategoryTheory.Sites.Preserves
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)) (hI : CategoryTheory.Limits.IsInitial I) {α : Type u_1} [Small.{w, u_1} α] {X : α → C} (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) [(CategoryTheory.Presieve.ofArrows X c.inj).HasPairwisePullbacks] [CategoryTheory.Limits.HasInitial C] [∀ (i : α), CategoryTheory.Mono (c.inj i)] (hd : Pairwise fun i j => CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j)) (c.inj i) (c.inj j)) (hF' : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X c.inj)) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun x => Opposite.op (X x)) F
• CategoryTheory.Presieve.isSheafFor_iff_preservesProduct 📋 Mathlib.CategoryTheory.Sites.Preserves
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)) (hI : CategoryTheory.Limits.IsInitial I) {α : Type u_1} [Small.{w, u_1} α] {X : α → C} (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) [(CategoryTheory.Presieve.ofArrows X c.inj).HasPairwisePullbacks] [CategoryTheory.Limits.HasInitial C] [∀ (i : α), CategoryTheory.Mono (c.inj i)] (hd : Pairwise fun i j => CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j)) (c.inj i) (c.inj j)) : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X c.inj) ↔ CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun x => Opposite.op (X x)) F
• CategoryTheory.Presieve.firstMap_eq_secondMap 📋 Mathlib.CategoryTheory.Sites.Preserves
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)) (hI : CategoryTheory.Limits.IsInitial I) {α : Type u_1} [Small.{w, u_1} α] {X : α → C} (c : CategoryTheory.Limits.Cofan X) [(CategoryTheory.Presieve.ofArrows X c.inj).HasPairwisePullbacks] [CategoryTheory.Limits.HasInitial C] [∀ (i : α), CategoryTheory.Mono (c.inj i)] (hd : Pairwise fun i j => CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j)) (c.inj i) (c.inj j)) : CategoryTheory.Equalizer.Presieve.Arrows.firstMap F X c.inj = CategoryTheory.Equalizer.Presieve.Arrows.secondMap F X c.inj
• CategoryTheory.Functor.Elements.corepresentableByOfIsInitial 📋 Mathlib.CategoryTheory.Limits.Elements
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {E : F.Elements} (he : CategoryTheory.Limits.IsInitial E) : F.CorepresentableBy E.fst
• CategoryTheory.Functor.Elements.representableByOfIsInitial 📋 Mathlib.CategoryTheory.Limits.Elements
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {E : F.Elements} (he : CategoryTheory.Limits.IsInitial E) : F.RepresentableBy (Opposite.unop E.fst)
• CategoryTheory.overEquivOfIsInitial 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasStrictInitialObjects C] (X : C) (h : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Over X ≌ CategoryTheory.Discrete PUnit.{w + 1}
• CategoryTheory.overEquivOfIsInitial_functor 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasStrictInitialObjects C] (X : C) (h : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.overEquivOfIsInitial.{w, v_1, u_1} X h).functor = CategoryTheory.Functor.star (CategoryTheory.Over X)
• CategoryTheory.overEquivOfIsInitial_inverse 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasStrictInitialObjects C] (X : C) (h : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.overEquivOfIsInitial.{w, v_1, u_1} X h).inverse = CategoryTheory.Functor.fromPUnit (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id X))
• CategoryTheory.MorphismProperty.overEquivOfIsInitial 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [CategoryTheory.Limits.HasStrictInitialObjects C] (X : C) (h : CategoryTheory.Limits.IsInitial X) : P.Over Q X ≌ CategoryTheory.Discrete PUnit.{w + 1}
• CategoryTheory.overEquivOfIsInitial_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasStrictInitialObjects C] (X : C) (h : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.overEquivOfIsInitial.{w, v_1, u_1} X h).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.Functor.fromPUnit (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id X))).comp (CategoryTheory.Functor.star (CategoryTheory.Over X)))
• CategoryTheory.MorphismProperty.overEquivOfIsInitial_functor 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [CategoryTheory.Limits.HasStrictInitialObjects C] (X : C) (h : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.MorphismProperty.overEquivOfIsInitial.{w, v_1, u_1} P Q X h).functor = CategoryTheory.Functor.star (P.Over Q X)
• CategoryTheory.MorphismProperty.overEquivOfIsInitial_inverse 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [CategoryTheory.Limits.HasStrictInitialObjects C] (X : C) (h : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.MorphismProperty.overEquivOfIsInitial.{w, v_1, u_1} P Q X h).inverse = CategoryTheory.Functor.fromPUnit (CategoryTheory.MorphismProperty.Over.mk Q (CategoryTheory.CategoryStruct.id X) ⋯)
• CategoryTheory.overEquivOfIsInitial_unitIso 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasStrictInitialObjects C] (X : C) (h : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.overEquivOfIsInitial.{w, v_1, u_1} X h).unitIso = CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Over.isoMk (CategoryTheory.asIso A.hom) ⋯) ⋯
• CategoryTheory.MorphismProperty.overEquivOfIsInitial_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [CategoryTheory.Limits.HasStrictInitialObjects C] (X : C) (h : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.MorphismProperty.overEquivOfIsInitial.{w, v_1, u_1} P Q X h).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.Functor.fromPUnit (CategoryTheory.MorphismProperty.Over.mk Q (CategoryTheory.CategoryStruct.id X) ⋯)).comp (CategoryTheory.Functor.star (P.Over Q X)))

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