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.

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 ∈ Submodule.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 ∈ Submodule.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) :

Submodule.restrictScalars R (Submodule.localized' S p f M') = Submodule.localized₀ p f M'

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

source

@[reducible, inline]

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] :

Submodule.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] :

Submodule.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] :

Submodule.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] :

Submodule.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) :

Submodule.localized' S p f (Submodule.span R s) = Submodule.span S (⇑f '' s)

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] ↥(Submodule.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') :

↑((Submodule.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] ↥(Submodule.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') :

↑((Submodule.toLocalized' S p f M') c) = f ↑c

source

@[reducible, inline]

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] ↥(Submodule.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 (Submodule.toLocalized₀ p f M')

Equations

⋯ = ⋯

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 (Submodule.toLocalized' S p f M')

Equations

⋯ = ⋯

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 ⧸ Submodule.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]

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 ⧸ Submodule.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) :

(Submodule.toLocalizedQuotient' S p f M') (Submodule.Quotient.mk x) = Submodule.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')

Equations

⋯ = ⋯

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')

Equations

⋯ = ⋯

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) :

LinearMap.ker ((IsLocalizedModule.map p f f') g) = Submodule.localized₀ p f (LinearMap.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 (LinearMap.ker g) = LinearMap.ker (LinearMap.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) :

LinearMap.ker ((IsLocalizedModule.map p f f') g) = Submodule.restrictScalars R (Submodule.localized' S p f (LinearMap.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) :

↥(LinearMap.ker g) →ₗ[R] ↥(LinearMap.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 : ↥(LinearMap.ker g)) :

↑((LinearMap.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 (LinearMap.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) :

LinearMap.range ((IsLocalizedModule.map p f f') g) = Submodule.localized₀ p f' (LinearMap.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' (LinearMap.range g) = LinearMap.range (LinearMap.extendScalarsOfIsLocalization p S ((IsLocalizedModule.map p f f') g))

Localization commutes with ranges.

HepLean Documentation

Mathlib.Algebra.Module.LocalizedModule.Submodule

Localization of Submodules #

Main results #

TODO #