Module

FiniteSubalgebraLocalization.lean

Nyll.SchemeTheory.RingTheory.Descent.FiniteSubalgebraLocalization

3 declarations indexed from sourceView source ↗

Module documentation

Finite subalgebras realizing two localizations

For an integral algebra, finitely many numerators generate a finite subalgebra. If two localizations are finite, the numerators of their module generators can be chosen together. The resulting subalgebra has exactly the original two localizations. This is the finite approximation used near a boundary point.

Imports6

Mathlib.Algebra.Module.LocalizedModule.Basic
Mathlib.RingTheory.Flat.Localization
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Mathlib.RingTheory.Localization.BaseChange
Mathlib.RingTheory.TensorProduct.Maps

Imported by3

theorem

exists_finset_span_eq_top_of_isLocalizedModule

L33 ↗

SchemeTheory.exists_finset_span_eq_top_of_isLocalizedModule

Documentation

Generators of a finite localized module can be chosen as images of a finite set in the original module, by clearing their individual denominators.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
open scoped TensorProduct
universe u v w w'

Lean source · statement

theorem exists_finset_span_eq_top_of_isLocalizedModule
    {R : Type u} [CommRing R] (S : Submonoid R)
    (R' : Type v) [CommRing R'] [Algebra R R'] [IsLocalization S R']
    {M : Type w} [AddCommGroup M] [Module R M]
    {M' : Type w'} [AddCommGroup M'] [Module R M']
    [Module R' M'] [IsScalarTower R R' M']
    (f : M →ₗ[R] M') [IsLocalizedModule S f] [Module.Finite R' M'] :
    ∃ t : Finset M, Submodule.span R' (f '' (t : Set M)) = ⊤

theorem

lTensor_subalgebra_bijective_of_span

L65 ↗

SchemeTheory.lTensor_subalgebra_bijective_of_span

Documentation

A subalgebra whose images span after a flat scalar extension realizes that entire scalar extension.

Source context 7 commands

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

noncomputable section
namespace SchemeTheory
open scoped TensorProduct
universe u v w w'
section Subalgebra
variable {R : Type u} [CommRing R]
variable {B : Type v} [CommRing B] [Algebra R B]

Lean source · full declaration

theorem lTensor_subalgebra_bijective_of_span
    (A : Type w) [CommRing A] [Algebra R A] [Module.Flat R A]
    (C : Subalgebra R B)
    (hC : Submodule.span A ((fun b : B ↦ (1 : A) ⊗ₜ[R] b) '' (C : Set B)) = ⊤) :
    Function.Bijective (Algebra.TensorProduct.lTensor (S := A) A C.val) := by
  constructor
  · change Function.Injective (C.val.toLinearMap.lTensor A)
    exact Module.Flat.lTensor_preserves_injective_linearMap C.val.toLinearMap
      Subtype.val_injective
  · apply LinearMap.range_eq_top.mp
    apply top_unique
    rw [← hC]
    refine Submodule.span_le.mpr ?_
    rintro _ ⟨b, hb, rfl⟩
    exact ⟨(1 : A) ⊗ₜ[R] (⟨b, hb⟩ : C), rfl⟩

theorem

exists_finite_subalgebra_two_localizations

L83 ↗

SchemeTheory.exists_finite_subalgebra_two_localizations

Documentation

An integral algebra with two finite localizations admits one finite subalgebra realizing both localizations, through the actual inclusion maps.

Source context 7 commands

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

noncomputable section
namespace SchemeTheory
open scoped TensorProduct
universe u v w w'
section Subalgebra
variable {R : Type u} [CommRing R]
variable {B : Type v} [CommRing B] [Algebra R B]

Lean source · statement

theorem exists_finite_subalgebra_two_localizations
    [Algebra.IsIntegral R B]
    (S T : Submonoid R)
    (A : Type w) [CommRing A] [Algebra R A] [IsLocalization S A]
    (D : Type w') [CommRing D] [Algebra R D] [IsLocalization T D]
    [Module.Finite A (A ⊗[R] B)] [Module.Finite D (D ⊗[R] B)] :
    ∃ C : Subalgebra R B, Module.Finite R C ∧
      Function.Bijective (Algebra.TensorProduct.lTensor (S := A) A C.val) ∧
      Function.Bijective (Algebra.TensorProduct.lTensor (S := D) D C.val)

Module documentation

Finite subalgebras realizing two localizations

Declarations

exists_finset_span_eq_top_of_isLocalizedModule

lTensor_subalgebra_bijective_of_span

exists_finite_subalgebra_two_localizations