affine_hasPullback — Mathlib

English

There is a canonical HasPullback instance for any pair of affine morphisms of schemes

Русский

Существует канонический экземпляр HasPullback для любой пары аффинных отображений между схемами

LaTeX

$$$$ \text{HasPullback}(f,g) $$$$

Lean4

instance affine_hasPullback {A B C : CommRingCat} (f : Spec A ⟶ Spec C) (g : Spec B ⟶ Spec C) : HasPullback f g :=
  by
  rw [← Scheme.Spec.map_preimage f, ← Scheme.Spec.map_preimage g]
  exact ⟨⟨⟨_, isLimitOfHasPullbackOfPreservesLimit Scheme.Spec (Scheme.Spec.preimage f) (Scheme.Spec.preimage g)⟩⟩⟩

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