English
Let L/K be a field extension with L algebraic over K. The Krull topology on the group of K-algebra automorphisms of L is a Hausdorff topology.
Русский
Пусть L/K — алгебраическое поле. Крульова топология на группе K-алгебрам automorphisms L является Хаусдорфовой.
LaTeX
$$$\\text{The Krull topology on } \\mathrm{Aut}_K(L) \\text{ is Hausdorff.}$$$
Lean4
/-- If `L/K` is an algebraic extension, then the Krull topology on `L ≃ₐ[K] L` is Hausdorff. -/
theorem krullTopology_t2 {K L : Type*} [Field K] [Field L] [Algebra K L] [Algebra.IsIntegral K L] :
T2Space (L ≃ₐ[K] L) :=
{
t2 := fun f g hfg => by
let φ := f⁻¹ * g
obtain ⟨x, hx⟩ := DFunLike.exists_ne hfg
have hφx : φ x ≠ x := by
apply ne_of_apply_ne f
change f (f.symm (g x)) ≠ f x
rw [AlgEquiv.apply_symm_apply f (g x), ne_comm]
exact hx
let E : IntermediateField K L := IntermediateField.adjoin K { x }
let h_findim : FiniteDimensional K E :=
IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
let H := E.fixingSubgroup
have h_basis : (H : Set (L ≃ₐ[K] L)) ∈ galGroupBasis K L := ⟨H, ⟨E, ⟨h_findim, rfl⟩⟩, rfl⟩
have h_nhds := GroupFilterBasis.mem_nhds_one (galGroupBasis K L) h_basis
rw [mem_nhds_iff] at h_nhds
rcases h_nhds with ⟨W, hWH, hW_open, hW_1⟩
refine ⟨f • W, g • W, ⟨hW_open.leftCoset f, hW_open.leftCoset g, ⟨1, hW_1, mul_one _⟩, ⟨1, hW_1, mul_one _⟩, ?_⟩⟩
rw [Set.disjoint_left]
rintro σ ⟨w1, hw1, h⟩ ⟨w2, hw2, rfl⟩
dsimp at h
rw [eq_inv_mul_iff_mul_eq.symm, ← mul_assoc, mul_inv_eq_iff_eq_mul.symm] at h
have h_in_H : w1 * w2⁻¹ ∈ H := H.mul_mem (hWH hw1) (H.inv_mem (hWH hw2))
rw [h] at h_in_H
change φ ∈ E.fixingSubgroup at h_in_H
rw [IntermediateField.mem_fixingSubgroup_iff] at h_in_H
specialize h_in_H x
have hxE : x ∈ E := by
apply IntermediateField.subset_adjoin
apply Set.mem_singleton
exact hφx (h_in_H hxE) }
