TameAbhyankar.bookExponentialValueSubgroup_eq_sup_iSup_zmultiples_of_radical_family
A finite family of prime-to-the-residue-characteristic radicals which generates the field also generates its value group.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations
open scoped IntermediateFieldLean source · statement
theorem bookExponentialValueSubgroup_eq_sup_iSup_zmultiples_of_radical_family
{K L : Type u} [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L]
(v : LubinTate.Valuations.ExponentialValuation K)
(w : LubinTate.Valuations.ExponentialValuation L)
(hExt : ∀ a : K, w (algebraMap K L a) = v a)
(hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
(LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
(hp : PositiveResidueCharacteristic v)
(hres : Function.Surjective (tameResidueFieldMap v w hExt))
(r : ℕ) (m : Fin r → ℕ) (a : Fin r → K) (alpha : Fin r → L)
(hmpos : ∀ i, 0 < m i)
(hmcop : ∀ i, Nat.Coprime (m i) (residueCharacteristic v))
(hpow : ∀ i, alpha i ^ m i = algebraMap K L (a i))
(hgen : IntermediateField.adjoin K (Set.range alpha) = ⊤) :
exponentialValueSubgroup w =
exponentialValueSubgroup v ⊔
⨆ i, AddSubgroup.zmultiples (w (alpha i)).untop₀