Module

FiniteSeparable.lean

Nyll.SchemeTheory.Normalization.FiniteSeparable

18 declarations indexed from sourceView source ↗

Module documentation

Finite normalizations in separable function-field extensions

This file records the scheme-level form of the trace-dual finiteness theorem: over a locally Noetherian normal integral scheme, normalization in a finite separable extension of the function field is finite.

Imports6

Mathlib.AlgebraicGeometry.FunctionField
Mathlib.AlgebraicGeometry.Normalization
Mathlib.AlgebraicGeometry.Noetherian
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.RingTheory.DedekindDomain.IntegralClosure
Nyll.SchemeTheory.Normalization.Normal

Imported by16

def

affineExtensionAlgebra

L38 ↗

AlgebraicGeometry.Scheme.affineExtensionAlgebra

Documentation

The algebra structure on a field extension induced from an affine chart through the function field.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) [IsIntegral X]

Lean source · statement

def affineExtensionAlgebra (U : X.Opens) [Nonempty U]
    (L : Type u) [CommRing L] [Algebra X.functionField L] : Algebra Γ(X, U) L

def

stalkExtensionAlgebra

L46 ↗

AlgebraicGeometry.Scheme.stalkExtensionAlgebra

Documentation

The algebra structure on a field extension induced from a local ring through the function field.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) [IsIntegral X]

Lean source · statement

def stalkExtensionAlgebra (x : X)
    (L : Type u) [CommRing L] [Algebra X.functionField L] :
    Algebra (X.presheaf.stalk x) L

instance

(anonymous instance)

L59 ↗

Source context 11 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) [IsIntegral X]
section AffineIntegralClosure
variable [IsNormalIntegral X] [IsLocallyNoetherian X]
variable (U : X.affineOpens) [Nonempty U.1]
variable (L : Type u) [Field L] [Algebra X.functionField L]
variable [FiniteDimensional X.functionField L] [Algebra.IsSeparable X.functionField L]

Lean source · statement

instance : Algebra Γ(X, U.1) L

instance

(anonymous instance)

L60 ↗

Source context 12 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) [IsIntegral X]
section AffineIntegralClosure
variable [IsNormalIntegral X] [IsLocallyNoetherian X]
variable (U : X.affineOpens) [Nonempty U.1]
variable (L : Type u) [Field L] [Algebra X.functionField L]
variable [FiniteDimensional X.functionField L] [Algebra.IsSeparable X.functionField L]
local instance : Algebra Γ(X, U.1) L := X.affineExtensionAlgebra U.1 L

Lean source · statement

instance : IsScalarTower Γ(X, U.1) X.functionField L

theorem

affineIntegralClosure_finite

L66 ↗

AlgebraicGeometry.Scheme.affineIntegralClosure_finite

Documentation

On a nonempty affine chart of a normal locally Noetherian integral scheme, the integral closure in a finite separable extension of the function field is module-finite.

Source context 13 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) [IsIntegral X]
section AffineIntegralClosure
variable [IsNormalIntegral X] [IsLocallyNoetherian X]
variable (U : X.affineOpens) [Nonempty U.1]
variable (L : Type u) [Field L] [Algebra X.functionField L]
variable [FiniteDimensional X.functionField L] [Algebra.IsSeparable X.functionField L]
local instance : Algebra Γ(X, U.1) L := X.affineExtensionAlgebra U.1 L
local instance : IsScalarTower Γ(X, U.1) X.functionField L :=
  IsScalarTower.of_algebraMap_eq' rfl

Lean source · statement

theorem affineIntegralClosure_finite :
    Module.Finite Γ(X, U.1) (integralClosure Γ(X, U.1) L)

instance

(anonymous instance)

L86 ↗

Source context 11 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) [IsIntegral X]
section StalkIntegralClosure
variable [IsNormalIntegral X] [IsLocallyNoetherian X]
variable (x : X)
variable (L : Type u) [Field L] [Algebra X.functionField L]
variable [FiniteDimensional X.functionField L] [Algebra.IsSeparable X.functionField L]

