Commit 2024-11-04 12:17 bb6a6f96

View on Github →

feat(RingTheory/LocalProperties): being projective can be checked locally on stalks (#18131) ... for finitely presented modules Written at the AIM algebraic geometry workshop

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/FinitePresentation.lean

Created Mathlib/RingTheory/LocalProperties/Projective.lean

added theorem LinearMap.split_surjective_of_localization_maximal

added theorem Module.projective_of_isLocalizedModule

added theorem Module.projective_of_localization_maximal'

added theorem Module.projective_of_localization_maximal

Created Mathlib/RingTheory/LocalProperties/Submodule.lean

added theorem Module.eq_of_localization_maximal

added theorem Module.eq_zero_of_localization_maximal

added theorem Module.subsingleton_of_localization_maximal

added theorem Submodule.eq_bot_of_localization_maximal

added theorem Submodule.eq_of_localization_maximal

added theorem Submodule.le_of_localization_maximal

added theorem Submodule.mem_of_localization_maximal