pullbackRestrictIsoRestrict_hom_morphismRestrict

English

The hom component of the restriction morphism composed with the restriction morphism equals the second projection of the restricted pullback: (pullbackRestrictIsoRestrict f U).hom ≫ morphismRestrict f U = pullback.snd f U.ι.

Русский

Компонента гомоморфизма ограничения, композиция с ограничением, равна второй проекции ограниченного произведения: (pullbackRestrictIsoRestrict f U).hom ≫ morphismRestrict f U = pullback.snd f U.ι.

LaTeX

$$$(\mathrm{pullbackRestrictIsoRestrict}(f,U))^{\mathrm{hom}} \;\circ \; \mathrm{morphismRestrict}(f,U) = \mathrm{pullback.snd}(f,U.ι).$$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackRestrictIsoRestrict_hom_morphismRestrict {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) :
    (pullbackRestrictIsoRestrict f U).hom ≫ f ∣_ U = pullback.snd _ _ :=
  Iso.hom_inv_id_assoc _ _

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