NYLL
Module

NormalizationPrimeOrdinaryFieldTower.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.NormalizationPrimeOrdinaryFieldTower
6 declarations indexed from sourceView source ↗

Module documentation

The original base field and actual ordinary-henselization fraction field

The native fraction map of the original local structure map supplies the displayed K → Frac(H). Its composite with the actual embedding in L is the original coefficient map, proved on A and extended by fraction-field uniqueness. The resulting scalar tower makes the original separably closed Galois field a separable closure of the actual ordinary fraction field.

Imports8
Imported by4

Declarations

def

ordinaryHenselizationFractionBaseMap

L43 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationFractionBaseMap
Documentation

The actual original fraction field maps to the actual fraction field of the ordinary henselization by the native localization map.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
section Base
variable (A : Type u) (K : Type v)
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A]
  [Field K] [Algebra A K] [IsFractionRing A K]
Lean source · statement
def ordinaryHenselizationFractionBaseMap : K →+* FractionRing (ordinaryHenselization A)
theorem

ordinaryHenselizationFractionBaseMap_algebraMap

L50 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationFractionBaseMap_algebraMap
Source context 7 commands

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

noncomputable section
open AlgebraicGeometry
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
section Base
variable (A : Type u) (K : Type v)
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A]
  [Field K] [Algebra A K] [IsFractionRing A K]
Lean source · statement
theorem ordinaryHenselizationFractionBaseMap_algebraMap (a : A) :
    ordinaryHenselizationFractionBaseMap A K (algebraMap A K a) =
      algebraMap (ordinaryHenselization A) (FractionRing (ordinaryHenselization A))
        (ordinaryHenselizationMap A a)
theorem

ordinaryHenselizationFractionBaseMap_eq_canonical

L62 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationFractionBaseMap_eq_canonical
Documentation

The displayed-field map uses the same canonical fraction map already attached to the existing pointed-stalk construction.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
section Base
variable (A : Type u) (K : Type v)
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A]
  [Field K] [Algebra A K] [IsFractionRing A K]
Lean source · statement
theorem ordinaryHenselizationFractionBaseMap_eq_canonical :
    ordinaryHenselizationFractionBaseMap A K =
      (geometricStalkFractionFieldMap (IsLocalRing.residue A)).comp
        (IsLocalization.algEquiv (nonZeroDivisors A) K (FractionRing A)).toRingHom
theorem

ordinaryHenselizationFractionToNormalizationField_comp_baseField

L92 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationFractionToNormalizationField_comp_baseField
Documentation

The actual ordinary fraction embedding preserves the displayed original fraction-field coefficient map, with no compatibility assumption.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
variable (A : Type u) (K : Type v) (L : Type u)
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
  [IsScalarTower A K L] [IsGalois K L] [IsSepClosed L]
  (Q : Ideal (integralClosure A L)) [Q.IsPrime]
  (hQ : Q.under A = IsLocalRing.maximalIdeal A)
Lean source · statement
theorem ordinaryHenselizationFractionToNormalizationField_comp_baseField :
    (ordinaryHenselizationFractionToNormalizationField A K L Q hQ).comp
      (ordinaryHenselizationFractionBaseMap A K) = algebraMap K L
theorem

ordinaryHenselizationFractionField_isScalarTower

L106 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationFractionField_isScalarTower
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
variable (A : Type u) (K : Type v) (L : Type u)
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
  [IsScalarTower A K L] [IsGalois K L] [IsSepClosed L]
  (Q : Ideal (integralClosure A L)) [Q.IsPrime]
  (hQ : Q.under A = IsLocalRing.maximalIdeal A)
Lean source · full declaration
theorem ordinaryHenselizationFractionField_isScalarTower :
    let : Algebra K (FractionRing (ordinaryHenselization A)) :=
      (ordinaryHenselizationFractionBaseMap A K).toAlgebra
    let : Algebra (FractionRing (ordinaryHenselization A)) L :=
      (ordinaryHenselizationFractionToNormalizationField A K L Q hQ).toAlgebra
    IsScalarTower K (FractionRing (ordinaryHenselization A)) L := by
  intro actualBaseAlgebra actualAmbientAlgebra
  exact IsScalarTower.of_algebraMap_eq'
    (ordinaryHenselizationFractionToNormalizationField_comp_baseField A K L Q hQ).symm
theorem

ordinaryHenselizationFractionField_isSepClosure

L118 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationFractionField_isSepClosure
Documentation

The original ambient field is a separable closure for the actual ordinary fraction-field action obtained from the original normalization.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
variable (A : Type u) (K : Type v) (L : Type u)
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
  [IsScalarTower A K L] [IsGalois K L] [IsSepClosed L]
  (Q : Ideal (integralClosure A L)) [Q.IsPrime]
  (hQ : Q.under A = IsLocalRing.maximalIdeal A)
Lean source · full declaration
theorem ordinaryHenselizationFractionField_isSepClosure :
    let : IsDomain (ordinaryHenselization A) :=
      geometricStalk_isDomain_of_normal (IsLocalRing.residue A)
    let : Algebra K (FractionRing (ordinaryHenselization A)) :=
      (ordinaryHenselizationFractionBaseMap A K).toAlgebra
    let : Algebra (FractionRing (ordinaryHenselization A)) L :=
      (ordinaryHenselizationFractionToNormalizationField A K L Q hQ).toAlgebra
    let : IsScalarTower K (FractionRing (ordinaryHenselization A)) L :=
      ordinaryHenselizationFractionField_isScalarTower A K L Q hQ
    IsSepClosure (FractionRing (ordinaryHenselization A)) L := by
  intro actualDomain actualBaseAlgebra actualAmbientAlgebra actualTower
  exact ⟨inferInstance, Algebra.isSeparable_tower_top_of_isSeparable K
    (FractionRing (ordinaryHenselization A)) L⟩

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