PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passjudge 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.

Composing a dinatural transformation with a natural transformation on either side gives a dinatural transformation

Statement

Let $P^{'}, P, Q, Q^{'} : C^{o p} \times C \to D$ be functors (Product category and its projection functors, Opposite category $C^{o p}$ ), let $σ : P^{'} \Rightarrow P$ and $τ : Q \Rightarrow Q^{'}$ be natural transformations (Natural transformation and its components), and let $α : P \to Q$ be dinatural (Dinatural transformation between functors on $C^{o p} \times C$ ). Then composing a dinatural transformation with a natural transformation on either side gives a dinatural transformation: the families

$(α σ)_{c} : = α_{c} \circ σ_{c, c} : P^{'} (c, c) \to Q (c, c), (τ α)_{c} : = τ_{c, c} \circ α_{c} : P (c, c) \to Q^{'} (c, c)$

are dinatural transformations $P^{'} \to Q$ and $P \to Q^{'}$ respectively.

Facts & Assumptions

Given: Functors $P^{'}, P, Q, Q^{'}$ on $C^{o p} \times C$ , natural transformations $σ : P^{'} \Rightarrow P$ and $τ : Q \Rightarrow Q^{'}$ , and a dinatural transformation $α : P \to Q$ .

[F1]

A dinatural transformation $α : P \to Q$ is a family $α_{c} : P (c, c) \to Q (c, c)$ such that every $f : c \to c^{'}$ satisfies $Q (1_{c}, f) \circ α_{c} \circ P (f, 1_{c}) = Q (f, 1_{c^{'}}) \circ α_{c^{'}} \circ P (1_{c^{'}}, f)$ , the equation displayed by the hexagon (Dinatural transformation between functors on $C^{o p} \times C$ ).

[F2]

A natural transformation $α : F \Rightarrow G$ is a family $α_{A} : F A \to G A$ such that every $f : A \to B$ satisfies the naturality equation $G f \circ α_{A} = α_{B} \circ F f$ (Natural transformation and its components).

[F3]

The product category $C \times D$ has objects $(C, D)$ , morphisms $(f, g) : (C, D) \to (C^{'}, D^{'})$ , componentwise identities, and componentwise composition (Product category and its projection functors).

[F4]

The opposite category has the same objects and $C^{o p} (A, B) = C (B, A)$ (Opposite category $C^{o p}$ ).

Proof

technique · direct

1.1F1F3F4given

A morphism $f : c \to c^{'}$ of $C$ supplies exactly four morphisms of $C^{o p} \times C$ between the objects that occur in a hexagon at $f$ , namely $(f, 1_{c}) : (c^{'}, c) \to (c, c)$ , $(1_{c^{'}}, f) : (c^{'}, c) \to (c^{'}, c^{'})$ , $(1_{c}, f) : (c, c) \to (c, c^{'})$ and $(f, 1_{c^{'}}) : (c^{'}, c^{'}) \to (c, c^{'})$ ; the first coordinate of each is the morphism of $C^{o p}$ corresponding to $f$ or an identity.

2.1F1F2step 1.1

For the pre-composition case, naturality of $σ$ at the first two morphisms of step 1.1 gives $σ_{c, c} \circ P^{'} (f, 1_{c}) = P (f, 1_{c}) \circ σ_{c^{'}, c}$ and $σ_{c^{'}, c^{'}} \circ P^{'} (1_{c^{'}}, f) = P (1_{c^{'}}, f) \circ σ_{c^{'}, c}$ , so both legs of the hexagon for $α σ$ at $f$ equal the corresponding leg of the hexagon for $α$ precomposed with $σ_{c^{'}, c}$ ; those two legs agree by [F1], hence so do the legs for $α σ$ , and $α σ$ is dinatural.

3.1F1F2step 1.1∎

For the post-composition case, naturality of $τ$ at the last two morphisms of step 1.1 gives $Q^{'} (1_{c}, f) \circ τ_{c, c} = τ_{c, c^{'}} \circ Q (1_{c}, f)$ and $Q^{'} (f, 1_{c^{'}}) \circ τ_{c^{'}, c^{'}} = τ_{c, c^{'}} \circ Q (f, 1_{c^{'}})$ , so both legs of the hexagon for $τ α$ at $f$ equal the corresponding leg of the hexagon for $α$ postcomposed with $τ_{c, c^{'}}$ ; those two legs agree by [F1], hence so do the legs for $τ α$ , and $τ α$ is dinatural.

Remarks

Neither half assumes anything about $σ$ or $τ$ beyond naturality on the product category, and neither assumes that $α$ is natural: the argument transports the hexagon for $α$ along $σ$ or $τ$ and never builds a new one. What it does not give is a composition rule for two dinatural transformations, and no such rule holds: Dinatural transformations do not compose in general exhibits $α$ and $β$ both dinatural whose componentwise composite is not.

Depends on

Used by

FALSE: dinatural transformations compose False statement

Dependency tree · two levels

6 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

F. Loregian, (Co)end Calculus (arXiv:1501.02503v7), Exercise 1.2 (standard reference, not scraped)