Module

AffineNormalizationFunctionField.lean

Nyll.EtaleFundamentalGroups.Inertia.AffineNormalizationFunctionField

8 declarations indexed from sourceView source ↗

Module documentation

Comparing an affine normalization with normalization in the function field

For a normal domain B over R, the integral closure of R inside B maps bijectively to the integral closure of R inside the fraction field of B. Indeed, an element integral over R is integral over B, so normality puts it back in B; injectivity then reflects integrality over R.

The resulting canonical affine normalization isomorphism intertwines the map from the fraction-field spectrum and the map to Spec R. Thus it compares the actual relative normalization used by geometric-point inertia with the field-theoretic integral closure used by local inertia theorems. This is a local normal-domain result and does not require the original ambient scheme of the manuscript to be normal or integral everywhere.

Imports4

Nyll.EtaleFundamentalGroups.Inertia.NormalizationLocalization
Nyll.EtaleFundamentalGroups.Inertia.AffineNormalizationGeometricPoint
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Imported by2

theorem

integralClosureToFractionField_bijective

L45 ↗

EtaleFundamentalGroups.Inertia.integralClosureToFractionField_bijective

Documentation

Normality of B makes its integral closure over R equal to the integral closure computed in its actual fraction field.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B L : Type u) [CommRing R] [CommRing B] [IsDomain B]
  [IsIntegrallyClosed B] [Field L]
  [Algebra R B] [Algebra B L] [IsFractionRing B L]
  [Algebra R L] [IsScalarTower R B L]
omit [IsDomain B] in

Lean source · statement

theorem integralClosureToFractionField_bijective :
    Function.Bijective (IsScalarTower.toAlgHom R B L).mapIntegralClosure

def

integralClosureFractionFieldEquiv

L63 ↗

EtaleFundamentalGroups.Inertia.integralClosureFractionFieldEquiv

Documentation

The comparison is the literal map into the fraction field, with its inverse supplied by integrally closedness.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B L : Type u) [CommRing R] [CommRing B] [IsDomain B]
  [IsIntegrallyClosed B] [Field L]
  [Algebra R B] [Algebra B L] [IsFractionRing B L]
  [Algebra R L] [IsScalarTower R B L]

Lean source · statement

def integralClosureFractionFieldEquiv :
    integralClosure R B ≃ₐ[R] integralClosure R L

theorem

integralClosureFractionFieldEquiv_val

L71 ↗

EtaleFundamentalGroups.Inertia.integralClosureFractionFieldEquiv_val

Documentation

The comparison agrees with the original inclusion into the fraction field.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B L : Type u) [CommRing R] [CommRing B] [IsDomain B]
  [IsIntegrallyClosed B] [Field L]
  [Algebra R B] [Algebra B L] [IsFractionRing B L]
  [Algebra R L] [IsScalarTower R B L]
omit [IsDomain B] in

Lean source · statement

theorem integralClosureFractionFieldEquiv_val (b : integralClosure R B) :
    (integralClosureFractionFieldEquiv R B L b : L) = algebraMap B L (b : B)

theorem

integralClosureFractionFieldEquiv_mapIntegralClosure

L79 ↗

EtaleFundamentalGroups.Inertia.integralClosureFractionFieldEquiv_mapIntegralClosure

Documentation

The integral-closure comparison intertwines a ring automorphism with its actual extension to the fraction field. Compatibility is a consequence of the fraction-field construction, not an additional input.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B L : Type u) [CommRing R] [CommRing B] [IsDomain B]
  [IsIntegrallyClosed B] [Field L]
  [Algebra R B] [Algebra B L] [IsFractionRing B L]
  [Algebra R L] [IsScalarTower R B L]
omit [IsDomain B] in

Lean source · statement

theorem integralClosureFractionFieldEquiv_mapIntegralClosure
    (σ : B ≃ₐ[R] B) (b : integralClosure R B) :
    integralClosureFractionFieldEquiv R B L (σ.mapIntegralClosure b) =
      (IsFractionRing.algEquivOfAlgEquiv σ : L ≃ₐ[R] L).mapIntegralClosure
        (integralClosureFractionFieldEquiv R B L b)

