Documentation

DerivedAlgGeo.Algebra.Module.LocalizedModule.NestedSubmoduleLeft

The opposite chart of nested principal localization #

The canonical map from M[1/s] to M[1/(r*s)] and the corresponding submodule-span identity. The product is kept in the order r*s, so both chart maps have literally the same target. No regularity or finiteness is required.

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

The canonical R-linear map from localization away from s 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.awayToAwayLeftLinearMap_mk {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (r s : R) (m : M) :
    (awayToAwayLeftLinearMap r s) (mk m 1) = mk m 1
    source
    theorem Submodule.localized'_comap_awayToAwayLeft_eq_span {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (r s : R) (P : Submodule (Localization.Away s) (LocalizedModule.Away s M)) :
    have fs := LocalizedModule.mkLinearMap (Submonoid.powers s) M; let frs := LocalizedModule.mkLinearMap (Submonoid.powers (r * s)) M; have α := LocalizedModule.awayToAwayLeftLinearMap r s; localized' (Localization.Away (r * s)) (Submonoid.powers (r * s)) frs (comap fs (restrictScalars R P)) = span (Localization.Away (r * s)) (⇑α '' ↑P)

    If P is a submodule of M[1/s], localization of its inverse image in M away from r*s is the R[1/(r*s)]-span of its canonical image. This also holds when either factor is a zero divisor or r*s = 0.

    source
    theorem Submodule.localized'_away_mul_eq_span_awayToAwayLeft {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (r s : R) (N : Submodule R M) :
    let fs := LocalizedModule.mkLinearMap (Submonoid.powers s) M; let frs := LocalizedModule.mkLinearMap (Submonoid.powers (r * s)) M; have α := LocalizedModule.awayToAwayLeftLinearMap r s; localized' (Localization.Away (r * s)) (Submonoid.powers (r * s)) frs N = span (Localization.Away (r * s)) (⇑α '' ↑(localized' (Localization.Away s) (Submonoid.powers s) fs N))

    Localizing a chosen submodule N ≤ M away from r*s is the span of the canonical image of its localization away from s. No finiteness or regularity hypothesis is needed.