Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)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.

Dinatural transformation between functors on Cop×C

Definition

Let C and D be categories (Category, object, morphism, domain, codomain, identity, composition, and hom-collection) and let

P,Q:Cop×C⟶D

be functors on the product of Cop with C (Opposite category Cop, Product category and its projection functors, Covariant functor, identity functor, composite functor, and contravariant functor). A morphism (a,b)→(a′,b′) of Cop×C is a pair (g,h) in which h:b→b′ is a morphism of C and g is a morphism of Cop from a to a′, that is, a morphism a′→a of C. Thus a morphism f:c→c′ of C supplies the four morphisms

(f,1c):(c′,c)→(c,c),(1c′,f):(c′,c)→(c′,c′),(1c,f):(c,c)→(c,c′),(f,1c′):(c′,c′)→(c,c′).

A dinatural transformation α:P→Q is a family of morphisms

αc:P(c,c)⟶Q(c,c)(c∈Ob⁡(C))

of D such that every morphism f:c→c′ of C satisfies the dinaturality equation

Q(1c,f)∘αc∘P(f,1c)  =  Q(f,1c′)∘αc′∘P(1c′,f)

between morphisms P(c′,c)→Q(c,c′). The morphism αc is the component of α at c.

The two sides pass through the six objects P(c′,c), P(c,c), Q(c,c), P(c′,c′), Q(c′,c′) and Q(c,c′), so the diagram expressing the dinaturality equation is a six-sided cycle and is called the hexagon:

P(c;c)Q(c;c)P(c0;c)Q(c;c0)P(c0;c0)Q(c0;c0)®cQ(1c;f)P(f;1c)P(1c0;f)®c0Q(f;1c0)

Remarks

A dinatural transformation is a family indexed by the objects of C and constrained by the morphisms of C, exactly as a natural transformation is (Natural transformation and its components); what differs is which constraint. A natural transformation between two functors on Cop×C is a family indexed by the pairs (a,b), and its naturality equation is imposed for every morphism of the product category. A dinatural transformation has components only on the diagonal, and the dinaturality equation is imposed only for the morphisms of C that connect two diagonal entries through the two off-diagonal entries displayed above.

At f=1c all four displayed morphisms of the product category are identities, so the hexagon reads αc=αc. The identity morphisms of C therefore impose no condition, and a dinatural transformation carries no analogue of the identity clause of a functor.

Depends on

Used by

Dependency tree · two levels

7 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