English
If K/k is a Galois extension and L is an intermediate field of K/k, then the degree [L: k] equals the index of the fixing subgroup of L.
Русский
Если K/k — Галуа-расслоение, и L — промежуточное поле K/k, то [L: k] равно индексу фиксационной подгруппы L.
LaTeX
$$$\\operatorname{Module.finrank}_k L = L.fixingSubgroup.index$$$
Lean4
/-- If `K / k` is a Galois extension, `L` is an intermediate field of `K / k`, then `[L : k]`
as a natural number is equal to the index of the fixing subgroup of `L`. -/
theorem finrank_eq_fixingSubgroup_index (L : IntermediateField k K) [IsGalois k K] :
Module.finrank k L = L.fixingSubgroup.index :=
by
wlog hnfd : FiniteDimensional k L generalizing L
· rw [Module.finrank_of_infinite_dimensional hnfd]
by_contra! h
replace h : L.fixingSubgroup.FiniteIndex := ⟨h.symm⟩
obtain ⟨L', hfd, hL'⟩ := exists_lt_finrank_of_infinite_dimensional hnfd L.fixingSubgroup.index
let i := (liftAlgEquiv L').toLinearEquiv
replace hfd := i.finiteDimensional
rw [i.finrank_eq, this _ hfd] at hL'
exact (Subgroup.index_antitone <| fixingSubgroup_le <| IntermediateField.lift_le L').not_gt hL'
let E := normalClosure k L K
have hle : L ≤ E := by simpa only [fieldRange_val] using L.val.fieldRange_le_normalClosure
let L' := restrict hle
have h := Module.finrank_mul_finrank k ↥L' ↥E
classical
rw [← IsGalois.card_fixingSubgroup_eq_finrank L', ← IsGalois.card_aut_eq_finrank k E] at h
rw [← L'.fixingSubgroup.index_mul_card, Nat.mul_left_inj Finite.card_pos.ne'] at h
rw [(restrict_algEquiv hle).toLinearEquiv.finrank_eq, h, ← L'.map_fixingSubgroup_index K]
congr 2
exact lift_restrict hle
