English
For a finite extension E/K inside L, the Gal(L/E) subgroup is an open subgroup of Aut_K(L).
Русский
Для конечного расширения E/K внутри L подгруппа Gal(L/E) является открытой подгруппой Aut_K(L).
LaTeX
$$$IsOpen\\ (E.fixingSubgroup : Set (L \\simeq_K L))$$$
Lean4
/-- Let `L/E/K` be a tower of fields with `E/K` finite. Then `Gal(L/E)` is an open subgroup of
`L ≃ₐ[K] L`. -/
theorem fixingSubgroup_isOpen {K L : Type*} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L)
[FiniteDimensional K E] : IsOpen (E.fixingSubgroup : Set (L ≃ₐ[K] L)) :=
by
have h_basis : E.fixingSubgroup.carrier ∈ galGroupBasis K L := ⟨E.fixingSubgroup, ⟨E, ‹_›, rfl⟩, rfl⟩
have h_nhds := GroupFilterBasis.mem_nhds_one (galGroupBasis K L) h_basis
exact Subgroup.isOpen_of_mem_nhds _ h_nhds
