Module

ActualFiniteTameCoordinateTower.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteTameCoordinateTower

3 declarations indexed from sourceView source ↗

Module documentation

Tower compatibility of canonical tame coordinates

Proves compatibility of finite tame coordinates with the power maps determined by tame-order ratios. Deduces independence of the finite stage when tame orders agree.

Imports15

Imported by3

theorem

actualFiniteTameNormalizationMap_tower

EtaleFundamentalGroups.Inertia.actualFiniteTameNormalizationMap_tower

Documentation

Apply the actual normalization operations to the proved raw scalar tower. Once the raw values and their equation are retained, the original inertia element is cleared before either e/n expression is opened.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory RamificationTheory.HilbertRamification
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]
  (Q : Ideal (normalizationCommAlgCat A L)) [Q.IsMaximal]

Lean source · statement

theorem actualFiniteTameNormalizationMap_tower
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F)
    (σ : actualNormalizationInertiaGroup A K L Q) :
    (actualFiniteTameNormalizationMap A K L Q E).toFun
        (actualFiniteRawTameValue A K L Q E σ) =
      (actualFiniteTameNormalizationMap A K L Q F).toFun
        (actualFiniteRawTameValue A K L Q F σ) ^
          (actualFiniteStageTameOrder A K L Q F / actualFiniteStageTameOrder A K L Q E)

theorem

actualFiniteTameCoordinate_tower

EtaleFundamentalGroups.Inertia.actualFiniteTameCoordinate_tower

Documentation

The SAME canonical ambient residue coordinate is compatible with the actual finite tower, with exponent the ratio of the actual tame orders. All restriction, residue, ramification and normalization inputs are proved from the original data, rather than supplied as comparison hypotheses.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory RamificationTheory.HilbertRamification
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]
  (Q : Ideal (normalizationCommAlgCat A L)) [Q.IsMaximal]

Lean source · statement

theorem actualFiniteTameCoordinate_tower
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F)
    (σ : actualNormalizationInertiaGroup A K L Q) :
    (((actualFiniteTameCoordinate A K L Q E).hom'.toFun σ).val).val =
      (((actualFiniteTameCoordinate A K L Q F).hom'.toFun σ).val).val ^
        (actualFiniteStageTameOrder A K L Q F / actualFiniteStageTameOrder A K L Q E)

theorem

actualFiniteTameCoordinate_eq_of_tameOrder_eq

EtaleFundamentalGroups.Inertia.actualFiniteTameCoordinate_eq_of_tameOrder_eq

Documentation

A finite stage representing a given tame order does not affect the SAME canonical ambient coordinate. The actual finite Galois compositum is used as a common upper stage, so no choice or comparison datum is assumed.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory RamificationTheory.HilbertRamification
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]
  (Q : Ideal (normalizationCommAlgCat A L)) [Q.IsMaximal]

Lean source · statement

theorem actualFiniteTameCoordinate_eq_of_tameOrder_eq
    (E F : FiniteGaloisIntermediateField K L)
    (hn : actualFiniteStageTameOrder A K L Q E = actualFiniteStageTameOrder A K L Q F)
    (σ : actualNormalizationInertiaGroup A K L Q) :
    (((actualFiniteTameCoordinate A K L Q E).hom'.toFun σ).val).val =
      (((actualFiniteTameCoordinate A K L Q F).hom'.toFun σ).val).val