Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-25 08:40 956af7c7

View on Github →

feat(representation_theory/group_cohomology_resolution): add projective resolution (#17443)

Estimated changes

Modified src/algebra/homology/quasi_iso.lean

added theorem category_theory.functor.quasi_iso_of_map_quasi_iso

added theorem homological_complex.hom.from_single₀_exact_at_succ

added theorem homological_complex.hom.from_single₀_exact_f_d_at_zero

added theorem homological_complex.hom.from_single₀_kernel_at_zero_iso_inv_eq

added theorem homological_complex.hom.from_single₀_mono_at_zero

added theorem homological_complex.hom.to_single₀_cokernel_at_zero_iso_hom_eq

added theorem homological_complex.hom.to_single₀_epi_at_zero

added theorem homological_complex.hom.to_single₀_exact_at_succ

added theorem homological_complex.hom.to_single₀_exact_d_f_at_zero

modified theorem homotopy_equiv.to_quasi_iso

added theorem homotopy_equiv.to_quasi_iso_inv

Modified src/algebraic_geometry/open_immersion.lean

Modified src/category_theory/abelian/homology.lean

Modified src/category_theory/abelian/injective_resolution.lean

added def homological_complex.hom.homological_complex.hom.from_single₀_InjectiveResolution

Modified src/category_theory/abelian/projective.lean

added def homological_complex.hom.to_single₀_ProjectiveResolution

Modified src/category_theory/limits/preserves/shapes/kernels.lean

added theorem category_theory.limits.kernel_map_comp_preserves_kernel_iso_inv

added theorem category_theory.limits.preserves_cokernel_iso_comp_cokernel_map

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

added theorem category_theory.limits.cokernel_map_comp_cokernel_comparison

added theorem category_theory.limits.kernel_comparison_comp_kernel_map

Modified src/category_theory/preadditive/injective.lean

added theorem category_theory.adjunction.injective_of_map_injective

added theorem category_theory.adjunction.map_injective

added def category_theory.adjunction.map_injective_presentation

added theorem category_theory.equivalence.enough_injectives_iff

added def category_theory.equivalence.injective_presentation_of_map_injective_presentation

Modified src/category_theory/preadditive/projective.lean

added theorem category_theory.adjunction.map_projective

added def category_theory.adjunction.map_projective_presentation

added theorem category_theory.adjunction.projective_of_map_projective

added theorem category_theory.equivalence.enough_projectives_iff

added def category_theory.equivalence.projective_presentation_of_map_projective_presentation

Modified src/category_theory/subobject/limits.lean

added theorem category_theory.limits.image_map_comp_image_subobject_iso_inv

added theorem category_theory.limits.image_subobject_iso_comp_image_map

added theorem category_theory.limits.kernel_map_comp_kernel_subobject_iso_inv

added theorem category_theory.limits.kernel_subobject_iso_comp_kernel_map

Modified src/representation_theory/group_cohomology_resolution.lean

added def group_cohomology.Ext_iso

added def group_cohomology.ProjectiveResolution

added theorem group_cohomology.resolution.X_projective

deleted theorem group_cohomology.resolution.exact_at_succ

deleted theorem group_cohomology.resolution.exact₀

deleted theorem group_cohomology.resolution.forget_to_Module_exact₀

deleted theorem group_cohomology.resolution.forget₂_to_Module_exact_succ

added theorem group_cohomology.resolution.quasi_iso_of_forget₂_ε_to_single₀

added def group_cohomology.resolution.ε_to_single₀

added theorem group_cohomology.resolution.ε_to_single₀_comp_eq

modified def group_cohomology.resolution