English
The filter basis on Aut_K(L) is given by Gal(L/E) for finite E/K and provides a neighborhood basis at identity.
Русский
Фильтр-база на Aut_K(L) задаётся Gal(L/E) для конечных E/K и образует окрестность у единицы.
LaTeX
$$$galBasis(K,L)\\;:\\; FilterBasis(Aut_K(L))$ with sets $(Gal(L/E))$ for finite E/K$$
Lean4
/-- Given a field extension `L/K`, `galBasis K L` is the filter basis on `L ≃ₐ[K] L` whose sets
are `Gal(L/E)` for intermediate fields `E` with `E/K` finite dimensional. -/
def galBasis (K L : Type*) [Field K] [Field L] [Algebra K L] : FilterBasis (L ≃ₐ[K] L)
where
sets := (fun g => g.carrier) '' fixedByFinite K L
nonempty := ⟨⊤, ⊤, top_fixedByFinite, rfl⟩
inter_sets := by
rintro _ _ ⟨_, ⟨E1, h_E1, rfl⟩, rfl⟩ ⟨_, ⟨E2, h_E2, rfl⟩, rfl⟩
have : FiniteDimensional K E1 := h_E1
have : FiniteDimensional K E2 := h_E2
refine ⟨(E1 ⊔ E2).fixingSubgroup.carrier, ⟨_, ⟨_, E1.finiteDimensional_sup E2, rfl⟩, rfl⟩, ?_⟩
exact Set.subset_inter (E1.fixingSubgroup_le le_sup_left) (E2.fixingSubgroup_le le_sup_right)