Lean source · statement

instance : Algebra (X.presheaf.stalk x) L

instance

(anonymous instance)

L88 ↗

Source context 12 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) [IsIntegral X]
section StalkIntegralClosure
variable [IsNormalIntegral X] [IsLocallyNoetherian X]
variable (x : X)
variable (L : Type u) [Field L] [Algebra X.functionField L]
variable [FiniteDimensional X.functionField L] [Algebra.IsSeparable X.functionField L]
local instance : Algebra (X.presheaf.stalk x) L :=
  X.stalkExtensionAlgebra x L

Lean source · statement

instance : IsScalarTower (X.presheaf.stalk x) X.functionField L

theorem

stalkIntegralClosure_finite

L93 ↗

AlgebraicGeometry.Scheme.stalkIntegralClosure_finite

Documentation

The integral closure of any local ring in a finite separable extension of the function field is module-finite.

Source context 13 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) [IsIntegral X]
section StalkIntegralClosure
variable [IsNormalIntegral X] [IsLocallyNoetherian X]
variable (x : X)
variable (L : Type u) [Field L] [Algebra X.functionField L]
variable [FiniteDimensional X.functionField L] [Algebra.IsSeparable X.functionField L]
local instance : Algebra (X.presheaf.stalk x) L :=
  X.stalkExtensionAlgebra x L
local instance : IsScalarTower (X.presheaf.stalk x) X.functionField L :=
  IsScalarTower.of_algebraMap_eq' rfl

Lean source · statement

theorem stalkIntegralClosure_finite :
    Module.Finite (X.presheaf.stalk x)
      (integralClosure (X.presheaf.stalk x) L)

def

genericExtensionMorphism

L105 ↗

AlgebraicGeometry.Scheme.genericExtensionMorphism

Documentation

The generic-point morphism associated to an extension of the function field.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) [IsIntegral X]

Lean source · statement

def genericExtensionMorphism (L : Type u) [CommRing L] [Algebra X.functionField L] :
    Spec (.of L) ⟶ X

lemma

genericExtensionMorphism_apply_closedPoint

L111 ↗

AlgebraicGeometry.Scheme.genericExtensionMorphism_apply_closedPoint

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) [IsIntegral X]

Lean source · statement

lemma genericExtensionMorphism_apply_closedPoint (L : Type u) [Field L]
    [Algebra X.functionField L] :
    X.genericExtensionMorphism L (IsLocalRing.closedPoint (CommRingCat.of L)) = genericPoint X

lemma

genericExtensionMorphism_preimage_eq_top

L117 ↗

AlgebraicGeometry.Scheme.genericExtensionMorphism_preimage_eq_top

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) [IsIntegral X]

Lean source · statement

lemma genericExtensionMorphism_preimage_eq_top (L : Type u) [Field L]
    [Algebra X.functionField L] (U : X.Opens) [Nonempty U] :
    X.genericExtensionMorphism L ⁻¹ᵁ U = ⊤

def

genericExtensionSectionsIso

L130 ↗

AlgebraicGeometry.Scheme.genericExtensionSectionsIso

Documentation

Sections on the inverse image of a nonempty open under the generic extension morphism identify canonically with the extension field.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) [IsIntegral X]

Lean source · statement

def genericExtensionSectionsIso (L : Type u) [Field L]
    [Algebra X.functionField L] (U : X.Opens) [Nonempty U] :
    Γ(Spec (.of L), X.genericExtensionMorphism L ⁻¹ᵁ U) ≅ CommRingCat.of L

lemma

genericExtensionSectionsIso_hom_app

L142 ↗

AlgebraicGeometry.Scheme.genericExtensionSectionsIso_hom_app

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) [IsIntegral X]

Lean source · statement

lemma genericExtensionSectionsIso_hom_app (L : Type u) [Field L]
    [Algebra X.functionField L] (U : X.Opens) [Nonempty U] (r : Γ(X, U)) :
    (X.genericExtensionSectionsIso L U).hom
        ((X.genericExtensionMorphism L).app U r) =
      algebraMap X.functionField L (X.germToFunctionField U r)

