NYLL
Module

NormalizationFractionField.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationFractionField
8 declarations indexed from sourceView source ↗

Module documentation

Normalizing in a normal affine scheme or its fraction field

If B is integrally closed, an element of its fraction field integral over R already belongs to B. Thus the two actual integral closures are canonically isomorphic. This isomorphism intertwines automorphisms and, on spectra, the relative-normalization deck maps and their point stabilizers.

Imports3
Imported by1

Declarations

def

integralClosureFractionFieldAlgEquiv

L34 ↗
EtaleFundamentalGroups.Inertia.integralClosureFractionFieldAlgEquiv
Documentation

Passing to the fraction field of a normal domain does not change the integral closure of any base ring in it.

Source context 7 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] [Field L]
variable [Algebra R B] [Algebra B L] [Algebra R L] [IsScalarTower R B L]
variable [IsDomain B] [IsFractionRing B L] [IsIntegrallyClosed B]
Lean source · statement
def integralClosureFractionFieldAlgEquiv :
    integralClosure R B ≃ₐ[R] integralClosure R L
theorem

integralClosureFractionFieldAlgEquiv_coe

L51 ↗
EtaleFundamentalGroups.Inertia.integralClosureFractionFieldAlgEquiv_coe
Source context 7 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] [Field L]
variable [Algebra R B] [Algebra B L] [Algebra R L] [IsScalarTower R B L]
variable [IsDomain B] [IsFractionRing B L] [IsIntegrallyClosed B]
Lean source · statement
theorem integralClosureFractionFieldAlgEquiv_coe (x : integralClosure R B) :
    (integralClosureFractionFieldAlgEquiv R B L x : L) = algebraMap B L (x : B)
def

fractionFieldAlgEquiv

L55 ↗
EtaleFundamentalGroups.Inertia.fractionFieldAlgEquiv
Documentation

Extend a base-linear automorphism to the actual fraction field.

Source context 7 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] [Field L]
variable [Algebra R B] [Algebra B L] [Algebra R L] [IsScalarTower R B L]
variable [IsDomain B] [IsFractionRing B L] [IsIntegrallyClosed B]
Lean source · statement
def fractionFieldAlgEquiv (sigma : B ≃ₐ[R] B) : L ≃ₐ[R] L
theorem

fractionFieldAlgEquiv_algebraMap

L60 ↗
EtaleFundamentalGroups.Inertia.fractionFieldAlgEquiv_algebraMap
Source context 8 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] [Field L]
variable [Algebra R B] [Algebra B L] [Algebra R L] [IsScalarTower R B L]
variable [IsDomain B] [IsFractionRing B L] [IsIntegrallyClosed B]
omit [IsDomain B] [IsIntegrallyClosed B] in
Lean source · statement
theorem fractionFieldAlgEquiv_algebraMap (sigma : B ≃ₐ[R] B) (b : B) :
    fractionFieldAlgEquiv R B L sigma (algebraMap B L b) =
      algebraMap B L (sigma b)
theorem

integralClosureFractionFieldAlgEquiv_equivariant

L68 ↗
EtaleFundamentalGroups.Inertia.integralClosureFractionFieldAlgEquiv_equivariant
Documentation

The closure comparison intertwines the literal restrictions of the two automorphisms.

Source context 7 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] [Field L]
variable [Algebra R B] [Algebra B L] [Algebra R L] [IsScalarTower R B L]
variable [IsDomain B] [IsFractionRing B L] [IsIntegrallyClosed B]
Lean source · statement
theorem integralClosureFractionFieldAlgEquiv_equivariant
    (sigma : B ≃ₐ[R] B) (x : integralClosure R B) :
    integralClosureFractionFieldAlgEquiv R B L (sigma.mapIntegralClosure x) =
      (fractionFieldAlgEquiv R B L sigma).mapIntegralClosure
        (integralClosureFractionFieldAlgEquiv R B L x)
def

affineNormalizationFractionFieldIso

L78 ↗
EtaleFundamentalGroups.Inertia.affineNormalizationFractionFieldIso
Documentation

The normalization in the fraction field is canonically the normalization in the original normal affine scheme.

Source context 7 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] [Field L]
variable [Algebra R B] [Algebra B L] [Algebra R L] [IsScalarTower R B L]
variable [IsDomain B] [IsFractionRing B L] [IsIntegrallyClosed B]
Lean source · statement
def affineNormalizationFractionFieldIso :
    (Spec.map (CommRingCat.ofHom (algebraMap R L))).normalization ≅
      (Spec.map (CommRingCat.ofHom (algebraMap R B))).normalization
theorem

affineNormalizationFractionFieldIso_hom_deck

L87 ↗
EtaleFundamentalGroups.Inertia.affineNormalizationFractionFieldIso_hom_deck
Documentation

The normalization comparison commutes with the actual deck extensions.

Source context 7 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] [Field L]
variable [Algebra R B] [Algebra B L] [Algebra R L] [IsScalarTower R B L]
variable [IsDomain B] [IsFractionRing B L] [IsIntegrallyClosed B]
Lean source · statement
theorem affineNormalizationFractionFieldIso_hom_deck
    (sigma : B ≃ₐ[R] B) :
    affineNormalizationDeck R L (fractionFieldAlgEquiv R B L sigma) ≫
        (affineNormalizationFractionFieldIso R B L).hom =
      (affineNormalizationFractionFieldIso R B L).hom ≫
        affineNormalizationDeck R B sigma
theorem

affineNormalizationFractionFieldIso_fixes_iff

L111 ↗
EtaleFundamentalGroups.Inertia.affineNormalizationFractionFieldIso_fixes_iff
Documentation

An actual normalization point has exactly the same stabilizer after transport to the normalization in the fraction field.

Source context 7 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] [Field L]
variable [Algebra R B] [Algebra B L] [Algebra R L] [IsScalarTower R B L]
variable [IsDomain B] [IsFractionRing B L] [IsIntegrallyClosed B]
Lean source · statement
theorem affineNormalizationFractionFieldIso_fixes_iff
    {T : Scheme.{u}}
    (z : T ⟶ (Spec.map (CommRingCat.ofHom (algebraMap R B))).normalization)
    (sigma : B ≃ₐ[R] B) :
    (z ≫ (affineNormalizationFractionFieldIso R B L).inv) ≫
        affineNormalizationDeck R L (fractionFieldAlgEquiv R B L sigma) =
      z ≫ (affineNormalizationFractionFieldIso R B L).inv ↔
    z ≫ affineNormalizationDeck R B sigma = z

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