ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 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 interior is a comonad on the preorder of subsets, with the open subsets as its coalgebras

Example

For a topological space $X$ , topological interior defines a comonad on the poset $(P (X), \subseteq)$ . Its coalgebras are exactly the open subsets of $X$ .

Facts & Assumptions

Given: A topological space $X$ .

[L1]

The interior $int (A)$ is the largest open subset of $A$ ; in particular $int (A) \subseteq A$ , and $A$ is open if and only if $A = int (A)$ (Interior, closure, boundary, exterior, derived set and isolated point in a topological space).

[L2]

Interior operators on a poset are exactly comonads on its associated category (On a preorder the comonads are exactly the monotone contractive maps with Gp below G(Gp); on a poset they are exactly the interior operators).

[L3]

A coalgebra structure on $A$ is an arrow $A \to G (A)$ satisfying the coalgebra equations (Coalgebra and coalgebra homomorphism for a comonad).

Verification

technique · direct

1.1

If $A \subseteq B$ , then $int (A)$ is an open subset of $B$ , so maximality in [L1] gives $int (A) \subseteq int (B)$ . Also [L1] gives $int (A) \subseteq A$ , and, since $int (A)$ is open, it gives $int (int (A)) = int (A)$ . These arguments include $A = \emptyset$ and the empty ambient space.

2.1

By [L2], the interior operator therefore defines a comonad.

L2step 1.1

3.1

By [L3], a coalgebra structure on $A$ is the inclusion $A \subseteq int (A)$ . Together with the reverse inclusion from [L1], this is equality, which holds exactly when $A$ is open.

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: 14 results over 5 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)