iso_hom_base_inv_base_apply — Mathlib

English

For any isomorphism e: X ≅ Y of schemes, the composition e.hom.base followed by e.inv.base is the identity on the base spaces.

Русский

Для изоморфизма e: X ≅ Y композиция e.hom.base затем e.inv.base является тождественным отображением на основаниях.

LaTeX

$$e.hom.base \circ e.inv.base = 𝟙$$

Lean4

@[simp]
theorem iso_hom_base_inv_base_apply {X Y : Scheme.{u}} (e : X ≅ Y) (x : X) : (e.inv.base (e.hom.base x)) = x :=
  by
  change (e.hom.base ≫ e.inv.base) x = 𝟙 X.toPresheafedSpace x
  simp

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