Ancestors

Written by C.B. Aberlé on 2024-11-22 at 15:35

Wondering if anyone here who knows some topos theory can help me out with something that's come up in my research lately. For (p : E \to B) a fibration, I'm interested in defining some additional structure on (p) which is equivalent to a pseudofunctor (P : B^{op} \to \mathbf{Site}), where (\mathbf{Site}) is the 2-category of categories equipped with coverages (i.e. sites) and morphisms of sites (i.e. functors which are covering-flat and preserve covering families) between them, such that postcomposing (P) with the forgetful 2-functor (\mathbf{Site} \to \mathbf{Cat}) yields the usual pseudofunctor given by taking fibres of (p). Essentially, such a structure should equip each fibre of (p) with a coverage in a manner compatible with the structure of (p) as a fibration. I'm wondering if anyone else has considered these sorts of things before, and if they have a name.

=> More informations about this toot | More toots from cbaberle@mathstodon.xyz

Toot

Written by C.B. Aberlé on 2024-11-22 at 15:40

My best guess so far for what such a "fibrewise coverage" would look like is the following:

For each object (y \in E) and morphism (f : a \to p(y) \in B), a collection of covering families over (f), written ({f_i : y_i \to y \in E \mid p(f_i) = f }_{i \in I}), such that:

1. if (g : x \to y \in E) is a Cartesian morphism, then the singleton family ({g}) is a covering family of (y) over (p(g)).

2. If ({f_i : y_i \to x \in E \mid p(f_i) = f}{i \in I}) is a covering family of (x) over (f : a \to p(x) \in B), and for each (i \in I), ({g_j : z_j \to y_i \in E \mid p(g_j) = g}{j \in J_i}) is a covering family of (y_i) over (g : b \to a \in B), then ({f_i \circ g_j : z_j \to x \in E \mid p(f_i \circ g_j) = f \circ g }_{i \in I, j \in J_i}) is a covering family of (x) over (f \circ g).

3. If ({f_i : x_i \to x \in E \mid p(f_i) = p(g)}) is a covering family of (x) over (p(g)) for some (g : y \to x \in E), and (h : a \to p(y)) is a morphism in (B), then there exists a covering family ({h_j : y_j \to y \in E \mid p(h_j) = h}) of (y) over (h), such that for each (j \in J) there exists some (i \in I) and (k : y_j \to x_i) such that (p(k) = h) and (g \circ h_j = f_i \circ k).

=> More informations about this toot | More toots from cbaberle@mathstodon.xyz

Descendants