ker_subschemeι_app — Mathlib

English

The value of I.subschemeι.app U is the composition of the quotient and the inverse of the isomorphism I.subschemeObjIso U.

Русский

Значение I.subschemeι.app U есть композиция фактор-морфизма и обратного изоморфизма I.subschemeObjIso U.

LaTeX

$$$I.subschemeι.app U = CommRingCat.ofHom(\text{Ideal.Quotient.mk}(I.ideal U)) \circ (I.subschemeObjIso U)^{-1}$$$

Lean4

theorem ker_subschemeι_app (U : X.affineOpens) : RingHom.ker (I.subschemeι.app U).hom = I.ideal U :=
  by
  rw [subschemeι_app]
  let e : CommRingCat.of (Γ(X, U) ⧸ I.ideal U) ≅ Γ(I.subscheme, I.subschemeι ⁻¹ᵁ U) :=
    (Scheme.ΓSpecIso _).symm ≪≫
      ((I.subschemeCover.f U).appIso _).symm ≪≫ I.subscheme.presheaf.mapIso (eqToIso (by simp)).op
  change RingHom.ker (e.commRingCatIsoToRingEquiv.toRingHom.comp (Ideal.Quotient.mk (I.ideal U))) = _
  rw [RingHom.ker_equiv_comp, Ideal.mk_ker]

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