SpecTensorTo

Mathlib.AlgebraicGeometry.PullbackCarrier

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Pullback.Triplet.SpecTensorTo

Lean4

/-- Given `x : X`, `y : Y` and `s : S` such that `f x = s = g y`,
this is `Spec (κ(x) ⊗[κ(s)] κ(y)) ⟶ X ×ₛ Y`. -/
def SpecTensorTo : Spec T.tensor ⟶ pullback f g :=
  pullback.lift (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x) (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y)
    (Spec_map_tensorInl_fromSpecResidueField _)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru