ExampleConstruction: Literature-sourcedVerification: Literature-sourcedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-17

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Topological closure is a monad on the preorder of subsets

Example

For a topological space $X$ , topological closure defines a monad on the poset $(P (X), \subseteq)$ . Its algebras are exactly the closed subsets of $X$ .

Facts & Assumptions

Given: A topological space $X$ .

[L1]

Closure is monotone, extensive, and idempotent; in particular $\overline{\emptyset} = \emptyset$ and $\overline{X} = X$ (Kuratowski: operators satisfying $c (\emptyset) = \emptyset$ , $A \subseteq c (A)$ , $c (c (A)) = c (A)$ and $c (A \cup B) = c (A) \cup c (B)$ correspond bijectively to topologies).

[L2]

Closure operators on a poset are exactly monads on its associated category (On a preorder the monads are exactly the monotone extensive maps with T(Tp) below Tp; on a poset they are exactly the closure operators).

[L3]

Algebras for such a monad are exactly its fixed points (Algebras for a preorder monad are exactly its fixed objects up to preorder equivalence; on a poset they are its fixed points).

Verification

technique · direct

1.1

On $P (X)$ ordered by inclusion, [L1] says $A \mapsto \overline{A}$ is monotone and satisfies $A \subseteq \overline{A}$ .

2.1

The identity $\overline{\overline{A}} = \overline{A}$ gives the multiplication comparison and, with step 1.1, makes closure a monad by [L2].

L1L2step 1.1

3.1

By [L3], its algebra objects are the subsets $A$ with $\overline{A} = A$ , exactly the closed subsets. The boundary subsets $\emptyset$ and $X$ are fixed by [L1].

L1L3step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 25 results over 9 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

E. Riehl, Category Theory in Context, 2nd ed., Examples 5.1.7 and 5.2.6(iv) (standard reference, not scraped)