# Localization of Submodules #

Results about localizations of submodules and quotient modules are provided in this file.

## Main results #

- `Submodule.localized`: The localization of an `R`-submodule of `M` at `p` viewed as an `Rₚ`-submodule of `Mₚ`. A direct consequence of this is that `Rₚ` is flat over `R`; see `IsLocalization.flat`.
- `Submodule.toLocalized`: The localization map of a submodule `M' →ₗ[R] M'.localized p`.
- `Submodule.toLocalizedQuotient`: The localization map of a quotient module `M ⧸ M' →ₗ[R] LocalizedModule p M ⧸ M'.localized p`.

## TODO #

- Statements regarding the exactness of localization.

source
def Submodule.localized₀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (p : Submonoid R) (f : M →ₗ[R] N) [IsLocalizedModule p f] (M' : Submodule R M) :
Submodule R N

Let `N` be a localization of an `R`-module `M` at `p`. This is the localization of an `R`-submodule of `M` viewed as an `R`-submodule of `N`.

Equations

- Submodule.localized₀ p f M' = { carrier := {x : N | ∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Instances For

source
def Submodule.localized' {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] (M' : Submodule R M) :
Submodule S N

Let `S` be the localization of `R` at `p` and `N` be a localization of `M` at `p`. This is the localization of an `R`-submodule of `M` viewed as an `S`-submodule of `N`.

Equations

- Submodule.localized' S p f M' = { toAddSubmonoid := (Submodule.localized₀ p f M').toAddSubmonoid, smul_mem' := ⋯ }

Instances For

source
theorem Submodule.mem_localized₀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (p : Submonoid R) (f : M →ₗ[R] N) [IsLocalizedModule p f] (M' : Submodule R M) (x : N) :
x ∈ localized₀ p f M' ↔ ∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x
source
theorem Submodule.mem_localized' {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] (M' : Submodule R M) (x : N) :
x ∈ localized' S p f M' ↔ ∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x
source
theorem Submodule.restrictScalars_localized' {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] (M' : Submodule R M) :
restrictScalars R (localized' S p f M') = localized₀ p f M'

`localized₀` is the same as `localized'` considered as a submodule over the base ring.

