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.
Whenever the endofunctor category exists, monads on a fixed category and their morphisms form a category
Statement
Let be a category for which the functor category exists. Monads on as objects and monad morphisms as arrows form a category.
Facts & Assumptions
Given: Monads , , and on .
A monad morphism is a natural transformation preserving the unit and multiplication (Morphisms between monads on one category).
When exists, natural transformations between endofunctors are arrows of a category and compose vertically (Functor category ).
Proof
The identity satisfies and , so it is a monad morphism.
If and are monad morphisms, then , so their vertical composite preserves the unit.
Naturality of gives ; substituting the multiplication equations for and yields , so the composite preserves multiplication.
By [L2], vertical composition is associative and the transformations in step 1.1 are identities. Steps 2.1 and 3.1 give closure under composition under the stated endofunctor-category size condition. Hence these objects and arrows form a category.
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: 12 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
- S. Mac Lane, Categories for the Working Mathematician, 2nd ed., Chapter VI, Section 1 (standard reference, not scraped)