ClassFieldTheory.lowerRamificationGroup_normal
Each lower ramification group is normal in the 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 lowerRamificationGroup_normal
(K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
(A : ValuationSubring L) (n : ℕ) :
(lowerRamificationGroup K A n).Normal where
conj_mem := by
intro σ hσ γ
change ∀ x : A,
(γ * σ * γ⁻¹) • x - x ∈ (IsLocalRing.maximalIdeal A) ^ (n + 1)
intro x
let e : A ≃+* A :=
MulSemiringAction.toRingAut (A.decompositionSubgroup K) A γ
have hmap :
e (σ • (γ⁻¹ • x) - (γ⁻¹ • x)) ∈
((IsLocalRing.maximalIdeal A) ^ (n + 1)).map e :=
Ideal.mem_map_of_mem e (hσ (γ⁻¹ • x))
have hstable :
γ • (σ • (γ⁻¹ • x) - (γ⁻¹ • x)) ∈
(IsLocalRing.maximalIdeal A) ^ (n + 1) := by
change γ • (σ • (γ⁻¹ • x) - (γ⁻¹ • x)) ∈
((IsLocalRing.maximalIdeal A) ^ (n + 1)).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