Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-21 17:19 618ea3d5

View on Github →

feat(representation_theory/group_cohomology_resolution): add exactness properties of resolution (#17005)

Estimated changes

Modified src/algebra/homology/homology.lean

added def chain_complex.homology_succ_iso

added def chain_complex.homology_zero_iso

added def cochain_complex.homology_succ_iso

added def cochain_complex.homology_zero_iso

added def homological_complex.homology_iso

Modified src/algebra/homology/homotopy.lean

added def homotopy_equiv.of_iso

Modified src/algebra/homology/image_to_kernel.lean

added def homology_of_zero_left

added def homology_of_zero_right

Modified src/algebraic_topology/cech_nerve.lean

added def category_theory.cech_nerve_terminal_from.iso

added def category_theory.cech_nerve_terminal_from.wide_cospan.limit_cone

added def category_theory.cech_nerve_terminal_from.wide_cospan

added def category_theory.cech_nerve_terminal_from

Modified src/category_theory/limits/shapes/types.lean

modified theorem category_theory.limits.types.product_iso_hom_comp_eval

modified theorem category_theory.limits.types.product_iso_inv_comp_π

modified def category_theory.limits.types.product_limit_cone

Modified src/representation_theory/group_cohomology_resolution.lean

deleted def classifying_space_universal_cover.cech_nerve_iso

deleted def classifying_space_universal_cover.cech_nerve_obj_iso

added def classifying_space_universal_cover.cech_nerve_terminal_from_iso

added def classifying_space_universal_cover.cech_nerve_terminal_from_iso_comp_forget

added def classifying_space_universal_cover.comp_forget_augmented.to_Module

added def classifying_space_universal_cover.comp_forget_augmented

added def classifying_space_universal_cover.extra_degeneracy_augmented_cech_nerve

added def classifying_space_universal_cover.extra_degeneracy_comp_forget_augmented

added def classifying_space_universal_cover.extra_degeneracy_comp_forget_augmented_to_Module

deleted def classifying_space_universal_cover.wide_cospan.limit_cone

deleted def classifying_space_universal_cover.wide_cospan

added def group_cohomology.resolution.comp_forget_augmented_iso

modified def group_cohomology.resolution.d

added theorem group_cohomology.resolution.d_comp_ε

modified theorem group_cohomology.resolution.d_of

added theorem group_cohomology.resolution.exact_at_succ

added theorem group_cohomology.resolution.exact₀

added theorem group_cohomology.resolution.forget_to_Module_exact₀

added def group_cohomology.resolution.forget₂_to_Module

added theorem group_cohomology.resolution.forget₂_to_Module_exact_succ

added def group_cohomology.resolution.forget₂_to_Module_homotopy_equiv

added theorem group_cohomology.resolution.forget₂_to_Module_homotopy_equiv_f_0_eq

added def group_cohomology.resolution.ε

Modified src/topology/sheaves/sheaf_condition/unique_gluing.lean