English
If R is a topological ring and the space R is T2 (Hausdorff), then for any A, the space Hom(A,R) is T2.
Русский
Если R — топологическое кольцо и R — хаусдорфово, то для любого A пространство Hom(A,R) также хаусдорфово.
LaTeX
$$$[T2Space(R)] \Rightarrow T2Space(A \to R)$$$
Lean4
theorem isClosedEmbedding_hom [IsTopologicalRing R] [T1Space R] : IsClosedEmbedding (fun f : A ⟶ R ↦ (f.hom : A → R)) :=
by
let f : CommRingCat.of (MvPolynomial A (⊥_ CommRingCat)) ⟶ A :=
CommRingCat.ofHom (MvPolynomial.eval₂Hom (initial.to A).hom id)
have : Function.Surjective f := Function.LeftInverse.surjective (g := .X) fun x ↦ by simp [f]
convert
((mvPolynomialHomeomorph A R (.of _)).trans (.uniqueProd (⊥_ CommRingCat ⟶ R) _)).isClosedEmbedding.comp
(isClosedEmbedding_precomp_of_surjective f this) using
2 with g
ext x
simp [f]
