English
In a finite-dimensional Galois situation, the fixed field of the fixingSubgroup equals the original intermediate field: fixedField (fixingSubgroup K) = K.
Русский
При конечномерном Галуа-расширении фиксированное поле подгруппы фиксации равно исходному промежуточному полю.
LaTeX
$$$[\text{FiniteDimensional } F E] \Rightarrow \operatorname{fixedField}(\operatorname{fixingSubgroup}(K)) = K$$$
Lean4
theorem fixedField_fixingSubgroup [FiniteDimensional F E] [h : IsGalois F E] :
IntermediateField.fixedField (IntermediateField.fixingSubgroup K) = K :=
by
have K_le : K ≤ IntermediateField.fixedField (IntermediateField.fixingSubgroup K) :=
(IntermediateField.le_iff_le _ _).mpr le_rfl
suffices finrank K E = finrank (IntermediateField.fixedField (IntermediateField.fixingSubgroup K)) E by
exact (IntermediateField.eq_of_le_of_finrank_eq' K_le this).symm
classical
rw [IntermediateField.finrank_fixedField_eq_card, Nat.card_congr (IntermediateField.fixingSubgroupEquiv K).toEquiv]
exact (card_aut_eq_finrank K E).symm
