English
In a pullback square with an open immersion iV, the kernel of the pulled-back morphism f' on W equals the comap of the kernel of f along iV, expressed on the affine open W via the specified isomorphism.
Русский
В квадрате вытяжки с открытым вложением iV ядро вытянутого по нему морфизма f' на W равно сопровождающему отображению ядра f вдоль iV, выраженному на аффинном открытом наборе W через заданное изоморфирование.
LaTeX
$$$f'.\ker.ideal W = (f.\ker.ideal ⟨iV ''ᵁ W, W.2.image_of_isOpenImmersion _⟩).comap (iV.appIso W).inv.hom$$$
Lean4
theorem ker_ideal_of_isPullback_of_isOpenImmersion {X Y U V : Scheme.{u}} (f : X ⟶ Y) (f' : U ⟶ V) (iU : U ⟶ X)
(iV : V ⟶ Y) [IsOpenImmersion iV] [QuasiCompact f] (H : IsPullback f' iU iV f) (W) :
f'.ker.ideal W = (f.ker.ideal ⟨iV ''ᵁ W, W.2.image_of_isOpenImmersion _⟩).comap (iV.appIso W).inv.hom :=
by
have : QuasiCompact f' := MorphismProperty.of_isPullback H.flip inferInstance
have : IsOpenImmersion iU := MorphismProperty.of_isPullback H inferInstance
ext x
have : iU ''ᵁ f' ⁻¹ᵁ W = f ⁻¹ᵁ iV ''ᵁ W := IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback H W
let e : Γ(X, f ⁻¹ᵁ iV ''ᵁ W) ≅ Γ(U, f' ⁻¹ᵁ W) := X.presheaf.mapIso (eqToIso this).op ≪≫ iU.appIso _
have : (iV.appIso W).inv ≫ f.app _ = f'.app W ≫ e.inv :=
by
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv]
simp only [Scheme.Hom.app_eq_appLE, Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, eqToIso.hom, eqToHom_op,
Scheme.Hom.appIso_hom', Scheme.Hom.map_appLE, e, Scheme.appLE_comp_appLE, H.w]
simp only [Scheme.Hom.ker_apply, RingHom.mem_ker, Ideal.mem_comap, ← RingHom.comp_apply, ← CommRingCat.hom_comp, this]
simpa using (map_eq_zero_iff _ (ConcreteCategory.bijective_of_isIso e.inv).1).symm
