pullbackSpecIso — Mathlib

English

The category of schemes is equipped with all pullbacks with respect to limit properties.

Русский

Категория схем имеет все пулбэки в рамках пределов.

LaTeX

$$$$ \text{HasPullbacks Scheme} $$$$

Lean4

/-- The isomorphism between the fibred product of two schemes `Spec S` and `Spec T`
over a scheme `Spec R` and the `Spec` of the tensor product `S ⊗[R] T`. -/
noncomputable def pullbackSpecIso :
    pullback (Spec.map (CommRingCat.ofHom (algebraMap R S))) (Spec.map (CommRingCat.ofHom (algebraMap R T))) ≅
      Spec (.of <| S ⊗[R] T) :=
  letI H :=
    IsLimit.equivIsoLimit (PullbackCone.eta _)
      (PushoutCocone.isColimitEquivIsLimitOp _ (CommRingCat.pushoutCoconeIsColimit R S T))
  limit.isoLimitCone ⟨_, isLimitPullbackConeMapOfIsLimit Scheme.Spec _ H⟩

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