morphismRestrict_comp — Mathlib

English

Restricting a composition equals composing the restrictions: (f ≫ g)|_U = f|_{g^{-1}(U)} ≫ g|_U.

Русский

Ограничение композиции равно композиции ограничений: (f ≫ g)|_U = f|_{g^{-1}(U)} ≫ g|_U.

LaTeX

$$$(f\gg)\!|_U = f|_{g^{-1}\!U} \;\gg|_U$$$

Lean4

theorem morphismRestrict_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Opens Z) :
    (f ≫ g) ∣_ U = f ∣_ g ⁻¹ᵁ U ≫ g ∣_ U := by
  delta morphismRestrict
  rw [← pullbackRightPullbackFstIso_inv_snd_snd]
  simp_rw [← Category.assoc]
  congr 1
  rw [← cancel_mono (pullback.fst _ _)]
  simp_rw [Category.assoc]
  rw [pullbackRestrictIsoRestrict_inv_fst, pullbackRightPullbackFstIso_inv_snd_fst, ← pullback.condition,
    pullbackRestrictIsoRestrict_inv_fst_assoc, pullbackRestrictIsoRestrict_inv_fst_assoc]
  rfl

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