morphismRestrict_ι — Mathlib

English

The diagram of a restricted morphism respects the canonical inclusions: (f|_U) ≫ U.ι = (f|^{-1}_{U} U).ι ≫ f.

Русский

Ограничение морфизма и включения согласованы: (f|_U) ≫ U.ι = (f^{-1}_U U).ι ≫ f.

LaTeX

$$$ (f|_U) \;\; ≫ U.ι = (f^{-1}_{U} U).ι \;\; ≫ f. $$$

Lean4

@[reassoc (attr := simp)]
theorem morphismRestrict_ι {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) : (f ∣_ U) ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f :=
  by
  delta morphismRestrict
  rw [Category.assoc, pullback.condition.symm, pullbackRestrictIsoRestrict_inv_fst_assoc]

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