Commit 2021-05-15 21:20 65e76465

View on Github →

feat(algebraic_topology): cosimplicial objects (#7614) Dualize the existing API for simplicial_object to provide cosimplicial_object, and move the contents of LTE's for_mathlib/simplicial/augmented.lean to mathlib.

Estimated changes

Modified src/algebraic_topology/simplicial_object.lean

added def category_theory.cosimplicial_object.augmented.drop

added def category_theory.cosimplicial_object.augmented.point

added def category_theory.cosimplicial_object.augmented

added def category_theory.cosimplicial_object.const

added def category_theory.cosimplicial_object.eq_to_iso

added theorem category_theory.cosimplicial_object.eq_to_iso_refl

added def category_theory.cosimplicial_object.sk

added def category_theory.cosimplicial_object.truncated

added def category_theory.cosimplicial_object.δ

added theorem category_theory.cosimplicial_object.δ_comp_δ

added theorem category_theory.cosimplicial_object.δ_comp_δ_self

added theorem category_theory.cosimplicial_object.δ_comp_σ_of_gt

added theorem category_theory.cosimplicial_object.δ_comp_σ_of_le

added theorem category_theory.cosimplicial_object.δ_comp_σ_self

added theorem category_theory.cosimplicial_object.δ_comp_σ_succ

added def category_theory.cosimplicial_object.σ

added theorem category_theory.cosimplicial_object.σ_comp_σ

added def category_theory.cosimplicial_object

added def category_theory.simplicial_object.augmented.drop

added def category_theory.simplicial_object.augmented.point