Module

SubmoduleAdjoinLocalization.lean

Nyll.SchemeTheory.RingTheory.SubmoduleAdjoinLocalization

7 declarations indexed from sourceView source ↗

Module documentation

Localization of algebras generated by submodules

The algebra generated by a submodule commutes with actual localization. The comparison is proved inside the given localized ambient algebra, and the actual restriction of its algebra map is a localization of modules. An integral ambient algebra makes the algebra generated by a finite submodule module-finite.

These are algebra-side suppliers for constructing compatible finite subalgebras on affine charts. No quasicoherent subsheaf extension, global finite model, or finite refinement of a nonaffine scheme is asserted here.

Imports5

Mathlib.Algebra.Algebra.Subalgebra.Lattice
Mathlib.Algebra.Module.LocalizedModule.Submodule
Mathlib.RingTheory.Adjoin.Basic
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Imported by3

theorem

localized'_adjoin

L45 ↗

Submodule.localized'_adjoin

Documentation

Localizing the module underlying the generated algebra gives exactly the algebra generated by the localized submodule in the actual target.

Source context 11 commands

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

noncomputable section
universe u v w z
namespace Submodule
section Localization
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]

Lean source · statement

theorem localized'_adjoin (N : Submodule R B) :
    (Algebra.adjoin R (N : Set B)).toSubmodule.localized' R' S f.toLinearMap =
      (Algebra.adjoin R' (N.localized' R' S f.toLinearMap : Set B')).toSubmodule

theorem

adjoinRestriction_mapsTo

L67 ↗

Submodule.adjoinRestriction_mapsTo

Source context 11 commands

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

noncomputable section
universe u v w z
namespace Submodule
section Localization
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]

Lean source · statement

theorem adjoinRestriction_mapsTo (N : Submodule R B) :
    ∀ x ∈ Algebra.adjoin R (N : Set B),
      f x ∈ Algebra.adjoin R' (N.localized' R' S f.toLinearMap : Set B')

def

adjoinRestriction

L79 ↗

Submodule.adjoinRestriction

Documentation

The actual ambient algebra map restricted to the algebras generated by the original submodule and its localization.

Source context 11 commands

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

noncomputable section
universe u v w z
namespace Submodule
section Localization
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]

Lean source · statement

def adjoinRestriction (N : Submodule R B) :
    Algebra.adjoin R (N : Set B) →ₐ[R]
      Algebra.adjoin R' (N.localized' R' S f.toLinearMap : Set B')

theorem

adjoinRestriction_apply

L87 ↗

Submodule.adjoinRestriction_apply

Documentation

The restricted map evaluates to the original ambient map.

Source context 11 commands

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

noncomputable section
universe u v w z
namespace Submodule
section Localization
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]

Lean source · statement

theorem adjoinRestriction_apply (N : Submodule R B)
    (x : Algebra.adjoin R (N : Set B)) :
    (adjoinRestriction R' S f N x : B') = f (x : B)

theorem

isLocalizedModule_restrict_of_localized₀_eq

L92 ↗

Submodule.isLocalizedModule_restrict_of_localized₀_eq

Source context 11 commands

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

noncomputable section
universe u v w z
namespace Submodule
section Localization
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]

Lean source · statement

theorem isLocalizedModule_restrict_of_localized₀_eq
    (K : Submodule R B) (L : Submodule R B')
    (hf : ∀ x ∈ K, f.toLinearMap x ∈ L)
    (h : K.localized₀ S f.toLinearMap = L) :
    IsLocalizedModule S (f.toLinearMap.restrict hf)

theorem

isLocalizedModule_adjoinRestriction

L102 ↗

Submodule.isLocalizedModule_adjoinRestriction

Documentation

The underlying linear map of the actual algebra restriction is a localization. The equality of generated algebras is derived above.

Source context 11 commands

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

noncomputable section
universe u v w z
namespace Submodule
section Localization
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]

Lean source · statement

theorem isLocalizedModule_adjoinRestriction (N : Submodule R B) :
    IsLocalizedModule S (adjoinRestriction R' S f N).toLinearMap

theorem

finite_adjoin_of_fg

L125 ↗

Submodule.finite_adjoin_of_fg

Documentation

A finitely generated submodule of an integral algebra generates an actual module-finite subalgebra.

Source context 6 commands

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

noncomputable section
universe u v w z
namespace Submodule
section Finiteness
variable {R : Type u} [CommRing R]
variable {B : Type w} [CommRing B] [Algebra R B]

Lean source · statement

theorem finite_adjoin_of_fg [Algebra.IsIntegral R B]
    (N : Submodule R B) (hN : N.FG) :
    Module.Finite R (Algebra.adjoin R (N : Set B))

Module documentation

Localization of algebras generated by submodules

Declarations

localized'_adjoin

adjoinRestriction_mapsTo

adjoinRestriction

adjoinRestriction_apply

isLocalizedModule_restrict_of_localized₀_eq

isLocalizedModule_adjoinRestriction

finite_adjoin_of_fg