StrictInitial

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean

Statistics

Metric	Count
Definitions HasStrictInitialObjects, HasStrictTerminalObjects, ofStrict, ofStrict, initialMul, isInitialMul, mulInitial, mulIsInitial	8
Theorems out, out, isIso_to, strict_hom_ext, subsingleton_to, isIso_from, strict_hom_ext, subsingleton_to, hasStrictInitialObjects_of_initial_is_strict, hasStrictTerminalObjects_of_terminal_is_strict, strict_hom_ext, strict_hom_ext_iff, subsingleton_to, initialMul_hom, initialMul_inv, initial_isIso_to, initial_mono_of_strict_initial_objects, isInitialMul_hom, isInitialMul_inv, limit_π_isIso_of_is_strict_terminal, mulInitial_hom, mulInitial_inv, mulIsInitial_hom, mulIsInitial_inv, strict_hom_ext, strict_hom_ext_iff, subsingleton_to, terminal_isIso_from	28
Total	36

CategoryTheory.Limits

Definitions

Name	Category	Theorems
HasStrictInitialObjects 📖	CompData	4 math math: CategoryTheory.hasStrictInitial_of_isUniversal, hasStrictInitialObjects_of_initial_is_strict, AlgebraicGeometry.instHasStrictInitialObjectsScheme, CategoryTheory.hasStrictInitialObjects_of_finitaryPreExtensive
HasStrictTerminalObjects 📖	CompData	2 math math: CommRingCat.commRingCat_hasStrictTerminalObjects, hasStrictTerminalObjects_of_terminal_is_strict
initialMul 📖	CompOp	2 math math: initialMul_inv, initialMul_hom
isInitialMul 📖	CompOp	2 math math: isInitialMul_hom, isInitialMul_inv
mulInitial 📖	CompOp	2 math math: mulInitial_inv, mulInitial_hom
mulIsInitial 📖	CompOp	2 math math: mulIsInitial_hom, mulIsInitial_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasStrictInitialObjects_of_initial_is_strict 📖	mathematical	CategoryTheory.IsIso initial	HasStrictInitialObjects	—	CategoryTheory.Category.assoc CategoryTheory.IsIso.hom_inv_id IsInitial.hom_ext
hasStrictTerminalObjects_of_terminal_is_strict 📖	mathematical	CategoryTheory.IsIso	HasStrictTerminalObjects	—	IsTerminal.hom_ext CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_hom_id
initialMul_hom 📖	mathematical	—	CategoryTheory.Iso.hom prod initial initialMul prod.fst	—	—
initialMul_inv 📖	mathematical	—	CategoryTheory.Iso.inv prod initial initialMul initial.to	—	Unique.instSubsingleton
initial_isIso_to 📖	mathematical	—	CategoryTheory.IsIso initial	—	IsInitial.isIso_to
initial_mono_of_strict_initial_objects 📖	mathematical	—	InitialMonoClass	—	IsInitial.strict_hom_ext
isInitialMul_hom 📖	mathematical	—	CategoryTheory.Iso.hom prod isInitialMul prod.fst	—	—
isInitialMul_inv 📖	mathematical	—	CategoryTheory.Iso.inv prod isInitialMul IsInitial.to	—	IsInitial.hom_ext
limit_π_isIso_of_is_strict_terminal 📖	mathematical	—	CategoryTheory.IsIso limit CategoryTheory.Functor.obj limit.π	—	CategoryTheory.Category.comp_id CategoryTheory.Functor.map_id IsTerminal.isIso_from CategoryTheory.IsIso.comp_inv_eq IsTerminal.hom_ext limit.hom_ext CategoryTheory.Category.assoc limit.lift_π CategoryTheory.Category.id_comp CategoryTheory.eqToHom_refl
mulInitial_hom 📖	mathematical	—	CategoryTheory.Iso.hom prod initial mulInitial prod.snd	—	—
mulInitial_inv 📖	mathematical	—	CategoryTheory.Iso.inv prod initial mulInitial initial.to	—	Unique.instSubsingleton
mulIsInitial_hom 📖	mathematical	—	CategoryTheory.Iso.hom prod mulIsInitial prod.snd	—	—
mulIsInitial_inv 📖	mathematical	—	CategoryTheory.Iso.inv prod mulIsInitial IsInitial.to	—	IsInitial.hom_ext
terminal_isIso_from 📖	mathematical	—	CategoryTheory.IsIso terminal	—	IsTerminal.isIso_from

CategoryTheory.Limits.HasStrictInitialObjects

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
out 📖	mathematical	—	CategoryTheory.IsIso	—	—

CategoryTheory.Limits.HasStrictTerminalObjects

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
out 📖	mathematical	—	CategoryTheory.IsIso	—	—

CategoryTheory.Limits.IsInitial

Definitions

Name	Category	Theorems
ofStrict 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_to 📖	mathematical	—	CategoryTheory.IsIso	—	CategoryTheory.Limits.HasStrictInitialObjects.out
strict_hom_ext 📖	—	—	—	—	CategoryTheory.eq_of_inv_eq_inv isIso_to hom_ext
subsingleton_to 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	strict_hom_ext

CategoryTheory.Limits.IsTerminal

Definitions

Name	Category	Theorems
ofStrict 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_from 📖	mathematical	—	CategoryTheory.IsIso	—	CategoryTheory.Limits.HasStrictTerminalObjects.out
strict_hom_ext 📖	—	—	—	—	CategoryTheory.eq_of_inv_eq_inv isIso_from hom_ext
subsingleton_to 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	strict_hom_ext

CategoryTheory.Limits.initial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strict_hom_ext 📖	—	—	—	—	CategoryTheory.Limits.IsInitial.strict_hom_ext
strict_hom_ext_iff 📖	—	—	—	—	strict_hom_ext
subsingleton_to 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.initial	—	CategoryTheory.Limits.IsInitial.subsingleton_to

CategoryTheory.Limits.terminal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strict_hom_ext 📖	—	—	—	—	CategoryTheory.Limits.IsTerminal.strict_hom_ext
strict_hom_ext_iff 📖	—	—	—	—	strict_hom_ext
subsingleton_to 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.terminal	—	CategoryTheory.Limits.IsTerminal.subsingleton_to

---

← Back to Index