ClassFieldTheory.realLowerRamificationGroup_normal
Each real lower ramification group is normal in its decomposition group.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTheory
universe u vLean source · full declaration
theorem realLowerRamificationGroup_normal
(K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
(A : ValuationSubring L) (s : ℝ) :
(realLowerRamificationGroup K A s).Normal where
conj_mem := by
intro σ hσ γ
change ∀ x : A,
(γ * σ * γ⁻¹) • x - x ∈
(IsLocalRing.maximalIdeal A) ^ (Int.ceil (s + 1)).toNat
intro x
let e : A ≃+* A :=
MulSemiringAction.toRingAut (A.decompositionSubgroup K) A γ
have hmap :
e (σ • (γ⁻¹ • x) - (γ⁻¹ • x)) ∈
((IsLocalRing.maximalIdeal A) ^ (Int.ceil (s + 1)).toNat).map e :=
Ideal.mem_map_of_mem e (hσ (γ⁻¹ • x))
have hstable :
γ • (σ • (γ⁻¹ • x) - (γ⁻¹ • x)) ∈
(IsLocalRing.maximalIdeal A) ^ (Int.ceil (s + 1)).toNat := by
change γ • (σ • (γ⁻¹ • x) - (γ⁻¹ • x)) ∈
((IsLocalRing.maximalIdeal A) ^ (Int.ceil (s + 1)).toNat).map e at hmap
rwa [Ideal.map_pow, IsLocalRing.map_ringEquiv_maximalIdeal] at hmap
simpa only [smul_sub, mul_smul, smul_inv_smul] using hstable