Module

ActualFiniteRawTameValue.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteRawTameValue

3 declarations indexed from sourceView source ↗

Module documentation

Raw coefficient-ratio values of finite inertia

Constructs the ambient residue of a finite local uniformizer ratio and supplies its unit coefficient witness. Expresses the canonical tame coordinate as its normalization power.

Imports12

Imported by6

def

actualFiniteRawTameValue

L44 ↗

EtaleFundamentalGroups.Inertia.actualFiniteRawTameValue

Documentation

The ambient residue of an actual coefficient ratio σ(π)/π. The uniformizer and ratio are constructed in the literal finite local ring; this is the raw value, before the canonical e/n power is applied.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory RamificationTheory.HilbertRamification.DiscreteValuationRing
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

def actualFiniteRawTameValue (E : FiniteGaloisIntermediateField K L)
    (σ : actualNormalizationInertiaGroup A K L Q) : Q.ResidueField

theorem

actualFiniteRawTameValue_exists_coefficient

L64 ↗

EtaleFundamentalGroups.Inertia.actualFiniteRawTameValue_exists_coefficient

Documentation

The constructed raw scalar comes from an actual unit coefficient of an actual uniformizer. No roots carrier or normalized character is exposed in this interface, so two raw stages may be compared before normalization.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory RamificationTheory.HilbertRamification.DiscreteValuationRing
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 · full declaration

theorem actualFiniteRawTameValue_exists_coefficient
    (E : FiniteGaloisIntermediateField K L)
    (σ : actualNormalizationInertiaGroup A K L Q) :
    letI := finiteAbsoluteNormalizationPrime_isPrime A K L Q E
    ∃ π c : Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q E),
      Irreducible π ∧ IsUnit c ∧
      π * c = (actualFiniteInertiaLocalRingHom A K L Q E σ).toFun π ∧
      actualFiniteRawTameValue A K L Q E σ =
        (actualFiniteLocalResidueMap A K L Q E).toFun c := by
  let := finiteAbsoluteNormalizationPrime_isPrime A K L Q E
  let := finiteAbsoluteNormalizationAlgebra_isDedekindDomain A K L E
  let : IsDiscreteValuationRing
      (Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q E)) :=
    localizationAtPrime_isDiscreteValuationRing
      (finiteAbsoluteNormalizationAlgebra A K L E)
      (finiteAbsoluteNormalizationPrime A K L Q E)
      (finiteAbsoluteNormalizationPrime_ne_bot A K L Q E)
  let hπ := IsDiscreteValuationRing.exists_irreducible
    (Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q E))
  let hc := actualFiniteTameCoordinate_exists_coefficient A K L Q E σ hπ.choose hπ.choose_spec
  have hs := ringHomUniformizerCoefficient_unit_spec
    (Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q E))
    (actualFiniteInertiaLocalRingHom A K L Q E σ) hπ.choose hπ.choose_spec.ne_zero
    ⟨hc.choose, hc.choose_spec.1, hc.choose_spec.2.1⟩
  exact ⟨hπ.choose, ringHomUniformizerCoefficient
      (Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q E))
      (actualFiniteInertiaLocalRingHom A K L Q E σ) hπ.choose,
    hπ.choose_spec, hs.1, hs.2, rfl⟩

theorem

actualFiniteTameCoordinate_eq_raw_pow

L95 ↗

EtaleFundamentalGroups.Inertia.actualFiniteTameCoordinate_eq_raw_pow

Documentation

The SAME existing canonical coordinate is the e/n power of the actual raw coefficient scalar just constructed.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory RamificationTheory.HilbertRamification.DiscreteValuationRing
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_raw_pow
    (E : FiniteGaloisIntermediateField K L)
    (σ : actualNormalizationInertiaGroup A K L Q) :
    (((actualFiniteTameCoordinate A K L Q E).hom'.toFun σ).val).val =
      actualFiniteRawTameValue A K L Q E σ ^
        ((finiteAbsoluteNormalizationPrime A K L Q E).ramificationIdx A /
          actualFiniteStageTameOrder A K L Q E)

Module documentation

Raw coefficient-ratio values of finite inertia

Declarations

actualFiniteRawTameValue

actualFiniteRawTameValue_exists_coefficient

actualFiniteTameCoordinate_eq_raw_pow