Commit 2023-04-11 12:30 d462f81d

View on Github →

feat: port AlgebraicTopology.SimplicialObject (#3302)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/SimplicialObject.lean

added def CategoryTheory.CosimplicialObject.Augmented.drop

added theorem CategoryTheory.CosimplicialObject.Augmented.hom_ext

added def CategoryTheory.CosimplicialObject.Augmented.leftOp

added def CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso

added def CategoryTheory.CosimplicialObject.Augmented.point

added def CategoryTheory.CosimplicialObject.Augmented.toArrow

added def CategoryTheory.CosimplicialObject.Augmented.whiskering

added def CategoryTheory.CosimplicialObject.Augmented.whiskeringObj

added def CategoryTheory.CosimplicialObject.Augmented

added def CategoryTheory.CosimplicialObject.Truncated.whiskering

added def CategoryTheory.CosimplicialObject.Truncated

added def CategoryTheory.CosimplicialObject.augment

added theorem CategoryTheory.CosimplicialObject.augment_hom_zero

added def CategoryTheory.CosimplicialObject.eqToIso

added theorem CategoryTheory.CosimplicialObject.eqToIso_refl

added theorem CategoryTheory.CosimplicialObject.hom_ext

added def CategoryTheory.CosimplicialObject.sk

added def CategoryTheory.CosimplicialObject.whiskering

added def CategoryTheory.CosimplicialObject.δ

added theorem CategoryTheory.CosimplicialObject.δ_comp_δ''

added theorem CategoryTheory.CosimplicialObject.δ_comp_δ'

added theorem CategoryTheory.CosimplicialObject.δ_comp_δ

added theorem CategoryTheory.CosimplicialObject.δ_comp_δ_self'

added theorem CategoryTheory.CosimplicialObject.δ_comp_δ_self

added theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt'

added theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt

added theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_le

added theorem CategoryTheory.CosimplicialObject.δ_comp_σ_self'

added theorem CategoryTheory.CosimplicialObject.δ_comp_σ_self

added theorem CategoryTheory.CosimplicialObject.δ_comp_σ_succ'

added theorem CategoryTheory.CosimplicialObject.δ_comp_σ_succ

added theorem CategoryTheory.CosimplicialObject.δ_naturality

added def CategoryTheory.CosimplicialObject.σ

added theorem CategoryTheory.CosimplicialObject.σ_comp_σ

added theorem CategoryTheory.CosimplicialObject.σ_naturality

added def CategoryTheory.CosimplicialObject

added def CategoryTheory.SimplicialObject.Augmented.drop

added theorem CategoryTheory.SimplicialObject.Augmented.hom_ext

added def CategoryTheory.SimplicialObject.Augmented.point

added def CategoryTheory.SimplicialObject.Augmented.rightOp

added def CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso

added def CategoryTheory.SimplicialObject.Augmented.toArrow

added def CategoryTheory.SimplicialObject.Augmented.whiskering

added def CategoryTheory.SimplicialObject.Augmented.whiskeringObj

added theorem CategoryTheory.SimplicialObject.Augmented.w₀

added def CategoryTheory.SimplicialObject.Augmented

added def CategoryTheory.SimplicialObject.Truncated.whiskering

added def CategoryTheory.SimplicialObject.Truncated

added def CategoryTheory.SimplicialObject.augment

added theorem CategoryTheory.SimplicialObject.augment_hom_zero

added def CategoryTheory.SimplicialObject.eqToIso

added theorem CategoryTheory.SimplicialObject.eqToIso_refl

added theorem CategoryTheory.SimplicialObject.hom_ext

added def CategoryTheory.SimplicialObject.sk

added def CategoryTheory.SimplicialObject.whiskering

added def CategoryTheory.SimplicialObject.δ

added theorem CategoryTheory.SimplicialObject.δ_comp_δ''

added theorem CategoryTheory.SimplicialObject.δ_comp_δ'

added theorem CategoryTheory.SimplicialObject.δ_comp_δ

added theorem CategoryTheory.SimplicialObject.δ_comp_δ_self'

added theorem CategoryTheory.SimplicialObject.δ_comp_δ_self

added theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_gt'

added theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_gt

added theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_le

added theorem CategoryTheory.SimplicialObject.δ_comp_σ_self'

added theorem CategoryTheory.SimplicialObject.δ_comp_σ_self

added theorem CategoryTheory.SimplicialObject.δ_comp_σ_succ'

added theorem CategoryTheory.SimplicialObject.δ_comp_σ_succ

added theorem CategoryTheory.SimplicialObject.δ_naturality

added def CategoryTheory.SimplicialObject.σ

added theorem CategoryTheory.SimplicialObject.σ_comp_σ

added theorem CategoryTheory.SimplicialObject.σ_naturality

added def CategoryTheory.SimplicialObject

added def CategoryTheory.cosimplicialSimplicialEquiv

added def CategoryTheory.cosimplicialToSimplicialAugmented

added def CategoryTheory.simplicialCosimplicialAugmentedEquiv

added def CategoryTheory.simplicialCosimplicialEquiv

added def CategoryTheory.simplicialToCosimplicialAugmented