Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-19 18:28 5797ef5c

View on Github →

feat(algebraic_topology): alternating_coface_map_complex (#14588) This PR constructs the alternating coface map complex of a cosimplicial object in an additive category. This construction is dual to the alternating face map complex.

Estimated changes

Modified src/algebraic_topology/alternating_face_map_complex.lean

added theorem algebraic_topology.alternating_coface_map_complex.d_eq_unop_d

added theorem algebraic_topology.alternating_coface_map_complex.d_squared

added def algebraic_topology.alternating_coface_map_complex.map

added def algebraic_topology.alternating_coface_map_complex.obj

added def algebraic_topology.alternating_coface_map_complex.obj_d

added def algebraic_topology.alternating_coface_map_complex

Modified src/algebraic_topology/simplicial_object.lean

added def category_theory.cosimplicial_simplicial_equiv

Modified src/category_theory/preadditive/opposite.lean

added def category_theory.op_hom

added theorem category_theory.op_neg

added theorem category_theory.op_sum

added theorem category_theory.op_zsmul

added def category_theory.unop_hom

added theorem category_theory.unop_neg

added theorem category_theory.unop_sum

added theorem category_theory.unop_zsmul