English
The injection maps ι_i are open immersions after transporting through the glued Locally Ringed Space structure.
Русский
Инъекции ι_i являются открытыми внедрениями после переноса через склеиваемую структуру Locally Ringed Space.
LaTeX
$$$\text{IsOpenImmersion}((D.toLocallyRingedSpaceGlueData).toGlueData.ι i)$$$
Lean4
@[simp]
theorem ι_isoCarrier_inv (i : D.J) : (D_).ι i ≫ D.isoCarrier.inv = (D.ι i).base :=
by
delta isoCarrier
rw [Iso.trans_inv, GlueData.ι_gluedIso_inv_assoc, Functor.mapIso_inv, Iso.trans_inv, Functor.mapIso_inv,
Iso.trans_inv, SheafedSpace.forgetToPresheafedSpace_map, PresheafedSpace.forget_map, PresheafedSpace.forget_map, ←
PresheafedSpace.comp_base, ← Category.assoc,
D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.ι_isoPresheafedSpace_inv i]
erw [← Category.assoc, D.toLocallyRingedSpaceGlueData.ι_isoSheafedSpace_inv i]
change (_ ≫ D.isoLocallyRingedSpace.inv).base = _
rw [D.ι_isoLocallyRingedSpace_inv i]
