toScheme_presheaf_map

Mathlib.AlgebraicGeometry.Restrict

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_map

English

A small simp lemma about equivalence in SpecToEquivOfField construction.

Русский

Маленькая лемма-упрощение для конструкции SpecToEquivOfField.

LaTeX

$$SpecToEquivOfField_eq_iff {K} …$$

Lean4

@[simp]
theorem toScheme_presheaf_map {V W} (i : V ⟶ W) :
    U.toScheme.presheaf.map i = X.presheaf.map (U.ι.opensFunctor.map i.unop).op :=
  rfl

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

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

Разделы

Аффилиация

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