topIso — Mathlib

English

`⊤` open set (the largest open) in X, as a scheme, is isomorphic to X.

Русский

Самое большое открытое множество ∶⊤ в X, как схема, изоморфна X.

LaTeX

$$$\\uparrow(\\top:\\ X.Opens) \\;\\cong\\; X$$$

Lean4

/-- `(⊤ : X.Opens)` as a scheme is isomorphic to `X`. -/
@[simps hom]
def topIso (X : Scheme) : ↑(⊤ : X.Opens) ≅ X where
  hom := Scheme.Opens.ι _
  inv := ⟨X.restrictTopIso.inv⟩
  hom_inv_id := Hom.ext' X.restrictTopIso.hom_inv_id
  inv_hom_id := Hom.ext' X.restrictTopIso.inv_hom_id

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