NYLL
Module

FiniteLevelNormalizationAlgebra.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteLevelNormalizationAlgebra
35 declarations indexed from sourceView source ↗

Module documentation

Native finite-normalization preimages before principal localization

An actual intermediate level is first regarded as its inherited A-subalgebra of L. The generic normalization owner then constructs the normalization and the preimage of the actual upper invariant algebra, without K/Galois data in that construction. No raw finite-level subalgebra producer is called here.

Imports9
Imported by7

Declarations

def

finiteLevelNormalizationSubalgebra

L41 ↗
EtaleFundamentalGroups.Inertia.finiteLevelNormalizationSubalgebra
Documentation

The original finite level with its inherited A-action, before any normalization is constructed. Restriction of scalars preserves its carrier.

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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
Lean source · statement
def finiteLevelNormalizationSubalgebra
    (E : FiniteGaloisIntermediateField K L) : Subalgebra A L
def

normalizationInertiaFixedCommAlgCat

L48 ↗
EtaleFundamentalGroups.Inertia.normalizationInertiaFixedCommAlgCat
Documentation

The native upper invariant algebra, with its original coefficient action.

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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
Lean source · statement
def normalizationInertiaFixedCommAlgCat : CommAlgCat.{w} A
def

normalizationInertiaFixedBaseMap

L52 ↗
EtaleFundamentalGroups.Inertia.normalizationInertiaFixedBaseMap
Documentation

The original coefficient map in the actual upper fixed algebra.

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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
Lean source · statement
def normalizationInertiaFixedBaseMap : A →+* normalizationInertiaFixedCommAlgCat A K L Q
theorem

normalizationInertiaFixedBaseMap_eq_algebraMap

L56 ↗
EtaleFundamentalGroups.Inertia.normalizationInertiaFixedBaseMap_eq_algebraMap
Documentation

The actual upper coefficient map is its native algebra map.

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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
Lean source · statement
theorem normalizationInertiaFixedBaseMap_eq_algebraMap :
    normalizationInertiaFixedBaseMap A K L Q =
      algebraMap A (normalizationInertiaFixedCommAlgCat A K L Q)
def

finiteLevelInertiaNormalizationAlgebra

L63 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationAlgebra
Documentation

The actual normalization preimage at a finite level, constructed in the lower A/L/subalgebra owner rather than from the raw held API.

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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
Lean source · statement
def finiteLevelInertiaNormalizationAlgebra
    (q : Ideal (normalizationCommAlgCat A L).carrier)
    (E : FiniteGaloisIntermediateField K L) : CommAlgCat.{w} A
def

finiteLevelInertiaNormalizationRingMap

L70 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationRingMap
Documentation

The actual native inclusion of the preimage into the upper fixed ring.

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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
Lean source · statement
def finiteLevelInertiaNormalizationRingMap
    (E : FiniteGaloisIntermediateField K L) :
    finiteLevelInertiaNormalizationAlgebra A K L Q E →+*
      normalizationInertiaFixedCommAlgCat A K L Q
def

finiteLevelInertiaNormalizationBaseMap

L78 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationBaseMap
Documentation

The original coefficients in the actual finite preimage algebra.

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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
Lean source · statement
def finiteLevelInertiaNormalizationBaseMap
    (E : FiniteGaloisIntermediateField K L) :
    A →+* finiteLevelInertiaNormalizationAlgebra A K L Q E
theorem

finiteLevelInertiaNormalizationRingMap_comp_base

L85 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationRingMap_comp_base
Documentation

The native finite preimage map satisfies its original coefficient square.

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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
Lean source · statement
theorem finiteLevelInertiaNormalizationRingMap_comp_base
    (E : FiniteGaloisIntermediateField K L) :
    (finiteLevelInertiaNormalizationRingMap A K L Q E).comp
        (finiteLevelInertiaNormalizationBaseMap A K L Q E) =
      normalizationInertiaFixedBaseMap A K L Q
theorem

finiteLevelInertiaNormalizationBaseMap_eq_algebraMap

L94 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationBaseMap_eq_algebraMap
Documentation

The finite preimage coefficient map is the actual native algebra map.

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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
Lean source · statement
theorem finiteLevelInertiaNormalizationBaseMap_eq_algebraMap
    (E : FiniteGaloisIntermediateField K L) :
    finiteLevelInertiaNormalizationBaseMap A K L Q E =
      algebraMap A (finiteLevelInertiaNormalizationAlgebra A K L Q E)
def

normalizationInertiaFixedNativePrime

