English
Partial sections of a cofiltered limit are sections when restricted to a finite subset of objects and morphisms of J; defined as the set of families u: ∀ j, F.obj j satisfying compatibility on a finite diagram.
Русский
Частичные секции ко-фильтрованного предела образуют множества семейств u_j ∈ F.obj j, которые удовлетворяют совместимости на некоторой конечной поддиаграмме J.
LaTeX
$$$ \mathrm{partialSections}(F,H) = \{ u : \forall j, F.obj j \mid \forall f: \text{FiniteDiagramArrow } G, f \in H \Rightarrow F.map f.2.2.2.2 (u f.1) = u f.2.1 \}$$$
Lean4
/-- Partial sections of a cofiltered limit are sections when restricted to
a finite subset of objects and morphisms of `J`.
-/
def partialSections {J : Type u} [SmallCategory J] (F : J ⥤ TopCat.{v}) {G : Finset J}
(H : Finset (FiniteDiagramArrow G)) : Set (∀ j, F.obj j) :=
{u | ∀ {f : FiniteDiagramArrow G} (_ : f ∈ H), F.map f.2.2.2.2 (u f.1) = u f.2.1}
