ΓIso_hom_map

Mathlib.AlgebraicGeometry.OpenImmersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsOpenImmersion.ΓIso_hom_map

← MathLib Explorer

English

Equality between ΓIsoTop and opensRange maps.

Русский

Равенство между ΓIsoTop и отображениями opensRange.

LaTeX

$$$ \Gamma\text{IsoTop } f U = \text{opensRange functor} f(U) $$$

Lean4

@[reassoc, elementwise]
theorem ΓIso_hom_map {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] (U : Y.Opens) :
    f.app U ≫ (ΓIso f U).hom = Y.presheaf.map (homOfLE inf_le_right).op :=
  by
  rw [← map_ΓIso_inv]
  simp [-ΓIso_inv]

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

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

Разделы

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

Аффилиация

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