English
If L/K is normal, a neighborhood of identity corresponds to a finite E with Normality and its fixing subgroup inside s.
Русский
Если расширение нормальное, окрестность единицы соответствует конечному E с нормальностью и фиксацией подгруппы внутри s.
LaTeX
$$$s \\in \\mathcal{N}(1) \\iff \\exists E: IntermediateField K L, FinDim(K,E) \\land Normal(K,E) \\land (E.fixingSubgroup) \\subseteq s$$$
Lean4
theorem krullTopology_mem_nhds_one_iff_of_normal (K L : Type*) [Field K] [Field L] [Algebra K L] [Normal K L]
(s : Set (L ≃ₐ[K] L)) :
s ∈ 𝓝 1 ↔
∃ E : IntermediateField K L, FiniteDimensional K E ∧ Normal K E ∧ (E.fixingSubgroup : Set (L ≃ₐ[K] L)) ⊆ s :=
by
rw [krullTopology_mem_nhds_one_iff]
refine ⟨fun ⟨E, _, hE⟩ ↦ ?_, fun ⟨E, hE⟩ ↦ ⟨E, hE.1, hE.2.2⟩⟩
use (IntermediateField.normalClosure K E L)
simp only [normalClosure.is_finiteDimensional K E L, normalClosure.normal K E L, true_and]
exact le_trans (E.fixingSubgroup_antitone E.le_normalClosure) hE
