tAux

Mathlib.AlgebraicGeometry.Gluing

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.IsLocallyDirected.tAux

Lean4

/-- (Implementation detail)
The inclusion map `V i j ⟶ F j` in the glue data associated to a locally directed diagram. -/
def tAux (i j : J) : (V F i j).toScheme ⟶ F.obj j :=
  (Scheme.Opens.iSupOpenCover _).glueMorphisms (fun k ↦ (F.map k.2.1).isoOpensRange.inv ≫ F.map k.2.2) fun k₁ k₂ ↦
    by
    dsimp [Scheme.Opens.iSupOpenCover]
    apply fst_inv_eq_snd_inv F

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

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

Разделы

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

Аффилиация

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