L102 ↗
EtaleFundamentalGroups.Inertia.normalizationInertiaFixedNativePrime
Documentation

The literal contraction to the native upper fixed algebra.

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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
Lean source · statement
def normalizationInertiaFixedNativePrime : Ideal (normalizationInertiaFixedCommAlgCat A K L Q)
def

finiteLevelInertiaNormalizationPrime

L106 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationPrime
Documentation

The literal further contraction to the actual finite preimage algebra.

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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
Lean source · statement
def finiteLevelInertiaNormalizationPrime
    (E : FiniteGaloisIntermediateField K L) :
    Ideal (finiteLevelInertiaNormalizationAlgebra A K L Q E)
def

finiteLevelInertiaPrincipalAlgebra

L115 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaPrincipalAlgebra
Documentation

The actual principal stage, constructed before its étaleness is stated.

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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
Lean source · statement
def finiteLevelInertiaPrincipalAlgebra
    (E : FiniteGaloisIntermediateField K L)
    (f : finiteLevelInertiaNormalizationAlgebra A K L Q E) : CommAlgCat.{w} A
theorem

finiteLevelInertiaNormalizationBaseMap_eq_coefficient

L121 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationBaseMap_eq_coefficient
Documentation

The finite native base map, stated through its computed coefficient map.

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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
Lean source · statement
theorem finiteLevelInertiaNormalizationBaseMap_eq_coefficient
    (E : FiniteGaloisIntermediateField K L) :
    finiteLevelInertiaNormalizationBaseMap A K L Q E =
      commAlgCoefficientMap (finiteLevelInertiaNormalizationAlgebra A K L Q E)
theorem

finiteLevelInertiaNormalizationRingMap_injective

L131 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationRingMap_injective
Documentation

The actual finite normalization preimage inclusion is injective. This is supplied by the native subtype proof before K/Galois data appear.

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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
Lean source · statement
theorem finiteLevelInertiaNormalizationRingMap_injective
    (E : FiniteGaloisIntermediateField K L) :
    Function.Injective (finiteLevelInertiaNormalizationRingMap A K L Q E).toFun
theorem

normalizationInertiaFixedCommAlgCat_isDomain

L139 ↗
EtaleFundamentalGroups.Inertia.normalizationInertiaFixedCommAlgCat_isDomain
Documentation

The actual upper fixed ring has the domain property of the native normalization subring of L.

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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
Lean source · statement
theorem normalizationInertiaFixedCommAlgCat_isDomain :
    IsDomain (normalizationInertiaFixedCommAlgCat A K L Q)
theorem

normalizationInertiaFixedNativePrime_isPrime

L146 ↗
EtaleFundamentalGroups.Inertia.normalizationInertiaFixedNativePrime_isPrime
Documentation

Primality is transported by the actual upper inclusion.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
theorem normalizationInertiaFixedNativePrime_isPrime :
    (normalizationInertiaFixedNativePrime A K L Q).IsPrime
theorem

finiteLevelInertiaNormalizationPrime_isPrime

L151 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationPrime_isPrime
Documentation

Primality is transported by the actual finite preimage inclusion.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
theorem finiteLevelInertiaNormalizationPrime_isPrime
    (E : FiniteGaloisIntermediateField K L) :
    (finiteLevelInertiaNormalizationPrime A K L Q E).IsPrime
def

normalizationInertiaFixedLocalizationBaseMap

L159 ↗
EtaleFundamentalGroups.Inertia.normalizationInertiaFixedLocalizationBaseMap
Documentation

The actual coefficient map into the native upper prime localization.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
def normalizationInertiaFixedLocalizationBaseMap :
    A →+* inertiaInvariantPrimeLocalizationAlgebra A K L Q
theorem

normalizationInertiaFixedLocalizationBaseMap_eq_upperBase

L169 ↗
EtaleFundamentalGroups.Inertia.normalizationInertiaFixedLocalizationBaseMap_eq_upperBase
Documentation

The native coefficient construction is the already constructed original upper localization base map, with its same native source and target.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
theorem normalizationInertiaFixedLocalizationBaseMap_eq_upperBase :
    normalizationInertiaFixedLocalizationBaseMap A K L Q =
      (inertiaInvariantPrimeLocalizationBaseMap A K L Q :
        A →+* inertiaInvariantPrimeLocalizationAlgebra A K L Q)
theorem

normalizationInertiaFixedLocalizationBaseMap_eq_coefficient

