instIsOpenImmersionCommRingCatFSheafedSpaceToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData

English

For glue data D and indices i, j, the glue map f_i_j is an open immersion of Locally Ringed Spaces.

Русский

Для данных склейки D и индексов i, j карта склейки f_i_j является открытым внедрением пространств с локально кольцами.

LaTeX

$$$\mathrm{LocallyRingedSpace.IsOpenImmersion}\left(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toGlueData.f\,i\,j\right)$$$

Lean4

instance (i j : 𝖣.J) :
    SheafedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toGlueData.f i j) := by
  apply GlueData.f_open

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