ideal_ker_le_ker_ΓSpecIso_inv_comp

English

Another part of proving the subscheme object iso validity.

Русский

Ещё одна часть доказательства корректности изоморфизма подсхемы.

LaTeX

$$$\text{proof}(subschemeObjIso)\_2$$$

Lean4

theorem ideal_ker_le_ker_ΓSpecIso_inv_comp :
    f.ker.ideal U ≤ RingHom.ker ((ΓSpecIso Γ(Y, ↑U)).inv ≫ (pullback.snd f U.1.ι ≫ U.1.toSpecΓ).appTop).hom :=
  by
  let e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(Limits.pullback (C := Scheme) f U.1.ι, ⊤) :=
    X.presheaf.mapIso (eqToIso (by simp [IsOpenImmersion.opensRange_pullback_fst_of_right])).op ≪≫
      (Limits.pullback.fst (C := Scheme) f U.1.ι).appIso ⊤
  have he : f.app U ≫ e.hom = (ΓSpecIso Γ(Y, ↑U)).inv ≫ (pullback.snd f U.1.ι ≫ U.1.toSpecΓ).appTop :=
    by
    rw [← (Iso.inv_comp_eq _).mpr U.2.isoSpec_inv_appTop, Category.assoc, Iso.eq_inv_comp]
    simp only [Opens.topIso_hom, eqToHom_op, Hom.app_eq_appLE, Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom,
      eqToIso.hom, Hom.appIso_hom, Hom.appLE_map, Hom.map_appLE, appLE_comp_appLE, Opens.map_top, e, pullback.condition,
      IsAffineOpen.toSpecΓ_isoSpec_inv, Category.assoc]
    rw [comp_appLE, Opens.ι_app]
    exact Hom.map_appLE _ _ (homOfLE le_top).op
  rw [← he]
  refine (IdealSheafData.ideal_ofIdeals_le _ _).trans_eq (RingHom.ker_equiv_comp _ e.commRingCatIsoToRingEquiv).symm

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