Commit 2024-10-29 13:01 8631a653

View on Github →

feat(RingTheory/*): prerequisites to the locality of projectivity (#18264) Partially written at the AIM algebraic geometry workshop

Estimated changes

Modified Mathlib/Algebra/Module/FinitePresentation.lean

deleted theorem Module.FinitePresentation.isLocalizedModule_map

Modified Mathlib/Algebra/Module/LocalizedModule.lean

added theorem IsLocalizedModule.map_comp'

added theorem IsLocalizedModule.map_id

added theorem IsLocalizedModule.map_injective

added theorem IsLocalizedModule.map_surjective

Modified Mathlib/Algebra/Module/Projective.lean

added theorem Module.Projective.of_ringEquiv

Modified Mathlib/Algebra/Module/Submodule/Localization.lean

added theorem Submodule.localized'_bot

added theorem Submodule.localized'_span

added theorem Submodule.localized'_top

Modified Mathlib/RingTheory/Localization/Module.lean

added def IsLocalizedModule.mapExtendScalars

added def LinearMap.extendScalarsOfIsLocalizationEquiv

added def LocalizedModule.map

added theorem LocalizedModule.map_id

added theorem LocalizedModule.map_injective

added theorem LocalizedModule.map_mk

added theorem LocalizedModule.map_surjective