comapIso_hom_snd — Mathlib

English

The morphism obtained by taking comap of the ideal data along f and then projecting with the pullback's second projection (snd) equals the subscheme restriction map from I to itself via f.

Русский

Отображение, получаемое взятием comap вдоль f и затем проецирование через вторую проекцию (snd) равняется отображению подсхем, получаемому ограничением I через f.

LaTeX

$$$ (I.comapIso f).hom \\; ≫ pullback.snd _ _ = subschemeMap \\_ \\_ f (I.le_map_comap f) $$$

Lean4

@[reassoc (attr := simp)]
theorem comapIso_hom_snd (I : Y.IdealSheafData) (f : X ⟶ Y) :
    (I.comapIso f).hom ≫ pullback.snd _ _ = subschemeMap _ _ f (I.le_map_comap f) :=
  by
  rw [← cancel_mono I.subschemeι]
  simp [← pullback.condition]

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