Commit 2021-06-01 05:20 31ba155f

View on Github →

feat(algebraic_topology/cech_nerve): The Cech nerve is a right adjoint. (#7716) Also fixes the namespace in the file algebraic_topology/cech_nerve.lean. This is needed for LTE

Estimated changes

Modified src/algebraic_topology/cech_nerve.lean

added def category_theory.arrow.augmented_cech_conerve

added def category_theory.arrow.cech_conerve

added def category_theory.cosimplicial_object.augmented_cech_conerve

added def category_theory.cosimplicial_object.cech_conerve

added def category_theory.cosimplicial_object.cech_conerve_adjunction

added def category_theory.cosimplicial_object.cech_conerve_equiv

added def category_theory.cosimplicial_object.equivalence_left_to_right

added def category_theory.cosimplicial_object.equivalence_right_to_left

added def category_theory.simplicial_object.augmented_cech_nerve

added def category_theory.simplicial_object.cech_nerve

added def category_theory.simplicial_object.cech_nerve_adjunction

added def category_theory.simplicial_object.cech_nerve_equiv

added def category_theory.simplicial_object.equivalence_left_to_right

added def category_theory.simplicial_object.equivalence_right_to_left

deleted def simplicial_object.augmented_cech_nerve

deleted def simplicial_object.cech_nerve

Modified src/algebraic_topology/simplex_category.lean

added def simplex_category.const

added theorem simplex_category.const_comp

Modified src/algebraic_topology/simplicial_object.lean

added def category_theory.cosimplicial_object.augmented.to_arrow

added def category_theory.simplicial_object.augmented.to_arrow