Alphabeta Math
TheoremStatement: AI-adaptedProof: Literature-sourcedSession-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.

The Eilenberg–Moore forgetful functor strictly creates every limit that exists in the base

Statement

For every monad T on C, the forgetful functor UT:CTC strictly creates every limit that exists in C. No preservation hypothesis on T is required.

Facts & Assumptions

Given: A diagram D:JCT with algebra structures aj:TUTDjUTDj, and a limiting cone pj:LUTDj in C.

[L1]

Strict creation requires a unique lifted limiting cone with exactly the supplied apex and legs (Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors).

Proof

technique · direct
1.1

The maps ajT(pj):TLUTDj form a cone because every arrow of D is an algebra homomorphism. By [L2] there is a unique :TLL with pj=ajT(pj) for every j.

L1L2
2.1

After composition with every pj, the equations ηL=1L and T()=μL become the corresponding algebra laws for aj by naturality; the limit legs are jointly monic by uniqueness in [L2], so both equations hold and (L,) is a T-algebra.

step 1.1L2
3.1

If a cone from an algebra (X,x) has underlying mediating arrow u:XL, then composing ux and T(u) with every pj gives the same map because each cone leg is an algebra homomorphism; joint monicity makes u an algebra homomorphism. Its uniqueness and the uniqueness of follow from the base limit, giving exactly the strict lift required by [L1], including when J is empty.

step 1.1step 2.1L1

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 17 results over 8 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