iso_hom_base_inv_base_apply — Mathlib

English

If X ≅ Y via an isomorphism e, then the base maps compose to the identity on the underlying carrier: the inverse base at the image equals the preimage point.

Русский

Если X и Y изоморфны через э, тогда базовые отображения композиции дают тождество на носителе пространства.

LaTeX

$$$(e.inv.base (e.hom.base x)) = x$$$

Lean4

@[simp]
theorem iso_hom_base_inv_base_apply {X Y : LocallyRingedSpace.{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

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