instance

(anonymous instance)

L176 ↗

Source context 9 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) [IsIntegral X]
section ExtensionSections
variable (L : Type u) [Field L] [Algebra X.functionField L]
variable (U : X.Opens) [Nonempty U]

Lean source · statement

instance : Algebra Γ(X, U)
    Γ(Spec (.of L), X.genericExtensionMorphism L ⁻¹ᵁ U)

instance

(anonymous instance)

L180 ↗

Source context 10 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) [IsIntegral X]
section ExtensionSections
variable (L : Type u) [Field L] [Algebra X.functionField L]
variable (U : X.Opens) [Nonempty U]
local instance : Algebra Γ(X, U)
    Γ(Spec (.of L), X.genericExtensionMorphism L ⁻¹ᵁ U) :=
  ((X.genericExtensionMorphism L).app U).hom.toAlgebra

Lean source · statement

instance : Algebra Γ(X, U) L

def

genericExtensionSectionsAlgEquiv

L184 ↗

AlgebraicGeometry.Scheme.genericExtensionSectionsAlgEquiv

Documentation

The section-ring identification over a nonempty open, as an algebra equivalence over the base chart.

Source context 11 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) [IsIntegral X]
section ExtensionSections
variable (L : Type u) [Field L] [Algebra X.functionField L]
variable (U : X.Opens) [Nonempty U]
local instance : Algebra Γ(X, U)
    Γ(Spec (.of L), X.genericExtensionMorphism L ⁻¹ᵁ U) :=
  ((X.genericExtensionMorphism L).app U).hom.toAlgebra
local instance : Algebra Γ(X, U) L := X.affineExtensionAlgebra U L

Lean source · statement

def genericExtensionSectionsAlgEquiv :
    Γ(Spec (.of L), X.genericExtensionMorphism L ⁻¹ᵁ U) ≃ₐ[Γ(X, U)] L

theorem

isFinite_fromNormalization_of_finite_integralClosure

L200 ↗

AlgebraicGeometry.Scheme.Hom.isFinite_fromNormalization_of_finite_integralClosure

Documentation

A relative normalization is finite as soon as its affine integral-closure charts are module-finite.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme.Hom
variable {Y Z : Scheme.{u}} (f : Y ⟶ Z) [QuasiCompact f] [QuasiSeparated f]

Lean source · full declaration

theorem isFinite_fromNormalization_of_finite_integralClosure
    (hfinite : ∀ (U : Z.Opens) (_hU : IsAffineOpen U),
      letI := (f.app U).hom.toAlgebra
      Module.Finite Γ(Z, U) (integralClosure Γ(Z, U) Γ(Y, f ⁻¹ᵁ U))) :
    IsFinite f.fromNormalization := by
  refine { finite_app := ?_ }
  intro U hU
  let := (f.app U).hom.toAlgebra
  rw [f.fromNormalization_app hU]
  exact RingHom.Finite.comp
    (f.normalizationObjIso hU).symm.commRingCatIsoToRingEquiv.finite
    (show (algebraMap Γ(Z, U)
      (integralClosure Γ(Z, U) Γ(Y, f ⁻¹ᵁ U))).Finite from
      hfinite U hU)

theorem

isFinite_fromNormalization_genericExtension

L217 ↗

AlgebraicGeometry.Scheme.Hom.isFinite_fromNormalization_genericExtension

Documentation

The relative normalization of a normal locally Noetherian integral scheme in a finite separable extension of its function field is finite.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme.Hom
variable {Y Z : Scheme.{u}} (f : Y ⟶ Z) [QuasiCompact f] [QuasiSeparated f]

Lean source · statement

theorem isFinite_fromNormalization_genericExtension
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X]
    (L : Type u) [Field L] [Algebra X.functionField L]
    [FiniteDimensional X.functionField L] [Algebra.IsSeparable X.functionField L] :
    IsFinite (X.genericExtensionMorphism L).fromNormalization

Module documentation

Finite normalizations in separable function-field extensions

Declarations