Module

Affine.lean

Nyll.SchemeTheory.Normalization.Affine

8 declarations indexed from sourceView source ↗

Module documentation

Relative normalization of an affine morphism

The relative normalization of Spec B → Spec R is canonically isomorphic to Spec (integralClosure R B). The comparison intertwines the canonical map into the normalization with the map induced by the inclusion of the integral closure into B. Thus Zariski's main theorem makes this literal inclusion an open immersion when B is a quasi-finite algebra of finite type over R.

Imports6

Mathlib.Algebra.Ring.Subring.Basic
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Normalization
Mathlib.AlgebraicGeometry.Scheme
Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Imported by6

abbrev

affineStructureMap

L37 ↗

AlgebraicGeometry.affineStructureMap

Documentation

The affine scheme morphism induced by the structural algebra map.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

abbrev affineStructureMap : Spec (CommRingCat.of B) ⟶ Spec (CommRingCat.of R)

def

specIntegralClosureIso

L42 ↗

AlgebraicGeometry.specIntegralClosureIso

Documentation

The global-section identifications restrict to the corresponding integral closures.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · full declaration

def specIntegralClosureIso :
    letI := (affineStructureMap R B).appTop.hom.toAlgebra
    CommRingCat.of (integralClosure Γ(Spec (CommRingCat.of R), ⊤)
      Γ(Spec (CommRingCat.of B), ⊤)) ≅ CommRingCat.of (integralClosure R B) := by
  letI := (affineStructureMap R B).appTop.hom.toAlgebra
  let e := (Scheme.ΓSpecIso (CommRingCat.of B)).commRingCatIsoToRingEquiv
  refine (e.restrict (integralClosure Γ(Spec (CommRingCat.of R), ⊤)
    Γ(Spec (CommRingCat.of B), ⊤)) (integralClosure R B) ?_).toCommRingCatIso
  intro x
  change _root_.IsIntegral Γ(Spec (CommRingCat.of R), ⊤) x ↔ _root_.IsIntegral R (e x)
  constructor
  · intro hx
    exact _root_.IsIntegral.map_of_comp_eq
      (Scheme.ΓSpecIso (CommRingCat.of R)).hom.hom
      (Scheme.ΓSpecIso (CommRingCat.of B)).hom.hom
      (congrArg (fun k : Γ(Spec (CommRingCat.of R), ⊤) ⟶ CommRingCat.of B ↦ k.hom)
        (Scheme.ΓSpecIso_naturality (CommRingCat.ofHom (algebraMap R B))).symm) hx
  · intro hx
    have hx' := _root_.IsIntegral.map_of_comp_eq
      (Scheme.ΓSpecIso (CommRingCat.of R)).inv.hom
      (Scheme.ΓSpecIso (CommRingCat.of B)).inv.hom
      (congrArg (fun k : CommRingCat.of R ⟶ Γ(Spec (CommRingCat.of B), ⊤) ↦ k.hom)
        (Scheme.ΓSpecIso_inv_naturality (CommRingCat.ofHom (algebraMap R B))).symm) hx
    change _root_.IsIntegral Γ(Spec (CommRingCat.of R), ⊤) (e.symm (e x)) at hx'
    simpa only [RingEquiv.symm_apply_apply] using hx'

def

specNormalizationRingIso

L70 ↗

AlgebraicGeometry.specNormalizationRingIso

Documentation

The ring of global sections of the relative normalization of an affine morphism is its literal integral closure.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

def specNormalizationRingIso :
    Γ((affineStructureMap R B).normalization, ⊤) ≅
      CommRingCat.of (integralClosure R B)

lemma

specNormalizationRingIso_hom_val

L78 ↗

AlgebraicGeometry.specNormalizationRingIso_hom_val

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

lemma specNormalizationRingIso_hom_val :
    (specNormalizationRingIso R B).hom ≫
        CommRingCat.ofHom (integralClosure R B).val.toRingHom =
      (affineStructureMap R B).toNormalization.appTop ≫
        (Scheme.ΓSpecIso (CommRingCat.of B)).hom

def

specNormalizationIso

L119 ↗

AlgebraicGeometry.specNormalizationIso

Documentation

The relative normalization of Spec B → Spec R, identified with the spectrum of the integral closure of R in B.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

def specNormalizationIso :
    (Spec.map (CommRingCat.ofHom (algebraMap R B))).normalization ≅
      Spec (CommRingCat.of (integralClosure R B))

lemma

toNormalization_specNormalizationIso_hom

L130 ↗

AlgebraicGeometry.toNormalization_specNormalizationIso_hom

Documentation

The affine normalization comparison sends the canonical normalization map to the map induced by the actual integral-closure inclusion.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

lemma toNormalization_specNormalizationIso_hom :
    (Spec.map (CommRingCat.ofHom (algebraMap R B))).toNormalization ≫
        (specNormalizationIso R B).hom =
      Spec.map (CommRingCat.ofHom (integralClosure R B).val.toRingHom)

theorem

spec_toNormalization_hom_ext

L146 ↗

AlgebraicGeometry.spec_toNormalization_hom_ext

Documentation

Morphisms from an affine relative normalization to an affine scheme are uniquely determined by their composites with the original affine scheme. The integral-closure inclusion is injective on coordinate rings.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

theorem spec_toNormalization_hom_ext
    {T : Scheme.{u}} [IsAffine T]
    {f g : (Spec.map (CommRingCat.ofHom (algebraMap R B))).normalization ⟶ T}
    (h : (Spec.map (CommRingCat.ofHom (algebraMap R B))).toNormalization ≫ f =
      (Spec.map (CommRingCat.ofHom (algebraMap R B))).toNormalization ≫ g) :
    f = g

theorem

isOpenImmersion_spec_integralClosure

L177 ↗

AlgebraicGeometry.isOpenImmersion_spec_integralClosure

Documentation

Zariski's main theorem for the literal integral-closure inclusion of a quasi-finite algebra of finite type.

Source context 5 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

theorem isOpenImmersion_spec_integralClosure
    [Algebra.FiniteType R B] [Algebra.QuasiFinite R B] :
    IsOpenImmersion
      (Spec.map (CommRingCat.ofHom (integralClosure R B).val.toRingHom))

Module documentation

Relative normalization of an affine morphism

Declarations