Loogle!

Result

Found 257 declarations mentioning CategoryTheory.Limits.HasTerminal. Of these, only the first 200 are shown.

CategoryTheory.Limits.HasTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : Prop
CategoryTheory.Limits.terminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : C
CategoryTheory.Limits.IsTerminal.hasTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (h : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.HasTerminal 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.terminalIsTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.IsTerminal (⊤_ C)
CategoryTheory.Limits.terminalIsoIsTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {P : C} (t : CategoryTheory.Limits.IsTerminal P) : ⊤_ C ≅ P
CategoryTheory.Limits.terminal.from 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] (P : C) : P ⟶ ⊤_ C
CategoryTheory.Limits.hasColimit_of_domain_hasTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasTerminal J] {F : CategoryTheory.Functor J C} : CategoryTheory.Limits.HasColimit F
CategoryTheory.Limits.uniqueToTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] (P : C) : Unique (P ⟶ ⊤_ C)
CategoryTheory.Limits.terminal.isSplitMono_from 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y : C} [CategoryTheory.Limits.HasTerminal C] (f : ⊤_ C ⟶ Y) : CategoryTheory.IsSplitMono f
CategoryTheory.Limits.hasTerminal_of_unique 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) [∀ (Y : C), Nonempty (Y ⟶ X)] [∀ (Y : C), Subsingleton (Y ⟶ X)] : CategoryTheory.Limits.HasTerminal 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.instHasLimitObjFunctorConstTerminal 📋 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.HasTerminal C] : CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.const J).obj (⊤_ C))
CategoryTheory.Limits.terminalComparison 📋 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.HasTerminal C] [CategoryTheory.Limits.HasTerminal D] : G.obj (⊤_ C) ⟶ ⊤_ D
CategoryTheory.Limits.colimitOfTerminal 📋 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.HasTerminal J] : CategoryTheory.Limits.colimit F ≅ F.obj (⊤_ J)
CategoryTheory.Limits.terminal.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {P : C} (f g : P ⟶ ⊤_ C) : f = g
CategoryTheory.Limits.terminalIsoIsTerminal_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {P : C} (t : CategoryTheory.Limits.IsTerminal P) : (CategoryTheory.Limits.terminalIsoIsTerminal t).hom = t.from (⊤_ C)
CategoryTheory.Limits.terminal.hom_ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {P : C} {f g : P ⟶ ⊤_ C} : f = g ↔ True
CategoryTheory.Limits.limitConstTerminal 📋 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.HasTerminal C] : CategoryTheory.Limits.limit ((CategoryTheory.Functor.const J).obj (⊤_ C)) ≅ ⊤_ C
CategoryTheory.Limits.terminalIsoIsTerminal_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {P : C} (t : CategoryTheory.Limits.IsTerminal P) : (CategoryTheory.Limits.terminalIsoIsTerminal t).inv = CategoryTheory.Limits.terminalIsTerminal.from P
CategoryTheory.Limits.terminal.comp_from 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {P Q : C} (f : P ⟶ Q) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.terminal.from Q) = CategoryTheory.Limits.terminal.from P
CategoryTheory.Limits.hasLimit_of_domain_hasTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasTerminal J] {F : CategoryTheory.Functor J C} [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : CategoryTheory.Limits.HasLimit F
CategoryTheory.Limits.isIso_ι_terminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasTerminal J] (F : CategoryTheory.Functor J C) : CategoryTheory.IsIso (CategoryTheory.Limits.colimit.ι F (⊤_ J))
CategoryTheory.Limits.limitOfTerminal 📋 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.HasTerminal J] [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : CategoryTheory.Limits.limit F ≅ F.obj (⊤_ J)
CategoryTheory.Limits.terminal.comp_from_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {P Q : C} (f : P ⟶ Q) {Z : C} (h : ⊤_ C ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.terminal.from Q) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.terminal.from P) h
CategoryTheory.Limits.isIso_π_terminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasTerminal J] (F : CategoryTheory.Functor J C) [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F (⊤_ J))
CategoryTheory.Limits.limitConstTerminal_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.HasTerminal C] : CategoryTheory.Limits.limitConstTerminal.hom = CategoryTheory.Limits.terminal.from (CategoryTheory.Limits.limit ((CategoryTheory.Functor.const J).obj (⊤_ C)))
CategoryTheory.Limits.limitConstTerminal_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.HasTerminal C] {j : J} : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.limitConstTerminal.inv (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.const J).obj (⊤_ C)) j) = CategoryTheory.Limits.terminal.from (⊤_ C)
CategoryTheory.Limits.limitConstTerminal_inv_π_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.HasTerminal C] {j : J} {Z : C} (h : ((CategoryTheory.Functor.const J).obj (⊤_ C)).obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.limitConstTerminal.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.const J).obj (⊤_ C)) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.terminal.from (⊤_ C)) h
CategoryTheory.Limits.prod.leftUnitor 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (P : C) [CategoryTheory.Limits.HasBinaryProduct (⊤_ C) P] : (⊤_ C) ⨯ P ≅ P
CategoryTheory.Limits.prod.rightUnitor 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (P : C) [CategoryTheory.Limits.HasBinaryProduct P (⊤_ C)] : P ⨯ ⊤_ C ≅ P
CategoryTheory.Limits.prod.leftUnitor_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (P : C) [CategoryTheory.Limits.HasBinaryProduct (⊤_ C) P] : (CategoryTheory.Limits.prod.leftUnitor P).hom = CategoryTheory.Limits.prod.snd
CategoryTheory.Limits.prod.rightUnitor_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (P : C) [CategoryTheory.Limits.HasBinaryProduct P (⊤_ C)] : (CategoryTheory.Limits.prod.rightUnitor P).hom = CategoryTheory.Limits.prod.fst
CategoryTheory.Limits.prod.leftUnitor_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (P : C) [CategoryTheory.Limits.HasBinaryProduct (⊤_ C) P] : (CategoryTheory.Limits.prod.leftUnitor P).inv = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.terminal.from P) (CategoryTheory.CategoryStruct.id P)
CategoryTheory.Limits.prod.rightUnitor_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (P : C) [CategoryTheory.Limits.HasBinaryProduct P (⊤_ C)] : (CategoryTheory.Limits.prod.rightUnitor P).inv = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id P) (CategoryTheory.Limits.terminal.from P)
CategoryTheory.Limits.prod_rightUnitor_inv_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor X).inv (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (⊤_ C))) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.prod.rightUnitor Y).inv
CategoryTheory.Limits.prod.leftUnitor_hom_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id (⊤_ C)) f) (CategoryTheory.Limits.prod.leftUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor X).hom f
CategoryTheory.Limits.prod.leftUnitor_inv_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor X).inv (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id (⊤_ C)) f) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.prod.leftUnitor Y).inv
CategoryTheory.Limits.prod.rightUnitor_hom_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (⊤_ C))) (CategoryTheory.Limits.prod.rightUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor X).hom f
CategoryTheory.Limits.prod_rightUnitor_inv_naturality_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⨯ ⊤_ C ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (⊤_ C))) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor Y).inv h)
CategoryTheory.Limits.prod.leftUnitor_hom_naturality_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id (⊤_ C)) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor Y).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor X).hom (CategoryTheory.CategoryStruct.comp f h)
CategoryTheory.Limits.prod.leftUnitor_inv_naturality_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : (⊤_ C) ⨯ Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id (⊤_ C)) f) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor Y).inv h)
CategoryTheory.Limits.prod.rightUnitor_hom_naturality_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (⊤_ C))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor Y).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor X).hom (CategoryTheory.CategoryStruct.comp f h)
CategoryTheory.Limits.prod.triangle 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator X (⊤_ C) Y).hom (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.prod.leftUnitor Y).hom) = CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.rightUnitor X).hom (CategoryTheory.CategoryStruct.id Y)
CategoryTheory.Limits.HasZeroObject.hasTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.HasTerminal C
CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasTerminal C] : 0 ≅ ⊤_ C
CategoryTheory.Limits.hasZeroObject_of_hasTerminal_object 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.HasZeroObject C
CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal.hom = 0
CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal.inv = 0
CategoryTheory.Limits.hasTerminal_of_hasTerminal_of_preservesLimit 📋 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.HasTerminal C] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] : CategoryTheory.Limits.HasTerminal D
CategoryTheory.Limits.isLimitOfHasTerminalOfPreservesLimit 📋 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.HasTerminal C] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] : CategoryTheory.Limits.IsTerminal (G.obj (⊤_ C))
CategoryTheory.Limits.preservesTerminal_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.HasTerminal C] [CategoryTheory.Limits.HasTerminal D] (f : G.obj (⊤_ C) ≅ ⊤_ D) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G
CategoryTheory.Limits.PreservesTerminal.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.HasTerminal C] [CategoryTheory.Limits.HasTerminal D] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] : G.obj (⊤_ C) ≅ ⊤_ D
CategoryTheory.Limits.instIsIsoTerminalComparison 📋 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.HasTerminal C] [CategoryTheory.Limits.HasTerminal D] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] : CategoryTheory.IsIso (CategoryTheory.Limits.terminalComparison G)
CategoryTheory.Limits.PreservesTerminal.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.HasTerminal C] [CategoryTheory.Limits.HasTerminal D] [i : CategoryTheory.IsIso (CategoryTheory.Limits.terminalComparison G)] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G
CategoryTheory.Limits.preservesTerminal_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.HasTerminal C] [CategoryTheory.Limits.HasTerminal D] (f : G.obj (⊤_ C) ⟶ ⊤_ D) [i : CategoryTheory.IsIso f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G
CategoryTheory.Limits.PreservesTerminal.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.HasTerminal C] [CategoryTheory.Limits.HasTerminal D] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] : (CategoryTheory.Limits.PreservesTerminal.iso G).hom = CategoryTheory.Limits.terminalComparison G
CategoryTheory.IsFiltered.of_hasTerminal 📋 Mathlib.CategoryTheory.Filtered.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.IsFiltered C
CategoryTheory.Comon.instHasTerminal 📋 Mathlib.CategoryTheory.Monoidal.Comon_
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Limits.HasTerminal (CategoryTheory.Comon C)
CategoryTheory.Limits.terminal.subsingleton_to 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] [CategoryTheory.Limits.HasTerminal C] {A : C} : Subsingleton (⊤_ C ⟶ A)
CategoryTheory.Limits.terminal_isIso_from 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] [CategoryTheory.Limits.HasTerminal C] {A : C} (f : ⊤_ C ⟶ A) : CategoryTheory.IsIso f
CategoryTheory.Limits.terminal.strict_hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] [CategoryTheory.Limits.HasTerminal C] {A : C} (f g : ⊤_ C ⟶ A) : f = g
CategoryTheory.Limits.terminal.strict_hom_ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] [CategoryTheory.Limits.HasTerminal C] {A : C} {f g : ⊤_ C ⟶ A} : f = g ↔ True
hasBinaryProducts_of_hasTerminal_and_pullbacks 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Limits.HasBinaryProducts C
limitConeOfTerminalAndPullbacks 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) : CategoryTheory.Limits.LimitCone F
preservesBinaryProducts_of_preservesTerminal_and_pullbacks 📋 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.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F
prodIsoPullback 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : X ⨯ Y ≅ CategoryTheory.Limits.pullback (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)
prodIsoPullback_hom_fst 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).hom (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)) = CategoryTheory.Limits.prod.fst
prodIsoPullback_hom_snd 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).hom (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)) = CategoryTheory.Limits.prod.snd
prodIsoPullback_inv_fst 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).inv CategoryTheory.Limits.prod.fst = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)
prodIsoPullback_inv_snd 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).inv CategoryTheory.Limits.prod.snd = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)
prodIsoPullback_hom_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
prodIsoPullback_hom_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h
prodIsoPullback_inv_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)) h
prodIsoPullback_inv_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)) h
CategoryTheory.IsPullback.of_hasBinaryProduct' 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.IsPullback CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)
CategoryTheory.Over.instHasTerminal 📋 Mathlib.CategoryTheory.Limits.Comma
{T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {X : T} : CategoryTheory.Limits.HasTerminal (CategoryTheory.Over X)
CategoryTheory.CostructuredArrow.hasTerminal 📋 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.HasTerminal (CategoryTheory.CostructuredArrow G (G.obj Y))
CategoryTheory.rightAdjointOfCostructuredArrowTerminals 📋 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.HasTerminal (CategoryTheory.CostructuredArrow G A)] : CategoryTheory.Functor C D
CategoryTheory.isLeftAdjoint_of_costructuredArrowTerminals 📋 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.HasTerminal (CategoryTheory.CostructuredArrow G A)] : G.IsLeftAdjoint
CategoryTheory.isLeftAdjoint_iff_hasTerminal_costructuredArrow 📋 Mathlib.CategoryTheory.Adjunction.Comma
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} : F.IsLeftAdjoint ↔ ∀ (A : D), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow F A)
CategoryTheory.adjunctionOfCostructuredArrowTerminals 📋 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.HasTerminal (CategoryTheory.CostructuredArrow G A)] : G ⊣ CategoryTheory.rightAdjointOfCostructuredArrowTerminals G
CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux 📋 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.HasTerminal (CategoryTheory.CostructuredArrow G A)] (B : D) (A : C) : (G.obj B ⟶ A) ≃ (B ⟶ (⊤_ CategoryTheory.CostructuredArrow G A).left)
CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux_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.HasTerminal (CategoryTheory.CostructuredArrow G A)] (B : D) (A : C) (g : G.obj B ⟶ A) : (CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux G B A) g = (CategoryTheory.Limits.terminal.from (CategoryTheory.CostructuredArrow.mk g)).left
CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux_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.HasTerminal (CategoryTheory.CostructuredArrow G A)] (B : D) (A : C) (g : B ⟶ (⊤_ CategoryTheory.CostructuredArrow G A).left) : (CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux G B A).symm g = CategoryTheory.CategoryStruct.comp (G.map g) (⊤_ CategoryTheory.CostructuredArrow G A).hom
CategoryTheory.Equivalence.hasTerminal_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.HasTerminal C ↔ CategoryTheory.Limits.HasTerminal D
CategoryTheory.hasTerminal_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.HasTerminal C] : CategoryTheory.Limits.HasTerminal D
CategoryTheory.Limits.hasLimit_iff_hasTerminal_cone 📋 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.HasLimit F ↔ CategoryTheory.Limits.HasTerminal (CategoryTheory.Limits.Cone F)
CategoryTheory.WithTerminal.instHasTerminal 📋 Mathlib.CategoryTheory.WithTerminal.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Limits.HasTerminal (CategoryTheory.WithTerminal C)
CategoryTheory.Functor.instFinalOfHasTerminalOfPreservesLimitDiscretePEmptyEmpty 📋 Mathlib.CategoryTheory.Limits.Final
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F] : F.Final
CategoryTheory.hasFiniteProducts_of_has_binary_and_terminal 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.HasFiniteProducts C
CategoryTheory.Limits.hasFiniteLimits_of_hasTerminal_and_pullbacks 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Limits.HasFiniteLimits C
CategoryTheory.Limits.preservesFiniteLimits_of_preservesTerminal_and_pullbacks 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) G] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan G] : CategoryTheory.Limits.PreservesFiniteLimits G
CategoryTheory.Limits.createsFiniteLimitsOfCreatesTerminalAndPullbacks 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasTerminal D] [CategoryTheory.Limits.HasPullbacks D] (G : CategoryTheory.Functor C D) [G.ReflectsIsomorphisms] [CategoryTheory.CreatesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) G] [CategoryTheory.CreatesLimitsOfShape CategoryTheory.Limits.WalkingCospan G] : CategoryTheory.Limits.CreatesFiniteLimits G
CategoryTheory.hasTerminal_of_isSeparating 📋 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.HasColimitsOfSize.{w, w, v₁, u₁} C] {P : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.Small.{w, v₁, u₁} P] (hP : P.IsSeparating) : CategoryTheory.Limits.HasTerminal C
CategoryTheory.Limits.Concrete.instUniqueToTypeTerminal 📋 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.HasTerminal C] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] : Unique (CategoryTheory.ToType (⊤_ C))
CategoryTheory.Limits.Concrete.terminalEquiv 📋 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.HasTerminal C] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] : CategoryTheory.ToType (⊤_ C) ≃ PUnit.{w + 1}
CategoryTheory.ObjectProperty.prop_terminal 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [CategoryTheory.Limits.HasTerminal C] : P (⊤_ C)
CategoryTheory.ObjectProperty.instNonemptyOfIsClosedUnderLimitsOfShapeDiscretePEmptyOfHasTerminal 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [CategoryTheory.Limits.HasTerminal C] : P.Nonempty
CategoryTheory.ObjectProperty.IsClosedUnderBinaryProducts.closedUnderIsomorphisms 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasTerminal C] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderBinaryProducts] : P.IsClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.binaryProductsClosure_le_iff 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasTerminal C] {P Q : CategoryTheory.ObjectProperty C} [Q.IsClosedUnderBinaryProducts] [Q.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] : P.binaryProductsClosure ≤ Q ↔ P ≤ Q
CategoryTheory.isConnected_of_hasTerminal 📋 Mathlib.CategoryTheory.Limits.IsConnected
(C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.IsConnected C
CategoryTheory.Functor.final_const_terminal 📋 Mathlib.CategoryTheory.Filtered.Final
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.IsFiltered C] [CategoryTheory.Limits.HasTerminal D] : ((CategoryTheory.Functor.const C).obj (⊤_ D)).Final
CategoryTheory.instFinallySmallOfHasTerminal 📋 Mathlib.CategoryTheory.Limits.FinallySmall
{J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasTerminal J] : CategoryTheory.FinallySmall J
Preorder.instHasTerminalOfOrderTop 📋 Mathlib.CategoryTheory.Limits.Preorder
{C : Type u} [Preorder C] [OrderTop C] : CategoryTheory.Limits.HasTerminal C
Preorder.orderTopOfHasTerminal 📋 Mathlib.CategoryTheory.Limits.Preorder
{C : Type u} [Preorder C] [CategoryTheory.Limits.HasTerminal C] : OrderTop C
CategoryTheory.isCardinalFiltered_of_hasTerminal 📋 Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
(J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasTerminal J] (κ : Cardinal.{w}) [Fact κ.IsRegular] : CategoryTheory.IsCardinalFiltered J κ
CategoryTheory.Over.over_hasTerminal 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) : CategoryTheory.Limits.HasTerminal (CategoryTheory.Over B)
CategoryTheory.MorphismProperty.Over.instHasTerminalTopOfContainsIdentities 📋 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.HasTerminal (P.Over ⊤ X)
SimplexCategory.instHasTerminal 📋 Mathlib.AlgebraicTopology.SimplexCategory.Basic
: CategoryTheory.Limits.HasTerminal SimplexCategory
CategoryTheory.CechNerveTerminalFrom.wideCospan 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) (X : C) : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape ι) C
CategoryTheory.CechNerveTerminalFrom.hasLimit_wideCospan 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) : CategoryTheory.Limits.HasLimit (CategoryTheory.CechNerveTerminalFrom.wideCospan ι X)
CategoryTheory.CechNerveTerminalFrom.wideCospan.limitCone 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) : CategoryTheory.Limits.LimitCone (CategoryTheory.CechNerveTerminalFrom.wideCospan ι X)
CategoryTheory.CechNerveTerminalFrom.hasWidePullback' 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) : CategoryTheory.Limits.HasWidePullback (⊤_ C) (fun x => X) fun x => CategoryTheory.Limits.terminal.from X
CategoryTheory.CechNerveTerminalFrom.uniqueToWideCospanNone 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) (X Y : C) : Unique (Y ⟶ (CategoryTheory.CechNerveTerminalFrom.wideCospan ι X).obj none)
CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) : CategoryTheory.Limits.limit (CategoryTheory.CechNerveTerminalFrom.wideCospan ι X) ≅ ∏ᶜ fun x => X
CategoryTheory.CechNerveTerminalFrom.hasWidePullback 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) : CategoryTheory.Limits.HasWidePullback (CategoryTheory.Arrow.mk (CategoryTheory.Limits.terminal.from X)).right (fun x => (CategoryTheory.Arrow.mk (CategoryTheory.Limits.terminal.from X)).left) fun x => (CategoryTheory.Arrow.mk (CategoryTheory.Limits.terminal.from X)).hom
CategoryTheory.CechNerveTerminalFrom.iso 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasFiniteProducts C] (X : C) : (CategoryTheory.Arrow.mk (CategoryTheory.Limits.terminal.from X)).cechNerve ≅ CategoryTheory.cechNerveTerminalFrom X
CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) (j : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).hom (CategoryTheory.Limits.Pi.π (fun x => X) j) = CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j
CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) (j : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).inv (CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j) = CategoryTheory.Limits.Pi.π (fun x => X) j
CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi_assoc 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) (j : ι) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => X) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j) h
CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi_assoc 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) (j : ι) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => X) j) h
HomotopicalAlgebra.IsFibrant 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : C) : Prop
HomotopicalAlgebra.isFibrant_iff 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : C) : HomotopicalAlgebra.IsFibrant X ↔ HomotopicalAlgebra.Fibration (CategoryTheory.Limits.terminal.from X)
HomotopicalAlgebra.isFibrant_iff_of_isTerminal 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [(HomotopicalAlgebra.fibrations C).RespectsIso] {X Y : C} (p : X ⟶ Y) (hY : CategoryTheory.Limits.IsTerminal Y) : HomotopicalAlgebra.IsFibrant X ↔ HomotopicalAlgebra.Fibration p
HomotopicalAlgebra.instFibrationFstOfIsFibrant 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X Y : C) [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] [CategoryTheory.Limits.HasBinaryProduct X Y] [hY : HomotopicalAlgebra.IsFibrant Y] : HomotopicalAlgebra.Fibration CategoryTheory.Limits.prod.fst
HomotopicalAlgebra.instFibrationSndOfIsFibrant 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X Y : C) [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] [CategoryTheory.Limits.HasBinaryProduct X Y] [hX : HomotopicalAlgebra.IsFibrant X] : HomotopicalAlgebra.Fibration CategoryTheory.Limits.prod.snd
HomotopicalAlgebra.isFibrant_of_fibration 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition] {X Y : C} (p : X ⟶ Y) [HomotopicalAlgebra.Fibration p] [hY : HomotopicalAlgebra.IsFibrant Y] : HomotopicalAlgebra.IsFibrant X
HomotopicalAlgebra.Cylinder.instIsFibrantIOfIsVeryGood 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A) [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition] [CategoryTheory.Limits.HasBinaryCoproduct A A] [CategoryTheory.Limits.HasTerminal C] [HomotopicalAlgebra.IsFibrant A] [P.IsVeryGood] : HomotopicalAlgebra.IsFibrant P.I
HomotopicalAlgebra.Cylinder.instIsFibrantIOfFactorizationDataOfIsStableUnderCompositionFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) (CategoryTheory.Limits.codiag A)) [CategoryTheory.Limits.HasTerminal C] [HomotopicalAlgebra.IsFibrant A] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition] : HomotopicalAlgebra.IsFibrant (HomotopicalAlgebra.Cylinder.ofFactorizationData h).I
HomotopicalAlgebra.PathObject.instIsFibrantP 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A) [CategoryTheory.Limits.HasBinaryProduct A A] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition] [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] [HomotopicalAlgebra.IsFibrant A] [P.IsGood] : HomotopicalAlgebra.IsFibrant P.P
HomotopicalAlgebra.PathObject.instFibrationP₀ 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A) [CategoryTheory.Limits.HasBinaryProduct A A] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition] [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] [HomotopicalAlgebra.IsFibrant A] [P.IsGood] : HomotopicalAlgebra.Fibration P.p₀
HomotopicalAlgebra.PathObject.instFibrationP₁ 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A) [CategoryTheory.Limits.HasBinaryProduct A A] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition] [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] [HomotopicalAlgebra.IsFibrant A] [P.IsGood] : HomotopicalAlgebra.Fibration P.p₁
CategoryTheory.Factorisation.instHasTerminal 📋 Mathlib.CategoryTheory.Category.Factorisation
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} : CategoryTheory.Limits.HasTerminal (CategoryTheory.Factorisation f)
HomotopicalAlgebra.FibrantObject 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
(C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : Type u
HomotopicalAlgebra.fibrantObjects 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
(C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal 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.FibrantObject.mk 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : C) [HomotopicalAlgebra.IsFibrant X] : HomotopicalAlgebra.FibrantObject C
HomotopicalAlgebra.FibrantObject.ι 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Functor (HomotopicalAlgebra.FibrantObject C) C
HomotopicalAlgebra.FibrantObject.instIsFibrantObjFibrantObjects 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.FibrantObject C) : HomotopicalAlgebra.IsFibrant 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.FibrantObject.instIsFibrantObjι 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.FibrantObject C) : HomotopicalAlgebra.IsFibrant (HomotopicalAlgebra.FibrantObject.ι.obj X)
HomotopicalAlgebra.FibrantObject.mk_surjective 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.FibrantObject C) : ∃ Y, ∃ (x : HomotopicalAlgebra.IsFibrant Y), X = HomotopicalAlgebra.FibrantObject.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.FibrantObject.homMk 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] {X Y : C} [HomotopicalAlgebra.IsFibrant X] [HomotopicalAlgebra.IsFibrant Y] (f : X ⟶ Y) : HomotopicalAlgebra.FibrantObject.mk X ⟶ HomotopicalAlgebra.FibrantObject.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.FibrantObject.weakEquivalence_homMk_iff 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] {X Y : C} [HomotopicalAlgebra.IsFibrant X] [HomotopicalAlgebra.IsFibrant Y] (f : X ⟶ Y) : HomotopicalAlgebra.WeakEquivalence (HomotopicalAlgebra.FibrantObject.homMk f) ↔ HomotopicalAlgebra.WeakEquivalence f
HomotopicalAlgebra.FibrantObject.homMk_id 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X : C) [HomotopicalAlgebra.IsFibrant X] : HomotopicalAlgebra.FibrantObject.homMk (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (HomotopicalAlgebra.FibrantObject.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.FibrantObject.homMk_surjective 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] {X Y : C} [HomotopicalAlgebra.IsFibrant X] [HomotopicalAlgebra.IsFibrant Y] (f : HomotopicalAlgebra.FibrantObject.mk X ⟶ HomotopicalAlgebra.FibrantObject.mk Y) : ∃ g, f = HomotopicalAlgebra.FibrantObject.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.FibrantObject.homMk_homMk 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] {X Y Z : C} [HomotopicalAlgebra.IsFibrant X] [HomotopicalAlgebra.IsFibrant Y] [HomotopicalAlgebra.IsFibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.FibrantObject.homMk f) (HomotopicalAlgebra.FibrantObject.homMk g) = HomotopicalAlgebra.FibrantObject.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.FibrantObject.homMk_homMk_assoc 📋 Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] {X Y Z : C} [HomotopicalAlgebra.IsFibrant X] [HomotopicalAlgebra.IsFibrant Y] [HomotopicalAlgebra.IsFibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : HomotopicalAlgebra.FibrantObject C} (h : HomotopicalAlgebra.FibrantObject.mk Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.FibrantObject.homMk f) (CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.FibrantObject.homMk g) h) = CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.FibrantObject.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
AlgebraicGeometry.instHasTerminalScheme 📋 Mathlib.AlgebraicGeometry.Limits
: CategoryTheory.Limits.HasTerminal AlgebraicGeometry.Scheme
CategoryTheory.Sheaf.isConstant_of_isIso_counit_app 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] (F : CategoryTheory.Sheaf J D) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.IsIso ((CategoryTheory.constantSheafAdj J D CategoryTheory.Limits.terminalIsTerminal).counit.app F)] : CategoryTheory.Sheaf.IsConstant J F
CategoryTheory.Functor.relativelyRepresentable.of_diag 📋 Mathlib.CategoryTheory.MorphismProperty.Representable
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks D] [CategoryTheory.Limits.HasBinaryProducts D] [CategoryTheory.Limits.HasTerminal D] [F.Full] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] {X : D} (h : F.relativelyRepresentable (CategoryTheory.Limits.diag X)) ⦃a : C⦄ (g : F.obj a ⟶ X) : F.relativelyRepresentable g
CategoryTheory.Functor.relativelyRepresentable.diag_of_map_from_obj 📋 Mathlib.CategoryTheory.MorphismProperty.Representable
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks D] [CategoryTheory.Limits.HasBinaryProducts D] [CategoryTheory.Limits.HasTerminal D] [F.Full] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] {X : D} (h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g) : F.relativelyRepresentable (CategoryTheory.Limits.diag X)
CategoryTheory.Functor.relativelyRepresentable.diag_iff 📋 Mathlib.CategoryTheory.MorphismProperty.Representable
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks D] [CategoryTheory.Limits.HasBinaryProducts D] [CategoryTheory.Limits.HasTerminal D] [F.Full] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] {X : D} [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] : F.relativelyRepresentable (CategoryTheory.Limits.diag X) ↔ ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
CategoryTheory.Functor.relativelyRepresentable.toPullbackTerminal 📋 Mathlib.CategoryTheory.MorphismProperty.Representable
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks D] [CategoryTheory.Limits.HasBinaryProducts D] [CategoryTheory.Limits.HasTerminal D] [F.Full] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] {X : D} {a : C} [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] (g : F.obj a ⟶ CategoryTheory.Limits.pullback (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from X)) : F.relativelyRepresentable (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id (F.obj a)) (CategoryTheory.CategoryStruct.id (F.obj a)) ⋯)
CategoryTheory.Cat.instHasTerminal 📋 Mathlib.CategoryTheory.Category.Cat.Terminal
: CategoryTheory.Limits.HasTerminal CategoryTheory.Cat
CategoryTheory.PreGaloisCategory.hasTerminal 📋 Mathlib.CategoryTheory.Galois.Basic
{C : Type u₁} {inst✝ : CategoryTheory.Category.{u₂, u₁} C} [self : CategoryTheory.PreGaloisCategory C] : CategoryTheory.Limits.HasTerminal C
CategoryTheory.PreGaloisCategory.mk 📋 Mathlib.CategoryTheory.Galois.Basic
{C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (hasTerminal : CategoryTheory.Limits.HasTerminal C := by infer_instance) (hasPullbacks : CategoryTheory.Limits.HasPullbacks C := by infer_instance) (hasFiniteCoproducts : CategoryTheory.Limits.HasFiniteCoproducts C := by infer_instance) (hasQuotientsByFiniteGroups : ∀ (G : Type u₂) [inst : Group G] [Finite G], CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.SingleObj G) C := by infer_instance) (monoInducesIsoOnDirectSummand : ∀ {X Y : C} (i : X ⟶ Y) [CategoryTheory.Mono i], ∃ Z u, Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk i u))) : CategoryTheory.PreGaloisCategory C
CategoryTheory.Limits.FormalCoproduct.instHasTerminal 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.HasTerminal (CategoryTheory.Limits.FormalCoproduct C)
CategoryTheory.instInhabitedSubterminalsOfHasTerminal 📋 Mathlib.CategoryTheory.Subterminal
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : Inhabited (CategoryTheory.Subterminals C)
CategoryTheory.isSubterminal_of_terminal 📋 Mathlib.CategoryTheory.Subterminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.IsSubterminal (⊤_ C)
CategoryTheory.isSubterminal_of_mono_terminal_from 📋 Mathlib.CategoryTheory.Subterminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Mono (CategoryTheory.Limits.terminal.from A)] : CategoryTheory.IsSubterminal A
CategoryTheory.IsSubterminal.mono_terminal_from 📋 Mathlib.CategoryTheory.Subterminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} [CategoryTheory.Limits.HasTerminal C] (hA : CategoryTheory.IsSubterminal A) : CategoryTheory.Mono (CategoryTheory.Limits.terminal.from A)
CategoryTheory.subterminalsEquivMonoOverTerminal 📋 Mathlib.CategoryTheory.Subterminal
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Subterminals C ≌ CategoryTheory.MonoOver (⊤_ C)
CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_obj_obj 📋 Mathlib.CategoryTheory.Subterminal
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] (X : CategoryTheory.MonoOver (⊤_ C)) : ((CategoryTheory.subterminalsEquivMonoOverTerminal C).inverse.obj X).obj = X.obj.left
CategoryTheory.subterminalsEquivMonoOverTerminal_functor_obj_obj 📋 Mathlib.CategoryTheory.Subterminal
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] (X : CategoryTheory.Subterminals C) : ((CategoryTheory.subterminalsEquivMonoOverTerminal C).functor.obj X).obj = CategoryTheory.Over.mk (CategoryTheory.Limits.terminal.from X.obj)
CategoryTheory.subterminals_to_monoOver_terminal_comp_forget 📋 Mathlib.CategoryTheory.Subterminal
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : (CategoryTheory.subterminalsEquivMonoOverTerminal C).functor.comp ((CategoryTheory.MonoOver.forget (⊤_ C)).comp (CategoryTheory.Over.forget (⊤_ C))) = CategoryTheory.subterminalInclusion C
CategoryTheory.monoOver_terminal_to_subterminals_comp 📋 Mathlib.CategoryTheory.Subterminal
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : (CategoryTheory.subterminalsEquivMonoOverTerminal C).inverse.comp (CategoryTheory.subterminalInclusion C) = (CategoryTheory.MonoOver.forget (⊤_ C)).comp (CategoryTheory.Over.forget (⊤_ C))
CategoryTheory.subterminalsEquivMonoOverTerminal_functor_map 📋 Mathlib.CategoryTheory.Subterminal
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {X✝ Y✝ : CategoryTheory.Subterminals C} (f : X✝ ⟶ Y✝) : (CategoryTheory.subterminalsEquivMonoOverTerminal C).functor.map f = CategoryTheory.MonoOver.homMk f.hom ⋯
CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_map 📋 Mathlib.CategoryTheory.Subterminal
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {X✝ Y✝ : CategoryTheory.MonoOver (⊤_ C)} (f : X✝ ⟶ Y✝) : (CategoryTheory.subterminalsEquivMonoOverTerminal C).inverse.map f = CategoryTheory.ObjectProperty.homMk f.hom.left
CategoryTheory.subterminalsEquivMonoOverTerminal_unitIso 📋 Mathlib.CategoryTheory.Subterminal
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : (CategoryTheory.subterminalsEquivMonoOverTerminal C).unitIso = CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Iso.refl X) ⋯
CategoryTheory.subterminalsEquivMonoOverTerminal_counitIso 📋 Mathlib.CategoryTheory.Subterminal
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : (CategoryTheory.subterminalsEquivMonoOverTerminal C).counitIso = CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.MonoOver.isoMk (CategoryTheory.Iso.refl (({ obj := fun X => { obj := X.obj.left, property := ⋯ }, map := fun {X Y} f => CategoryTheory.ObjectProperty.homMk f.hom.left, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun X => { obj := CategoryTheory.Over.mk (CategoryTheory.Limits.terminal.from X.obj), property := ⋯ }, map := fun {X Y} f => CategoryTheory.MonoOver.homMk f.hom ⋯, map_id := ⋯, map_comp := ⋯ }).obj X).obj.left) ⋯) ⋯
CategoryTheory.CardinalDirectedPoset.instHasTerminalElemCarrierObjPartOrdEmbIsCardinalFilteredValSetPropSet 📋 Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
{κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ) (S : Subtype J.PropSet) : CategoryTheory.Limits.HasTerminal ↑↑S
CategoryTheory.CardinalDirectedPoset.instHasTerminalElemCarrierObjPartOrdEmbIsCardinalFilteredWithTopValSetPropSetWithTop 📋 Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
{κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] (S : Subtype (J.PropSetWithTop κ')) : CategoryTheory.Limits.HasTerminal ↑↑S
CategoryTheory.hasGlobalSectionsFunctor_of_hasTerminal 📋 Mathlib.CategoryTheory.Sites.GlobalSections
{C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.HasGlobalSectionsFunctor J A
CategoryTheory.Sheaf.ΓNatIsoSheafSections 📋 Mathlib.CategoryTheory.Sites.GlobalSections
{C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasTerminal C] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Sheaf.Γ J A ≅ (CategoryTheory.sheafSections J A).obj (Opposite.op T)
CategoryTheory.GrothendieckTopology.IsLocalSite.instTrivialOfHasTerminal 📋 Mathlib.CategoryTheory.Sites.LocalSite
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] : (CategoryTheory.GrothendieckTopology.trivial C).IsLocalSite
CategoryTheory.SubobjectRepresentableBy.hasTerminal 📋 Mathlib.CategoryTheory.Subobject.Classifier.Defs
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {Ω : C} (h : CategoryTheory.SubobjectRepresentableBy Ω) : CategoryTheory.Limits.HasTerminal C

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