F-algebra

Tag. F-algebra

F-algebra

Notes (10)

Algebras as a displayed category algebras-displayed

Fix an endofunctor $𝐹 : 𝒞︀ \to 𝒞︀$ . The $𝐹$ -algebras form a displayed category $AlgStr (𝐹)$ over $𝒞︀$ .

Over an object $𝑥$ , a displayed object of $AlgStr (𝐹)$ is a structure map

𝛼 \in 𝒞︀ (𝐹 𝑥, 𝑥) .

Over $𝑓 : 𝑥 \to 𝑦$ , a displayed morphism from $𝛼$ to $𝛽$ is the proposition that $𝑓$ is an algebra homomorphism:

𝛼 ⋆ 𝑓 = 𝐹 𝑓 ⋆ 𝛽 .

The total category $Alg (𝐹) = \int AlgStr (𝐹)$ is the category of $𝐹$ -algebras.

The co-Eilenberg–Moore category as a displayed category co-eilenberg-moore-displayed

A comonad on $𝒞︀$ is a monad $𝑊$ on ${𝒞︀}^{op}$ . Everything about its coalgebras is then inherited from the Eilenberg–Moore construction, instantiated at the opposite category — nothing is defined twice.

Algebras of $𝑊$ over ${𝒞︀}^{op}$ are coalgebras $𝛾 \in 𝒞︀ (𝑥, 𝑊 𝑥)$ of the underlying endofunctor, and the monad algebra laws, read in ${𝒞︀}^{op}$ , are the comonad coalgebra laws — the unit and multiplication of $𝑊$ , viewed in $𝒞︀$ , are the counit $𝜀$ and comultiplication $𝛿$ :

𝛾 ⋆ 𝜀_{𝑥} = {𝗂𝖽}_{𝑥} 𝛾 ⋆ 𝛿_{𝑥} = 𝛾 ⋆ 𝑊 𝛾 .

The co-Eilenberg–Moore category is the opposite of the total category:

coEM (𝑊) = {(EM (𝑊))}^{op} .

Coalgebras as a displayed category coalgebras-displayed

Fix an endofunctor $𝐹 : 𝒞︀ \to 𝒞︀$ . Coalgebras require no new construction: a coalgebra is an algebra in the opposite category. Define

CoalgStr (𝐹) = AlgStr (𝐹^{op}),

a displayed category over ${𝒞︀}^{op}$ , where $𝐹^{op} : {𝒞︀}^{op} \to {𝒞︀}^{op}$ is $𝐹$ acting on the opposite category.

Concretely, over an object $𝑥$ a displayed object is a structure map

𝛾 \in 𝒞︀ (𝑥, 𝐹 𝑥) .

The category of coalgebras is the opposite of the total category:

Coalg (𝐹) = {(\int CoalgStr (𝐹))}^{op} .

The outer opposite returns morphisms to the direction of $𝒞︀$ : a morphism $(𝑥, 𝛾) \to (𝑦, 𝛿)$ is a map $𝑓 : 𝑥 \to 𝑦$ with

𝑓 ⋆ 𝛿 = 𝛾 ⋆ 𝐹 𝑓 .

The Eilenberg–Moore category as a displayed category eilenberg-moore-displayed

Fix a monad $(𝑇, 𝜂, 𝜇)$ on $𝒞︀$ . Its Eilenberg–Moore category arises in two displayed layers. The first layer is the displayed category of algebras $AlgStr (𝑇)$ of the underlying endofunctor.

The second layer, $EMStr (𝑇)$ , is displayed over the total category $Alg (𝑇)$ . Over an algebra $(𝑥, 𝛼)$ the displayed objects are the propositions that $𝛼$ satisfies the monad algebra laws:

𝜂_{𝑥} ⋆ 𝛼 = {𝗂𝖽}_{𝑥} 𝜇_{𝑥} ⋆ 𝛼 = 𝑇 𝛼 ⋆ 𝛼 .

The Eilenberg–Moore category is the total category of the tower:

EM (𝑇) = \int EMStr (𝑇) .

Definition. Initial algebra initial-algebra

