NYLL
Module

AbsoluteFiniteNormalization.lean

Nyll.EtaleFundamentalGroups.Inertia.AbsoluteFiniteNormalization
6 declarations indexed from sourceView source ↗

Module documentation

Native finite normalizations at the chosen absolute prime

The existing finite-level subalgebra and normalization owners construct the actual integral closures and their literal ring map. Prime contraction and localization are performed on those native objects, without introducing a second scalar action or carrying the finite field's scalar tower into the localized ring owner.

Imports3
Imported by37

Declarations

def

finiteAbsoluteNormalizationAlgebra

L35 ↗
EtaleFundamentalGroups.Inertia.finiteAbsoluteNormalizationAlgebra
Documentation

The actual finite normalization with its native coefficient action.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [Field K] [Field Ω]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsGalois K Ω]
Lean source · statement
def finiteAbsoluteNormalizationAlgebra
    (E : FiniteGaloisIntermediateField K Ω) : CommAlgCat.{w} A
def

finiteAbsoluteNormalizationRingMap

L40 ↗
EtaleFundamentalGroups.Inertia.finiteAbsoluteNormalizationRingMap
Documentation

The literal finite-to-absolute normalization inclusion.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [Field K] [Field Ω]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsGalois K Ω]
Lean source · statement
def finiteAbsoluteNormalizationRingMap
    (E : FiniteGaloisIntermediateField K Ω) :
    finiteAbsoluteNormalizationAlgebra A K Ω E →+* normalizationCommAlgCat A Ω
theorem

finiteAbsoluteNormalizationRingMap_injective

L48 ↗
EtaleFundamentalGroups.Inertia.finiteAbsoluteNormalizationRingMap_injective
Documentation

The finite normalization inclusion is injective by its existing native normalization owner.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [Field K] [Field Ω]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsGalois K Ω]
omit [IsFractionRing A K] [IsGalois K Ω] in
Lean source · statement
theorem finiteAbsoluteNormalizationRingMap_injective
    (E : FiniteGaloisIntermediateField K Ω) :
    Function.Injective (finiteAbsoluteNormalizationRingMap A K Ω E).toFun
def

finiteAbsoluteNormalizationPrime

L54 ↗
EtaleFundamentalGroups.Inertia.finiteAbsoluteNormalizationPrime
Documentation

The actual contraction of the chosen absolute normalization prime.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [Field K] [Field Ω]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsGalois K Ω]
Lean source · statement
def finiteAbsoluteNormalizationPrime
    (Q : Ideal (normalizationCommAlgCat A Ω))
    (E : FiniteGaloisIntermediateField K Ω) :
    Ideal (finiteAbsoluteNormalizationAlgebra A K Ω E)
theorem

finiteAbsoluteNormalizationPrime_isPrime

L64 ↗
EtaleFundamentalGroups.Inertia.finiteAbsoluteNormalizationPrime_isPrime
Documentation

The contracted ideal is prime because the actual coefficient map is a ring homomorphism.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [Field K] [Field Ω]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsGalois K Ω]
omit [IsFractionRing A K] [IsGalois K Ω] in
Lean source · statement
theorem finiteAbsoluteNormalizationPrime_isPrime
    (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsPrime]
    (E : FiniteGaloisIntermediateField K Ω) :
    (finiteAbsoluteNormalizationPrime A K Ω Q E).IsPrime
def

finiteAbsoluteNormalizationLocalization

L72 ↗
EtaleFundamentalGroups.Inertia.finiteAbsoluteNormalizationLocalization
Documentation

The actual localized finite normalization used by the ring-only finite inertia character. Its data are supplied by the native localization owner.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [Field K] [Field Ω]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsGalois K Ω]
Lean source · statement
def finiteAbsoluteNormalizationLocalization
    (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsPrime]
    (E : FiniteGaloisIntermediateField K Ω) : CommAlgCat.{w} A

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