NYLL
Module

SubmoduleAdjoinRestriction.lean

Nyll.SchemeTheory.RingTheory.SubmoduleAdjoinRestriction
5 declarations indexed from sourceView source ↗

Module documentation

Generated algebras under an actual localized submodule restriction

The lower submodule is given by the actual restriction map, as with sections of a quasicoherent subsheaf. Its identification with the native localized submodule follows from denominators of its own sections. The previous generated-algebra localization theorem then applies to the literal algebra restriction. No submodule-comparison premise is added.

Imports4
Imported by2

Declarations

theorem

localized'_eq_of_isLocalizedModule_restrict

L39 ↗
Submodule.localized'_eq_of_isLocalizedModule_restrict
Documentation

If the actual restriction between the two submodules is a localization, the target is precisely the native localized submodule of the ambient ring.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w z
namespace Submodule
variable {R : Type u} [CommRing R]
variable (R' : Type v) [CommRing R'] [Algebra R R']
variable {B : Type w} [CommRing B] [Algebra R B]
variable {B' : Type z} [CommRing B'] [Algebra R B'] [Algebra R' B']
variable [IsScalarTower R R' B']
variable (S : Submonoid R) [IsLocalization S R']
variable (f : B →ₐ[R] B') [IsLocalizedModule S f.toLinearMap]
variable (N : Submodule R B) (N' : Submodule R' B')
Lean source · statement
theorem localized'_eq_of_isLocalizedModule_restrict (hf : ∀ x ∈ N, f x ∈ N')
    [IsLocalizedModule S
      (f.toLinearMap.restrict (p := N) (q := N'.restrictScalars R) hf)] :
    N.localized' R' S f.toLinearMap = N'
theorem

adjoinRestrictionTo_mapsTo

L59 ↗
Submodule.adjoinRestrictionTo_mapsTo
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w z
namespace Submodule
variable {R : Type u} [CommRing R]
variable (R' : Type v) [CommRing R'] [Algebra R R']
variable {B : Type w} [CommRing B] [Algebra R B]
variable {B' : Type z} [CommRing B'] [Algebra R B'] [Algebra R' B']
variable [IsScalarTower R R' B']
variable (S : Submonoid R) [IsLocalization S R']
variable (f : B →ₐ[R] B') [IsLocalizedModule S f.toLinearMap]
variable (N : Submodule R B) (N' : Submodule R' B')
Lean source · statement
theorem adjoinRestrictionTo_mapsTo (hf : ∀ x ∈ N, f x ∈ N') :
    ∀ x ∈ Algebra.adjoin R (N : Set B), f x ∈ Algebra.adjoin R' (N' : Set B')
def

adjoinRestrictionTo

L68 ↗
Submodule.adjoinRestrictionTo
Documentation

The literal ambient algebra restriction on the generated algebras.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w z
namespace Submodule
variable {R : Type u} [CommRing R]
variable (R' : Type v) [CommRing R'] [Algebra R R']
variable {B : Type w} [CommRing B] [Algebra R B]
variable {B' : Type z} [CommRing B'] [Algebra R B'] [Algebra R' B']
variable [IsScalarTower R R' B']
variable (S : Submonoid R) [IsLocalization S R']
variable (f : B →ₐ[R] B') [IsLocalizedModule S f.toLinearMap]
variable (N : Submodule R B) (N' : Submodule R' B')
Lean source · statement
def adjoinRestrictionTo (hf : ∀ x ∈ N, f x ∈ N') :
    Algebra.adjoin R (N : Set B) →ₐ[R] Algebra.adjoin R' (N' : Set B')
theorem

isLocalizedModule_adjoinRestrictionTo

L76 ↗
Submodule.isLocalizedModule_adjoinRestrictionTo
Documentation

The actual restriction on generated algebras localizes their modules when the ambient restriction and the original submodule restriction do.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w z
namespace Submodule
variable {R : Type u} [CommRing R]
variable (R' : Type v) [CommRing R'] [Algebra R R']
variable {B : Type w} [CommRing B] [Algebra R B]
variable {B' : Type z} [CommRing B'] [Algebra R B'] [Algebra R' B']
variable [IsScalarTower R R' B']
variable (S : Submonoid R) [IsLocalization S R']
variable (f : B →ₐ[R] B') [IsLocalizedModule S f.toLinearMap]
variable (N : Submodule R B) (N' : Submodule R' B')
Lean source · statement
theorem isLocalizedModule_adjoinRestrictionTo (hf : ∀ x ∈ N, f x ∈ N')
    [IsLocalizedModule S
      (f.toLinearMap.restrict (p := N) (q := N'.restrictScalars R) hf)] :
    IsLocalizedModule S (adjoinRestrictionTo R' f N N' hf).toLinearMap
theorem

isLocalizationAway_adjoinRestrictionTo

L87 ↗
Submodule.isLocalizationAway_adjoinRestrictionTo
Documentation

Over a principal localization, the actual generated-algebra ring map is a principal localization at the same structure coefficient.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w z
namespace Submodule
variable {R : Type u} [CommRing R]
variable (R' : Type v) [CommRing R'] [Algebra R R']
variable {B : Type w} [CommRing B] [Algebra R B]
variable {B' : Type z} [CommRing B'] [Algebra R B'] [Algebra R' B']
variable [IsScalarTower R R' B']
variable (S : Submonoid R) [IsLocalization S R']
variable (f : B →ₐ[R] B') [IsLocalizedModule S f.toLinearMap]
variable (N : Submodule R B) (N' : Submodule R' B')
Lean source · full declaration
theorem isLocalizationAway_adjoinRestrictionTo (hf : ∀ x ∈ N, f x ∈ N') (r : R)
    [IsLocalization.Away r R'] [IsLocalizedModule.Away r f.toLinearMap]
    [IsLocalizedModule.Away r
      (f.toLinearMap.restrict (p := N) (q := N'.restrictScalars R) hf)] :
    let g := adjoinRestrictionTo R' f N N' hf
    let : Algebra (Algebra.adjoin R (N : Set B)) (Algebra.adjoin R' (N' : Set B')) :=
      g.toRingHom.toAlgebra
    IsLocalization.Away (algebraMap R (Algebra.adjoin R (N : Set B)) r)
      (Algebra.adjoin R' (N' : Set B')) := by
  intro g algebra
  have hloc : IsLocalizedModule.Away r g.toLinearMap :=
    isLocalizedModule_adjoinRestrictionTo R' (Submonoid.powers r) f N N' hf
  have htower : IsScalarTower R (Algebra.adjoin R (N : Set B))
      (Algebra.adjoin R' (N' : Set B')) := IsScalarTower.of_algHom g
  have h : IsLocalization
      (Algebra.algebraMapSubmonoid (Algebra.adjoin R (N : Set B)) (Submonoid.powers r))
      (Algebra.adjoin R' (N' : Set B')) :=
    isLocalizedModule_iff_isLocalization.mp hloc
  simpa only [Algebra.algebraMapSubmonoid, Submonoid.map_powers] using h

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.