NYLL
Module

GenericFiber.lean

Nyll.EtaleFundamentalGroups.Normalization.GenericFiber
7 declarations indexed from sourceView source ↗

Module documentation

The generic fibre of an integral closure

For an algebraic commutative algebra L over the fraction field K of a commutative ring R, localizing the integral closure of R in L at the nonzero elements of R gives L. Consequently its generic fibre is the literal scheme Spec L, including when L is a finite product rather than a field. The comparison uses the original inclusions into L on both sides.

Imports6
Imported by4

Declarations

theorem

integralClosure_generic_isLocalization

L41 ↗
EtaleFundamentalGroups.integralClosure_generic_isLocalization
Documentation

Clearing an algebraic element's denominators identifies L with the localization of the integral closure at the nonzero elements of R.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped nonZeroDivisors TensorProduct
namespace EtaleFundamentalGroups
universe u
variable (R K L : Type u) [CommRing R] [Field K] [CommRing L]
  [Algebra R K] [IsFractionRing R K] [Algebra K L] [Algebra R L]
  [IsScalarTower R K L] [Algebra.IsAlgebraic K L]
include K in
Lean source · statement
theorem integralClosure_generic_isLocalization :
    IsLocalization (Algebra.algebraMapSubmonoid (integralClosure R L) R⁰) L
theorem

integralClosure_generic_isPushout

L48 ↗
EtaleFundamentalGroups.integralClosure_generic_isPushout
Documentation

The integral closure and the base fraction field have pushout L, with the given structural maps. No finiteness of the integral closure is required.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped nonZeroDivisors TensorProduct
namespace EtaleFundamentalGroups
universe u
variable (R K L : Type u) [CommRing R] [Field K] [CommRing L]
  [Algebra R K] [IsFractionRing R K] [Algebra K L] [Algebra R L]
  [IsScalarTower R K L] [Algebra.IsAlgebraic K L]
Lean source · statement
theorem integralClosure_generic_isPushout :
    Algebra.IsPushout R (integralClosure R L) K L
def

integralClosureGenericFiberAlgEquiv

L56 ↗
EtaleFundamentalGroups.integralClosureGenericFiberAlgEquiv
Documentation

The coordinate ring of the generic fibre is the prescribed algebra, compatibly with its K-algebra structure.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped nonZeroDivisors TensorProduct
namespace EtaleFundamentalGroups
universe u
variable (R K L : Type u) [CommRing R] [Field K] [CommRing L]
  [Algebra R K] [IsFractionRing R K] [Algebra K L] [Algebra R L]
  [IsScalarTower R K L] [Algebra.IsAlgebraic K L]
Lean source · statement
def integralClosureGenericFiberAlgEquiv :
    K ⊗[R] integralClosure R L ≃ₐ[K] L
theorem

integralClosureGenericFiberAlgEquiv_tmul

L64 ↗
EtaleFundamentalGroups.integralClosureGenericFiberAlgEquiv_tmul
Documentation

The generic-fibre comparison sends a pure tensor to the product of the two original inclusions into L.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped nonZeroDivisors TensorProduct
namespace EtaleFundamentalGroups
universe u
variable (R K L : Type u) [CommRing R] [Field K] [CommRing L]
  [Algebra R K] [IsFractionRing R K] [Algebra K L] [Algebra R L]
  [IsScalarTower R K L] [Algebra.IsAlgebraic K L]
Lean source · statement
theorem integralClosureGenericFiberAlgEquiv_tmul
    (k : K) (b : integralClosure R L) :
    integralClosureGenericFiberAlgEquiv R K L (k ⊗ₜ[R] b) =
      algebraMap K L k * (b : L)
theorem

isPullback_spec_integralClosure_generic

L74 ↗
EtaleFundamentalGroups.isPullback_spec_integralClosure_generic
Documentation

The generic fibre of the spectrum of the integral closure is the actual Spec L, using the actual inclusion of the integral closure into L.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped nonZeroDivisors TensorProduct
namespace EtaleFundamentalGroups
universe u
variable (R K L : Type u) [CommRing R] [Field K] [CommRing L]
  [Algebra R K] [IsFractionRing R K] [Algebra K L] [Algebra R L]
  [IsScalarTower R K L] [Algebra.IsAlgebraic K L]
Lean source · statement
theorem isPullback_spec_integralClosure_generic :
    IsPullback
      (Spec.map (CommRingCat.ofHom (algebraMap (integralClosure R L) L)))
      (Spec.map (CommRingCat.ofHom (algebraMap K L)))
      (Spec.map (CommRingCat.ofHom (algebraMap R (integralClosure R L))))
      (Spec.map (CommRingCat.ofHom (algebraMap R K)))
theorem

specNormalizationIso_hom_base

L90 ↗
EtaleFundamentalGroups.specNormalizationIso_hom_base
Documentation

The affine normalization comparison respects its structural map to Spec R.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped nonZeroDivisors TensorProduct
namespace EtaleFundamentalGroups
universe u
variable (R K L : Type u) [CommRing R] [Field K] [CommRing L]
  [Algebra R K] [IsFractionRing R K] [Algebra K L] [Algebra R L]
  [IsScalarTower R K L] [Algebra.IsAlgebraic K L]
omit [Field K] [Algebra R K] [IsFractionRing R K]
  [Algebra K L] [IsScalarTower R K L] [Algebra.IsAlgebraic K L] in
Lean source · statement
theorem specNormalizationIso_hom_base :
    (specNormalizationIso R L).hom ≫
        Spec.map (CommRingCat.ofHom (algebraMap R (integralClosure R L))) =
      (Spec.map (CommRingCat.ofHom (algebraMap R L))).fromNormalization
theorem

isPullback_affineNormalization_generic

L101 ↗
EtaleFundamentalGroups.isPullback_affineNormalization_generic
Documentation

The relative normalization of Spec R in Spec L has generic fibre Spec L, with the canonical map into that normalization as the first leg.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped nonZeroDivisors TensorProduct
namespace EtaleFundamentalGroups
universe u
variable (R K L : Type u) [CommRing R] [Field K] [CommRing L]
  [Algebra R K] [IsFractionRing R K] [Algebra K L] [Algebra R L]
  [IsScalarTower R K L] [Algebra.IsAlgebraic K L]
Lean source · statement
theorem isPullback_affineNormalization_generic :
    IsPullback
      (Spec.map (CommRingCat.ofHom (algebraMap R L))).toNormalization
      (Spec.map (CommRingCat.ofHom (algebraMap K L)))
      (Spec.map (CommRingCat.ofHom (algebraMap R L))).fromNormalization
      (Spec.map (CommRingCat.ofHom (algebraMap R K)))

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