Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-07 19:50 34ae62ad

View on Github →

feat(algebra/homology): functoriality of induced maps on cycles (#2338)

feat(algebra/homology): Functoriality of induced maps on cycles
Rename cycles to cocycles, induced_maps_on_cocycles_functor to kernels_functor
update names

Estimated changes

Modified src/algebra/homology/homology.lean

deleted def cochain_complex.induced_map_on_cycles

added def cochain_complex.kernel_functor

added def cochain_complex.kernel_map

added theorem cochain_complex.kernel_map_comp

added theorem cochain_complex.kernel_map_condition

added theorem cochain_complex.kernel_map_id

Modified src/category_theory/differential_object.lean

added theorem category_theory.differential_object.zero_f

Modified src/category_theory/graded_object.lean

added theorem category_theory.graded_object.zero_apply