Localization of Submodules

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

Main result

• Submodule.localized: The localization of an R-submodule of M at p viewed as an Rₚ-submodule of Mₚ.
• 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.
• Connection with flatness.

def Submodule.localized' {R : Type u} (S : Type u') {M : Type v} {N : Type v'} [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) : Submodule S N

Let S be the localization of R at p and N be the 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' = { carrier := {x : N | ∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[reducible, inline]

abbrev Submodule.localized {R : Type u} {M : Type v} [CommRing R] [AddCommGroup 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'

@[simp]

theorem Submodule.toLocalized'_apply_coe {R : Type u} (S : Type u') {M : Type v} {N : Type v'} [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) (c : ↥M') : ↑((Submodule.toLocalized' S p f M') c) = f ↑c

def Submodule.toLocalized' {R : Type u} (S : Type u') {M : Type v} {N : Type v'} [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' →ₗ[R] ↥(Submodule.localized' S p f M')

The localization map of a submodule.

Equations

• Submodule.toLocalized' S p f M' = f.restrict ⋯

@[reducible, inline]

abbrev Submodule.toLocalized {R : Type u} {M : Type v} [CommRing R] [AddCommGroup 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'

instance Submodule.isLocalizedModule {R : Type u} (S : Type u') {M : Type v} {N : Type v'} [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.toLocalized' S p f M')

Equations

• ⋯ = ⋯

def Submodule.toLocalizedQuotient' {R : Type u} (S : Type u') {M : Type v} {N : Type v'} [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 ⋯

@[reducible, inline]

abbrev Submodule.toLocalizedQuotient {R : Type u} {M : Type v} [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'

@[simp]

theorem Submodule.toLocalizedQuotient'_mk {R : Type u} (S : Type u') {M : Type v} {N : Type v'} [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)

instance IsLocalizedModule.toLocalizedQuotient' {R : Type u} (S : Type u') {M : Type v} {N : Type v'} [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

• ⋯ = ⋯

instance instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (p : Submonoid R) (M' : Submodule R M) : IsLocalizedModule p (Submodule.toLocalizedQuotient p M')

Equations

• ⋯ = ⋯