hasPullback_of_cover — Mathlib

English

If X = Spec A and Y = Spec B map to Spec C, then the pullback exists in the affine world, given by Spec(A ⊗_C B).

Русский

Если X = Spec A и Y = Spec B и существуют отображения в Spec C, то в аффинном случае существует пулбэк, равный Spec(A ⊗_C B).

LaTeX

$$$$ \text{HasPullback}(f,g) \text{ with } X=\mathrm{Spec}(A), Y=\mathrm{Spec}(B) \Rightarrow \mathrm{pullback}(f,g) \cong \mathrm{Spec}(A \otimes_C B) $$$$

Lean4

theorem hasPullback_of_cover : HasPullback f g :=
  ⟨⟨⟨_, gluedIsLimit 𝒰 f g⟩⟩⟩

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