preimage

Mathlib.AlgebraicGeometry.GammaSpecAdjunction

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Spec.preimage

Lean4

/-- The preimage under Spec. -/
def preimage : R ⟶ S :=
  (Scheme.Spec.preimage f).unop

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

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

Разделы

Аффилиация

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