pointsPi

Mathlib.AlgebraicGeometry.PointsPi

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.pointsPi

Lean4

/-- The canonical map `X(Π Rᵢ) ⟶ Π X(Rᵢ)`.
This is injective if `X` is quasi-separated, surjective if `X` is affine,
or if `X` is compact and each `Rᵢ` is local. -/
noncomputable def pointsPi : (Spec (.of <| Π i, R i) ⟶ X) → Π i, Spec (R i) ⟶ X := fun f i ↦
  Spec.map (CommRingCat.ofHom (Pi.evalRingHom (R ·) i)) ≫ f

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

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

Разделы

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

Аффилиация

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