ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-11

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 opposite-group functor is naturally isomorphic to the identity functor by inversion

Example

Reversing multiplication defines an endofunctor on groups, and inversion gives a natural isomorphism from the identity functor to it.

Facts & Assumptions

Given: A group $G$ and group homomorphisms.

[L1]

Groups and homomorphisms form $G r p$ , and group isomorphisms are bijective homomorphisms (Groups and group homomorphisms form the large locally small category $G r p$ , Group isomorphisms, automorphisms and the set $Aut (G)$ ).

[L2]

Opposite composition reverses the order (Opposite category $C^{o p}$ ); a natural isomorphism is a natural transformation with a two-sided inverse natural transformation (Natural isomorphism), which holds exactly when every component is an isomorphism (A natural transformation is a natural isomorphism exactly when every component is an isomorphism).

Verification

technique · direct

1.1

Let $G^{o p}$ have the same set and identity as $G$ , with $a ⋆ b = b a$ . A homomorphism $f : G \to H$ is also a homomorphism $G^{o p} \to H^{o p}$ , since $f (a ⋆ b) = f (b) f (a) = f (a) ⋆ f (b)$ . Thus $G \mapsto G^{o p}$ defines an endofunctor $O$ on $G r p$ .

L1L2

1.2

Define $ν_{G} : G \to G^{o p}$ by $ν_{G} (a) = a^{- 1}$ . Then $ν_{G} (a b) = b^{- 1} a^{- 1} = ν_{G} (a) ⋆ ν_{G} (b)$ , and $ν_{G}$ is its own inverse as a set map, so it is a group isomorphism.

2.1

Every homomorphism preserves inverses, so for $f : G \to H$ one has $O (f) ν_{G} (a) = f (a^{- 1}) = f (a)^{- 1} = ν_{H} f (a)$ . Hence the component square commutes.

step 1.1step 1.2

3.1

The isomorphisms $ν_{G}$ are natural by step 2.1. Therefore inversion defines a natural isomorphism $1_{G r p} ≅ O$ .

step 2.1L2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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

Emily Riehl, Category Theory in Context, Exercise 1.4.i (standard reference, not scraped)