Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-26 18:15 598722a2

View on Github →

feat(algebraic_topology/simplicial_object): Add augment construction (#8085) Adds the augmentation construction for (co)simplicial objects. From LTE.

Estimated changes

Modified src/algebraic_topology/simplex_category.lean

added theorem simplex_category.hom_zero_zero

Modified src/algebraic_topology/simplicial_object.lean

added def category_theory.cosimplicial_object.augment

added theorem category_theory.cosimplicial_object.augment_hom_zero

added def category_theory.simplicial_object.augment

added theorem category_theory.simplicial_object.augment_hom_zero