Module

ActualFiniteCanonicalTameValue.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteCanonicalTameValue

3 declarations indexed from sourceView source ↗

Module documentation

Ambient scalar values of finite canonical characters

Projects the SAME finite canonical character and actual residue-root embedding to their ambient residue scalar. The one-stage construction closes the finite root group before the finite inertia tower compares two stages.

Imports10

Imported by2

def

actualFiniteCanonicalTameValue

L41 ↗

EtaleFundamentalGroups.Inertia.actualFiniteCanonicalTameValue

Documentation

The ambient residue value of the existing finite canonical character, embedded by the existing actual residue-root map.

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] [IsDomain A] [IsDiscreteValuationRing 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 actualFiniteCanonicalTameValue
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [Q.IsMaximal]
    (E : FiniteGaloisIntermediateField K L)
    (τ : (commAlgIdealInertiaGroup A (finiteAbsoluteNormalizationAlgebra A K L E)
      (finiteAbsoluteNormalizationPrime A K L Q E)).carrier) : Q.ResidueField

theorem

actualFiniteCanonicalTameValue_restriction

L51 ↗

EtaleFundamentalGroups.Inertia.actualFiniteCanonicalTameValue_restriction

Documentation

On an actual original inertia lift, this scalar is the SAME ambient coordinate already used in the canonical finite-stage tower theorem.

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] [IsDomain A] [IsDiscreteValuationRing 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

theorem actualFiniteCanonicalTameValue_restriction
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [Q.IsMaximal]
    (E : FiniteGaloisIntermediateField K L)
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
    actualFiniteCanonicalTameValue A K L Q E
        ((actualFiniteInertiaRestriction A K L Q E).hom'.toFun σ) =
      ((actualFiniteTameCoordinate A K L Q E).hom'.toFun σ).val.val

theorem

actualFiniteCanonicalTameValue_restriction_normalizationMap

L62 ↗

EtaleFundamentalGroups.Inertia.actualFiniteCanonicalTameValue_restriction_normalizationMap

Documentation

The same finite canonical value on an actual inertia lift equals the already constructed raw scalar after its actual e/n normalization. The ambient root carrier is closed in this one-stage comparison.

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] [IsDomain A] [IsDiscreteValuationRing 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

theorem actualFiniteCanonicalTameValue_restriction_normalizationMap
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [Q.IsMaximal]
    (E : FiniteGaloisIntermediateField K L)
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
    actualFiniteCanonicalTameValue A K L Q E
        ((actualFiniteInertiaRestriction A K L Q E).hom'.toFun σ) =
      (actualFiniteTameNormalizationMap A K L Q E).toFun
        (actualFiniteRawTameValue A K L Q E σ)

Module documentation

Ambient scalar values of finite canonical characters

Declarations

actualFiniteCanonicalTameValue

actualFiniteCanonicalTameValue_restriction

actualFiniteCanonicalTameValue_restriction_normalizationMap