diagramOverOpen — Mathlib

English

The projection through the colimit cocone aligns with the original cocone maps, i.e., the naturality with respect to index j holds.

Русский

Проекция через колимитный кокон согласуется с исходными картами кокона; сохраняется натуральность по индексу j.

LaTeX

$$$(colimitCocone F).ι.app j ≫ desc F s = s.ι.app j$$$

Lean4

/-- (Implementation) Given an open subset of one of the spaces `U ⊆ Uᵢ`, the sheaf component of
the image `ι '' U` in the glued space is the limit of this diagram. -/
abbrev diagramOverOpen {i : D.J} (U : Opens (D.U i).carrier) : (WalkingMultispan (.prod D.J))ᵒᵖ ⥤ C :=
  componentwiseDiagram 𝖣.diagram.multispan ((D.ι_isOpenEmbedding i).isOpenMap.functor.obj U)

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