Fix an endofunctor $𝐹 : 𝒞︀ \to 𝒞︀$ . An initial $𝐹$ -algebra, written $𝜇 𝐹$ , is an initial object of the category of algebras $Alg (𝐹)$ .

Unfolding the universal property: an initial algebra is an algebra $(𝜇 𝐹, in)$ such that every algebra $(𝑥, 𝛼)$ admits a unique morphism $fold 𝛼 : 𝜇 𝐹 \to 𝑥$ satisfying

in ⋆ (fold 𝛼) = 𝐹 (fold 𝛼) ⋆ 𝛼 .

Definition. Terminal coalgebra terminal-coalgebra

Fix an endofunctor $𝐹 : 𝒞︀ \to 𝒞︀$ . A terminal $𝐹$ -coalgebra, written $𝜈 𝐹$ , is a terminal object of the category of coalgebras $Coalg (𝐹)$ — equivalently, an initial algebra for $𝐹^{op}$ .

Unfolding the universal property: a terminal coalgebra is a coalgebra $(𝜈 𝐹, out)$ such that every coalgebra $(𝑥, 𝛾)$ admits a unique morphism $unfold 𝛾 : 𝑥 \to 𝜈 𝐹$ satisfying

(unfold 𝛾) ⋆ out = 𝛾 ⋆ 𝐹 (unfold 𝛾) .

Definition. Corecursive algebra corecursive-algebra

Fix an endofunctor $𝐹 : 𝒞︀ \to 𝒞︀$ . An algebra $𝛼 : 𝐹 𝐵 \to 𝐵$ is corecursive when for every coalgebra $𝛾 : 𝑋 \to 𝐹 𝑋$ there is exactly one hylomorphism from $𝛾$ to $𝛼$ . Equivalently, the functor $𝖧𝗒𝗅𝗈 (-, 𝛼)$ of the hylomorphism profunctor is constantly a singleton. It is the dual of a recursive coalgebra: an $𝐹$ -algebra in $𝒞︀$ is corecursive exactly when it is recursive as an $𝐹^{op}$ -coalgebra in ${𝒞︀}^{op}$ .

Example. If $(𝜈 𝐹, 𝗈𝗎𝗍)$ is a terminal coalgebra, then $𝗈𝗎𝗍$ is invertible and ${𝗈𝗎𝗍}^{- 1} : 𝐹 (𝜈 𝐹) \to 𝜈 𝐹$ is a corecursive algebra: a solution of $ℎ = 𝛾 ⋆ 𝐹 ℎ ⋆ {𝗈𝗎𝗍}^{- 1}$ is the same thing as a solution of $ℎ ⋆ 𝗈𝗎𝗍 = 𝛾 ⋆ 𝐹 ℎ$ , that is, a coalgebra map into the terminal coalgebra, and there is exactly one, $𝗎𝗇𝖿𝗈𝗅𝖽 𝛾$ .

Definition. Hylomorphism hylomorphism

Fix an endofunctor $𝐹 : 𝒞︀ \to 𝒞︀$ , a coalgebra $𝛾 : 𝑋 \to 𝐹 𝑋$ and an algebra $𝛼 : 𝐹 𝐵 \to 𝐵$ . A hylomorphism (or coalgebra-to-algebra morphism) from $𝛾$ to $𝛼$ is a morphism $ℎ : 𝑋 \to 𝐵$ satisfying

ℎ = 𝛾 ⋆ 𝐹 ℎ ⋆ 𝛼 .

Definition. The hylomorphism profunctor hylomorphism-profunctor

Fix an endofunctor $𝐹 : 𝒞︀ \to 𝒞︀$ . Hylomorphisms form a profunctor from coalgebras to algebras,

𝖧𝗒𝗅𝗈 : 𝖢𝗈𝖺𝗅𝗀 {(𝐹)}^{op} \times 𝖠𝗅𝗀 (𝐹) \to 𝐒𝐞𝐭,

