English
For any L ∈ IntermediateField k K, the fixed field of L.fixingSubgroup equals L itself when IsGalois holds.
Русский
Для любой L ∈ IntermediateField k K, при выполнении IsGalois, фиксированное поле L.fixingSubgroup равно самому L.
LaTeX
$$$ IntermediateField.fixedField L.fixingSubgroup = L $$$
Lean4
theorem fixedField_fixingSubgroup (L : IntermediateField k K) [IsGalois k K] :
IntermediateField.fixedField L.fixingSubgroup = L :=
by
apply le_antisymm
· intro x hx
rw [IntermediateField.mem_fixedField_iff] at hx
have mem : x ∈ (adjoin L { x }).1 := subset_adjoin _ _ rfl
have : IntermediateField.fixedField (⊤ : Subgroup ((adjoin L { x }) ≃ₐ[L] (adjoin L { x }))) = ⊥ :=
(IsGalois.tfae.out 0 1).mp (by infer_instance)
have : ⟨x, mem⟩ ∈ (⊥ : IntermediateField L (adjoin L { x })) :=
by
rw [← this, IntermediateField.mem_fixedField_iff]
intro f _
rcases restrictNormalHom_surjective K f with ⟨σ, hσ⟩
apply Subtype.val_injective
rw [← hσ, restrictNormalHom_apply (adjoin L { x }).1 σ ⟨x, mem⟩]
have := hx ((IntermediateField.fixingSubgroupEquiv L).symm σ)
simpa only [SetLike.coe_mem, true_implies]
rcases IntermediateField.mem_bot.mp this with ⟨y, hy⟩
obtain ⟨rfl⟩ : y = x := congrArg Subtype.val hy
exact y.2
· exact (IntermediateField.le_iff_le L.fixingSubgroup L).mpr le_rfl
