Spec_map_tensor_isPullback — Mathlib

English

Same pullback property for the triplet tensor maps to residue fields.

Русский

Та же пулбек-структура для тензорных отображений и резидуальных полей.

LaTeX

$$$\text{IsPullback} (\operatorname{Spec.map} T.tensorInl) (\operatorname{Spec.map} T.tensorInr) (\operatorname{Spec.map} (S.residueFieldCongr T.hx).inv \circ f.residueFieldMap T.x) (\operatorname{Spec.map} (S.residueFieldCongr T.hy).inv \circ g.residueFieldMap T.y)$$$

Lean4

theorem Spec_map_tensor_isPullback (T : Triplet f g) :
    CategoryTheory.IsPullback (Spec.map T.tensorInl) (Spec.map T.tensorInr)
      (Spec.map ((S.residueFieldCongr T.hx).inv ≫ f.residueFieldMap T.x))
      (Spec.map ((S.residueFieldCongr T.hy).inv ≫ g.residueFieldMap T.y)) :=
  isPullback_Spec_map_pushout _ _

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