English
Let X be a scheme and U an affine open subset of X. Then the canonical morphism U → Spec Γ(X, U) exhibits U as isomorphic to Spec Γ(X, U); more precisely, the topological component of the morphism U.toSpecΓ.appTop agrees with the composition (Scheme.ΓSpecIso Γ(X, U)).hom ∘ U.topIso.inv.
Русский
Пусть X — схема, U — аффинное открытое подмножество X. Тогда каноническое отображение U → Spec Γ(X, U) является изоморфизмом U ≅ Spec Γ(X, U); более точно, компонент topologicalof этого отображения совпадает с композицией (Scheme.ΓSpecIso Γ(X, U)).hom ∘ U.topIso.inv.
LaTeX
$$$U.toSpecΓ.appTop = (Scheme.ΓSpecIso \\Gamma(X, U)).hom \\circ U.topIso.inv$$$
Lean4
@[reassoc]
theorem toSpecΓ_appTop {X : Scheme.{u}} (U : X.Opens) :
U.toSpecΓ.appTop = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv := by simp [Scheme.Opens.toSpecΓ]
