English
Morphisms to affine space are determined by their base map and all coordinate components; hence two morphisms are equal if they agree on each coordinate and agree after projection to the base.
Русский
Гомоморфизмы в аффинное пространство определяются базовой картой и всеми координатами; следовательно, два гомоморфизма равны, если они совпадают по каждой координате и после проекции на основание.
LaTeX
$$$$(f=g) \iff (f \circ \text{proj} = g \circ \text{proj}) \land (\forall i, f_i = g_i).$$$$
Lean4
@[ext 1100]
theorem hom_ext {f g : X ⟶ 𝔸(n; S)} (h₁ : f ≫ 𝔸(n; S) ↘ S = g ≫ 𝔸(n; S) ↘ S)
(h₂ : ∀ i, f.appTop (coord S i) = g.appTop (coord S i)) : f = g :=
by
apply pullback.hom_ext h₁
change f ≫ toSpecMvPoly _ _ = g ≫ toSpecMvPoly _ _
apply (toSpecMvPolyIntEquiv n).injective
ext i
rw [toSpecMvPolyIntEquiv_comp, toSpecMvPolyIntEquiv_comp]
exact h₂ i
