Module

FiniteLevelInvariantRingComparison.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteLevelInvariantRingComparison

3 declarations indexed from sourceView source ↗

Module documentation

Actual finite-stage invariant ring comparison

The existing native finite-normalization diagram supplies injectivity, equivariance and the full inertia image. The ring-only preimage theorem therefore identifies the already constructed normalization-preimage stage with the actual finite inertia-fixed ring. Neither the old dense fixed- subalgebra equality nor a new comparison assumption is used.

Imports3

Imported by1

Nyll.EtaleFundamentalGroups.Inertia.All

def

finiteLevelNativeInertiaFixedRing

L37 ↗

EtaleFundamentalGroups.Inertia.finiteLevelNativeInertiaFixedRing

Documentation

The actual finite inertia-fixed ring, computed from the native finite normalization and its prescribed original 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) (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]
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [Q.IsPrime]

Lean source · statement

def finiteLevelNativeInertiaFixedRing (E : FiniteGaloisIntermediateField K L) :
    CommRingCat.{w}

def

finiteLevelInertiaNormalizationFixedEquiv

L44 ↗

EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationFixedEquiv

Documentation

The actual finite preimage is the finite inertia-fixed ring. All three inputs to the ring-only comparison are supplied by original-data theorems.

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]
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [Q.IsPrime]

Lean source · statement

def finiteLevelInertiaNormalizationFixedEquiv
    (E : FiniteGaloisIntermediateField K L) :
    (finiteLevelInertiaNormalizationAlgebra A K L Q E).carrier ≃+*
      (finiteLevelNativeInertiaFixedRing A K L Q E).carrier

theorem

finiteLevelInertiaNormalizationFixedEquiv_comp_subtype

L55 ↗

EtaleFundamentalGroups.Inertia.finiteLevelInertiaNormalizationFixedEquiv_comp_subtype

Documentation

The actual comparison preserves each lower normalization coefficient.

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]
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [Q.IsPrime]

Lean source · statement

theorem finiteLevelInertiaNormalizationFixedEquiv_comp_subtype
    (E : FiniteGaloisIntermediateField K L) :
    ((finiteNormalizationActionDiagram A K L E).lowerInertiaFixedSubring
        (finiteAbsoluteNormalizationPrime A K L Q E)).subtype.comp
        (finiteLevelInertiaNormalizationFixedEquiv A K L Q E).toRingHom =
      ((finiteNormalizationActionDiagram A K L E).inertiaFixedPreimageSubring Q).subtype

Module documentation

Actual finite-stage invariant ring comparison

Declarations

finiteLevelNativeInertiaFixedRing

finiteLevelInertiaNormalizationFixedEquiv

finiteLevelInertiaNormalizationFixedEquiv_comp_subtype