left_affine_comp_pullback_hasPullback

English

The pullback of the left affine composition with the right morphisms exists and is a pullback.

Русский

Существует пулбэк левого аффинного композиционного отображения и он является пулбэком.

LaTeX

$$$$ \text{HasPullback} ( (Z_{affine}.pullback) \circ f, g) $$$$

Lean4

instance left_affine_comp_pullback_hasPullback {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) (i : Z.affineCover.I₀) :
    HasPullback ((Z.affineCover.pullback₁ f).f i ≫ f) g := by
  simpa [pullback.condition] using hasPullback_assoc_symm f (Z.affineCover.f i) (Z.affineCover.f i) g

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