toSpecΓ_fromSpec

Mathlib.AlgebraicGeometry.AffineScheme

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec

English

The composition of U.toSpecΓ with hU.fromSpec equals the inclusion U ↪ X, i.e., U.toSpecΓ ≫ hU.fromSpec = U.ι.

Русский

Сложение U.toSpecΓ с hU.fromSpec даёт включение U в X: U.toSpecΓ ≫ hU.fromSpec = U.ι.

LaTeX

$$U.toSpecΓ ≫ hU.fromSpec = U.ι$$

Lean4

@[reassoc (attr := simp)]
theorem toSpecΓ_fromSpec : U.toSpecΓ ≫ hU.fromSpec = U.ι :=
  toSpecΓ_isoSpec_inv_assoc _ _

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

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

Разделы

Аффилиация

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