ιIsOpenImmersion — Mathlib

English

For every i and U, the composite D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U equals the identity on the relevant limit.

Русский

Для каждого i и U композиция D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U равна тождественному отображению на соответствующем пределе.

LaTeX

$$$D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = \mathrm{Id}$$$

Lean4

instance ιIsOpenImmersion (i : D.J) : IsOpenImmersion (𝖣.ι i)
    where
  base_open := D.ι_isOpenEmbedding i
  c_iso U := by erw [← colimitPresheafObjIsoComponentwiseLimit_hom_π]; infer_instance

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