source
theorem Submodule.localized'_eq_span {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] (M' : Submodule R M) :
localized' S p f M' = span S (⇑f '' ↑M')
source
def Submodule.localized'gi {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] :
GaloisInsertion (localized' S p f) fun (x : Submodule S N) => comap f (restrictScalars R x)

The Galois insertion between `Submodule R M` and `Submodule S N`, where `S` is the localization of `R` at `p` and `N` is the localization of `M` at `p`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[reducible, inline]
noncomputable abbrev Submodule.localized {R : Type u_1} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (p : Submonoid R) (M' : Submodule R M) :
Submodule (Localization p) (LocalizedModule p M)

The localization of an `R`-submodule of `M` at `p` viewed as an `Rₚ`-submodule of `Mₚ`.

Equations

- Submodule.localized p M' = Submodule.localized' (Localization p) p (LocalizedModule.mkLinearMap p M) M'

Instances For

source
@[simp]
theorem Submodule.localized₀_bot {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (p : Submonoid R) (f : M →ₗ[R] N) [IsLocalizedModule p f] :
localized₀ p f ⊥ = ⊥
source
@[simp]
theorem Submodule.localized'_bot {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] :
localized' S p f ⊥ = ⊥
source
@[simp]
theorem Submodule.localized₀_top {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (p : Submonoid R) (f : M →ₗ[R] N) [IsLocalizedModule p f] :
localized₀ p f ⊤ = ⊤
source
@[simp]
theorem Submodule.localized'_top {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] :
localized' S p f ⊤ = ⊤
source
@[simp]
theorem Submodule.localized'_span {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] (s : Set M) :
localized' S p f (span R s) = span S (⇑f '' s)
source
theorem Submodule.localized₀_smul {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (p : Submonoid R) (f : M →ₗ[R] N) [IsLocalizedModule p f] (M' : Submodule R M) (I : Submodule R R) :
localized₀ p f (I • M') = I • localized₀ p f M'
source
theorem Submodule.restrictScalars_localized'_smul {R : Type u_1} (S : Type u_2) {N : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid N] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (I : Submodule R R) (N' : Submodule S N) :
restrictScalars R (localized' S p (Algebra.linearMap R S) I • N') = I • restrictScalars R N'
source
theorem Submodule.localized'_smul {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] (M' : Submodule R M) (I : Submodule R R) :
localized' S p f (I • M') = localized' S p (Algebra.linearMap R S) I • localized' S p f M'
source
def Submodule.toLocalized₀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (p : Submonoid R) (f : M →ₗ[R] N) [IsLocalizedModule p f] (M' : Submodule R M) :
↥M' →ₗ[R] ↥(localized₀ p f M')

The localization map of a submodule.

Equations

- Submodule.toLocalized₀ p f M' = f.restrict ⋯

Instances For

source
@[simp]
theorem Submodule.toLocalized₀_apply_coe {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (p : Submonoid R) (f : M →ₗ[R] N) [IsLocalizedModule p f] (M' : Submodule R M) (c : ↥M') :
↑((toLocalized₀ p f M') c) = f ↑c
source
def Submodule.toLocalized' {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] (M' : Submodule R M) :
↥M' →ₗ[R] ↥(localized' S p f M')

The localization map of a submodule.

Equations

- Submodule.toLocalized' S p f M' = Submodule.toLocalized₀ p f M'

Instances For

source
@[simp]
theorem Submodule.toLocalized'_apply_coe {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] (M' : Submodule R M) (c : ↥M') :
↑((toLocalized' S p f M') c) = f ↑c
source
@[reducible, inline]
noncomputable abbrev Submodule.toLocalized {R : Type u_1} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (p : Submonoid R) (M' : Submodule R M) :
↥M' →ₗ[R] ↥(localized p M')

The localization map of a submodule.

Equations

- Submodule.toLocalized p M' = Submodule.toLocalized' (Localization p) p (LocalizedModule.mkLinearMap p M) M'

Instances For

source
instance Submodule.instIsLocalizedModuleSubtypeMemLocalized₀ToLocalized₀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (p : Submonoid R) (f : M →ₗ[R] N) [IsLocalizedModule p f] (M' : Submodule R M) :
IsLocalizedModule p (toLocalized₀ p f M')
source
instance Submodule.isLocalizedModule {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] (M' : Submodule R M) :
IsLocalizedModule p (toLocalized' S p f M')
source
noncomputable def Submodule.localizedEquiv {R : Type u_1} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (p : Submonoid R) (M' : Submodule R M) :
↥(localized p M') ≃ₗ[Localization p] LocalizedModule p ↥M'

The canonical isomorphism between the localization of a submodule and its realization as a submodule in the localized module.

Equations

- Submodule.localizedEquiv p M' = LinearEquiv.restrictScalars (Localization p) (IsLocalizedModule.linearEquiv p (Submodule.toLocalized p M') (LocalizedModule.mkLinearMap p ↥M'))

Instances For

source
theorem Submodule.localized₀_le_localized₀_of_smul_le {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (p : Submonoid R) (f : M →ₗ[R] N) [IsLocalizedModule p f] {P Q : Submodule R M} (x : ↥p) (h : x • P ≤ Q) :
localized₀ p f P ≤ localized₀ p f Q
source
theorem Submodule.localized'_le_localized'_of_smul_le {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] {P Q : Submodule R M} (x : ↥p) (h : x • P ≤ Q) :
localized' S p f P ≤ localized' S p f Q
source
def Submodule.toLocalizedQuotient' {R : Type u_5} (S : Type u_6) {M : Type u_7} {N : Type u_8} [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] (M' : Submodule R M) :
M ⧸ M' →ₗ[R] N ⧸ localized' S p f M'

The localization map of a quotient module.

Equations

- Submodule.toLocalizedQuotient' S p f M' = M'.mapQ (Submodule.restrictScalars R (Submodule.localized' S p f M')) f ⋯

Instances For

source
@[reducible, inline]
noncomputable abbrev Submodule.toLocalizedQuotient {R : Type u_5} {M : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] (p : Submonoid R) (M' : Submodule R M) :
M ⧸ M' →ₗ[R] LocalizedModule p M ⧸ localized p M'

The localization map of a quotient module.

Equations

- Submodule.toLocalizedQuotient p M' = Submodule.toLocalizedQuotient' (Localization p) p (LocalizedModule.mkLinearMap p M) M'

Instances For

source
@[simp]
theorem Submodule.toLocalizedQuotient'_mk {R : Type u_5} (S : Type u_6) {M : Type u_7} {N : Type u_8} [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] (M' : Submodule R M) (x : M) :
(toLocalizedQuotient' S p f M') (Quotient.mk x) = Quotient.mk (f x)
source
instance IsLocalizedModule.toLocalizedQuotient' {R : Type u_5} (S : Type u_6) {M : Type u_7} {N : Type u_8} [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] (M' : Submodule R M) :
IsLocalizedModule p (Submodule.toLocalizedQuotient' S p f M')
source
instance instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient {R : Type u_5} {M : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] (p : Submonoid R) (M' : Submodule R M) :
IsLocalizedModule p (Submodule.toLocalizedQuotient p M')
source
noncomputable def localizedQuotientEquiv {R : Type u_5} {M : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] (p : Submonoid R) (M' : Submodule R M) :
(LocalizedModule p M ⧸ Submodule.localized p M') ≃ₗ[Localization p] LocalizedModule p (M ⧸ M')

The canonical isomorphism between the localization of a quotient module and its realization as a quotient of the localized module.

Equations

- localizedQuotientEquiv p M' = LinearEquiv.restrictScalars (Localization p) (IsLocalizedModule.linearEquiv p (Submodule.toLocalizedQuotient p M') (LocalizedModule.mkLinearMap p (M ⧸ M')))

Instances For

source
theorem LinearMap.ker_localizedMap_eq_localized₀_ker {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (p : Submonoid R) (f : M →ₗ[R] N) [IsLocalizedModule p f] {P : Type u_5} [AddCommMonoid P] [Module R P] {Q : Type u_6} [AddCommMonoid Q] [Module R Q] (f' : P →ₗ[R] Q) [IsLocalizedModule p f'] (g : M →ₗ[R] P) :
ker ((IsLocalizedModule.map p f f') g) = Submodule.localized₀ p f (ker g)
source
theorem LinearMap.localized'_ker_eq_ker_localizedMap {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] {P : Type u_5} [AddCommMonoid P] [Module R P] {Q : Type u_6} [AddCommMonoid Q] [Module R Q] [Module S Q] [IsScalarTower R S Q] (f' : P →ₗ[R] Q) [IsLocalizedModule p f'] (g : M →ₗ[R] P) :
Submodule.localized' S p f (ker g) = ker (extendScalarsOfIsLocalization p S ((IsLocalizedModule.map p f f') g))
source
theorem LinearMap.ker_localizedMap_eq_localized'_ker {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] {P : Type u_5} [AddCommMonoid P] [Module R P] {Q : Type u_6} [AddCommMonoid Q] [Module R Q] [Module S Q] [IsScalarTower R S Q] (f' : P →ₗ[R] Q) [IsLocalizedModule p f'] (g : M →ₗ[R] P) :
ker ((IsLocalizedModule.map p f f') g) = Submodule.restrictScalars R (Submodule.localized' S p f (ker g))
source
noncomputable def LinearMap.toKerIsLocalized {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (p : Submonoid R) (f : M →ₗ[R] N) [IsLocalizedModule p f] {P : Type u_5} [AddCommMonoid P] [Module R P] {Q : Type u_6} [AddCommMonoid Q] [Module R Q] (f' : P →ₗ[R] Q) [IsLocalizedModule p f'] (g : M →ₗ[R] P) :
↥(ker g) →ₗ[R] ↥(ker ((IsLocalizedModule.map p f f') g))

The canonical map from the kernel of `g` to the kernel of `g` localized at a submonoid.

This is a localization map by `LinearMap.toKerLocalized_isLocalizedModule`.

Equations

- LinearMap.toKerIsLocalized p f f' g = f.restrict ⋯

Instances For

source
@[simp]
theorem LinearMap.toKerIsLocalized_apply_coe {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (p : Submonoid R) (f : M →ₗ[R] N) [IsLocalizedModule p f] {P : Type u_5} [AddCommMonoid P] [Module R P] {Q : Type u_6} [AddCommMonoid Q] [Module R Q] (f' : P →ₗ[R] Q) [IsLocalizedModule p f'] (g : M →ₗ[R] P) (c : ↥(ker g)) :
↑((toKerIsLocalized p f f' g) c) = f ↑c
source
theorem LinearMap.toKerLocalized_isLocalizedModule {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] {P : Type u_5} [AddCommMonoid P] [Module R P] {Q : Type u_6} [AddCommMonoid Q] [Module R Q] [Module S Q] [IsScalarTower R S Q] (f' : P →ₗ[R] Q) [IsLocalizedModule p f'] (g : M →ₗ[R] P) :
IsLocalizedModule p (toKerIsLocalized p f f' g)

The canonical map to the kernel of the localization of `g` is localizing. In other words, localization commutes with kernels.

source
theorem LinearMap.range_localizedMap_eq_localized₀_range {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (p : Submonoid R) (f : M →ₗ[R] N) [IsLocalizedModule p f] {P : Type u_5} [AddCommMonoid P] [Module R P] {Q : Type u_6} [AddCommMonoid Q] [Module R Q] (f' : P →ₗ[R] Q) [IsLocalizedModule p f'] (g : M →ₗ[R] P) :
range ((IsLocalizedModule.map p f f') g) = Submodule.localized₀ p f' (range g)
source
theorem LinearMap.localized'_range_eq_range_localizedMap {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] {P : Type u_5} [AddCommMonoid P] [Module R P] {Q : Type u_6} [AddCommMonoid Q] [Module R Q] [Module S Q] [IsScalarTower R S Q] (f' : P →ₗ[R] Q) [IsLocalizedModule p f'] (g : M →ₗ[R] P) :
Submodule.localized' S p f' (range g) = range (extendScalarsOfIsLocalization p S ((IsLocalizedModule.map p f f') g))

Localization commutes with ranges.