Documentation

DerivedAlgGeo.Algebra.Module.LocalizedModule.NestedSubmodule

Submodules under nested principal localizations #

The canonical map from a module localized away from r to its localization away from r * s is constructed using the universal property. No regularity or finiteness assumption on r, s, or the module is needed.

source
noncomputable def LocalizedModule.awayToAwayRightLinearMap {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (r s : R) :
LocalizedModule.Away r M →ₗ[R] LocalizedModule.Away (r * s) M

The canonical R-linear map from localization away from r to localization away from r * s.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem LocalizedModule.awayToAwayRightLinearMap_mk {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (r s : R) (m : M) :
    (awayToAwayRightLinearMap r s) (mk m 1) = mk m 1
    source
    theorem Submodule.localized'_comap_awayToAwayRight_eq_span {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (r s : R) (P : Submodule (Localization.Away r) (LocalizedModule.Away r M)) :
    have fr := LocalizedModule.mkLinearMap (Submonoid.powers r) M; let frs := LocalizedModule.mkLinearMap (Submonoid.powers (r * s)) M; have α := LocalizedModule.awayToAwayRightLinearMap r s; localized' (Localization.Away (r * s)) (Submonoid.powers (r * s)) frs (comap fr (restrictScalars R P)) = span (Localization.Away (r * s)) (⇑α '' ↑P)

    Let P be a submodule of M[1/r], and pull it back to M. Its localization away from r * s is the R[1/(r*s)]-span of the image of P under the canonical map M[1/r] → M[1/(r*s)]. This works even when r or s is a zero divisor.

    source
    theorem Submodule.localized'_awayToAwayRight_eq_span {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (r s : R) (N : Submodule R M) :
    localized' (Localization.Away (r * s)) (Submonoid.powers (r * s)) (LocalizedModule.mkLinearMap (Submonoid.powers (r * s)) M) N = span (Localization.Away (r * s)) (⇑(LocalizedModule.awayToAwayRightLinearMap r s) '' ↑(localized' (Localization.Away r) (Submonoid.powers r) (LocalizedModule.mkLinearMap (Submonoid.powers r) M) N))

    Localizing a chosen submodule first away from r and then mapping to the common localization gives the same R[1/(r*s)]-submodule as localizing it directly away from r * s. The image is spanned in the target ring, not used as a raw set.