EtaleFundamentalGroups.Inertia.actualFiniteRawTameValue_tower
The two independently constructed raw values of the SAME original inertia element satisfy the literal finite local tower relation. The ratio witnesses, commuting square, residue fixedness and ambient triangle are all supplied by their original-input owners. No finite inertia action or roots carrier is opened.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v wLean source · full declaration
theorem actualFiniteRawTameValue_tower
(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]
(E F : FiniteGaloisIntermediateField K L) (h : E ≤ F)
(σ : actualNormalizationInertiaGroup A K L Q) :
letI := finiteAbsoluteNormalizationPrime_isPrime A K L Q E
letI := finiteAbsoluteNormalizationPrime_isPrime A K L Q F
letI := finiteAbsoluteNormalizationAlgebra_isDedekindDomain A K L F
letI := localizationAtPrime_isDiscreteValuationRing
(finiteAbsoluteNormalizationAlgebra A K L F)
(finiteAbsoluteNormalizationPrime A K L Q F)
(finiteAbsoluteNormalizationPrime_ne_bot A K L Q F)
∃ π : Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q E),
Irreducible π ∧
actualFiniteRawTameValue A K L Q E σ =
actualFiniteRawTameValue A K L Q F σ ^
((IsDiscreteValuationRing.addVal
(Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q F))).toFun
((actualFiniteNormalizationTowerLocalRingMap A K L Q E F h).toFun π)).toNat := by
let pE := finiteAbsoluteNormalizationPrime_isPrime A K L Q E
let pF := finiteAbsoluteNormalizationPrime_isPrime A K L Q F
let dF := finiteAbsoluteNormalizationAlgebra_isDedekindDomain A K L F
let vF := localizationAtPrime_isDiscreteValuationRing
(finiteAbsoluteNormalizationAlgebra A K L F)
(finiteAbsoluteNormalizationPrime A K L Q F)
(finiteAbsoluteNormalizationPrime_ne_bot A K L Q F)
obtain ⟨π, c, hπ, _, hc, hE⟩ := actualFiniteRawTameValue_exists_coefficient A K L Q E σ
obtain ⟨ρ, d, hρ, _, hd, hF⟩ := actualFiniteRawTameValue_exists_coefficient A K L Q F σ
refine ⟨π, hπ, ?_⟩
have hraw := uniformizerAmbientCoefficient_tower_addVal_of_ringHom
(Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q E))
(Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q F)) Q.ResidueField
(actualFiniteNormalizationTowerLocalRingMap A K L Q E F h)
(actualFiniteNormalizationTowerLocalRingMap_injective A K L Q E F h)
(actualFiniteInertiaLocalRingHom A K L Q E σ)
(actualFiniteInertiaLocalRingHom A K L Q F σ)
(actualFiniteInertiaLocalRingHom_tower A K L Q E F h σ)
(actualFiniteLocalResidueMap A K L Q E) (actualFiniteLocalResidueMap A K L Q F)
(actualFiniteLocalResidueMap_tower A K L Q E F h)
(actualFiniteLocalResidueMap_comp_inertia A K L Q F σ)
π hπ ρ hρ c d hc hd
exact hE.trans (hraw.trans (congrArg
(fun z : Q.ResidueField => z ^
((IsDiscreteValuationRing.addVal
(Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q F))).toFun
((actualFiniteNormalizationTowerLocalRingMap A K L Q E F h).toFun π)).toNat)
hF.symm))