English
If f: A ⟶ B is surjective and R is T1, then the map (f ≫ ·): (B ⟶ R) → (A ⟶ R) is a closed embedding.
Русский
Если f: A ⟶ B сюръективно, а R — T1, то отображение (f ≫ ·): (B ⟶ R) → (A ⟶ R) является замкнутым вложением.
LaTeX
$$$[T1Space\,R]\; (f:\,A\to B)\;\text{Surjective} \Rightarrow \text{IsClosedEmbedding}\big((f ≫ \cdot): (B \to R) \to (A \to R)\big)$$$
Lean4
/-- `Hom(A/I, R)` is a closed subspace of `Hom(A, R)` if `R` is T1. -/
theorem isClosedEmbedding_precomp_of_surjective [T1Space R] (f : A ⟶ B) (hf : Function.Surjective f) :
Topology.IsClosedEmbedding ((f ≫ ·) : (B ⟶ R) → (A ⟶ R)) :=
by
refine ⟨isEmbedding_precomp_of_surjective f hf, ?_⟩
have : IsClosed (⋂ i : RingHom.ker f.hom, {f : A ⟶ R | f i = 0}) :=
isClosed_iInter fun x ↦ (isClosed_singleton (x := 0)).preimage (continuous_apply (R := R) x.1)
convert this
ext x
simp only [Set.mem_range, Set.mem_iInter, Set.mem_setOf_eq, Subtype.forall, RingHom.mem_ker]
constructor
· rintro ⟨g, rfl⟩ a ha; simp [ha]
·
exact fun H ↦
⟨CommRingCat.ofHom (RingHom.liftOfSurjective f.hom hf ⟨x.hom, H⟩), by ext;
simp [RingHom.liftOfRightInverse_comp_apply]⟩