L176 ↗
EtaleFundamentalGroups.Inertia.normalizationInertiaFixedLocalizationBaseMap_eq_coefficient
Documentation

The computed upper base map is the coefficient map stored by its actual native algebra object.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
theorem normalizationInertiaFixedLocalizationBaseMap_eq_coefficient :
    normalizationInertiaFixedLocalizationBaseMap A K L Q =
      commAlgCoefficientMap (inertiaInvariantPrimeLocalizationAlgebra A K L Q)
def

finiteLevelInertiaPrincipalBaseMap

L186 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaPrincipalBaseMap
Documentation

The original coefficients in the actual principal stage, retained without opening the coefficient action in later ring-map scopes.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
def finiteLevelInertiaPrincipalBaseMap
    (E : FiniteGaloisIntermediateField K L)
    (d : finiteLevelInertiaNormalizationAlgebra A K L Q E) :
    A →+* finiteLevelInertiaPrincipalAlgebra A K L Q E d
theorem

finiteLevelInertiaPrincipalBaseMap_eq_coefficient

L196 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaPrincipalBaseMap_eq_coefficient
Documentation

The native principal tower gives the actual stored coefficient map.

Source context 8 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
omit [Q.IsPrime] in
Lean source · statement
theorem finiteLevelInertiaPrincipalBaseMap_eq_coefficient
    (E : FiniteGaloisIntermediateField K L)
    (d : finiteLevelInertiaNormalizationAlgebra A K L Q E) :
    finiteLevelInertiaPrincipalBaseMap A K L Q E d =
      commAlgCoefficientMap (finiteLevelInertiaPrincipalAlgebra A K L Q E d)
def

normalizationInertiaFixedLocalizationCoefficientMap

L217 ↗
EtaleFundamentalGroups.Inertia.normalizationInertiaFixedLocalizationCoefficientMap
Documentation

The native coefficient map in the already constructed actual upper localization, retained before its original-data applications.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
def normalizationInertiaFixedLocalizationCoefficientMap :
    normalizationInertiaFixedCommAlgCat A K L Q →+*
      inertiaInvariantPrimeLocalizationAlgebra A K L Q
def

finiteLevelInertiaNormalizationToUpperMap

L227 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationToUpperMap
Documentation

The actual coefficient map from the finite normalization preimage to the upper localization, constructed before a principal source is introduced.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
def finiteLevelInertiaNormalizationToUpperMap
    (E : FiniteGaloisIntermediateField K L) :
    finiteLevelInertiaNormalizationAlgebra A K L Q E →+*
      inertiaInvariantPrimeLocalizationAlgebra A K L Q
theorem

normalizationInertiaFixedLocalizationCoefficientMap_injective

L236 ↗
EtaleFundamentalGroups.Inertia.normalizationInertiaFixedLocalizationCoefficientMap_injective
Documentation

The existing native prime coefficient map is injective on the actual upper fixed domain. The principal source does not occur in this scope.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
theorem normalizationInertiaFixedLocalizationCoefficientMap_injective :
    Function.Injective (normalizationInertiaFixedLocalizationCoefficientMap A K L Q).toFun
theorem

finiteLevelInertiaNormalizationToUpperMap_injective

L247 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationToUpperMap_injective
Documentation

The actual finite-to-upper coefficient map is injective.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
theorem finiteLevelInertiaNormalizationToUpperMap_injective
    (E : FiniteGaloisIntermediateField K L) :
    Function.Injective (finiteLevelInertiaNormalizationToUpperMap A K L Q E).toFun
theorem

finiteLevelInertiaNormalizationToUpperMap_isUnit

L255 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationToUpperMap_isUnit
Documentation

The original contracted-prime condition supplies the actual unit needed by the principal lift. The upper fixed ring is closed here.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
theorem finiteLevelInertiaNormalizationToUpperMap_isUnit
    (E : FiniteGaloisIntermediateField K L)
    (d : finiteLevelInertiaNormalizationAlgebra A K L Q E)
    (hd : d ∉ finiteLevelInertiaNormalizationPrime A K L Q E) :
    IsUnit ((finiteLevelInertiaNormalizationToUpperMap A K L Q E).toFun d)
theorem

finiteLevelInertiaNormalizationToUpperMap_comp_base

L270 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationToUpperMap_comp_base
Documentation

The actual coefficient map preserves the original base map, by the already proved finite-normalization coefficient square.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
theorem finiteLevelInertiaNormalizationToUpperMap_comp_base
    (E : FiniteGaloisIntermediateField K L) :
    (finiteLevelInertiaNormalizationToUpperMap A K L Q E).comp
        (finiteLevelInertiaNormalizationBaseMap A K L Q E) =
      normalizationInertiaFixedLocalizationBaseMap A K L Q
