RamificationTheory.HilbertRamification.ValuationSubring.henselianResidueAction_restrictNormal_eq_one
Trivial residue action remains trivial after restriction to an intermediate Galois extension, with the canonical residue-field maps of the chosen valuations.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace RamificationTheory.HilbertRamification.ValuationSubring
open IsLocalRing
variable {K L Ω Γ Δ Θ : Type*} [Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω] [IsScalarTower K L Ω]
[IsGalois K L] [IsGalois K Ω]
[LinearOrderedCommGroupWithZero Γ] [LinearOrderedCommGroupWithZero Δ]
[LinearOrderedCommGroupWithZero Θ]
(v : _root_.Valuation K Γ) (w : _root_.Valuation L Δ) (z : _root_.Valuation Ω Θ)
[v.HasExtension w] [w.HasExtension z] [v.HasExtension z]
[HenselianRing v.valuationSubring (maximalIdeal v.valuationSubring)]Lean source · statement
theorem henselianResidueAction_restrictNormal_eq_one
(σ : Gal(Ω/K)) (hσ : henselianResidueAction v z σ = 1) :
henselianResidueAction v w (σ.restrictNormal L) = 1