English
An auxiliary construction lowerCone Us S provides a cone over a diagram associated to principal opens and Kan extensions.
Русский
Вспомогательная конструкция lowerCone Us S образует конус над диаграммой, связанной с принципиальными открытыми множествами и кан-расширениями.
LaTeX
$$$\\mathrm{lowerCone}(\\mathrm{Us}, S)$ is a cone over the diagram $((\\mathrm{ObjectProperty.\\!Iota}\, f)^{op} \\circ \\mathrm{principalsKanExtension}F)$$$
Lean4
/-- Given a structured arrow `f` with domain `iSup Us` over `principals X`,
where `Us` is a family of `Opens X`, this functor sends `f` to the principal open
associated with it, considered as an object in the full subcategory of all `V : Opens X`
such that `V ≤ Us i` for some `i`.
This definition is primarily meant to be used in `lowerCone`, and `isLimit` below.
-/
@[simps]
def projSup {ι : Type v} (Us : ι → Opens X) :
StructuredArrow (.op <| iSup Us) (principals X) ⥤ (ObjectProperty.FullSubcategory fun V => ∃ i, V ≤ Us i)ᵒᵖ
where
obj f := .op <| .mk (principalOpen f.right) <| exists_le_of_le_sup Us f.hom.unop.le
map e := .op <| LE.le.hom <| principalOpen_le <| e.right.le