where $𝖧𝗒𝗅𝗈 ((𝑋, 𝛾), (𝐵, 𝛼))$ is the set of $ℎ : 𝑋 \to 𝐵$ with $ℎ = 𝛾 ⋆ 𝐹 ℎ ⋆ 𝛼$ .

The action is by composition. If $𝑔 : (𝑌, 𝛿) \to (𝑋, 𝛾)$ is a coalgebra morphism ( $𝑔 ⋆ 𝛾 = 𝛿 ⋆ 𝐹 𝑔$ ) and $𝑘 : (𝐵, 𝛼) \to (𝐵', 𝛼')$ is an algebra morphism ( $𝛼 ⋆ 𝑘 = 𝐹 𝑘 ⋆ 𝛼'$ ), then $𝑔 ⋆ ℎ ⋆ 𝑘$ is again a hylomorphism:

𝛿 ⋆ 𝐹 (𝑔 ⋆ ℎ ⋆ 𝑘) ⋆ 𝛼' = 𝛿 ⋆ 𝐹 𝑔 ⋆ 𝐹 ℎ ⋆ 𝛼 ⋆ 𝑘 = 𝑔 ⋆ 𝛾 ⋆ 𝐹 ℎ ⋆ 𝛼 ⋆ 𝑘 = 𝑔 ⋆ ℎ ⋆ 𝑘 .

In these terms, a coalgebra $𝛾$ is recursive when $𝖧𝗒𝗅𝗈 (𝛾, -)$ is the terminal functor, and an algebra $𝛼$ is corecursive when $𝖧𝗒𝗅𝗈 (-, 𝛼)$ is. For the inverse of an initial algebra the profunctor is representable, $𝖧𝗒𝗅𝗈 ({𝗂𝗇}^{- 1}, -) ≅ 𝖠𝗅𝗀 (𝐹) (𝗂𝗇, -)$ , and dually $𝖧𝗒𝗅𝗈 (-, {𝗈𝗎𝗍}^{- 1}) ≅ 𝖢𝗈𝖺𝗅𝗀 (𝐹) (-, 𝗈𝗎𝗍)$ for a terminal coalgebra.

When every value of $𝖧𝗒𝗅𝗈$ is a singleton, every divide-and-conquer specification over $𝐹$ has exactly one solution. This is what local contractivity guarantees.

Definition. Recursive coalgebra recursive-coalgebra

Fix an endofunctor $𝐹 : 𝒞︀ \to 𝒞︀$ . A coalgebra $𝛾 : 𝑋 \to 𝐹 𝑋$ is recursive when for every algebra $𝛼 : 𝐹 𝐵 \to 𝐵$ there is exactly one hylomorphism $ℎ : 𝑋 \to 𝐵$ from $𝛾$ to $𝛼$ , that is, exactly one solution of

ℎ = 𝛾 ⋆ 𝐹 ℎ ⋆ 𝛼 .

Equivalently, the functor $𝖧𝗒𝗅𝗈 (𝛾, -)$ of the hylomorphism profunctor is constantly a singleton.

Recursiveness is a coalgebraic form of well-foundedness: $𝛾$ decomposes each input into subproblems, and recursiveness says that every divide-and-conquer program built on this decomposition has a unique meaning, without mentioning an order on inputs. [1] use recursive coalgebras on categories of indexed families to obtain algorithms that are correct by the type of the map they compute.

Example. If $(𝜇 𝐹, 𝗂𝗇)$ is an initial algebra, then $𝗂𝗇$ is invertible (Lambek’s lemma) and ${𝗂𝗇}^{- 1} : 𝜇 𝐹 \to 𝐹 (𝜇 𝐹)$ is a recursive coalgebra. Precomposing with the isomorphism $𝗂𝗇$ , the equation $ℎ = {𝗂𝗇}^{- 1} ⋆ 𝐹 ℎ ⋆ 𝛼$ is equivalent to $𝗂𝗇 ⋆ ℎ = 𝐹 ℎ ⋆ 𝛼$ , which says $ℎ$ is an algebra map out of the initial algebra; there is exactly one, $𝖿𝗈𝗅𝖽 𝛼$ .

The dual notion is a corecursive algebra.