isPullback_Spec_map_isPushout — Mathlib

English

If f and g form a pushout in rings, then the induced Spec maps form a pullback in schemes.

Русский

Если f и g образуют пулп-обобщение (pushout) в кольцах, то индуцированные отображения Spec образуют пулбэк в схемах.

LaTeX

$$$$ \text{IsPushout}(f,g,inl,inr) \Rightarrow \text{IsPullback}( \mathrm{Spec.map}(inl), \mathrm{Spec.map}(inr), \mathrm{Spec.map}(f), \mathrm{Spec.map}(g)) $$$$

Lean4

theorem isPullback_Spec_map_isPushout {A B C P : CommRingCat} (f : A ⟶ B) (g : A ⟶ C) (inl : B ⟶ P) (inr : C ⟶ P)
    (h : IsPushout f g inl inr) : IsPullback (Spec.map inl) (Spec.map inr) (Spec.map f) (Spec.map g) :=
  IsPullback.map Scheme.Spec h.op.flip

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