Loogle!

Result

Found 307 declarations mentioning CategoryTheory.Limits.HasInitial. Of these, only the first 200 are shown.

CategoryTheory.Limits.HasInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : Prop
CategoryTheory.Limits.initial 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] : C
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.hasInitial_of_hasTerminal_op 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal Cᵒᵖ] : CategoryTheory.Limits.HasInitial C
CategoryTheory.Limits.hasInitial_op_of_hasTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.HasInitial Cᵒᵖ
CategoryTheory.Limits.hasTerminal_of_hasInitial_op 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial Cᵒᵖ] : CategoryTheory.Limits.HasTerminal C
CategoryTheory.Limits.hasTerminal_op_of_hasInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.HasTerminal 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.initial.to 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] (P : C) : ⊥_ C ⟶ P
CategoryTheory.Limits.hasLimit_of_domain_hasInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasInitial J] {F : CategoryTheory.Functor J C} : CategoryTheory.Limits.HasLimit F
CategoryTheory.Limits.uniqueFromInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] (P : C) : Unique (⊥_ C ⟶ P)
CategoryTheory.Limits.InitialMonoClass.of_initial 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] (h : ∀ (X : C), CategoryTheory.Mono (CategoryTheory.Limits.initial.to X)) : CategoryTheory.Limits.InitialMonoClass C
CategoryTheory.Limits.initial.isSplitEpi_to 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y : C} [CategoryTheory.Limits.HasInitial C] (f : Y ⟶ ⊥_ C) : CategoryTheory.IsSplitEpi f
CategoryTheory.Limits.hasInitial_of_unique 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) [∀ (Y : C), Nonempty (X ⟶ Y)] [∀ (Y : C), Subsingleton (X ⟶ Y)] : CategoryTheory.Limits.HasInitial C
CategoryTheory.Limits.InitialMonoClass.of_terminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasTerminal C] (h : CategoryTheory.Mono (CategoryTheory.Limits.initial.to (⊤_ C))) : CategoryTheory.Limits.InitialMonoClass C
CategoryTheory.Limits.initial.mono_from 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.InitialMonoClass C] (X : C) (f : ⊥_ C ⟶ X) : CategoryTheory.Mono f
CategoryTheory.Limits.instHasColimitObjFunctorConstInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2} [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.const J).obj (⊥_ C))
CategoryTheory.Limits.initialComparison 📋 Mathlib.CategoryTheory.Limits.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.HasInitial D] : ⊥_ D ⟶ G.obj (⊥_ C)
CategoryTheory.Limits.limitOfInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasInitial J] : CategoryTheory.Limits.limit F ≅ F.obj (⊥_ J)
CategoryTheory.Limits.initial.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] {P : C} (f g : ⊥_ C ⟶ P) : f = g
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.initial.hom_ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] {P : C} {f g : ⊥_ C ⟶ P} : f = g ↔ True
CategoryTheory.Limits.colimitConstInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2} [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.colimit ((CategoryTheory.Functor.const J).obj (⊥_ C)) ≅ ⊥_ C
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.initial.to_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] {P Q : C} (f : Q ⟶ P) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.initial.to Q) f = CategoryTheory.Limits.initial.to P
CategoryTheory.Limits.hasColimit_of_domain_hasInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasInitial J] {F : CategoryTheory.Functor J C} [∀ (i j : J) (f : j ⟶ i), CategoryTheory.IsIso (F.map f)] : CategoryTheory.Limits.HasColimit F
CategoryTheory.Limits.isIso_π_initial 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasInitial J] (F : CategoryTheory.Functor J C) : CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F (⊥_ J))
CategoryTheory.Limits.colimitOfInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasInitial J] [∀ (i j : J) (f : j ⟶ i), CategoryTheory.IsIso (F.map f)] : CategoryTheory.Limits.colimit F ≅ F.obj (⊥_ J)
CategoryTheory.Limits.isIso_ι_initial 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasInitial J] (F : CategoryTheory.Functor J C) [∀ (i j : J) (f : j ⟶ i), CategoryTheory.IsIso (F.map f)] : CategoryTheory.IsIso (CategoryTheory.Limits.colimit.ι F (⊥_ J))
CategoryTheory.Limits.colimitConstInitial_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2} [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.colimitConstInitial.inv = CategoryTheory.Limits.initial.to (CategoryTheory.Limits.colimit ((CategoryTheory.Functor.const J).obj (⊥_ C)))
CategoryTheory.Limits.ι_colimitConstInitial_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2} [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasInitial C] {j : J} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.const J).obj (⊥_ C)) j) CategoryTheory.Limits.colimitConstInitial.hom = CategoryTheory.Limits.initial.to (⊥_ C)
CategoryTheory.Limits.ι_colimitConstInitial_hom_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2} [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasInitial C] {j : J} {Z : C} (h : ⊥_ C ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.const J).obj (⊥_ C)) j) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.colimitConstInitial.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.initial.to (⊥_ C)) h
CategoryTheory.Limits.coprod.leftUnitor 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (P : C) : (⊥_ C) ⨿ P ≅ P
CategoryTheory.Limits.coprod.rightUnitor 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (P : C) : P ⨿ ⊥_ C ≅ P
CategoryTheory.Limits.coprod.leftUnitor_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (P : C) : (CategoryTheory.Limits.coprod.leftUnitor P).inv = CategoryTheory.Limits.coprod.inr
CategoryTheory.Limits.coprod.rightUnitor_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (P : C) : (CategoryTheory.Limits.coprod.rightUnitor P).inv = CategoryTheory.Limits.coprod.inl
CategoryTheory.Limits.coprod.leftUnitor_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (P : C) : (CategoryTheory.Limits.coprod.leftUnitor P).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.initial.to P) (CategoryTheory.CategoryStruct.id P)
CategoryTheory.Limits.coprod.rightUnitor_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (P : C) : (CategoryTheory.Limits.coprod.rightUnitor P).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id P) (CategoryTheory.Limits.initial.to P)
CategoryTheory.Limits.coprod.leftUnitor_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id (⊥_ C)) f) (CategoryTheory.Limits.coprod.leftUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.leftUnitor X).hom f
CategoryTheory.Limits.coprod.rightUnitor_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id (⊥_ C))) (CategoryTheory.Limits.coprod.rightUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.rightUnitor X).hom f
CategoryTheory.Limits.coprod.triangle 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.associator X (⊥_ C) Y).hom (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.coprod.leftUnitor Y).hom) = CategoryTheory.Limits.coprod.map (CategoryTheory.Limits.coprod.rightUnitor X).hom (CategoryTheory.CategoryStruct.id Y)
CategoryTheory.Limits.HasZeroObject.hasInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.HasInitial C
CategoryTheory.Limits.HasZeroObject.zeroIsoInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasInitial C] : 0 ≅ ⊥_ C
CategoryTheory.Limits.hasZeroObject_of_hasInitial_object 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.HasZeroObject C
CategoryTheory.Limits.HasZeroObject.zeroIsoInitial_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.HasZeroObject.zeroIsoInitial.hom = 0
CategoryTheory.Limits.HasZeroObject.zeroIsoInitial_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.HasZeroObject.zeroIsoInitial.inv = 0
CategoryTheory.Limits.hasInitial_of_hasInitial_of_preservesColimit 📋 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.HasInitial D
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.preservesInitial_of_iso 📋 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.HasInitial D] (f : ⊥_ D ≅ G.obj (⊥_ C)) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G
CategoryTheory.Limits.PreservesInitial.iso 📋 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.HasInitial D] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G] : G.obj (⊥_ C) ≅ ⊥_ D
CategoryTheory.Limits.instIsIsoInitialComparison 📋 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.HasInitial D] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G] : CategoryTheory.IsIso (CategoryTheory.Limits.initialComparison G)
CategoryTheory.Limits.PreservesInitial.of_iso_comparison 📋 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.HasInitial D] [i : CategoryTheory.IsIso (CategoryTheory.Limits.initialComparison G)] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G
CategoryTheory.Limits.preservesInitial_of_isIso 📋 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.HasInitial D] (f : ⊥_ D ⟶ G.obj (⊥_ C)) [i : CategoryTheory.IsIso f] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G
CategoryTheory.Limits.PreservesInitial.iso_hom 📋 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.HasInitial D] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G] : (CategoryTheory.Limits.PreservesInitial.iso G).inv = CategoryTheory.Limits.initialComparison G
CategoryTheory.IsCofiltered.of_hasInitial 📋 Mathlib.CategoryTheory.Filtered.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.IsCofiltered C
CategoryTheory.AddMon.instHasInitial 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Limits.HasInitial (CategoryTheory.AddMon C)
CategoryTheory.Mon.instHasInitial 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Limits.HasInitial (CategoryTheory.Mon C)
CategoryTheory.Limits.initial.subsingleton_to 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] {A : C} : Subsingleton (A ⟶ ⊥_ C)
CategoryTheory.Limits.hasStrictInitialObjects_of_initial_is_strict 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] (h : ∀ (A : C) (f : A ⟶ ⊥_ C), CategoryTheory.IsIso f) : CategoryTheory.Limits.HasStrictInitialObjects C
CategoryTheory.Limits.initial_isIso_to 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] {A : C} (f : A ⟶ ⊥_ C) : CategoryTheory.IsIso f
CategoryTheory.Limits.initialMul 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] (X : C) [CategoryTheory.Limits.HasBinaryProduct (⊥_ C) X] : (⊥_ C) ⨯ X ≅ ⊥_ C
CategoryTheory.Limits.mulInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] (X : C) [CategoryTheory.Limits.HasBinaryProduct X (⊥_ C)] : X ⨯ ⊥_ C ≅ ⊥_ C
CategoryTheory.Limits.initial.strict_hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] {A : C} (f g : A ⟶ ⊥_ C) : f = g
CategoryTheory.Limits.initial.strict_hom_ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] {A : C} {f g : A ⟶ ⊥_ C} : f = g ↔ True
CategoryTheory.Limits.initialMul_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] (X : C) [CategoryTheory.Limits.HasBinaryProduct (⊥_ C) X] : (CategoryTheory.Limits.initialMul X).hom = CategoryTheory.Limits.prod.fst
CategoryTheory.Limits.mulInitial_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] (X : C) [CategoryTheory.Limits.HasBinaryProduct X (⊥_ C)] : (CategoryTheory.Limits.mulInitial X).hom = CategoryTheory.Limits.prod.snd
CategoryTheory.Limits.initialMul_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] (X : C) [CategoryTheory.Limits.HasBinaryProduct (⊥_ C) X] : (CategoryTheory.Limits.initialMul X).inv = CategoryTheory.Limits.initial.to ((⊥_ C) ⨯ X)
CategoryTheory.Limits.mulInitial_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] (X : C) [CategoryTheory.Limits.HasBinaryProduct X (⊥_ C)] : (CategoryTheory.Limits.mulInitial X).inv = CategoryTheory.Limits.initial.to (X ⨯ ⊥_ C)
hasBinaryCoproducts_of_hasInitial_and_pushouts 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] : CategoryTheory.Limits.HasBinaryCoproducts C
colimitCoconeOfInitialAndPushouts 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) : CategoryTheory.Limits.ColimitCocone F
preservesBinaryCoproducts_of_preservesInitial_and_pushouts 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan F] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F
coprodIsoPushout 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : X ⨿ Y ≅ CategoryTheory.Limits.pushout (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)
inl_coprodIsoPushout_inv 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) (coprodIsoPushout X Y).inv = CategoryTheory.Limits.coprod.inl
inr_coprodIsoPushout_inv 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) (coprodIsoPushout X Y).inv = CategoryTheory.Limits.coprod.inr
inl_coprodIsoPushout_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (coprodIsoPushout X Y).hom = CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)
inr_coprodIsoPushout_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (coprodIsoPushout X Y).hom = CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)
inl_coprodIsoPushout_inv_assoc 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : X ⨿ Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) (CategoryTheory.CategoryStruct.comp (coprodIsoPushout X Y).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h
inr_coprodIsoPushout_inv_assoc 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : X ⨿ Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) (CategoryTheory.CategoryStruct.comp (coprodIsoPushout X Y).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h
inl_coprodIsoPushout_hom_assoc 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : CategoryTheory.Limits.pushout (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (coprodIsoPushout X Y).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) h
inr_coprodIsoPushout_hom_assoc 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : CategoryTheory.Limits.pushout (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (coprodIsoPushout X Y).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)) h
CategoryTheory.IsPushout.of_hasBinaryCoproduct' 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.IsPushout (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y) CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr
CategoryTheory.Under.instHasInitial 📋 Mathlib.CategoryTheory.Limits.Comma
{T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {X : T} : CategoryTheory.Limits.HasInitial (CategoryTheory.Under X)
CategoryTheory.StructuredArrow.instHasInitialObjOfFaithfulOfFull 📋 Mathlib.CategoryTheory.Limits.Comma
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {G : CategoryTheory.Functor A T} [G.Faithful] [G.Full] {Y : A} : CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow (G.obj Y) G)
CategoryTheory.leftAdjointOfStructuredArrowInitials 📋 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) [∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)] : CategoryTheory.Functor C D
CategoryTheory.isRightAdjointOfStructuredArrowInitials 📋 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) [∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)] : G.IsRightAdjoint
CategoryTheory.isRightAdjoint_iff_hasInitial_structuredArrow 📋 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} : G.IsRightAdjoint ↔ ∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)
CategoryTheory.adjunctionOfStructuredArrowInitials 📋 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) [∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)] : CategoryTheory.leftAdjointOfStructuredArrowInitials G ⊣ G
CategoryTheory.leftAdjointOfStructuredArrowInitialsAux 📋 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) [∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)] (A : C) (B : D) : ((⊥_ CategoryTheory.StructuredArrow A G).right ⟶ B) ≃ (A ⟶ G.obj B)
CategoryTheory.leftAdjointOfStructuredArrowInitialsAux_apply 📋 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) [∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)] (A : C) (B : D) (g : (⊥_ CategoryTheory.StructuredArrow A G).right ⟶ B) : (CategoryTheory.leftAdjointOfStructuredArrowInitialsAux G A B) g = CategoryTheory.CategoryStruct.comp (⊥_ CategoryTheory.StructuredArrow A G).hom (G.map g)
CategoryTheory.leftAdjointOfStructuredArrowInitialsAux_symm_apply 📋 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) [∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)] (A : C) (B : D) (f : A ⟶ G.obj B) : (CategoryTheory.leftAdjointOfStructuredArrowInitialsAux G A B).symm f = (CategoryTheory.Limits.initial.to (CategoryTheory.StructuredArrow.mk f)).right
CategoryTheory.Equivalence.hasInitial_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : CategoryTheory.Limits.HasInitial C ↔ CategoryTheory.Limits.HasInitial D
CategoryTheory.hasInitial_of_equivalence 📋 Mathlib.CategoryTheory.Limits.Shapes.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : CategoryTheory.Functor D C) [e.IsEquivalence] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.HasInitial D
CategoryTheory.Limits.hasColimit_iff_hasInitial_cocone 📋 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) : CategoryTheory.Limits.HasColimit F ↔ CategoryTheory.Limits.HasInitial (CategoryTheory.Limits.Cocone F)
CategoryTheory.WithInitial.instHasInitial 📋 Mathlib.CategoryTheory.WithTerminal.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Limits.HasInitial (CategoryTheory.WithInitial C)
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.hasFiniteCoproducts_of_has_binary_and_initial 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.HasFiniteCoproducts C
CategoryTheory.Limits.hasFiniteColimits_of_hasInitial_and_pushouts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] : CategoryTheory.Limits.HasFiniteColimits C
CategoryTheory.Limits.preservesFiniteColimits_of_preservesInitial_and_pushouts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) G] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan G] : CategoryTheory.Limits.PreservesFiniteColimits G
CategoryTheory.Limits.createsFiniteColimitsOfCreatesInitialAndPushouts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasInitial D] [CategoryTheory.Limits.HasPushouts D] (G : CategoryTheory.Functor C D) [G.ReflectsIsomorphisms] [CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) G] [CategoryTheory.CreatesColimitsOfShape CategoryTheory.Limits.WalkingSpan G] : CategoryTheory.Limits.CreatesFiniteColimits G
CategoryTheory.MonoOver.instBot 📋 Mathlib.CategoryTheory.Subobject.Lattice
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.InitialMonoClass C] {X : C} : Bot (CategoryTheory.MonoOver X)
CategoryTheory.Subobject.boundedOrder 📋 Mathlib.CategoryTheory.Subobject.Lattice
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.InitialMonoClass C] {B : C} : BoundedOrder (CategoryTheory.Subobject B)
CategoryTheory.Subobject.orderBot 📋 Mathlib.CategoryTheory.Subobject.Lattice
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.InitialMonoClass C] {X : C} : OrderBot (CategoryTheory.Subobject X)
CategoryTheory.MonoOver.bot_left 📋 Mathlib.CategoryTheory.Subobject.Lattice
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.InitialMonoClass C] (X : C) : ⊥.obj.left = ⊥_ C
CategoryTheory.MonoOver.botLE 📋 Mathlib.CategoryTheory.Subobject.Lattice
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.InitialMonoClass C] {X : C} (f : CategoryTheory.MonoOver X) : ⊥ ⟶ f
CategoryTheory.MonoOver.bot_arrow 📋 Mathlib.CategoryTheory.Subobject.Lattice
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.InitialMonoClass C] {X : C} : ⊥.arrow = CategoryTheory.Limits.initial.to X
CategoryTheory.Subobject.bot_eq_initial_to 📋 Mathlib.CategoryTheory.Subobject.Lattice
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.InitialMonoClass C] {B : C} : ⊥ = CategoryTheory.Subobject.mk (CategoryTheory.Limits.initial.to B)
CategoryTheory.Subobject.botCoeIsoInitial 📋 Mathlib.CategoryTheory.Subobject.Lattice
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.InitialMonoClass C] {B : C} : CategoryTheory.Subobject.underlying.obj ⊥ ≅ ⊥_ C
CategoryTheory.Subobject.finset_sup_factors 📋 Mathlib.CategoryTheory.Subobject.Lattice
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.InitialMonoClass C] {I : Type u_1} {A B : C} {s : Finset I} {P : I → CategoryTheory.Subobject B} {f : A ⟶ B} (h : ∃ i ∈ s, (P i).Factors f) : (s.sup P).Factors f
CategoryTheory.MonoOver.mapBot 📋 Mathlib.CategoryTheory.Subobject.Lattice
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.InitialMonoClass C] (f : X ⟶ Y) [CategoryTheory.Mono f] : (CategoryTheory.MonoOver.map f).obj ⊥ ≅ ⊥
CategoryTheory.Subobject.map_bot 📋 Mathlib.CategoryTheory.Subobject.Lattice
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.InitialMonoClass C] (f : X ⟶ Y) [CategoryTheory.Mono f] : (CategoryTheory.Subobject.map f).obj ⊥ = ⊥
CategoryTheory.Functor.Elements.instHasInitialObjOppositeTypeFlipShrinkYonedaOp 📋 Mathlib.CategoryTheory.Limits.Presheaf
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.LocallySmall.{w, v₁, u₁} C] (X : C) : CategoryTheory.Limits.HasInitial (CategoryTheory.shrinkYoneda.{w, v₁, u₁}.flip.obj (Opposite.op X)).Elements
CategoryTheory.hasInitial_of_isCoseparating 📋 Mathlib.CategoryTheory.Generator.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.LocallySmall.{w, v₁, u₁} C] [CategoryTheory.WellPowered.{w, v₁, u₁} C] [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v₁, u₁} C] {P : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.Small.{w, v₁, u₁} P] (hP : P.IsCoseparating) : CategoryTheory.Limits.HasInitial C
CategoryTheory.hasInitial_of_weakly_initial_and_hasWideEqualizers 📋 Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasWideEqualizers C] {T : C} [CategoryTheory.LocallySmall.{w, v, u} C] (hT : ∀ (X : C), Nonempty (T ⟶ X)) : CategoryTheory.Limits.HasInitial C
CategoryTheory.CommMon.instHasInitial 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Limits.HasInitial (CategoryTheory.CommMon C)
CategoryTheory.CommGrp.instHasInitial 📋 Mathlib.CategoryTheory.Monoidal.CommGrp_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Limits.HasInitial (CategoryTheory.CommGrp C)
CategoryTheory.ObjectProperty.prop_initial 📋 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})] [CategoryTheory.Limits.HasInitial C] : P (⊥_ C)
CategoryTheory.ObjectProperty.instNonemptyOfIsClosedUnderColimitsOfShapeDiscretePEmptyOfHasInitial 📋 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})] [CategoryTheory.Limits.HasInitial C] : P.Nonempty
CategoryTheory.ObjectProperty.IsClosedUnderBinaryCoproducts.closedUnderIsomorphisms 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasInitial C] [P.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderBinaryCoproducts] : P.IsClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.binaryCoproductsClosure_le_iff 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasInitial C] {P Q : CategoryTheory.ObjectProperty C} [Q.IsClosedUnderBinaryCoproducts] [Q.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] : P.binaryCoproductsClosure ≤ Q ↔ P ≤ Q
CategoryTheory.Initial.mono_to 📋 Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Limits.HasInitial C] (B : C) [CategoryTheory.MonoidalClosed C] : CategoryTheory.Mono (CategoryTheory.Limits.initial.to B)
CategoryTheory.to_initial_isIso 📋 Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {A : C} [CategoryTheory.Closed A] [CategoryTheory.Limits.HasInitial C] (f : A ⟶ ⊥_ C) : CategoryTheory.IsIso f
CategoryTheory.isConnected_of_hasInitial 📋 Mathlib.CategoryTheory.Limits.IsConnected
(C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.IsConnected C
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.instInitiallySmallOfHasInitial 📋 Mathlib.CategoryTheory.Limits.FinallySmall
{J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasInitial J] : CategoryTheory.InitiallySmall J
CategoryTheory.hasStrictInitial_of_isUniversal 📋 Mathlib.CategoryTheory.Limits.VanKampen
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] (H : CategoryTheory.IsUniversalColimit (CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.CategoryStruct.id (⊥_ C)) (CategoryTheory.CategoryStruct.id (⊥_ C)))) : CategoryTheory.Limits.HasStrictInitialObjects C
CategoryTheory.BinaryCofan.mono_inr_of_isVanKampen 📋 Mathlib.CategoryTheory.Limits.VanKampen
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] {X Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.IsVanKampenColimit c) : CategoryTheory.Mono c.inr
CategoryTheory.mono_of_cofan_isVanKampen 📋 Mathlib.CategoryTheory.Limits.VanKampen
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] {ι : Type u_3} {F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.IsVanKampenColimit c) (i : CategoryTheory.Discrete ι) : CategoryTheory.Mono (c.ι.app i)
CategoryTheory.BinaryCofan.isPullback_initial_to_of_isVanKampen 📋 Mathlib.CategoryTheory.Limits.VanKampen
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasInitial C] {c : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.IsVanKampenColimit c) : CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (CategoryTheory.Limits.initial.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right })) c.inl c.inr
CategoryTheory.isPullback_initial_to_of_cofan_isVanKampen 📋 Mathlib.CategoryTheory.Limits.VanKampen
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] {ι : Type u_3} {F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.IsVanKampenColimit c) (i j : CategoryTheory.Discrete ι) (hi : i ≠ j) : CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (F.obj i)) (CategoryTheory.Limits.initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
CategoryTheory.isPullback_of_cofan_isVanKampen 📋 Mathlib.CategoryTheory.Limits.VanKampen
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] {ι : Type u_3} {X : ι → C} {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.IsVanKampenColimit c) (i j : ι) [DecidableEq ι] : CategoryTheory.IsPullback (if h : j = i then CategoryTheory.eqToHom ⋯ else CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.initial.to (X i))) (if h : j = i then CategoryTheory.eqToHom ⋯ else CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.initial.to (X j))) (c.inj i) (c.inj j)
Preorder.instHasInitialOfOrderBot 📋 Mathlib.CategoryTheory.Limits.Preorder
{C : Type u} [Preorder C] [OrderBot C] : CategoryTheory.Limits.HasInitial C
Preorder.orderBotOfHasInitial 📋 Mathlib.CategoryTheory.Limits.Preorder
{C : Type u} [Preorder C] [CategoryTheory.Limits.HasInitial C] : OrderBot C
CategoryTheory.MorphismProperty.Under.instHasInitialTopOfContainsIdentities 📋 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.HasInitial (P.Under ⊤ X)
HomotopicalAlgebra.IsCofibrant 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X : C) : Prop
HomotopicalAlgebra.isCofibrant_iff 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X : C) : HomotopicalAlgebra.IsCofibrant X ↔ HomotopicalAlgebra.Cofibration (CategoryTheory.Limits.initial.to X)
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
HomotopicalAlgebra.instCofibrationInlOfIsCofibrant 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X Y : C) [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange] [CategoryTheory.Limits.HasBinaryCoproduct X Y] [hY : HomotopicalAlgebra.IsCofibrant Y] : HomotopicalAlgebra.Cofibration CategoryTheory.Limits.coprod.inl
HomotopicalAlgebra.instCofibrationInrOfIsCofibrant 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X Y : C) [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange] [CategoryTheory.Limits.HasBinaryCoproduct X Y] [hX : HomotopicalAlgebra.IsCofibrant X] : HomotopicalAlgebra.Cofibration CategoryTheory.Limits.coprod.inr
HomotopicalAlgebra.isCofibrant_of_cofibration 📋 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).IsStableUnderComposition] {X Y : C} (i : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [hX : HomotopicalAlgebra.IsCofibrant X] : HomotopicalAlgebra.IsCofibrant Y
HomotopicalAlgebra.Cylinder.instIsCofibrantI 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [(HomotopicalAlgebra.cofibrations C).IsStableUnderComposition] [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange] [HomotopicalAlgebra.IsCofibrant A] [P.IsGood] : HomotopicalAlgebra.IsCofibrant P.I
HomotopicalAlgebra.Cylinder.instCofibrationI₀ 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [(HomotopicalAlgebra.cofibrations C).IsStableUnderComposition] [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange] [HomotopicalAlgebra.IsCofibrant A] [P.IsGood] : HomotopicalAlgebra.Cofibration P.i₀
HomotopicalAlgebra.Cylinder.instCofibrationI₁ 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [(HomotopicalAlgebra.cofibrations C).IsStableUnderComposition] [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange] [HomotopicalAlgebra.IsCofibrant A] [P.IsGood] : HomotopicalAlgebra.Cofibration P.i₁
HomotopicalAlgebra.PathObject.instIsCofibrantPOfIsVeryGood 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A) [HomotopicalAlgebra.CategoryWithFibrations C] [HomotopicalAlgebra.CategoryWithCofibrations C] [(HomotopicalAlgebra.cofibrations C).IsStableUnderComposition] [CategoryTheory.Limits.HasBinaryProduct A A] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.IsCofibrant A] [P.IsVeryGood] : HomotopicalAlgebra.IsCofibrant P.P
HomotopicalAlgebra.PathObject.instIsCofibrantPOfFactorizationDataOfIsStableUnderCompositionCofibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) (CategoryTheory.Limits.diag A)) [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.IsCofibrant A] [(HomotopicalAlgebra.cofibrations C).IsStableUnderComposition] : HomotopicalAlgebra.IsCofibrant (HomotopicalAlgebra.PathObject.ofFactorizationData h).P
CategoryTheory.Factorisation.instHasInitial 📋 Mathlib.CategoryTheory.Category.Factorisation
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} : CategoryTheory.Limits.HasInitial (CategoryTheory.Factorisation f)
HomotopicalAlgebra.CofibrantObject 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
(C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] : Type u
HomotopicalAlgebra.cofibrantObjects 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
(C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.ObjectProperty C
HomotopicalAlgebra.BifibrantObject 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
(C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : Type u
HomotopicalAlgebra.bifibrantObjects 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
(C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.ObjectProperty C
HomotopicalAlgebra.CofibrantObject.mk 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X : C) [HomotopicalAlgebra.IsCofibrant X] : HomotopicalAlgebra.CofibrantObject C
HomotopicalAlgebra.CofibrantObject.ι 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Functor (HomotopicalAlgebra.CofibrantObject C) C
HomotopicalAlgebra.CofibrantObject.instIsCofibrantObjCofibrantObjects 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X : HomotopicalAlgebra.CofibrantObject C) : HomotopicalAlgebra.IsCofibrant X.obj
HomotopicalAlgebra.BifibrantObject.mk 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : C) [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsFibrant X] : HomotopicalAlgebra.BifibrantObject C
HomotopicalAlgebra.BifibrantObject.ι 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Functor (HomotopicalAlgebra.BifibrantObject C) C
HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjBifibrantObjects 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.BifibrantObject C) : HomotopicalAlgebra.IsCofibrant X.obj
HomotopicalAlgebra.BifibrantObject.instIsFibrantObjBifibrantObjects 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.BifibrantObject C) : HomotopicalAlgebra.IsFibrant X.obj
HomotopicalAlgebra.bifibrantObjects_le_cofibrantObject 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
(C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : HomotopicalAlgebra.bifibrantObjects C ≤ HomotopicalAlgebra.cofibrantObjects C
HomotopicalAlgebra.bifibrantObjects_le_fibrantObject 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
(C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : HomotopicalAlgebra.bifibrantObjects C ≤ HomotopicalAlgebra.fibrantObjects C
HomotopicalAlgebra.CofibrantObject.instIsCofibrantObjι 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X : HomotopicalAlgebra.CofibrantObject C) : HomotopicalAlgebra.IsCofibrant (HomotopicalAlgebra.CofibrantObject.ι.obj X)
HomotopicalAlgebra.CofibrantObject.mk_surjective 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X : HomotopicalAlgebra.CofibrantObject C) : ∃ Y, ∃ (x : HomotopicalAlgebra.IsCofibrant Y), X = HomotopicalAlgebra.CofibrantObject.mk Y
HomotopicalAlgebra.BifibrantObject.ιCofibrantObject 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Functor (HomotopicalAlgebra.BifibrantObject C) (HomotopicalAlgebra.CofibrantObject C)
HomotopicalAlgebra.BifibrantObject.ιFibrantObject 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Functor (HomotopicalAlgebra.BifibrantObject C) (HomotopicalAlgebra.FibrantObject C)
HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjι 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.BifibrantObject C) : HomotopicalAlgebra.IsCofibrant (HomotopicalAlgebra.BifibrantObject.ι.obj X)
HomotopicalAlgebra.BifibrantObject.instIsFibrantObjι 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.BifibrantObject C) : HomotopicalAlgebra.IsFibrant (HomotopicalAlgebra.BifibrantObject.ι.obj X)
HomotopicalAlgebra.BifibrantObject.mk_surjective 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.BifibrantObject C) : ∃ Y, ∃ (x : HomotopicalAlgebra.IsCofibrant Y) (x_1 : HomotopicalAlgebra.IsFibrant Y), X = HomotopicalAlgebra.BifibrantObject.mk Y
HomotopicalAlgebra.CofibrantObject.homMk 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] {X Y : C} [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsCofibrant Y] (f : X ⟶ Y) : HomotopicalAlgebra.CofibrantObject.mk X ⟶ HomotopicalAlgebra.CofibrantObject.mk Y
HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjFibrantObjectsObjFibrantObjectιFibrantObject 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.BifibrantObject C) : HomotopicalAlgebra.IsCofibrant (HomotopicalAlgebra.BifibrantObject.ιFibrantObject.obj X).obj
HomotopicalAlgebra.BifibrantObject.instIsFibrantObjCofibrantObjectsObjCofibrantObjectιCofibrantObject 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.BifibrantObject C) : HomotopicalAlgebra.IsFibrant (HomotopicalAlgebra.BifibrantObject.ιCofibrantObject.obj X).obj
HomotopicalAlgebra.CofibrantObject.weakEquivalence_homMk_iff 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] {X Y : C} [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsCofibrant Y] (f : X ⟶ Y) : HomotopicalAlgebra.WeakEquivalence (HomotopicalAlgebra.CofibrantObject.homMk f) ↔ HomotopicalAlgebra.WeakEquivalence f
HomotopicalAlgebra.CofibrantObject.homMk_id 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] (X : C) [HomotopicalAlgebra.IsCofibrant X] : HomotopicalAlgebra.CofibrantObject.homMk (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (HomotopicalAlgebra.CofibrantObject.mk X)
HomotopicalAlgebra.BifibrantObject.homMk 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] {X Y : C} [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsCofibrant Y] [HomotopicalAlgebra.IsFibrant X] [HomotopicalAlgebra.IsFibrant Y] (f : X ⟶ Y) : HomotopicalAlgebra.BifibrantObject.mk X ⟶ HomotopicalAlgebra.BifibrantObject.mk Y
HomotopicalAlgebra.BifibrantObject.weakEquivalence_homMk_iff 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] {X Y : C} [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsFibrant X] [HomotopicalAlgebra.IsCofibrant Y] [HomotopicalAlgebra.IsFibrant Y] (f : X ⟶ Y) : HomotopicalAlgebra.WeakEquivalence (HomotopicalAlgebra.BifibrantObject.homMk f) ↔ HomotopicalAlgebra.WeakEquivalence f
HomotopicalAlgebra.CofibrantObject.homMk_surjective 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] {X Y : C} [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsCofibrant Y] (f : HomotopicalAlgebra.CofibrantObject.mk X ⟶ HomotopicalAlgebra.CofibrantObject.mk Y) : ∃ g, f = HomotopicalAlgebra.CofibrantObject.homMk g
HomotopicalAlgebra.BifibrantObject.homMk_id 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : C) [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsFibrant X] : HomotopicalAlgebra.BifibrantObject.homMk (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (HomotopicalAlgebra.BifibrantObject.mk X)
HomotopicalAlgebra.CofibrantObject.homMk_homMk 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] {X Y Z : C} [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsCofibrant Y] [HomotopicalAlgebra.IsCofibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.homMk f) (HomotopicalAlgebra.CofibrantObject.homMk g) = HomotopicalAlgebra.CofibrantObject.homMk (CategoryTheory.CategoryStruct.comp f g)
HomotopicalAlgebra.BifibrantObject.homMk_surjective 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] {X Y : C} [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsCofibrant Y] [HomotopicalAlgebra.IsFibrant X] [HomotopicalAlgebra.IsFibrant Y] (f : HomotopicalAlgebra.BifibrantObject.mk X ⟶ HomotopicalAlgebra.BifibrantObject.mk Y) : ∃ g, f = HomotopicalAlgebra.BifibrantObject.homMk g
HomotopicalAlgebra.BifibrantObject.homMk_homMk 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] {X Y Z : C} [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsCofibrant Y] [HomotopicalAlgebra.IsCofibrant Z] [HomotopicalAlgebra.IsFibrant X] [HomotopicalAlgebra.IsFibrant Y] [HomotopicalAlgebra.IsFibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.BifibrantObject.homMk f) (HomotopicalAlgebra.BifibrantObject.homMk g) = HomotopicalAlgebra.BifibrantObject.homMk (CategoryTheory.CategoryStruct.comp f g)
HomotopicalAlgebra.CofibrantObject.homMk_homMk_assoc 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] {X Y Z : C} [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsCofibrant Y] [HomotopicalAlgebra.IsCofibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : HomotopicalAlgebra.CofibrantObject C} (h : HomotopicalAlgebra.CofibrantObject.mk Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.homMk f) (CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.homMk g) h) = CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.homMk (CategoryTheory.CategoryStruct.comp f g)) h
HomotopicalAlgebra.BifibrantObject.homMk_homMk_assoc 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] {X Y Z : C} [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsCofibrant Y] [HomotopicalAlgebra.IsCofibrant Z] [HomotopicalAlgebra.IsFibrant X] [HomotopicalAlgebra.IsFibrant Y] [HomotopicalAlgebra.IsFibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : HomotopicalAlgebra.BifibrantObject C} (h : HomotopicalAlgebra.BifibrantObject.mk Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.BifibrantObject.homMk f) (CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.BifibrantObject.homMk g) h) = CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.BifibrantObject.homMk (CategoryTheory.CategoryStruct.comp f g)) h
CategoryTheory.GradedObject.single 📋 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) : CategoryTheory.Functor C (CategoryTheory.GradedObject J C)
CategoryTheory.GradedObject.single₀ 📋 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] [Zero J] : CategoryTheory.Functor C (CategoryTheory.GradedObject J C)
CategoryTheory.GradedObject.singleObjApplyIso 📋 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) : (CategoryTheory.GradedObject.single j).obj X j ≅ X
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.singleObjApplyIsoOfEq 📋 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.GradedObject.single j).obj X i ≅ X
CategoryTheory.GradedObject.singleCompEval 📋 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) : (CategoryTheory.GradedObject.single j).comp (CategoryTheory.GradedObject.eval j) ≅ CategoryTheory.Functor.id C
CategoryTheory.GradedObject.singleCompEval_hom_app 📋 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) : (CategoryTheory.GradedObject.singleCompEval C j).hom.app X = (CategoryTheory.GradedObject.singleObjApplyIso j X).hom
CategoryTheory.GradedObject.singleCompEval_inv_app 📋 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) : (CategoryTheory.GradedObject.singleCompEval C j).inv.app X = (CategoryTheory.GradedObject.singleObjApplyIso j X).inv
CategoryTheory.GradedObject.singleObjApplyIso_inv_single_map 📋 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 Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIso j X).inv ((CategoryTheory.GradedObject.single j).map f j) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.GradedObject.singleObjApplyIso j Y).inv
CategoryTheory.GradedObject.singleObjApplyIsoOfEq_inv_single_map 📋 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 Y : C} (f : X ⟶ Y) (i : J) (h : i = j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIsoOfEq j X i h).inv ((CategoryTheory.GradedObject.single j).map f i) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.GradedObject.singleObjApplyIsoOfEq j Y i h).inv
CategoryTheory.GradedObject.single_map_singleObjApplyIso_hom 📋 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 Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.single j).map f j) (CategoryTheory.GradedObject.singleObjApplyIso j Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIso j X).hom f
CategoryTheory.GradedObject.single_map_singleObjApplyIsoOfEq_hom 📋 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 Y : C} (f : X ⟶ Y) (i : J) (h : i = j) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.single j).map f i) (CategoryTheory.GradedObject.singleObjApplyIsoOfEq j Y i h).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIsoOfEq j X i h).hom f
CategoryTheory.GradedObject.singleObjApplyIso_inv_single_map_assoc 📋 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 Y : C} (f : X ⟶ Y) {Z : C} (h : (CategoryTheory.GradedObject.single j).obj Y j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIso j X).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.single j).map f j) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIso j Y).inv h)
CategoryTheory.GradedObject.single_map_singleObjApplyIso_hom_assoc 📋 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 Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.single j).map f j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIso j Y).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIso j X).hom (CategoryTheory.CategoryStruct.comp f h)
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₀ObjIso 📋 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) (e : F.obj X ≅ CategoryTheory.Functor.id D) (Y : CategoryTheory.GradedObject J D) (a : I × J) (ha : a.1 = 0) : ((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y a ≅ Y a.2
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.mapBifunctorObjObjSingle₀Iso 📋 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) (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) (X : CategoryTheory.GradedObject J D) (a : J × I) (ha : a.2 = 0) : ((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y) a ≅ X a.1
CategoryTheory.GradedObject.mapBifunctorLeftUnitor_hasMap 📋 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) (e : F.obj X ≅ CategoryTheory.Functor.id D) [∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap p
CategoryTheory.GradedObject.mapBifunctorRightUnitor_hasMap 📋 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) (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D) : (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p

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:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
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
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.
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