Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-10 06:31 66db1ad2

View on Github →

refactor(algebra/homology): handle co/homology uniformly (#3316) A refactor of algebra/homology so homology and cohomology are handled uniformly, and factor out a file image_to_kernel_map.lean which gains some extra lemmas (which will be useful for talking about exact sequences).

Estimated changes

Modified src/algebra/homology/chain_complex.lean

deleted theorem chain_complex.comm

deleted theorem chain_complex.comm_at

deleted theorem chain_complex.d_squared

deleted def chain_complex.forget

deleted theorem cochain_complex.comm

deleted theorem cochain_complex.comm_at

deleted theorem cochain_complex.d_squared

deleted def cochain_complex.forget

added theorem homological_complex.comm

added theorem homological_complex.comm_at

added theorem homological_complex.d_squared

added def homological_complex.forget

added def homological_complex

Modified src/algebra/homology/homology.lean

modified def cochain_complex.cohomology

deleted def cochain_complex.cohomology_functor

added def cochain_complex.cohomology_group

modified def cochain_complex.cohomology_map

deleted theorem cochain_complex.cohomology_map_comp

deleted theorem cochain_complex.cohomology_map_condition

deleted theorem cochain_complex.cohomology_map_id

added def cochain_complex.graded_cohomology

deleted def cochain_complex.image_map

deleted theorem cochain_complex.image_map_ι

deleted def cochain_complex.image_to_kernel_map

deleted theorem cochain_complex.image_to_kernel_map_condition

deleted theorem cochain_complex.induced_maps_commute

deleted def cochain_complex.kernel_functor

deleted def cochain_complex.kernel_map

deleted theorem cochain_complex.kernel_map_comp

deleted theorem cochain_complex.kernel_map_condition

deleted theorem cochain_complex.kernel_map_id

added def homological_complex.graded_homology

added def homological_complex.homology

added def homological_complex.homology_group

added def homological_complex.homology_map

added theorem homological_complex.homology_map_comp

added theorem homological_complex.homology_map_condition

added theorem homological_complex.homology_map_id

added def homological_complex.image_map

added theorem homological_complex.image_map_ι

added def homological_complex.image_to_kernel_map

added theorem homological_complex.image_to_kernel_map_comp_kernel_map

added theorem homological_complex.image_to_kernel_map_condition

added def homological_complex.kernel_functor

added def homological_complex.kernel_map

added theorem homological_complex.kernel_map_comp

added theorem homological_complex.kernel_map_condition

added theorem homological_complex.kernel_map_id

Created src/algebra/homology/image_to_kernel_map.lean

added def category_theory.image_to_kernel_map

added theorem category_theory.image_to_kernel_map_epi_of_epi_of_zero

added theorem category_theory.image_to_kernel_map_epi_of_zero_of_mono

added theorem category_theory.image_to_kernel_map_zero_left

added theorem category_theory.image_to_kernel_map_zero_right

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