Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicableSession-authored (Fable 5 assisted)audited 2026-08-26
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.

Set-weighted limits and colimits

Definition

Let J be a small category, let M be locally small (Small, locally small, and large categories) and let D:JM be a diagram. Because J is small and Set is locally small, the functor category [J,Set] is locally small (Functor category [C,D], If C is small and D is locally small then [C,D] is locally small; if both are small it is small, Sets and functions form the large locally small category Set), so each collection of natural transformations named below is a set (Natural transformation and its components).

A weight for a limit is a functor W:JSet. A weighted limit {W,D} is an object of M that represents the functor sending an object to the set of natural transformations from the weight (Presheaves, covariantly and contravariantly representable functors, and representations), namely

M(,{W,D})    [J,Set](W,M(,D)):MopSet,

where M(m,D):JSet is the covariant hom-functor M(m,) composed with D (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category). Written out, the isomorphism is a bijection natural in m between morphisms m{W,D} and families of functions αj:W(j)M(m,Dj) satisfying D(u)αj(w)=αk(W(u)(w)) for every u:jk and wW(j).

A weight for a colimit is a presheaf W:JopSet (Opposite category Cop). A weighted colimit WD is an object of M with

M(WD,)    [Jop,Set](W,M(D,)):MSet,

naturally in the second variable, where M(D,m):JopSet sends j to M(Dj,m) and is obtained by composing the contravariant hom-functor M(,m):MopSet with Dop:JopMop.

The natural transformation corresponding to the identity of {W,D} is the counit cylinder of the weighted limit, with components κj:W(j)M({W,D},Dj); dually for a weighted colimit. Neither object need exist.

Remarks

The variances are the ones that read correctly against the presheaf convention in force in this library: a weight for a limit is covariant, matching the covariant hom-functor M(m,D), and a weight for a colimit is contravariant, matching M(D,m). Writing a colimit weight covariantly would ask for a natural transformation between functors of opposite variance, which is not a well-formed condition.

Nothing here mentions cones. A cone over D is recovered by taking the weight that is constantly a one-element set, and that this reproduces the ordinary limit is a theorem rather than a convention: Weighting by the constant singleton gives exactly the ordinary limit.

Depends on

Used by

Dependency tree · two levels

19 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources