RamificationTheory.HilbertRamification.Higher.valuationSubringAutOfUniqueExtension_integerMap_restrictNormal
Acting on an integral element from a normal intermediate field and then viewing it in the top valuation ring agrees with first restricting the Galois automorphism and acting in the intermediate valuation ring.
Source context 16 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w x y z
namespace RamificationTheory.HilbertRamification
namespace Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} {M : Type y}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra K M] [Algebra L M]
variable [IsScalarTower K L M] [Normal K L]
variable {base : DVF.{u, v} K}
variable {middle : DVF.{w, x} L}
variable {target : DVF.{y, z} M}
variable [base.valuation.HasExtension middle.valuation]
variable [middle.valuation.HasExtension target.valuation]
variable [base.valuation.HasExtension target.valuation]Lean source · statement
theorem
valuationSubringAutOfUniqueExtension_integerMap_restrictNormal
(hmiddle :
RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension
base middle)
(htarget :
RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension
base target)
(σ : Gal(M/K)) (a : middle.valuationSubring) :
valuationSubringAutOfUniqueExtension
(base := base) (target := target) htarget σ
(integerMap middle target a) =
integerMap middle target
(valuationSubringAutOfUniqueExtension
(base := base) (target := middle) hmiddle
(σ.restrictNormal L) a)