English
A neighborhood of the identity in Aut_K(L) corresponds to a finite extension E/K through its fixing subgroup.
Русский
Окрестность единицы в Aut_K(L) соответствуют конечному расширению E/K через фиксирующую подгруппу.
LaTeX
$$$s \\in \\mathcal{N}(1) \\iff \\exists E: IntermediateField K L,FinDim(K,E) \\land (E.fixingSubgroup) \\subseteq s$$$
Lean4
theorem krullTopology_mem_nhds_one_iff (K L : Type*) [Field K] [Field L] [Algebra K L] (s : Set (L ≃ₐ[K] L)) :
s ∈ 𝓝 1 ↔ ∃ E : IntermediateField K L, FiniteDimensional K E ∧ (E.fixingSubgroup : Set (L ≃ₐ[K] L)) ⊆ s :=
by
rw [GroupFilterBasis.nhds_one_eq]
constructor
· rintro ⟨-, ⟨-, ⟨E, fin, rfl⟩, rfl⟩, hE⟩
exact ⟨E, fin, hE⟩
· rintro ⟨E, fin, hE⟩
exact ⟨E.fixingSubgroup, ⟨E.fixingSubgroup, ⟨E, fin, rfl⟩, rfl⟩, hE⟩
