ofPoint_SpecTensorTo

Mathlib.AlgebraicGeometry.PullbackCarrier

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

English

The ofPoint construction for base SpecTensorTo base recovers T.

Русский

Построение ofPoint по базовому SpecTensorTo восстанавливает T.

LaTeX

$$$\text{ofPoint} (T.SpecTensorTo.base p) = T$$$

Lean4

@[simp]
theorem ofPoint_SpecTensorTo (T : Triplet f g) (p : Spec T.tensor) : ofPoint (T.SpecTensorTo.base p) = T := by
  ext <;> simp

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

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

Разделы

Аффилиация

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