PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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.

An adjunction restricts to an equivalence on the subcategories fixed by its unit and counit

Statement

For an adjunction $F ⊣ G$ , let $C_{η}$ be the full subcategory of objects $c$ for which $η_{c}$ is an isomorphism, and let $D_{ε}$ be the full subcategory of objects $d$ for which $ε_{d}$ is an isomorphism. Then $F$ and $G$ restrict to an adjoint equivalence

$C_{η} ≃ D_{ε} .$

Facts & Assumptions

Given: An adjunction $F ⊣ G$ with unit $η$ and counit $ε$ .

[F1]

A full subcategory contains chosen objects and all morphisms between them from the ambient category (Subcategory and full subcategory).

[F2]

An equivalence consists of quasi-inverse functors and natural isomorphisms between their composites and the identity functors (Equivalence, quasi-inverse, and adjoint equivalence of categories).

[L1]

The triangle identities are $ε_{F c} F (η_{c}) = 1_{F c}$ and $G (ε_{d}) η_{G d} = 1_{G d}$ (Adjunction by unit, counit, and the triangle identities).

Proof

technique · direct

1.1L1

If $η_{c}$ is invertible, then $F (η_{c})$ is invertible, and the first triangle identity makes $ε_{F c} = F (η_{c})^{- 1}$ ; hence $F c \in D_{ε}$ .

1.2L1

Dually, if $ε_{d}$ is invertible, then the second triangle identity makes $η_{G d} = G (ε_{d})^{- 1}$ ; hence $G d \in C_{η}$ .

2.1step 1.1step 1.2F1

By [F1], $F$ and $G$ therefore restrict to functors between the two full subcategories, and the restricted unit and counit remain natural.

3.1step 2.1F2L1∎

Every component of the restricted unit and counit is an isomorphism by definition, so [F2] makes the restrictions quasi-inverse equivalences; the inherited triangle identities make the equivalence adjoint.

Depends on

Used by

Nothing in the library uses this result yet.

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

Emily Riehl, Category Theory in Context, 2nd ed., Lemma 4.2.11 (standard reference, not scraped)