def

affineNormalizationFunctionFieldIso

L92 ↗

EtaleFundamentalGroups.Inertia.affineNormalizationFunctionFieldIso

Documentation

The actual relative normalization of Spec B → Spec R, expressed using the integral closure in the fraction field of B.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B L : Type u) [CommRing R] [CommRing B] [IsDomain B]
  [IsIntegrallyClosed B] [Field L]
  [Algebra R B] [Algebra B L] [IsFractionRing B L]
  [Algebra R L] [IsScalarTower R B L]

Lean source · statement

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

theorem

fractionField_toNormalization_affineNormalizationFunctionFieldIso

L103 ↗

EtaleFundamentalGroups.Inertia.fractionField_toNormalization_affineNormalizationFunctionFieldIso

Documentation

The point from the fraction field has its canonical integral-closure coordinates under the normalization comparison.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B L : Type u) [CommRing R] [CommRing B] [IsDomain B]
  [IsIntegrallyClosed B] [Field L]
  [Algebra R B] [Algebra B L] [IsFractionRing B L]
  [Algebra R L] [IsScalarTower R B L]
omit [IsDomain B] in

Lean source · statement

theorem fractionField_toNormalization_affineNormalizationFunctionFieldIso :
    Spec.map (CommRingCat.ofHom (algebraMap B L)) ≫
        (Spec.map (CommRingCat.ofHom (algebraMap R B))).toNormalization ≫
        (affineNormalizationFunctionFieldIso R B L).hom =
      Spec.map (CommRingCat.ofHom (integralClosure R L).val.toRingHom)

theorem

affineNormalizationFunctionFieldIso_hom_structureMap

L127 ↗

EtaleFundamentalGroups.Inertia.affineNormalizationFunctionFieldIso_hom_structureMap

Documentation

The function-field normalization comparison preserves the structure map to the original affine base.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B L : Type u) [CommRing R] [CommRing B] [IsDomain B]
  [IsIntegrallyClosed B] [Field L]
  [Algebra R B] [Algebra B L] [IsFractionRing B L]
  [Algebra R L] [IsScalarTower R B L]
omit [IsDomain B] in

Lean source · statement

theorem affineNormalizationFunctionFieldIso_hom_structureMap :
    (affineNormalizationFunctionFieldIso R B L).hom ≫
        Spec.map (CommRingCat.ofHom (algebraMap R (integralClosure R L))) =
      (Spec.map (CommRingCat.ofHom (algebraMap R B))).fromNormalization

theorem

affineNormalizationDeck_affineNormalizationFunctionFieldIso

L150 ↗

EtaleFundamentalGroups.Inertia.affineNormalizationDeck_affineNormalizationFunctionFieldIso

Documentation

Under the function-field normalization comparison, the actual normalization deck extension is the restriction of the actual fraction-field automorphism to its integral closure.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B L : Type u) [CommRing R] [CommRing B] [IsDomain B]
  [IsIntegrallyClosed B] [Field L]
  [Algebra R B] [Algebra B L] [IsFractionRing B L]
  [Algebra R L] [IsScalarTower R B L]
omit [IsDomain B] in

Lean source · statement

theorem affineNormalizationDeck_affineNormalizationFunctionFieldIso
    (σ : B ≃ₐ[R] B) :
    affineNormalizationDeck R B σ ≫
        (affineNormalizationFunctionFieldIso R B L).hom =
      (affineNormalizationFunctionFieldIso R B L).hom ≫
        Spec.map (CommRingCat.ofHom
          (((IsFractionRing.algEquivOfAlgEquiv σ :
            L ≃ₐ[R] L).toAlgHom.mapIntegralClosure).toRingHom))

Module documentation

Comparing an affine normalization with normalization in the function field

Declarations