Commit 2024-11-25 11:04 a151e519

View on Github →

feat(RingTheory/LocalProperties): Add theorems about LocalizedModule (#19080) This PR contains:

A proof that localization commutes with ranges.
Some missing lemmas about localized submodules.
A proof that injective, surjective, bijective (of linear maps) are local properties. These theorems will be used to prove that flat is a local property in a later PR.

Estimated changes

Modified Mathlib.lean

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

modified theorem LinearMap.ker_localizedMap_eq_localized'_ker

added theorem LinearMap.ker_localizedMap_eq_localized₀_ker

modified theorem LinearMap.localized'_ker_eq_ker_localizedMap

added theorem LinearMap.localized'_range_eq_range_localizedMap

added theorem LinearMap.range_localizedMap_eq_localized₀_range

modified theorem LinearMap.toKerLocalized_isLocalizedModule

Modified Mathlib/RingTheory/Ideal/Maximal.lean

added theorem Ideal.exists_disjoint_powers_of_span_eq_top

Created Mathlib/RingTheory/LocalProperties/Exactness.lean

added theorem bijective_of_isLocalized_maximal

added theorem bijective_of_isLocalized_span

added theorem bijective_of_localized_maximal

added theorem bijective_of_localized_span

added theorem exact_of_isLocalized_maximal

added theorem exact_of_isLocalized_span

added theorem exact_of_localized_maximal

added theorem exact_of_localized_span

added theorem injective_of_isLocalized_maximal

added theorem injective_of_isLocalized_span

added theorem injective_of_localized_maximal

added theorem injective_of_localized_span

added theorem surjective_of_isLocalized_maximal

added theorem surjective_of_isLocalized_span

added theorem surjective_of_localized_maximal

added theorem surjective_of_localized_span

Modified Mathlib/RingTheory/LocalProperties/Submodule.lean

added theorem Module.eq_of_isLocalized_span

added theorem Module.eq_zero_of_isLocalized_span

added theorem Submodule.eq_bot_of_isLocalized'_span

added theorem Submodule.eq_bot_of_isLocalized₀_span

added theorem Submodule.eq_of_isLocalized'_span

added theorem Submodule.eq_of_isLocalized₀_span

added theorem Submodule.eq_top_of_isLocalized'_span

added theorem Submodule.eq_top_of_isLocalized₀_span

added theorem Submodule.le_of_isLocalized_span

added theorem Submodule.mem_of_isLocalized_span