Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-15 08:16 b4b38da8

View on Github →

feat(category_theory/*/projective): refactor treatment of projective objects (#7485)

Estimated changes

Modified src/algebra/homology/exact.lean

Modified src/algebra/homology/homological_complex.lean

Modified src/algebra/homology/image_to_kernel.lean

Modified src/category_theory/abelian/non_preadditive.lean

Modified src/category_theory/abelian/projective.lean

added theorem category_theory.exact_d_f

deleted def category_theory.projective.d

deleted theorem category_theory.projective.exact_d_f

deleted def category_theory.projective.factor_thru

deleted theorem category_theory.projective.factor_thru_comp

deleted theorem category_theory.projective.iso_iff

deleted def category_theory.projective.left

deleted theorem category_theory.projective.of_iso

deleted def category_theory.projective.over

deleted def category_theory.projective.π

deleted structure category_theory.projective_presentation

Modified src/category_theory/closed/zero.lean

Modified src/category_theory/differential_object.lean

Modified src/category_theory/graded_object.lean

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

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

Modified src/category_theory/preadditive/additive_functor.lean

Modified src/category_theory/preadditive/default.lean

Created src/category_theory/preadditive/projective.lean

added def category_theory.exact.lift

added theorem category_theory.exact.lift_comp

added def category_theory.projective.d

added def category_theory.projective.factor_thru

added theorem category_theory.projective.factor_thru_comp

added theorem category_theory.projective.iso_iff

added theorem category_theory.projective.of_iso

added def category_theory.projective.over

added def category_theory.projective.syzygies

added def category_theory.projective.π

added structure category_theory.projective_presentation

Modified src/category_theory/simple.lean

Modified src/category_theory/subobject/lattice.lean

Modified src/category_theory/triangulated/basic.lean