families

Tag. families

families

Notes (4)

Definition. Later on families later-family

Conjugation with the adjunction between presheaves and families $𝑈 ⊣ Cofree$ lets us induce a later construction on families from the one on presheaves,

⊳_{Fam} = 𝑈 \circ ⊳ \circ Cofree : Fam (𝒞︀) \to Fam (𝒞︀) .

Concretely, later on families evaluates to

⊳_{Fam} 𝐴 (𝑥) ≅ \prod_{𝑦 ≺ 𝑥} \prod_{𝑓 : 𝑦 \to 𝑥} 𝐴 (𝑦)

Theorem. Löb induction on families lob-family

Like later on families, the recursion principle for families is inherited from that on presheaves. Given a family $𝐴$ and a step

𝜑_{𝑥} : ⊳_{Fam} 𝐴 (𝑥) \to 𝐴 (𝑥) for each 𝑥,

the construction is a chain of transpositions with Löb for presheaves used in the middle:

Just as for presheaves, the fixed point constructed above is unique: the two transpositions are bijections, and the presheaf-level fixed point is already unique.

The adjoint triple between presheaves and families presheaf-family-adjoint-triple

A family over $𝒞︀$ is a set $𝐴 (𝑥)$ for each object $𝑥$ , with no action of morphisms. Families form a category $Fam (𝒞︀)$ : a morphism $𝐴 \to 𝐵$ is a function $𝐴 (𝑥) \to 𝐵 (𝑥)$ for each $𝑥$ .

Forgetting the restriction maps of a presheaf gives a functor

𝑈 : 𝖯𝗌𝗁 𝒞︀ \to Fam (𝒞︀) .

It has both a left and a right adjoint,

Free ⊣ 𝑈 ⊣ Cofree .

The two adjoints demonstrate different means of forcing a family to be functorial. The right adjoint universally quantifies over morphisms in,

Cofree (𝐴) (𝑥) = \prod_{𝑦} 𝒞︀ (𝑦, 𝑥) \to 𝐴 (𝑦),

with restriction along $𝑓$ given by precomposition. The left adjoint instead existentially quantifiers over morphisms out:

Free (𝐴) (𝑥) = \sum_{𝑦} 𝒞︀ (𝑥, 𝑦) \times 𝐴 (𝑦),

with restriction acting on the first component. (For $Free$ we ask that $𝒞︀$ have a set of objects, so that this sum is a set and thus $Free$ defines a presheaf.)

Theorem. Presheaves are monadic and comonadic over families presheaves-monadic-comonadic-over-families

The adjoint triple $Free ⊣ 𝑈 ⊣ Cofree$ induces a monad $𝑇 = 𝑈 \circ Free$ and a comonad $𝑊 = 𝑈 \circ Cofree$ on $Fam (𝒞︀)$ .

Both comparison functors are equivalences: presheaves are the Eilenberg–Moore algebras of $𝑇$ and the co-Eilenberg–Moore coalgebras of $𝑊$ ,

𝖯𝗌𝗁 𝒞︀ ≃ EM (𝑇) 𝖯𝗌𝗁 𝒞︀ ≃ coEM (𝑊) .

So presheaves are both monadic and comonadic over families.

Reading the algebra structure concretely: a $𝑇$ -algebra on a family $𝐴$ is a map $\sum_{𝑦} 𝒞︀ (𝑥, 𝑦) \times 𝐴 (𝑦) \to 𝐴 (𝑥)$ for each $𝑥$ , subject to the monad algebra laws — that is, exactly a functorial action of restriction.

The comonadic reading is the same structure seen from the element’s side: a $𝑊$ -coalgebra is a map $𝐴 (𝑥) \to \prod_{𝑦} 𝒞︀ (𝑦, 𝑥) \to 𝐴 (𝑦)$ , giving each value its restriction along every morphism into $𝑥$ . Where the monad says restriction acts on values, the comonad says a value already carries all of its restrictions — and the coalgebra laws say it does so coherently.