functor

Mathlib.AlgebraicGeometry.AffineSpace

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.AffineSpace.functor

Lean4

/-- The affine space as a functor. -/
@[simps]
def functor : (Type v)ᵒᵖ ⥤ Scheme.{max u v} ⥤ Scheme.{max u v}
    where
  obj n := { obj := AffineSpace n.unop, map := map n.unop, map_id := map_id, map_comp := map_comp }
  map {n m} i := { app := reindex i.unop, naturality := fun _ _ ↦ map_reindex i.unop }
  map_id n := by ext : 2; exact reindex_id _
  map_comp f g := by ext : 2; dsimp; exact reindex_comp _ _ _

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

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

Разделы

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

Аффилиация

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