instNontrivialCarrierTensor — Mathlib

English

The square formed by Spec.map and the pullback projections is a pullback square.

Русский

Квадрат, образованный через Spec.map и проекции пулбека, является пулбек-квадратом.

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

instance (T : Triplet f g) : Nontrivial T.tensor :=
  CommRingCat.nontrivial_of_isPushout_of_isField (Field.toIsField _) (IsPushout.of_hasPushout _ _)

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