Commit 2023-05-09 06:12 5d7b89a8

View on Github →

feat: port CategoryTheory.Preadditive.Injective (#3859)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Preadditive/Injective.lean

added theorem CategoryTheory.Adjunction.injective_of_map_injective

added def CategoryTheory.Adjunction.mapInjectivePresentation

added theorem CategoryTheory.Adjunction.map_injective

added theorem CategoryTheory.Equivalence.enoughInjectives_iff

added def CategoryTheory.Equivalence.injectivePresentationOfMapInjectivePresentation

added theorem CategoryTheory.Injective.Exact.comp_desc

added def CategoryTheory.Injective.Exact.desc

added theorem CategoryTheory.Injective.comp_factorThru

added theorem CategoryTheory.Injective.enoughInjectives_of_enoughProjectives_op

added theorem CategoryTheory.Injective.enoughProjectives_of_enoughInjectives_op

added def CategoryTheory.Injective.factorThru

added theorem CategoryTheory.Injective.injective_iff_preservesEpimorphisms_yoneda_obj

added theorem CategoryTheory.Injective.injective_iff_projective_op

added theorem CategoryTheory.Injective.injective_of_adjoint

added theorem CategoryTheory.Injective.iso_iff

added theorem CategoryTheory.Injective.of_iso

added theorem CategoryTheory.Injective.projective_iff_injective_op

added def CategoryTheory.Injective.syzygies

added def CategoryTheory.Injective.under

added def CategoryTheory.Injective.ι

added structure CategoryTheory.InjectivePresentation