def

finiteLevelInertiaPrincipalRingInclusion

L284 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaPrincipalRingInclusion
Documentation

The actual principal-stage native map into the original upper localization. Only the original contracted-prime denominator proof is used.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
def finiteLevelInertiaPrincipalRingInclusion
    (E : FiniteGaloisIntermediateField K L)
    (d : finiteLevelInertiaNormalizationAlgebra A K L Q E)
    (hd : d ∉ finiteLevelInertiaNormalizationPrime A K L Q E) :
    finiteLevelInertiaPrincipalAlgebra A K L Q E d →+*
      inertiaInvariantPrimeLocalizationAlgebra A K L Q
theorem

finiteLevelInertiaPrincipalRingInclusion_comp_base

L298 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaPrincipalRingInclusion_comp_base
Documentation

The actual native principal square follows from the one coefficient lift equation and the already proved finite-normalization base square.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
theorem finiteLevelInertiaPrincipalRingInclusion_comp_base
    (E : FiniteGaloisIntermediateField K L)
    (d : finiteLevelInertiaNormalizationAlgebra A K L Q E)
    (hd : d ∉ finiteLevelInertiaNormalizationPrime A K L Q E) :
    (finiteLevelInertiaPrincipalRingInclusion A K L Q E d hd).comp
        (finiteLevelInertiaPrincipalBaseMap A K L Q E d) =
      normalizationInertiaFixedLocalizationBaseMap A K L Q
theorem

finiteLevelInertiaPrincipalRingInclusion_injective

L324 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaPrincipalRingInclusion_injective
Documentation

The actual principal-stage map is injective by the native coefficient injection and the existing localization argument in its sparse owner.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
theorem finiteLevelInertiaPrincipalRingInclusion_injective
    (E : FiniteGaloisIntermediateField K L)
    (d : finiteLevelInertiaNormalizationAlgebra A K L Q E)
    (hd : d ∉ finiteLevelInertiaNormalizationPrime A K L Q E) :
    Function.Injective (finiteLevelInertiaPrincipalRingInclusion A K L Q E d hd).toFun
def

finiteLevelInertiaNormalizationLocalizationAlgebra

L338 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationLocalizationAlgebra
Documentation

The actual prime-localized finite normalization stage, with its existing native coefficient action constructed before it is consumed.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
def finiteLevelInertiaNormalizationLocalizationAlgebra
    (E : FiniteGaloisIntermediateField K L) : CommAlgCat.{w} A
def

finiteLevelInertiaNormalizationLocalizationCoefficientMap

L346 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationLocalizationCoefficientMap
Documentation

The native coefficient map in the actual finite prime localization.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
def finiteLevelInertiaNormalizationLocalizationCoefficientMap
    (E : FiniteGaloisIntermediateField K L) :
    finiteLevelInertiaNormalizationAlgebra A K L Q E →+*
      finiteLevelInertiaNormalizationLocalizationAlgebra A K L Q E
def

finiteLevelInertiaNormalizationLocalizationRingInclusion

L357 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationLocalizationRingInclusion
Documentation

The actual native localRingHom from the finite contracted prime to the original upper invariant localization.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
def finiteLevelInertiaNormalizationLocalizationRingInclusion
    (E : FiniteGaloisIntermediateField K L) :
    finiteLevelInertiaNormalizationLocalizationAlgebra A K L Q E →+*
      inertiaInvariantPrimeLocalizationAlgebra A K L Q
theorem

finiteLevelInertiaNormalizationLocalizationRingInclusion_comp_coefficient

L371 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationLocalizationRingInclusion_comp_coefficient
Documentation

The existing native localRingHom coefficient equation on the actual finite and upper objects. No localization square is assumed.

Source context 7 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) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
variable (Q : Ideal (integralClosure A L))
variable [Q.IsPrime]
Lean source · statement
theorem finiteLevelInertiaNormalizationLocalizationRingInclusion_comp_coefficient
    (E : FiniteGaloisIntermediateField K L) :
    (finiteLevelInertiaNormalizationLocalizationRingInclusion A K L Q E).comp
        (finiteLevelInertiaNormalizationLocalizationCoefficientMap A K L Q E) =
      (normalizationInertiaFixedLocalizationCoefficientMap A K L Q).comp
        (finiteLevelInertiaNormalizationRingMap A K L Q E)

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