English
There is a canonical equivalence between the S-morphisms X → 𝔸(n; S) over S and n-tuples of global sections of X, i.e., Hom^over_S(X, 𝔸(n; S)) ≅ Γ(X, 𝒪_X)^n.
Русский
Существует естественное биективное соответствие между морфизмами над S из X в 𝔸(n; S) и n-кортежами глобальных секций X, то есть Hom^over_S(X, 𝔸(n; S)) ≅ Γ(X, 𝒪_X)^n.
LaTeX
$$$\\operatorname{Hom}_{S}(X, \\mathbb{A}(n; S))^{\\mathrm{over}} \\cong \\Gamma(X, \\mathcal{O}_X)^n$$$
Lean4
/-- `S`-morphisms into `Spec 𝔸(n; S)` are equivalent to the choice of `n` global sections. -/
@[simps]
def homOverEquiv : { f : X ⟶ 𝔸(n; S) // f.IsOver S } ≃ (n → Γ(X, ⊤))
where
toFun f i := f.1.appTop (coord S i)
invFun v := ⟨homOfVector (X ↘ S) v, inferInstance⟩
left_inv
f := by
ext : 2
· simp [f.2.1]
· rw [homOfVector_appTop_coord]
right_inv v := by ext i; simp [-TopologicalSpace.Opens.map_top, homOfVector_appTop_coord]
