Commit 2021-05-19 01:16 24d2713d

View on Github →

feat(algebraic_topology/simplicial_object): Whiskering of simplicial objects. (#7651) This adds whiskering constructions for (truncated, augmented) (co)simplicial objects.

Estimated changes

Modified src/algebraic_topology/simplicial_object.lean

added def category_theory.cosimplicial_object.augmented.whiskering

added def category_theory.cosimplicial_object.augmented.whiskering_obj

added def category_theory.cosimplicial_object.truncated.whiskering

added def category_theory.cosimplicial_object.whiskering

added def category_theory.simplicial_object.augmented.whiskering

added def category_theory.simplicial_object.augmented.whiskering_obj

added def category_theory.simplicial_object.truncated.whiskering

added def category_theory.simplicial_object.whiskering