subschemeObjIso — Mathlib

English

There is a canonical isomorphism between the subscheme object and the quotient presheaf: Γ(subscheme, ...) ≅ Γ(X, U)/I(U).

Русский

Существует каноническое изоморфизм между подсхемой и фактор-прешейфом: Γ(subscheme, ...) ≅ Γ(X, U)/I(U).

LaTeX

$$$\Gamma(I.subscheme, I.subschemeι^{-1}U) \cong \mathcal{O}_X(U)/I(U)$$$

Lean4

/-- `Γ(𝒪ₓ/I, U) ≅ 𝒪ₓ(U)/I(U)`. -/
noncomputable def subschemeObjIso (U : X.affineOpens) :
    Γ(I.subscheme, I.subschemeι ⁻¹ᵁ U) ≅ .of (Γ(X, U) ⧸ I.ideal U) :=
  I.subscheme.presheaf.mapIso (eqToIso (by simp)).op ≪≫
    (I.subschemeCover.f U).appIso _ ≪≫ Scheme.ΓSpecIso (.of (Γ(X, U) ⧸ I.ideal U))

Похожие утверждения