iso_inv_base_hom_base — Mathlib

English

For an isomorphism e: X ≅ Y, the composite in the other order also gives the identity on the base level.

Русский

Для изоморфизма e: X ≅ Y композиция в обратном порядке также даёт тождество на базовом уровне.

LaTeX

$$$$e.inv.base \\circ e.hom.base = \\mathrm{id}$$$$

Lean4

@[simp]
theorem iso_inv_base_hom_base {X Y : LocallyRingedSpace.{u}} (e : X ≅ Y) : e.inv.base ≫ e.hom.base = 𝟙 _ :=
  by
  rw [← SheafedSpace.comp_base, ← LocallyRingedSpace.comp_toShHom]
  simp

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