SpecOfPoint

Mathlib.AlgebraicGeometry.PullbackCarrier

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

Lean4

/-- If `t` is a point in `X ×[S] Y` above `(x, y, s)`, then this is the image of the unique
point of `Spec κ(s)` in `Spec κ(x) ⊗[κ(s)] κ(y)`. -/
def SpecOfPoint (t : ↑(pullback f g)) : Spec (Triplet.ofPoint t).tensor :=
  (Spec.map (ofPointTensor t)).base (⊥ : PrimeSpectrum _)

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

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

Разделы

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

Аффилиация

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