Homotopy

📁 Source: Mathlib/AlgebraicTopology/SimplicialObject/Homotopy.lean

Statistics

Metric	Count
Definitions h, postcomp, precomp, refl, whiskerRight	5
Theorems ext, ext_iff, h_castSucc_comp_δ_succ_of_lt, h_castSucc_comp_δ_succ_of_lt_assoc, h_comp_σ_castSucc_of_le, h_comp_σ_castSucc_of_le_assoc, h_comp_σ_succ_of_lt, h_comp_σ_succ_of_lt_assoc, h_last_comp_δ_last, h_last_comp_δ_last_assoc, h_succ_comp_δ_castSucc_of_lt, h_succ_comp_δ_castSucc_of_lt_assoc, h_succ_comp_δ_castSucc_succ, h_succ_comp_δ_castSucc_succ_assoc, h_zero_comp_δ_zero, h_zero_comp_δ_zero_assoc, postcomp_h, precomp_h, refl_h, whiskerRight_h	20
Total	25

CategoryTheory.SimplicialObject.Homotopy

Definitions

Name	Category	Theorems
h 📖	CompOp	20 math math: ext_iff, h_last_comp_δ_last_assoc, h_succ_comp_δ_castSucc_of_lt, h_comp_σ_castSucc_of_le_assoc, h_comp_σ_castSucc_of_le, h_last_comp_δ_last, h_comp_σ_succ_of_lt_assoc, precomp_h, refl_h, h_comp_σ_succ_of_lt, h_castSucc_comp_δ_succ_of_lt_assoc, h_zero_comp_δ_zero_assoc, whiskerRight_h, h_succ_comp_δ_castSucc_succ_assoc, h_zero_comp_δ_zero, postcomp_h, h_castSucc_comp_δ_succ_of_lt, ToChainHomotopy.hom_eq, h_succ_comp_δ_castSucc_succ, h_succ_comp_δ_castSucc_of_lt_assoc
postcomp 📖	CompOp	1 math math: postcomp_h
precomp 📖	CompOp	1 math math: precomp_h
refl 📖	CompOp	1 math math: refl_h
whiskerRight 📖	CompOp	1 math math: whiskerRight_h

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	h	—	—	—
ext_iff 📖	mathematical	—	h	—	ext
h_castSucc_comp_δ_succ_of_lt 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op h CategoryTheory.SimplicialObject.δ	—	—
h_castSucc_comp_δ_succ_of_lt_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op h CategoryTheory.SimplicialObject.δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' h_castSucc_comp_δ_succ_of_lt
h_comp_σ_castSucc_of_le 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op h CategoryTheory.SimplicialObject.σ	—	—
h_comp_σ_castSucc_of_le_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op h CategoryTheory.SimplicialObject.σ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' h_comp_σ_castSucc_of_le
h_comp_σ_succ_of_lt 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op h CategoryTheory.SimplicialObject.σ	—	—
h_comp_σ_succ_of_lt_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op h CategoryTheory.SimplicialObject.σ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' h_comp_σ_succ_of_lt
h_last_comp_δ_last 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op h CategoryTheory.SimplicialObject.δ CategoryTheory.NatTrans.app	—	—
h_last_comp_δ_last_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op h CategoryTheory.SimplicialObject.δ CategoryTheory.NatTrans.app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' h_last_comp_δ_last
h_succ_comp_δ_castSucc_of_lt 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op h CategoryTheory.SimplicialObject.δ	—	—
h_succ_comp_δ_castSucc_of_lt_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op h CategoryTheory.SimplicialObject.δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' h_succ_comp_δ_castSucc_of_lt
h_succ_comp_δ_castSucc_succ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op h CategoryTheory.SimplicialObject.δ	—	—
h_succ_comp_δ_castSucc_succ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op h CategoryTheory.SimplicialObject.δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' h_succ_comp_δ_castSucc_succ
h_zero_comp_δ_zero 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op h CategoryTheory.SimplicialObject.δ CategoryTheory.NatTrans.app	—	—
h_zero_comp_δ_zero_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op h CategoryTheory.SimplicialObject.δ CategoryTheory.NatTrans.app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' h_zero_comp_δ_zero
postcomp_h 📖	mathematical	—	h CategoryTheory.CategoryStruct.comp CategoryTheory.SimplicialObject CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory postcomp CategoryTheory.Functor.obj Opposite.op CategoryTheory.NatTrans.app	—	—
precomp_h 📖	mathematical	—	h CategoryTheory.CategoryStruct.comp CategoryTheory.SimplicialObject CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory precomp CategoryTheory.Functor.obj Opposite.op CategoryTheory.NatTrans.app	—	—
refl_h 📖	mathematical	—	h refl CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op CategoryTheory.SimplicialObject.σ CategoryTheory.NatTrans.app	—	—
whiskerRight_h 📖	mathematical	—	h CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor CategoryTheory.SimplicialObject.whiskering CategoryTheory.Functor.map whiskerRight Opposite.op	—	—

---

← Back to Index