ι_isoLocallyRingedSpace_inv — Mathlib

English

For each i, the composite of the i-th injection with the inverse of the glued Locally Ringed Space isomorphism equals the base injection.

Русский

Для каждого i композиция i-й инъекции с обратной стороной склейки по Locally Ringed Space равна базовой инъекции.

LaTeX

$$$(D. toLocallyRingedSpaceGlueData.toGlueData.ι i) \;≫\; D.isoLocallyRingedSpace.inv = (D.ι i).base$$$

Lean4

theorem ι_isoLocallyRingedSpace_inv (i : D.J) :
    D.toLocallyRingedSpaceGlueData.toGlueData.ι i ≫ D.isoLocallyRingedSpace.inv = (𝖣.ι i).toLRSHom :=
  𝖣.ι_gluedIso_inv forgetToLocallyRingedSpace i

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