Commit 2023-04-28 11:10 bfb4a245

View on Github →

feat: port CategoryTheory.Preadditive.Projective (#3615)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/CechNerve.lean

Modified Mathlib/CategoryTheory/Adjunction/Evaluation.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Finite.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Products.lean

added theorem CategoryTheory.Limits.Pi.hom_ext

added theorem CategoryTheory.Limits.Sigma.hom_ext

Created Mathlib/CategoryTheory/Preadditive/Projective.lean

added def CategoryTheory.Adjunction.mapProjectivePresentation

added theorem CategoryTheory.Adjunction.map_projective

added theorem CategoryTheory.Adjunction.projective_of_map_projective

added theorem CategoryTheory.Equivalence.enoughProjectives_iff

added def CategoryTheory.Equivalence.projectivePresentationOfMapProjectivePresentation

added def CategoryTheory.Exact.lift

added theorem CategoryTheory.Exact.lift_comp

added def CategoryTheory.Projective.factorThru

added theorem CategoryTheory.Projective.factorThru_comp

added theorem CategoryTheory.Projective.iso_iff

added theorem CategoryTheory.Projective.of_iso

added def CategoryTheory.Projective.over

added theorem CategoryTheory.Projective.projective_iff_preservesEpimorphisms_coyoneda_obj

added def CategoryTheory.Projective.syzygies

added def CategoryTheory.Projective.π

added structure CategoryTheory.ProjectivePresentation