Mathlib Changelog
v3
Changelog
About
Github
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