NYLL
Module

ActualFiniteInertiaTowerTameValue.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteInertiaTowerTameValue
2 declarations indexed from sourceView source ↗

Module documentation

Canonical character squares for actual finite inertia restrictions

Actual surjectivity lifts each intrinsic finite inertia element to the original inertia. The proved restriction factor equation and the SAME canonical scalar normalization tower then give the n_F/n_E power square. Restriction through a common upper stage uses the already proved finite map composition.

Imports9
Imported by1

Declarations

theorem

actualFiniteInertiaTowerRestriction_tameValue

L39 ↗
EtaleFundamentalGroups.Inertia.actualFiniteInertiaTowerRestriction_tameValue
Documentation

The SAME finite canonical characters commute with the actual finite inertia restriction and the n_F/n_E power map in the ambient residue field.

Source context 4 commands

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

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 actualFiniteInertiaTowerRestriction_tameValue
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [hQ : Q.IsMaximal]
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F)
    (τ : (commAlgIdealInertiaGroup A (finiteAbsoluteNormalizationAlgebra A K L F)
      (finiteAbsoluteNormalizationPrime A K L Q F)).carrier) :
    actualFiniteCanonicalTameValue A K L Q E
        ((actualFiniteInertiaTowerRestriction (hQ := hQ.isPrime) A K L Q E F h).hom'.toFun τ) =
      actualFiniteCanonicalTameValue A K L Q F τ ^
        (actualFiniteStageTameOrder A K L Q F / actualFiniteStageTameOrder A K L Q E)
theorem

actualFiniteInertiaTowerRestriction_tameValue_trans

L57 ↗
EtaleFundamentalGroups.Inertia.actualFiniteInertiaTowerRestriction_tameValue_trans
Documentation

Through any common larger stage the same canonical character value has the direct n_H/n_E exponent, by the actual restriction composition law.

Source context 4 commands

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

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 actualFiniteInertiaTowerRestriction_tameValue_trans
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [hQ : Q.IsMaximal]
    (E F H : FiniteGaloisIntermediateField K L) (hEF : E ≤ F) (hFH : F ≤ H)
    (τ : (commAlgIdealInertiaGroup A (finiteAbsoluteNormalizationAlgebra A K L H)
      (finiteAbsoluteNormalizationPrime A K L Q H)).carrier) :
    actualFiniteCanonicalTameValue A K L Q E
        ((actualFiniteInertiaTowerRestriction (hQ := hQ.isPrime) A K L Q E F hEF).hom'.toFun
          ((actualFiniteInertiaTowerRestriction (hQ := hQ.isPrime) A K L Q F H hFH).hom'.toFun τ)) =
      actualFiniteCanonicalTameValue A K L Q H τ ^
        (actualFiniteStageTameOrder A K L Q H / actualFiniteStageTameOrder 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.