Foundational corpus mapping FC03 Riehl Category Theory in Context

FC03 — Riehl, Category Theory in Context mapping

Status: Sweep II complete for FC03. All 434 canonical units C01–C06 and the Epilogue are audited below.

Canonical catalogue: FC03 — Riehl, Category Theory in Context.

Pinned project baseline: Mathlib db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0. Current Mathlib was refreshed 2026-09-06 to 810b3888d0aa94294b18587c453466bc86c1f0fc; declarations first appearing after the project pin are reference-port routes, not pinned Mathlib.

Every canonical unit receives exactly one Sweep-II route: mathlib, project-existing, package-import, reference-port, or unmatched. Project source is searched first, followed by pinned/current Mathlib, open/current work, indexed search services, Reservoir/GitHub, and relevant source-atlas repositories. External routes record exact revision, license/provenance, and Lean/Mathlib compatibility; unmatched rows carry dated scoped negative evidence.

Provenance contract for C01

Project search: LeanCategories/** outside .lake/.agents/.git was searched first for the C01 category/functor/natural-transformation material and for each concrete example. No project-owned C01 owner was found; generic syntax/interpreter infrastructure is not credited as a source-shaped realization.
Pinned Mathlib: project pin db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0, Lean v4.33.0) is denoted P. Exact file/declaration membership was rechecked at that revision rather than inferred from git history. In particular Mathlib/CategoryTheory/Category/PartialFun.lean and its partialFunEquivPointed API are already present at the pin.
Current Mathlib/open work: upstream 810b3888d0aa94294b18587c453466bc86c1f0fc (Apache-2.0, Lean v4.34.0-rc2) was refreshed/rechecked 2026-09-06. Post-pin declarations would be reference-port; no C01 row below depends on a current-only Mathlib declaration.
External/source-atlas search: harfe/fixed-point-theorems-lean4@770940ddf9878cf61952ed53d910b92bca841838 is MIT and pins Lean v4.32.0 / Mathlib 81a5d257c8e410db227a6665ed08f64fea08e997; its Brouwer theorem is therefore reference-port, not importable. rkirov/category-theory-in-context-lean is MIT but on Lean v4.24.0-rc1 and covers only earlier Chapter-1 material, yielding no additional later-C01 owner. Qiu233/ctic@7929dc698ee3eb5de5cbe2f0cf0dcbcf5a4a7c79 contains an EssentiallyDiscrete definition but no repository license was established and it pins Lean v4.25.0-rc2 / Mathlib e721e526…, so it is not a usable route.
N marks dated 2026-09-06 negative evidence after project-first search, pinned/current Mathlib, relevant source-atlas repositories, GitHub/Reservoir, and Loogle/LeanSearch as feasible. Concrete bundles are not credited from generic ingredients unless a declaration realizes the source example.

C01 — Categories, Functors, and Natural Transformations

FC03 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
`FC03-C01-U001`	exact match	`mathlib`	`Mathlib/CategoryTheory/Category/Basic.lean::CategoryStruct`; `Category`	P	Direct object, typed-hom, identity, composition, unit and associativity structure.
`FC03-C01-U002`	unmatched after search	`unmatched`	—	N	No arrow-only/partial-composition presentation equivalent to the source definition was found; Mathlib takes objects and typed homs as primitive.
`FC03-C01-U003`	unmatched bundled example	`unmatched`	—	N	Many listed concrete categories exist separately, but no realization of the complete source bundle was found, notably including the manifold/model-theoretic examples in the stated categorical form.
`FC03-C01-U004`	unmatched bundled example	`unmatched`	—	N	Matrix, one-object, preorder and discrete categories exist, but the complete abstract-example bundle is absent, in particular the source homotopy and measure categories.
`FC03-C01-U005`	exact match	`mathlib`	`Mathlib/CategoryTheory/Category/Basic.lean::SmallCategory`	P	Direct universe-theoretic formulation of a small category.
`FC03-C01-U006`	exact data, dependent encoding	`mathlib`	`Mathlib/Combinatorics/Quiver/Basic.lean::Quiver.Hom`; `Mathlib/CategoryTheory/Category/Basic.lean::CategoryStruct.id`; `CategoryStruct.comp`	P	Source/domain/codomain are encoded by the indices of `X ⟶ Y`, rather than separate maps on one morphism set; identities and composition are the same data.
`FC03-C01-U007`	exact match	`mathlib`	`Mathlib/CategoryTheory/EssentiallySmall.lean::LocallySmall`; `LocallySmall.hom_small`	P	Exact universe-aware locally-small condition.
`FC03-C01-U008`	exact match	`mathlib`	`Mathlib/Combinatorics/Quiver/Basic.lean::Quiver.Hom`; notation `X ⟶ Y`	P	Exactly the hom-set/type object, with Mathlib notation replacing `C(X,Y)`.
`FC03-C01-U009`	exact match	`mathlib`	`Mathlib/CategoryTheory/Iso.lean::IsIso`; `Iso`	P	Direct two-sided-inverse and bundled object-isomorphism notions.
`FC03-C01-U010`	exact match	`mathlib`	`Mathlib/CategoryTheory/Endomorphism.lean::End`; `Aut`	P	Exact endomorphism and automorphism objects.
`FC03-C01-U011`	unmatched bundled example	`unmatched`	—	N	Set/algebra/topology isomorphism instances exist separately, but no source-shaped bundle including homotopy equivalences in the homotopy category was found.
`FC03-C01-U012`	exact match	`mathlib`	`Mathlib/CategoryTheory/Groupoid.lean::Groupoid`; `IsGroupoid`	P	Exactly the condition that every morphism is invertible.
`FC03-C01-U013`	exact examples	`mathlib`	`Mathlib/CategoryTheory/SingleObj.lean::SingleObj`; `Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean::FundamentalGroupoid`; `fundamentalGroupoidFunctor`	P	Directly realizes groups as one-object groupoids and the fundamental groupoid of a space.
`FC03-C01-U014`	unmatched bundled construction	`unmatched`	—	N	Full/wide subcategory mechanisms and several algebraic forgetful functors exist, but no declaration realizes the arbitrary selected-object/selected-morphism definition together with the full `CRing ⊂ Ring ⊂ Rng` example chain.
`FC03-C01-U015`	exact match	`mathlib`	`Mathlib/CategoryTheory/Core.lean::Core`; `CoreHom`; `coreCategory`; `Core.inclusion`	P	Exact maximal subgroupoid: all objects and precisely the invertible morphisms.
`FC03-C01-U016`	exact match	`mathlib`	`Mathlib/CategoryTheory/Opposites.lean`; `Mathlib/Combinatorics/Quiver/Basic.lean::Quiver.Hom.op`; `Quiver.Hom.unop`	P	Exact reversal of arrows and composition.
`FC03-C01-U017`	exact match	`mathlib`	`Mathlib/CategoryTheory/Opposites.lean::opOp`; `unopUnop`; `opOpEquivalence`; `Mathlib/Data/Opposite.lean::op_unop`; `unop_op`; `Mathlib/Tactic/ToDual.lean`	P	Opposite is involutive up to the canonical equivalence/equalities, and `to_dual` formalizes systematic syntactic dualization.
`FC03-C01-U018`	unmatched bundled example	`unmatched`	—	N	Opposite preorders and action infrastructure exist, but the complete source examples are absent, notably the matrix-handedness categorical comparison.
`FC03-C01-U019`	exact metatheoretic realization	`mathlib`	`Mathlib/Tactic/ToDual.lean`; pervasive `@[to_dual]` declarations	P	Mathlib implements the duality principle by generating arrow-reversed dual declarations rather than by a proposition named “duality principle.”
`FC03-C01-U020`	exact match	`mathlib`	`Mathlib/CategoryTheory/Yoneda.lean::isIso_iff_yoneda_map_bijective`; `isIso_iff_coyoneda_map_bijective`	P	Exact characterization of an isomorphism by bijectivity of every pre/postcomposition hom map.
`FC03-C01-U021`	exact match	`mathlib`	`Mathlib/CategoryTheory/Yoneda.lean::isIso_iff_yoneda_map_bijective`; `isIso_iff_coyoneda_map_bijective`	P	The representable detection statement is the same theorem in universe-aware form.
`FC03-C01-U022`	exact match	`mathlib`	`Mathlib/CategoryTheory/Category/Basic.lean::Mono`; `Epi`	P	Definitions are exactly left/right cancellation; the dual pair is generated systematically.
`FC03-C01-U023`	exact match	`mathlib`	`Mathlib/CategoryTheory/Category/Basic.lean::mono_iff_forall_injective`; `epi_iff_forall_injective`	P	Exact hom-map injectivity characterizations.
`FC03-C01-U024`	exact match	`mathlib`	`Mathlib/CategoryTheory/Types/Basic.lean::mono_iff_injective`; `epi_iff_surjective`	P	Exactly the Set/Type mono-is-injective and epi-is-surjective result.
`FC03-C01-U025`	exact match	`mathlib`	`Mathlib/CategoryTheory/EpiMono.lean::SplitMono`; `SplitEpi`; `IsSplitMono`; `IsSplitEpi`; `Mathlib/CategoryTheory/Retract.lean::Retract`	P	Direct chosen section/retraction and retract data.
`FC03-C01-U026`	unmatched concrete example	`unmatched`	—	N	Localization maps are proved epic in ring categories, but no declaration realizes the concrete `ℤ → ℚ` map as simultaneously mono, epi, and non-isomorphic in the source category.
`FC03-C01-U027`	exact match	`mathlib`	`Mathlib/CategoryTheory/Category/Basic.lean::mono_comp`; `mono_of_mono`; `epi_comp`; `epi_of_epi`	P	Exact composition and cancellation laws for monos/epis.
`FC03-C01-U028`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/Basic.lean::Functor`	P	Exact object/map assignment with identity and composition laws.
`FC03-C01-U029`	unmatched bundled example	`unmatched`	—	N	Many listed functors exist separately, but the complete source bundle is not realized; targeted search found no derivative/Jacobian categorical example completing it.
`FC03-C01-U030`	stronger theorem, incompatible pin	`reference-port`	`harfe/fixed-point-theorems-lean4@770940ddf9878cf61952ed53d910b92bca841838`, `FixedPointTheorems/brouwer.lean::brouwer_fixed_point`; `brouwer_fixed_point_isFixedPt`; `brouwer_fixedPoints_nonempty`	R	Stronger Brouwer theorem for every continuous self-map of a nonempty compact convex subset of a finite-dimensional real normed space; specialize to the closed disk. MIT, Lean v4.32.0 / Mathlib `81a5d257…`, so reference-port rather than import.
`FC03-C01-U031`	unmatched concrete theory	`unmatched`	—	N	No Lean realization of `FinMetric`, `Cluster`, `PCluster`, Kleinberg’s impossibility theorem, or the distinguished persistent-clustering functor was found in the scoped search.
`FC03-C01-U032`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/Basic.lean::Functor`; `Mathlib/CategoryTheory/Opposites.lean`	P	A contravariant functor is represented exactly as `Cᵒᵖ ⥤ D`; reversed composition is inherited from the opposite category.
`FC03-C01-U033`	unmatched convention	`unmatched`	—	N	The source item is a diagram-drawing convention; no corresponding formal declaration was found.
`FC03-C01-U034`	unmatched bundled example	`unmatched`	—	N	Duals, spectra, presheaves, simplicial objects and opens provide ingredients, but no declaration set realizes the complete contravariant-example bundle.
`FC03-C01-U035`	exact match	`mathlib`	`Mathlib/CategoryTheory/Iso.lean::Functor.mapIso`; `Functor.map_isIso`	P	Exact preservation of isomorphisms by arbitrary functors.
`FC03-C01-U036`	exact match	`mathlib`	`Mathlib/CategoryTheory/Action/Basic.lean::Action`; `Action.functorCategoryEquivalence`	P	`Action V G ≌ SingleObj G ⥤ V` is exactly the source action/functor correspondence; opposite groups/categories give the right-action convention.
`FC03-C01-U037`	exact match	`mathlib`	`Mathlib/CategoryTheory/Action/Basic.lean::Action.ρAut`	P	An action gives a homomorphism into automorphisms, and inversion in the group corresponds to inverse automorphisms.
`FC03-C01-U038`	exact match	`mathlib`	`Mathlib/CategoryTheory/EpiMono.lean::SplitEpi.map`; generated dual `SplitMono.map`	P	Exact preservation of chosen splittings by a functor.
`FC03-C01-U039`	exact match	`mathlib`	`Mathlib/CategoryTheory/Yoneda.lean::yoneda`; `coyoneda`	P	Exact represented covariant and contravariant hom functors.
`FC03-C01-U040`	exact encoding	`mathlib`	`Mathlib/CategoryTheory/Products/Bifunctor.lean::Bifunctor.map_id`; `map_id_comp`; `map_comp_id`	P	Mathlib represents a bifunctor literally as a functor `C × D ⥤ E`; the cited API exposes the two-variable functor laws.
`FC03-C01-U041`	exact match	`mathlib`	`Mathlib/CategoryTheory/Products/Basic.lean`; `prod_id`; `prod_comp`	P	Exact product category with componentwise objects, morphisms, identities and composition.
`FC03-C01-U042`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/Hom.lean::Functor.hom`	P	The two-sided hom functor `Cᵒᵖ × C ⥤ Type` maps a morphism by pre- and postcomposition exactly as in the source.
`FC03-C01-U043`	exact universe translation	`mathlib`	`Mathlib/CategoryTheory/Category/Cat.lean::Cat`; `Cat.Hom`; `Mathlib/CategoryTheory/EssentiallySmall.lean::locallySmall_max`	P	Mathlib uses universe-polymorphic `Cat.{v,u}` rather than two literal constants `Cat`/`CAT`; larger universe levels realize the same size distinction.
`FC03-C01-U044`	exact match	`mathlib`	`Mathlib/CategoryTheory/Category/Cat.lean::Cat.equivOfIso`; `Cat.isoOfEquiv`	P	An isomorphism in `Cat` has strictly inverse functors; `isoOfEquiv` records the extra strictness needed to upgrade a categorical equivalence.
`FC03-C01-U045`	unmatched bundled example	`unmatched`	—	N	Several strict-isomorphism components exist individually, but the full source example bundle, especially matrix transpose/module-handedness, is not realized.
`FC03-C01-U046`	exact mathematical match	`mathlib`	`Mathlib/FieldTheory/Galois/Basic.lean::intermediateFieldEquivSubgroup`; `Mathlib/CategoryTheory/Category/Preorder.lean::OrderIso.equivalence`	P	The finite Galois correspondence is an order-reversing equivalence between intermediate fields and subgroups; thin-category translation gives precisely the categorical correspondence.
`FC03-C01-U047`	exact match	`mathlib`	`Mathlib/CategoryTheory/Category/PartialFun.lean::PartialFun`; category instance	P	Exact category of types/sets and partially defined functions. The file is present at the pinned revision.
`FC03-C01-U048`	exact equivalence	`mathlib`	`Mathlib/CategoryTheory/Category/PartialFun.lean::pointedToPartialFun`; `partialFunToPointed`; `partialFunEquivPointed`; `typeToPartialFunIsoPartialFunToPointed`	P	Direct adding/removing-basepoint comparison and categorical equivalence. The source highlights one strict composite identity; Mathlib packages the comparison principally through equivalence/natural-isomorphism data.
`FC03-C01-U049`	exact match	`mathlib`	`Mathlib/CategoryTheory/NatTrans.lean::NatTrans`; `Mathlib/CategoryTheory/NatIso.lean::isIso_of_isIso_app`; `NatTrans.isIso_iff_isIso_app`	P	Exact naturality-component definition and pointwise invertibility criterion for natural isomorphisms.
`FC03-C01-U050`	unmatched bundled example	`unmatched`	—	N	Individual ingredients exist, but no source-shaped bundle realizes the natural/nonnatural examples, notably finite-dimensional `V ≅ V*` nonnaturality and the theorem that every natural `V → V ⊗ V` is zero.
`FC03-C01-U051`	unmatched theorem	`unmatched`	—	N	Torsion subgroups, quotients, PID structure theorems and noncanonical decompositions exist, but no theorem proves that splittings `A ≅ T A ⊕ A/T A` cannot be chosen naturally.
`FC03-C01-U052`	unmatched theorem	`unmatched`	—	N	Riesz–Markov–Kakutani infrastructure exists for positive functionals/regular measures, but no natural isomorphism of signed Baire measures with the continuous dual over compact Hausdorff spaces was found.
`FC03-C01-U053`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/Hom.lean::Functor.hom`; `Mathlib/CategoryTheory/Yoneda.lean::yoneda`; `coyoneda`	P	The two-sided hom functor encodes commuting pre/postcomposition, and Yoneda/coyoneda supply the induced natural transformations.
`FC03-C01-U054`	strong ingredients, source package absent	`unmatched`	partial: `Mathlib/Logic/Equiv/Sum.lean::Equiv.prodSumDistrib`; `Mathlib/Logic/Equiv/Prod.lean::Equiv.curry`; `Mathlib/CategoryTheory/Limits/Types/Products.lean::Types.binaryProductIso`; `Mathlib/CategoryTheory/Limits/Types/Coproducts.lean::Types.binaryCoproductIso`; `Mathlib/Data/Fintype/Prod.lean::Fintype.card_prod`; `Mathlib/Data/Fintype/Sum.lean::Fintype.card_sum`	N	Canonical set equivalences, categorical products/coproducts, and finite-cardinality identities are present, but neither pinned nor current Mathlib packages the source’s natural distributive/exponential isomorphisms together with the `Fin_iso` decategorification statement. Generic ingredients are insufficient for this bundled unit.
`FC03-C01-U055`	unmatched theorem	`unmatched`	—	N	No declaration was found identifying natural transformations `F ⇒ G` with functors `C × 2 ⥤ D` restricting to `F,G`; arrow-category and currying infrastructure do not realize the walking-arrow theorem.
`FC03-C01-U056`	partial walking-isomorphism coverage	`unmatched`	partial: `Mathlib/AlgebraicTopology/SimplicialSet/CoherentIso.lean::WalkingIso`; `WalkingIso.toIso`; `WalkingIso.fromIso`; `WalkingIso.equiv`	N	Mathlib realizes the free/walking isomorphism, but the source unit also requires the free walking arrow and its `C × 2` interpretation; no complete declaration-level realization was found.
`FC03-C01-U057`	exact match	`mathlib`	`Mathlib/CategoryTheory/Equivalence.lean::CategoryTheory.Equivalence`; `Equivalence.mk`	P	`Equivalence.mk F G η ε` accepts quasi-inverse functors with natural isomorphisms to the identities and packages precisely a categorical equivalence.
`FC03-C01-U058`	exact match	`mathlib`	`Mathlib/CategoryTheory/Equivalence.lean::Equivalence.refl`; `Equivalence.symm`; `Equivalence.trans`	P	Directly proves categorical equivalence is reflexive, symmetric and transitive.
`FC03-C01-U059`	exact match	`mathlib`	`Mathlib/CategoryTheory/Category/PartialFun.lean::partialFunEquivPointed`	P	Exact equivalence between partial functions and pointed sets.
`FC03-C01-U060`	unmatched concrete comparison	`unmatched`	partial: `Mathlib/CategoryTheory/Preadditive/Mat.lean::Mat_`; `equivalenceSelfOfHasFiniteBiproducts`	N	Generic finite-biproduct matrix machinery does not instantiate the source comparison `Mat_k → Vect_k^{basis} → Vect_k^{fd}` with coordinate and quasi-inverse functors.
`FC03-C01-U061`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/FullyFaithful.lean::Functor.Full`; `Functor.Faithful`; `Mathlib/CategoryTheory/EssentialImage.lean::Functor.essImage`; `Functor.EssSurj`	P	Definitions are exactly surjectivity/injectivity on hom maps and essential surjectivity on objects up to isomorphism.
`FC03-C01-U062`	exact interface match	`mathlib`	`Mathlib/CategoryTheory/Functor/FullyFaithful.lean::Functor.Full`; `Functor.Faithful`; `Functor.FullyFaithful`; `Functor.map_injective`; `Functor.map_surjective`	P	Exact full/faithful/fully-faithful terminology; source object-injectivity is the ordinary predicate `Function.Injective F.obj`.
`FC03-C01-U063`	exact match	`mathlib`	`Mathlib/CategoryTheory/Equivalence.lean::Functor.IsEquivalence`; `Equivalence.fullyFaithfulFunctor`; `Equivalence.essSurj_functor`; `Functor.IsEquivalence.mk'`; `Functor.asEquivalence`	P	`IsEquivalence` is full + faithful + essentially surjective; the converse construction is noncomputable, matching the source’s use of choice.
`FC03-C01-U064`	exact match	`mathlib`	`Mathlib/CategoryTheory/HomCongr.lean::Iso.homCongr`	P	Gives the canonical bijection of hom-sets induced by endpoint isomorphisms, with exactly the unique commuting transport used in the source.
`FC03-C01-U065`	unmatched concrete equivalence	`unmatched`	—	N	No declaration packages the concrete equivalence `Mat_k ≃ Vect_k^{fd}`; generic matrices/linear maps and `Preadditive.Mat` do not realize this source example.
`FC03-C01-U066`	exact match	`mathlib`	`Mathlib/CategoryTheory/IsConnected.lean::Zag`; `Zigzag`; `IsPreconnected`; `IsConnected`; `isConnected_of_zigzag`; `exists_zigzag'`	P	Exact finite-zigzag characterization; Mathlib’s `IsConnected` additionally includes nonemptiness, excluding the vacuous empty category.
`FC03-C01-U067`	unmatched theorem	`unmatched`	partial: `Mathlib/CategoryTheory/Groupoid/VertexGroup.lean::Groupoid.vertexGroup`; `vertexGroupIsomOfPath`; `Mathlib/CategoryTheory/SingleObj.lean::SingleObj.functor`; `SingleObj.toEnd`	N	The vertex automorphism group and path-induced isomorphisms exist, but no theorem packages an arbitrary connected groupoid as equivalent to the one-object category of a chosen vertex group.
`FC03-C01-U068`	exact match	`mathlib`	`Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::FundamentalGroup.fundamentalGroupMulEquivOfPathConnected`	P	Under path connectedness, gives exactly the change-of-basepoint multiplicative equivalence of fundamental groups.
`FC03-C01-U069`	unmatched naturality statement	`unmatched`	—	N	Basepoint/path-change equivalences exist, but no declaration realizes the natural equivalence from based path-connected spaces into the fundamental groupoid together with the stated nonnaturality of a path-choice inverse.
`FC03-C01-U070`	exact match	`mathlib`	`Mathlib/CategoryTheory/Skeletal.lean::Skeletal`; `IsSkeletonOf`; `Skeleton`; `fromSkeleton`; `skeletonEquivalence`; `skeleton_isSkeleton`; `Equivalence.skeletonEquiv`	P	Exact skeletal/skeleton definitions and the canonical equivalence of a category with its skeleton.
`FC03-C01-U071`	unmatched full remark	`unmatched`	partial: `Mathlib/CategoryTheory/Skeletal.lean::mapSkeleton`; `toSkeletonFunctorCompMapSkeletonIso`	N	Skeleton mapping infrastructure exists, but no declaration packages both the nonfunctoriality of arbitrary representative choices and the strict-isomorphism upgrade for equivalences between skeletal categories.
`FC03-C01-U072`	unmatched bundled examples	`unmatched`	—	N	Generic skeleton infrastructure is present, but the complete source suite—connected groupoids, finite-dimensional vector spaces/matrices, and the finite-set isomorphism groupoid with symmetric automorphism groups—is not realized declaration-wise.
`FC03-C01-U073`	exact match	`mathlib`	`Mathlib/CategoryTheory/Action/Basic.lean::ActionCategory`; `hom_as_subtype`; `stabilizerIsoEnd`; `endMulEquivSubgroup`; `Mathlib/GroupTheory/GroupAction/Quotient.lean::orbitEquivQuotientStabilizer`; `MulAction.card_orbit_mul_card_stabilizer_eq_card_group`	P	Action-groupoid homs, endomorphism stabilizers, orbit components and finite orbit–stabilizer are all realized directly.
`FC03-C01-U074`	unmatched second notion	`unmatched`	partial: `Mathlib/CategoryTheory/EssentiallySmall.lean::EssentiallySmall`	N	`EssentiallySmall` is exact, but no `EssentiallyDiscrete` declaration exists in pinned/current Mathlib. `Qiu233/ctic@7929dc…` has one but lacks established license and is toolchain-incompatible, so it is not a usable route.
`FC03-C01-U075`	exact structural coverage	`mathlib`	`Mathlib/CategoryTheory/EssentiallySmall.lean::locallySmall_congr`; `Mathlib/CategoryTheory/Products/Basic.lean::Equivalence.prod`; `Mathlib/CategoryTheory/Functor/ReflectsIso/Basic.lean::FullyFaithful.reflectsIsomorphisms`; `Mathlib/CategoryTheory/Groupoid.lean::isGroupoid_of_reflects_iso`	P	These directly give the stated invariance under equivalence of local smallness, products/opposites, groupoid status and isomorphism detection.
`FC03-C01-U076`	exact match	`mathlib`	`Mathlib/CategoryTheory/EssentialImage.lean::Functor.essImage`; `EssImageSubcategory`; `toEssImage`; `toEssImageCompι`	P	A fully faithful functor factors through its full essential-image subcategory, and the factor is full, faithful and essentially surjective, hence an equivalence.
`FC03-C01-U077`	unmatched generic diagram predicate	`unmatched`	—	N	`CommSq`, path categories and categorical quotients provide ingredients, but no generic declaration states that a displayed directed graph is commutative exactly when every two parallel composable paths have equal composites.
`FC03-C01-U078`	exact match	`mathlib`	`Mathlib/CategoryTheory/Monoidal/Mon.lean::MonObj`; `Mathlib/CategoryTheory/Monoidal/Internal/Types/Basic.lean::monTypeEquivalenceMon`	P	Internal monoids in `Type` are equivalent to ordinary monoids, exactly realizing the source internal-monoid diagram.
`FC03-C01-U079`	exact specialization	`mathlib`	`Mathlib/CategoryTheory/Monoidal/Mon.lean::MonObj`; `Mathlib/Topology/Category/TopCat/Monoidal.lean` cartesian monoidal instance	P	A `MonObj` in `TopCat` is precisely a space with continuous multiplication/unit satisfying the monoid diagrams.
`FC03-C01-U080`	exact specialization	`mathlib`	`Mathlib/CategoryTheory/Monoidal/Internal/Module.lean::monModuleEquivalenceAlgebra`; `Mathlib/Algebra/Category/AlgCat/Basic.lean::AlgCat.intEquivalence`	P	At `R = ℤ`, internal monoids in `ModuleCat ℤ` are associative unital `ℤ`-algebras, identified with rings; this is the tensor-product formulation in the source.
`FC03-C01-U081`	exact match	`mathlib`	`Mathlib/CategoryTheory/Monoidal/Internal/Module.lean::monModuleEquivalenceAlgebra`	P	For a field `k`, `Mon (ModuleCat k) ≌ AlgCat k` is exactly the internal-monoid description of unital associative `k`-algebras.
`FC03-C01-U082`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/Basic.lean::Functor`	P	A diagram of shape `J` in `C` is represented literally as a functor `J ⥤ C`; Mathlib is universe-polymorphic rather than imposing the source’s smallness convention syntactically.
`FC03-C01-U083`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/Basic.lean::Functor.map_id`; `Functor.map_comp`; `Mathlib/CategoryTheory/CommSq.lean::CommSq.map_commSq`	P	Functors preserve path composites, hence commutative diagrams; `map_commSq` is the explicit square case.
`FC03-C01-U084`	unmatched source indexing example	`unmatched`	partial: `Mathlib/CategoryTheory/CommSq.lean::CommSq`; `Mathlib/CategoryTheory/Square.lean::Square`	N	Commuting squares are formalized, but no declaration identifies them with diagrams indexed by the source’s explicit category `2 × 2`; generic square structures are not credited as that example.
`FC03-C01-U085`	exact generators/relations infrastructure	`mathlib`	`Mathlib/CategoryTheory/PathCategory/Basic.lean::PathCategory.lift`; `Mathlib/CategoryTheory/Quotient.lean::HomRel`; `Congruence`; `Quotient.lift`; `Quotient.lift_unique`; `Quotient.sound`	P	Free path categories followed by quotienting by a composition-stable relation give precisely a category presented by generators and relations and its universal extension property.
`FC03-C01-U086`	exact match	`mathlib`	`Mathlib/CategoryTheory/ComposableArrows/Basic.lean::ComposableArrows`; `mk₃`	P	`ComposableArrows C 3 = Fin 4 ⥤ C` realizes three composable arrows together with all functorially forced composites.
`FC03-C01-U087`	unmatched explicit indexing example	`unmatched`	partial: `Mathlib/CategoryTheory/CommSq.lean::CommSq.horiz_comp`	N	Horizontal square pasting proves the outer rectangle commutes, but no declaration realizes the source’s explicit `2 × 3` indexing-category presentation.
`FC03-C01-U088`	exact relation closure	`mathlib`	`Mathlib/CategoryTheory/Quotient.lean::HomRel.CompClosure.intro`; category associativity	P	Composition closure is exactly contextual substitution of equal/related subpaths inside larger paths.
`FC03-C01-U089`	unmatched theorem	`unmatched`	—	N	No theorem was found stating that commutativity of simple acyclic poset-indexed diagrams can be checked on a source-specified minimal family of relations/subdiagrams.
`FC03-C01-U090`	exact match	`mathlib`	`Mathlib/CategoryTheory/Iso.lean::Iso.inv_comp_eq`; `Iso.eq_inv_comp`; `Iso.comp_inv_eq`; `Iso.eq_comp_inv`	P	These equivalences transport a commuting equation through an invertible edge exactly as in the source triangle manipulation.
`FC03-C01-U091`	exact match	`mathlib`	`Mathlib/CategoryTheory/CommSq.lean::CommSq.vert_inv`; `CommSq.horiz_inv`	P	Exact theorem that reversing isomorphism edges of a commuting square preserves commutativity.
`FC03-C01-U092`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean::IsInitial`; `IsTerminal`; `IsInitial.ofUniqueHom`; `IsTerminal.ofUniqueHom`	P	Exact unique-morphism definitions/interfaces for initial and terminal objects.
`FC03-C01-U093`	unmatched bundled examples	`unmatched`	partial: `TopCat.isInitialPEmpty`; `TopCat.isTerminalPUnit`; `CommRingCat.zIsInitial`; `CommRingCat.punitIsTerminal`	N	Numerous individual initial/terminal examples exist, but the complete source example/nonexample suite across sets, topology, pointed sets, modules, groups, rings/rngs, fields, `Cat`, and preorders is not realized.
`FC03-C01-U094`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean::IsInitial.hom_ext`; `IsTerminal.hom_ext`	P	Uniqueness from an initial source or into a terminal target gives exactly the equality of parallel composites used in the source.
`FC03-C01-U095`	exact structural match	`mathlib`	`Mathlib/CategoryTheory/ConcreteCategory/Basic.lean::ConcreteCategory`; `forget`	P	Mathlib encodes concreteness structurally and canonically supplies a faithful forgetful functor to `Type`, equivalent to the source datum.
`FC03-C01-U096`	unmatched concrete example	`unmatched`	—	N	No categorical graph declaration realizes the combined `V ⊔ E` faithful underlying-set functor together with proofs that the vertex-only and edge-only forgetful functors are nonfaithful.
`FC03-C01-U097`	exact consequence	`mathlib`	`Mathlib/CategoryTheory/Functor/FullyFaithful.lean::Functor.map_injective`; `Mathlib/CategoryTheory/Functor/Basic.lean::Functor.map_comp`; `ConcreteCategory` faithful forget	P	Faithfulness is hom-map injectivity, so equality of mapped path composites reflects to equality before applying the functor.
`FC03-C01-U098`	exact match	`mathlib`	`Mathlib/CategoryTheory/CommSq.lean::CommSq.eq_of_mono`; `CommSq.eq_of_epi`; `Mathlib/CategoryTheory/EpiMono.lean::cancel_mono`; `cancel_epi`	P	Directly formalizes cancellation in pasted diagrams under the required mono/epi outer edge.
`FC03-C01-U099`	exact consequence	`mathlib`	`Mathlib/CategoryTheory/CommSq.lean::CommSq.horiz_comp`; `Mathlib/CategoryTheory/EpiMono.lean::cancel_mono`; `cancel_epi`	P	Pasting supplies the outer rectangle; the known inner square reduces the missing one exactly to mono/epi cancellation.
`FC03-C01-U100`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/Category.lean::Functor.category`	P	Objects are functors and morphisms are natural transformations, exactly the functor category `D^C`.
`FC03-C01-U101`	exact match	`mathlib`	`Mathlib/CategoryTheory/NatTrans.lean::vcomp`; `vcomp_app`; `Mathlib/CategoryTheory/Functor/Category.lean::NatTrans.vcomp_app'`	P	Vertical composition of natural transformations is componentwise composition, exactly the source formula.
`FC03-C01-U102`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/Category.lean::Functor.category`; `NatTrans.id`; `NatTrans.vcomp`	P	Functors with natural transformations, identity transformations and vertical composition form the source functor category.
`FC03-C01-U103`	exact size theorem plus exponential construction	`mathlib`	`Mathlib/CategoryTheory/EssentiallySmall.lean`, instance `[LocallySmall A] (C : Type w) [SmallCategory C] : LocallySmall (C ⥤ A)`; `Mathlib/CategoryTheory/Category/Cat/CartesianClosed.lean::Cat.exp`; `curryingIso`; `Mathlib/CategoryTheory/Whiskering.lean::whiskeringLeft`; `whiskeringRight`	P	The local-smallness theorem has exactly the source hypotheses. `Cat.exp C` forms the functor category out of `C`; pre- and postcomposition supply the contravariant/covariant functoriality. Universe-polymorphic `Cat` expresses the source’s `Cat`/`CAT` size regimes.
`FC03-C01-U104`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/Category.lean::NatTrans.hcomp`	P	Horizontal composition is defined componentwise as `β.app (F.obj X) ≫ I.map (α.app X)`, the source formula up to notation/convention.
`FC03-C01-U105`	exact match	`mathlib`	`Mathlib/CategoryTheory/Whiskering.lean::Functor.whiskerLeft`; `Functor.whiskerRight`; `whiskeringLeft`; `whiskeringRight`	P	Exact left and right whiskering of natural transformations and their functorial packaging.
`FC03-C01-U106`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/Category.lean::NatTrans.exchange`	P	This is the middle-four interchange law for horizontal and vertical composition.
`FC03-C01-U107`	exact structural realization	`mathlib`	`Mathlib/CategoryTheory/Bicategory/Basic.lean::Bicategory`; `Mathlib/CategoryTheory/Bicategory/Strict/Basic.lean::Bicategory.Strict`; `Mathlib/CategoryTheory/Category/Cat.lean::Cat.bicategory`; `Cat.bicategory.strict`	P	Mathlib’s `Bicategory.Strict` is explicitly the library encoding of a strict 2-category: homs are categories, 1-composition is strictly associative/unital, 2-cells compose in hom categories, and whiskering satisfies interchange. `Cat` is instantiated as such.

Provenance contract for C02

Project search: LeanCategories/** outside .lake/.agents/.git was searched first for representability, Yoneda, categories of elements, actions/torsors, polynomial and tensor universal properties, and every concrete C02 example. LeanCategories/ForMathlib/CategoryOfElementsCocartesian.lean extends Mathlib’s category-of-elements projection by a cocartesian property but does not realize a C02 source unit; no project-owned C02 route was found.
Pinned Mathlib: project pin db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0, Lean v4.33.0), denoted P, was declaration-checked. Its Yoneda.lean, Elements.lean, Limits/Elements.lean, tensor-product, torsor, polynomial, monoid-algebra, and group-action APIs provide the exact structural matches below.
Current/open Mathlib: upstream 810b3888d0aa94294b18587c453466bc86c1f0fc (Apache-2.0, Lean v4.34.0-rc2) was rechecked 2026-09-06. Open PR #15055 at head 1139ef2782492a1c9a9cf94e210cca8ffbae85b0, Mathlib/CategoryTheory/ConcreteCategory/Pointed.lean, is revision-specific reference-port: it is Apache-2.0, still open with merge conflicts, and its head uses Lean v4.10.0-rc2, so it is not directly importable against this project’s pin.
Book/source-atlas search: rkirov/category-theory-in-context-lean@cae97fae75665bb93d36ff763c9243346806d12a is MIT, Lean v4.24.0-rc1 / Mathlib 4b9a202af4759dfe2119961646e4c0f4aa2c5778, and still contains only Chapter 1 §§1.1–1.4 plus an appendix; it owns no C02 unit. Qiu233/ctic@7929dc698ee3eb5de5cbe2f0cf0dcbcf5a4a7c79 has related Yoneda/representation code but no established repository license and uses Lean v4.25.0-rc2 / Mathlib e721…, so it is not a usable route. A MiscLean discrete-dynamics candidate has proof holes, no declared license, and Lean v4.24.0-rc1, so it is likewise not credited.
N denotes dated 2026-09-06 negative evidence after project-first search, pinned/current Mathlib, relevant source-atlas and Reservoir/GitHub Lean repositories/open work, and Loogle/LeanSearch as feasible. Generic ingredients are not credited for a concrete source example unless an existing declaration realizes that example.

C02 — Representability and the Yoneda Lemma

FC03 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
`FC03-C02-U001`	unmatched concrete example	`unmatched`	—	N	Pinned/current Mathlib has ordinary `Nat` recursion/induction, but no declaration packages discrete dynamical systems and the initial pointed endomap `(ℕ,succ,0)` with the source existence-and-uniqueness commuting law.
`FC03-C02-U002`	unmatched characterization	`unmatched`	partial: `Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean::IsInitial`; `IsTerminal`; `Mathlib/CategoryTheory/Yoneda.lean::RepresentableBy`; `CorepresentableBy`	N	Initial/terminal unique-hom data and representability are present, but no searched declaration proves the source iff identifying the corresponding represented hom functor with the constant singleton functor in both variances.
`FC03-C02-U003`	exact match	`mathlib`	`Mathlib/CategoryTheory/Yoneda.lean::Functor.RepresentableBy`; `CorepresentableBy`; `representableByEquiv`; `corepresentableByEquiv`	P	Exact chosen representing object plus chosen natural hom-set/type equivalence, in both variances.
`FC03-C02-U004`	unmatched bundled examples	`unmatched`	—	N	Mathlib has many individual free/forgetful and walking-object ingredients, but no declaration-level realization of the complete source bundle (including the stated path/loop and walking-arrow/isomorphism cases).
`FC03-C02-U005`	unmatched terminology	`unmatched`	—	N	Free/cofree constructions occur throughout Mathlib, but no declaration or formal interface identifies the general source convention “covariant representable universal = free, dual = cofree.”
`FC03-C02-U006`	unmatched bundled examples	`unmatched`	—	N	Power sets, Sierpiński topology, exponentials, vector duals and homotopy infrastructure exist separately, but the complete contravariant representability bundle, in particular the `K(A,n)`/principal-`G`-bundle cases, has no formal owner.
`FC03-C02-U007`	unmatched concrete example	`unmatched`	—	N	The abstract Yoneda lemma is formalized, but no declaration realizes its source-specific ordinal-`ω` specialization `Nat(ω(k,-),F) ≃ F k`.
`FC03-C02-U008`	unmatched concrete example	`unmatched`	partial: `Mathlib/CategoryTheory/Action/Concrete.lean::Action.leftRegular`; `Mathlib/GroupTheory/GroupAction/Hom.lean::MulActionHom.End.equivMulOpposite`	N	Regular-action infrastructure exists, but no declaration identifies the covariant/contravariant representables of `BG` with the regular left/right `G`-sets and the stated universal evaluation property.
`FC03-C02-U009`	unmatched concrete theorem	`unmatched`	—	N	Targeted search found self-action endomorphism equivalences but no declaration `(G →[G] X) ≃ X` by evaluation at the identity for an arbitrary left `G`-set `X`.
`FC03-C02-U010`	exact match	`mathlib`	`Mathlib/CategoryTheory/Yoneda.lean::yonedaLemma`; `coyonedaLemma`; `yonedaPairing`; `yonedaEvaluation`	P	Exact natural Yoneda isomorphism and dual, universe-aware for locally small categories.
`FC03-C02-U011`	exact match	`mathlib`	`Mathlib/CategoryTheory/Yoneda.lean::yonedaLemma`; `coyonedaLemma`	P	These are natural isomorphisms of the natural-transformation pairing bifunctor with evaluation, not merely pointwise bijections; the `Type` universe supplies the set-sizedness conclusion.
`FC03-C02-U012`	exact match	`mathlib`	`Mathlib/CategoryTheory/Yoneda.lean::Yoneda.fullyFaithful`; `Coyoneda.fullyFaithful`; `yoneda_full`; `yoneda_faithful`; `coyoneda_full`; `coyoneda_faithful`	P	Exact full-faithfulness of both Yoneda embeddings.
`FC03-C02-U013`	unmatched editorial convention	`unmatched`	—	N	Mathlib formalizes the Yoneda natural isomorphism and full-faithfulness separately, but has no declaration representing the source’s naming convention that both are called “the Yoneda lemma.”
`FC03-C02-U014`	unmatched concrete theorem	`unmatched`	partial: `Mathlib/Data/Matrix/Mul.lean::Matrix.addMonoidHomMulLeft`	N	Left multiplication is formalized, and current Mathlib adds elementary row-operation machinery, but no pinned/current theorem classifies every `n`-row operation as unique left multiplication recoverable from its value at the identity matrix.
`FC03-C02-U015`	exact match	`mathlib`	`Mathlib/GroupTheory/Perm/Subgroup.lean::Equiv.Perm.subgroupOfMulAction`	P	Explicit Cayley theorem; specializing the stronger faithful-action statement to the regular action gives the source result.
`FC03-C02-U016`	exact structural match	`mathlib`	`Mathlib/CategoryTheory/Yoneda.lean::Yoneda.fullyFaithful`; `Coyoneda.fullyFaithful`; `RepresentableBy.uniqueUpToIso`; `CorepresentableBy.uniqueUpToIso`	P	Full faithfulness detects object isomorphism through representables, and `uniqueUpToIso` gives the representing-object consequence in both variances.
`FC03-C02-U017`	exact match	`mathlib`	`Mathlib/CategoryTheory/Yoneda.lean::RepresentableBy.uniqueUpToIso`; `CorepresentableBy.uniqueUpToIso`; `RepresentableBy.ext`; `CorepresentableBy.ext`	P	The chosen representation determines the canonical compatible isomorphism; extensionality by the universal element supplies exactly the source’s “unique compatible isomorphism” sense.
`FC03-C02-U018`	exact structural match	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean::IsTerminal.hom_ext`; `IsTerminal.uniqueUpToIso`; `isIso_of_isTerminal`	P	Between terminal objects there is exactly one morphism, and it is invertible; hence the full subcategory of terminal objects is either empty or a contractible groupoid.
`FC03-C02-U019`	exact match	`mathlib`	`Mathlib/CategoryTheory/PUnit.lean::equiv_punit_iff_unique`; `Mathlib/CategoryTheory/Groupoid.lean::Groupoid.ofHomUnique`	P	`equiv_punit_iff_unique` is exactly equivalence to the one-object discrete category iff nonempty with a unique morphism in every hom; `Groupoid.ofHomUnique` records that such a category is automatically a groupoid.
`FC03-C02-U020`	exact match	`mathlib`	`Mathlib/CategoryTheory/Yoneda.lean::Functor.reprx`; `coreprx`; `RepresentableBy.homEquiv_eq`; `CorepresentableBy.homEquiv_eq`; `reprW_hom_app`; `coreprW_hom_app`	P	`reprx/coreprx` are the universal elements, and the hom-equivalence formulas classify every element by applying the functor to the unique representing morphism.
`FC03-C02-U021`	exact match	`mathlib`	`Mathlib/Algebra/Polynomial/AlgebraMap.lean::Polynomial.aevalEquiv`; `aeval_X`; `Mathlib/Algebra/Algebra/Hom.lean::RingHom.equivIntAlgHom`	P	At base `ℤ`, ring homomorphisms `ℤ[X] → R` are exactly `ℤ`-algebra homomorphisms and `aevalEquiv` evaluates them at `X`, giving the source universal property even for noncommutative target rings.
`FC03-C02-U022`	unmatched concrete classification	`unmatched`	partial: `Mathlib/Algebra/Torsor/Defs.lean::Torsor`; `Mathlib/CategoryTheory/Action.lean::ActionCategory`; `actionAsFunctor`	N	`Torsor` is exactly nonempty free transitive action data, but no declaration proves that a `G`-set is representable iff it is a torsor or identifies a chosen torsor point with a representation/universal element.
`FC03-C02-U023`	exact structural match	`mathlib`	`Mathlib/Algebra/Torsor/Defs.lean::AddTorsor`; `Mathlib/LinearAlgebra/AffineSpace/Defs.lean`; `Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean::AffineEquiv.vaddConst`; `Equiv.vaddConst`	P	An affine space is an additive torsor; choosing an origin gives the translation affine equivalence with its vector space, exactly the source identification for `A^n` and `R^n`.
`FC03-C02-U024`	exact match	`mathlib`	`Mathlib/LinearAlgebra/TensorProduct/Basic.lean::TensorProduct.lift.equiv`; `lift.equiv_apply`; `TensorProduct.mk`	P	Exact universal bilinear map and unique factorization equivalence defining `V ⊗ W`.
`FC03-C02-U025`	exact match	`mathlib`	`Mathlib/LinearAlgebra/TensorProduct/Basic.lean::TensorProduct.comm`; `comm_tmul`; `lift_comp_comm_eq`	P	Canonical tensor symmetry sends `v ⊗ w` to `w ⊗ v` and is induced from the flipped universal bilinear map.
`FC03-C02-U026`	exact match	`mathlib`	`Mathlib/LinearAlgebra/TensorProduct/Basic.lean::TensorProduct.comm`; `comm_tmul`; `comm_symm`; `comm_symm_tmul`; `comm_trans_comm`	P	The symmetry is definitionally constructed by `lift` from the swapped universal map, and swapping back supplies its inverse.
`FC03-C02-U027`	exact structural match	`mathlib`	`Mathlib/Algebra/MonoidAlgebra/Basic.lean::MonoidAlgebra.lift`; `lift_of`; `lift_unique'`; `Mathlib/Algebra/Group/Units/Hom.lean::MonoidHom.toHomUnitsMulEquiv`; `RingHom.equivIntAlgHom`	P	Specializing the monoid-algebra universal property to `ℤ[G]` identifies ring maps with group maps from `G` into target units; `MonoidAlgebra.of ℤ G` is the universal group map.
`FC03-C02-U028`	exact match	`mathlib`	`Mathlib/CategoryTheory/Elements.lean::Functor.Elements`; category instance `categoryOfElements`; `CategoryOfElements.π`; `homMk`	P	Exact sigma-type objects, mapped-element morphism condition, and forgetful projection for the category of elements.
`FC03-C02-U029`	exact orientation translation	`mathlib`	`Mathlib/CategoryTheory/Elements.lean::CategoryOfElements.toCostructuredArrow`; `costructuredArrowYonedaEquivalence`	P	For `F : Cᵒᵖ ⥤ Type`, Riehl’s convention is `(F.Elements)ᵒᵖ`; this reverses Mathlib’s projection to give the source projection into `C`.
`FC03-C02-U030`	exact orientation translation	`mathlib`	`Mathlib/CategoryTheory/Elements.lean::Functor.Elements`; category instance `categoryOfElements`	P	After taking the opposite as in U029, Mathlib’s element-morphism equation is exactly `F(f)(x') = x` for a source arrow `f : c → c'`.
`FC03-C02-U031`	unmatched concrete example	`unmatched`	—	N	No searched declaration realizes `n-Color : Graphᵒᵖ → Set` and identifies its category of elements with `n`-colored graphs and color-preserving graph homomorphisms.
`FC03-C02-U032`	exact owner, incompatible open revision	`reference-port`	mathlib4 PR #15055 head `1139ef2782492a1c9a9cf94e210cca8ffbae85b0`, `Mathlib/CategoryTheory/ConcreteCategory/Pointed.lean::ConcreteCategory.Pointed`; `Pointed.toCategoryOfElement`; `Pointed.fromCategoryOfElements`; `Pointed.elementsEquivalence`	R	Exact equivalence `Pointed C ≌ (forget C).Elements`, matching based objects with the category of elements of the underlying-set functor. Apache-2.0 but open/merge-conflicted and on Lean v4.10.0-rc2, hence reference-port only.
`FC03-C02-U033`	unmatched full example	`unmatched`	partial: `Mathlib/CategoryTheory/Elements.lean::Functor.Elements`; `Mathlib/CategoryTheory/Types/Basic.lean::Functor.sections`	N	The object type of `F.Elements` is the dependent sigma, and sections are formalized, but no declaration identifies discrete-index elements with the dependent sum and sections of `π` with the dependent product as one source example.
`FC03-C02-U034`	unmatched concrete identification	`unmatched`	partial: `Mathlib/CategoryTheory/Elements.lean::Functor.Elements`; `Mathlib/CategoryTheory/Comma/Over/Basic.lean`; `Mathlib/CategoryTheory/Comma/Under/Basic.lean`	N	Slice/under/over categories and represented element categories exist, but no searched declaration identifies `∫ C(c,-)` with `c/C` and `∫ C(-,c)` with `C/c` in the source orientation.
`FC03-C02-U035`	exact match up to equivalence	`mathlib`	`Mathlib/CategoryTheory/Elements.lean::CategoryOfElements.costructuredArrowYonedaEquivalence`; `structuredArrowEquivalence`	P	The opposite of the category of elements of a presheaf is equivalent to the Yoneda costructured/comma category, with the covariant structured-arrow dual; this is the source comparison up to categorical equivalence rather than literal equality.
`FC03-C02-U036`	exact match with orientation translation	`mathlib`	`Mathlib/CategoryTheory/Limits/Elements.lean::Functor.Elements.hasInitial_iff_isCorepresentable`; `hasInitial_iff_isRepresentable`	P	Covariant representability is exactly initiality of Mathlib’s elements category; for a presheaf Riehl uses the opposite category, translating Mathlib initiality to source terminality.
`FC03-C02-U037`	unmatched source subcategory theorem	`unmatched`	partial: `Elements.isInitialOfCorepresentableBy`; `Limits.IsInitial.uniqueUpToIso`; `CategoryTheory.equiv_punit_iff_unique`	N	Mathlib proves uniqueness/contractibility ingredients for individual initial elements, but no declaration constructs the full subcategory of all representations and proves it empty or contractible.
`FC03-C02-U038`	unmatched concrete classification	`unmatched`	partial: `Mathlib/CategoryTheory/Action.lean::ActionCategory`; groupoid instance; `Mathlib/Algebra/Torsor/Defs.lean::Torsor`	N	The translation groupoid and torsor ingredients exist, but no declaration states the source chain `X representable ↔︎ ActionCategory contractible ↔︎ X nonempty, free, transitive`.
`FC03-C02-U039`	unmatched concrete example	`unmatched`	—	N	No project/pinned/current declaration packages discrete endomap systems as a category of elements with `(ℕ,succ,0)` initial. The external MiscLean candidate `mdnestor/MiscLean@bd150bcd568b3a80dee1f6465ae4b1ac7feb40a7` has proof holes, no declared license, and an incompatible Lean v4.24.0-rc1 toolchain.
`FC03-C02-U040`	unmatched bundled examples	`unmatched`	partial: `Polynomial.aevalEquiv`; `TensorProduct.lift.equiv`; `FreeGroup.lift`	N	Several constituent universal properties are pinned, but no declaration-level realization of the complete six-example category-of-elements suite was found; the bundle is therefore not credited from generic ingredients.

Provenance contract for C03

Project search: LeanCategories/** outside .lake/.agents/.git was searched first for limits, colimits, creation/preservation/reflection, functor-category limits, filtered categories, and every concrete Chapter-3 example. No project-owned C03 route was found; generic infrastructure is not credited for a concrete example unless a declaration realizes it.
Pinned Mathlib: project pin db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0, Lean v4.33.0), denoted P, was declaration-checked. The limits, Yoneda, Fubini, filtered-colimit, TopCat, Type, lattice, and Cat APIs below are present at that exact revision.
Current/open Mathlib: upstream 810b3888d0aa94294b18587c453466bc86c1f0fc (Apache-2.0, Lean v4.34.0-rc2) was refreshed/rechecked 2026-09-06. Open PR #29792 at head a22dba36dd9e5763f2df8d85c0087046f225faba is Apache-2.0, uses Lean v4.24.0-rc1, and supplies the CW-skeleton portion of U022, so that row is revision-specific reference-port, not pinned Mathlib.
External/reference search: jwiegley/category-theory@c490e6343af2038ea4fd387e3e0ab6a2dfdc6316 is BSD-3-Clause Coq code (Coq 9.1.1 plus Equations 1.3); its Instance/Grp/Quotient/Colimit.v::normal_closure_IsCokernel realizes U021 but is non-Lean and therefore reference-port. rkirov/category-theory-in-context-lean@cae97fae75665bb93d36ff763c9243346806d12a is MIT, Lean v4.24.0-rc1 / Mathlib 4b9a202…, and covers only early Chapter 1. Qiu233/ctic@7929dc698ee3eb5de5cbe2f0cf0dcbcf5a4a7c79 has related limits code but no established repository license and an incompatible Lean v4.25.0-rc2 / Mathlib e721…, so it is not a usable route.
N denotes dated 2026-09-06 negative evidence after project-first search, pinned/current Mathlib, relevant open work and source-atlas repositories, Reservoir/GitHub, and Loogle/LeanSearch as feasible. Rows marked unmatched were additionally searched under their source-specific terminology; generic ingredients are not credited for concrete or editorial source units.

C03 — Limits and Colimits

FC03 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
`FC03-C03-U001`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/Const.lean::Functor.const`	P	Exact constant functor and diagonal embedding data used to define cones.
`FC03-C03-U002`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Cones.lean::Cone`; `Cocone`; `ConeMorphism`; `CoconeMorphism`	P	Cone/cocone objects are natural transformations from/to a constant functor, with the same leg and commuting-triangle data.
`FC03-C03-U003`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Cones.lean::cones`; `cocones`; `Mathlib/CategoryTheory/Limits/IsLimit.lean::IsLimit`; `IsColimit`	P	The cone and cocone functors plus terminal/initial universal structures give exactly the represented universal-property formulation of limits and colimits.
`FC03-C03-U004`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/ConeCategory.lean::Cone.isLimitEquivIsTerminal`; `Cocone.isColimitEquivIsInitial`	P	Direct equivalence between a limit cone and a terminal object of the cone category, and dually for colimits.
`FC03-C03-U005`	exact notation/data match	`mathlib`	`Mathlib/CategoryTheory/Limits/HasLimits.lean::LimitCone`; `ColimitCocone`; `limit`; `colimit`; `limit.cone`; `colimit.cocone`; `limit.π`; `colimit.ι`	P	Mathlib’s chosen limit/colimit objects and universal cones are the source notation with explicit choice data.
`FC03-C03-U006`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/IsLimit.lean::IsLimit.uniqueUpToIso`; `conePointUniqueUpToIso`; `IsColimit.uniqueUpToIso`; `coconePointUniqueUpToIso`	P	Exact unique isomorphism between universal cone points compatible with all legs, and the dual statement.
`FC03-C03-U007`	exact structural match	`mathlib`	`Mathlib/CategoryTheory/WithTerminal/Basic.lean::WithInitial`; `WithTerminal`; `Mathlib/CategoryTheory/WithTerminal/Cone.lean::equivComma`; `coconeEquiv`; `coneEquiv`	P	Adjoining a formal initial/terminal index and the cone/cocone equivalences realize the source “limit diagram” indexing construction.
`FC03-C03-U008`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/Products.lean::Discrete.functor`; `Fan`; `Pi`; `Pi.π`; `Pi.lift`; `Pi.hom_ext`	P	Products are limits of discrete diagrams with the exact projection and universal mapping property.
`FC03-C03-U009`	exact categorical example	`mathlib`	`Mathlib/Topology/Category/TopCat/Limits/Products.lean::TopCat.piFan`; `piFanIsLimit`; `piIsoPi`	P	The product topology is constructed as the categorical product in `TopCat`; the source’s box-topology warning is pedagogical rather than additional formal data.
`FC03-C03-U010`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean::Functor.empty`; `terminalIsTerminal`	P	The empty-diagram limit is exactly a terminal object.
`FC03-C03-U011`	exact match	`mathlib`	`Mathlib/CategoryTheory/Category/Cat/Terminal.lean::isTerminalDiscretePUnit`; `isTerminalOfUniqueOfIsDiscrete`	P	The one-object one-arrow category is terminal in the universe-polymorphic category of categories.
`FC03-C03-U012`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean::parallelPair`; `Fork`; `equalizer`; `equalizer.ι`; `equalizer.lift`; `equalizer.condition`	P	Exact equalizer diagram and universal property.
`FC03-C03-U013`	exact structural match	`mathlib`	`Mathlib/Algebra/Category/Grp/Limits.lean::GrpCat.HasLimits.limitCone`; `limitConeIsLimit`; `forget_createsLimitsOfSize`; `Mathlib/Algebra/Category/Grp/Kernel.lean::AddCommGrpCat.kernelIsoKer`	P	Group limits are created on underlying types; equalizers specialize to the subgroup where the two homomorphisms agree, including the kernel case.
`FC03-C03-U014`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/Pullback/Basic.lean::cospan`; `PullbackCone.mk`; `PullbackCone.IsLimit.mk`; `pullback`; `pullback.fst`; `pullback.snd`	P	Exact pullback cospan, commuting square, and universal mapping property.
`FC03-C03-U015`	exact concrete ingredients	`mathlib`	`Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean::Circle.exp_eq_one`; `Circle.isCoveringMap_exp`; `Mathlib/Topology/Covering/Basic.lean::discreteTopology_fiber`	P	The exponential covering of the circle and its discrete fibers realize the source pullback example after the standard normalization `r = 2πt`.
`FC03-C03-U016`	unmatched concrete example	`unmatched`	—	N	No project/pinned/current/open declaration computes in `Ab` the pullback of multiplication-by-`m` and multiplication-by-`n` on `ℤ` as `ℤ` with the source’s lcm-derived legs.
`FC03-C03-U017`	exact generic realization	`mathlib`	`Mathlib/CategoryTheory/Limits/HasLimits.lean::HasLimit`; `limit`; `limit.π`	P	The inverse limit of the displayed `ωᵒᵖ` tower is exactly the ordinary limit of that functor; no extra source-specific structure is required.
`FC03-C03-U018`	exact concrete universal property	`mathlib`	`Mathlib/NumberTheory/Padics/RingHoms.lean::PadicInt.toZModPow`; `zmod_cast_comp_toZModPow`; `PadicInt.lift`; `lift_spec`; `lift_unique`	P	The compatible residue maps and their unique lift are the projective-limit universal property characterizing the p-adic integers.
`FC03-C03-U019`	exact dual constructions	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/Products.lean`; `Shapes/Terminal.lean`; `Shapes/Equalizers.lean`; pullback/pushout API; `Mathlib/CategoryTheory/Limits/HasLimits.lean::colimit`; `colimit.ι`	P	Mathlib carries the coproduct/initial/coequalizer/pushout duals and chosen colimit API directly.
`FC03-C03-U020`	unmatched concrete construction	`unmatched`	—	N	No searched Lean declaration realizes the source construction of the torus as the pushout obtained by attaching a 2-cell to `S¹ ∨ S¹` along the commutator loop.
`FC03-C03-U021`	exact external owner, non-Lean	`reference-port`	`jwiegley/category-theory@c490e6343af2038ea4fd387e3e0ab6a2dfdc6316`, `Instance/Grp/Quotient/Colimit.v::normal_closure_IsCokernel`	R	The Coq theorem identifies the quotient by the normal closure of the image with the group cokernel. BSD-3-Clause Coq 9.1.1 code is not importable into Lean, so it is preserved as a revision-pinned reference implementation.
`FC03-C03-U022`	exact components, open-revision CW owner	`reference-port`	pinned `Mathlib/Data/Set/UnionLift.lean::Set.iUnionLift`; `iUnionLift_inclusion`; mathlib4 PR #29792 head `a22dba36dd9e5763f2df8d85c0087046f225faba`, `Mathlib/Topology/CWComplex/Classical/Subcomplex.lean::CWComplex.descBySkeleton`; `descBySkeleton_inclusion`; `descBySkeleton_inclusion_apply`	R	Pinned Mathlib realizes increasing-union colimits of sets; the open PR gives the maps-out universal property from CW skeleta. Because the CW component is open/post-pin and on Lean v4.24.0-rc1, the whole source row is reference-port.
`FC03-C03-U023`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean`; `Mathlib/CategoryTheory/Preadditive/Biproducts.lean`; `Mathlib/CategoryTheory/Preadditive/Mat.lean::biproduct.matrix`; `matrix_components`	P	Finite biproducts and their matrix calculus give the source direct-sum/product comparison and matrix composition law.
`FC03-C03-U024`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/HasLimits.lean::HasLimitsOfShape`; `HasColimitsOfShape`; `HasLimitsOfSize`; `HasColimitsOfSize`; `HasLimits`; `HasColimits`	P	Exact shape-wise and size-bounded completeness/cocompleteness interfaces.
`FC03-C03-U025`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Types/Limits.lean::Types.coneOfSection`; `sectionOfCone`; `isLimitEquivSections`; `Types.Small.limitCone`	P	A limit of a Type-valued diagram is represented by the type of compatible sections, exactly as in the source.
`FC03-C03-U026`	exact size criterion	`mathlib`	`Mathlib/CategoryTheory/Limits/Types/Limits.lean::Types.Small`; `hasLimit_iff_small_sections`	P	The existence of the Type-valued limit is characterized by smallness of the section type, matching the source size caveat.
`FC03-C03-U027`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Types/Limits.lean::Types.Small.limitConeIsLimit`; `Types.hasLimitsOfSize`	P	Type has all limits in the required universe regime, constructed from compatible sections.
`FC03-C03-U028`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Types/Products.lean::Types.productLimitCone`; `productIso`	P	Type products are dependent products with the exact categorical universal property.
`FC03-C03-U029`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Types/Products.lean::Types.isTerminalPUnit`; `terminalLimitCone`; `terminalIso`	P	`PUnit` is the terminal Type and the empty product.
`FC03-C03-U030`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Types/Equalizers.lean::Types.equalizerLimit`; `equalizerIso`	P	The equalizer is the subtype on which the parallel functions agree.
`FC03-C03-U031`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Types/Limits.lean::Types.limitEquivSections`; `Types.Limit.mk`	P	The limit is canonically equivalent to compatible families/sections with the stated coordinate condition.
`FC03-C03-U032`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Types/Pullbacks.lean::Types.PullbackObj`; `pullbackCone`; `pullbackLimitCone`	P	Set/Type pullbacks are the dependent pairs satisfying equality of the two images.
`FC03-C03-U033`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean::SingleObj.Types.sections.equivFixedPoints`; `limitEquivFixedPoints`	P	The limit of a group action is exactly its fixed-point type.
`FC03-C03-U034`	exact construction	`mathlib`	`Mathlib/CategoryTheory/Limits/Constructions/Pullbacks.lean::hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair`	P	Binary products plus equalizers construct pullbacks exactly by equalizing the two maps out of a product.
`FC03-C03-U035`	exact construction	`mathlib`	`Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean::limitConeOfEqualizerAndProduct`; `buildLimit`; `buildIsLimit`; `hasLimit_of_equalizer_and_product`	P	The general limit construction from a product of objects and an equalizer encoding all diagram relations is exactly the source proof.
`FC03-C03-U036`	exact structural match	`mathlib`	`Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean::limitConeOfEqualizerAndProduct`; `buildIsLimit`	P	The two parallel maps from the product encode target projection versus source projection followed by the diagram morphism, matching the source relation equations.
`FC03-C03-U037`	exact theorem	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean::splitMonoOfIdempotentOfIsLimitFork`; split-mono/retraction API	P	An equalizer splitting an idempotent yields the retraction data; the converse direction is the standard split-idempotent equalizer construction already expressible by the same API.
`FC03-C03-U038`	exact definitions	`mathlib`	`Mathlib/CategoryTheory/Limits/Preserves/Basic.lean::PreservesLimit`; `ReflectsLimit`; `Mathlib/CategoryTheory/Limits/Creates.lean::LiftableCone`; `LiftableCocone`; `CreatesLimit`	P	Direct preservation, reflection, and creation interfaces for universal cones.
`FC03-C03-U039`	exact consequences	`mathlib`	`Mathlib/CategoryTheory/Limits/Creates.lean::hasLimit_of_created`; `hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape`; `hasLimits_of_hasLimits_createsLimits`; `preservesLimit_of_createsLimit_and_hasLimit`	P	A creator transports existence and preserves created limits, exactly the source consequences; dual declarations cover colimits.
`FC03-C03-U040`	exact concrete sheaf criterion	`mathlib`	`Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean::TopCat.Presheaf.IsSheafEqualizerProducts`; `isSheaf_iff_isSheafEqualizerProducts`; `SheafConditionEqualizerProducts.fork`	P	The sheaf condition is packaged as the source product/equalizer limit condition.
`FC03-C03-U041`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Preserves/Basic.lean::fullyFaithful_reflectsLimits`; generated colimit dual	P	Fully faithful functors reflect universal cones, exactly as stated.
`FC03-C03-U042`	exact equivalence case	`mathlib`	`Mathlib/CategoryTheory/Adjunction/Limits.lean::Functor.createsLimitsOfIsEquivalence`; `createsColimitsOfIsEquivalence`; `reflectsLimits_of_isEquivalence`; `reflectsColimits_of_isEquivalence`	P	Equivalences create and reflect all limits/colimits and hence preserve them, matching the source.
`FC03-C03-U043`	unmatched strict-creation strengthening	`unmatched`	partial: `Mathlib/CategoryTheory/Limits/Creates.lean::CreatesLimit`; external `jwiegley/category-theory` has `Structure/Limit/Creation.v::StrictlyCreatesLimit`	N	The source demands a unique on-the-nose lifted cone. Mathlib creation is only the ordinary categorical notion, and the external Coq notion gives canonical cone-isomorphism/hom-setoid data rather than the source’s literal unique lift.
`FC03-C03-U044`	exact connectivity interface	`mathlib`	`Mathlib/CategoryTheory/IsConnected.lean::IsPreconnected`; `IsConnected`; `Zigzag`; `exists_zigzag'`	P	Exact connected-index condition used for connected colimits.
`FC03-C03-U045`	unmatched strict-creation theorem	`unmatched`	partial: `Mathlib/CategoryTheory/Limits/Over.lean::Under.createsLimitsOfSize`; `Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.lean::createsColimitsOfShapeForgetOfIsConnected`	N	The slice/under forgetful functor ordinarily creates limits and connected colimits, but no declaration supplies the source’s stronger strict unique-lift creation statement.
`FC03-C03-U046`	unmatched strict objectwise-creation theorem	`unmatched`	partial: `Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean::evaluation_preservesLimitsOfShape`; `evaluation_preservesColimitsOfShape`	N	Mathlib computes functor-category limits and colimits objectwise and evaluation preserves them, but no declaration states that restriction to the discrete object category strictly creates all such (co)limits in the source’s on-the-nose sense.
`FC03-C03-U047`	exact representable preservation theorem	`mathlib`	`Mathlib/CategoryTheory/Limits/Yoneda.lean::coyonedaPreservesLimitsOfShape`	P	The covariant represented hom functor preserves limits, yielding `C(X,lim F) ≅ lim C(X,F-)`.
`FC03-C03-U048`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/Products.lean::Pi.π`; `Pi.lift`; `Pi.lift_π`; `Pi.hom_ext`; `Mathlib/CategoryTheory/Limits/IsLimit.lean::IsLimit.homEquiv`; `Mathlib/CategoryTheory/Limits/Types/Products.lean::Types.productIso`	P	A constant-family product gives the power/cotensor `A^I`, with `C(X,A^I) ≃ (I → C(X,A))` exactly.
`FC03-C03-U049`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Yoneda.lean::coyoneda_preservesLimit`; `coyoneda_preservesLimits`	P	`coyoneda.obj (op X) = C(X,-)` and preserves every existing limit.
`FC03-C03-U050`	exact preservation/reflection	`mathlib`	`Mathlib/CategoryTheory/Limits/Yoneda.lean::coyoneda_preservesLimit`; `yonedaFunctor_preservesLimits`; `yonedaFunctor_reflectsLimits`	P	Representables preserve limits and the Yoneda embedding preserves and reflects them, exactly the source statement.
`FC03-C03-U051`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Yoneda.lean::yoneda_preservesLimit`; `Limits.Cocone.isColimitYonedaEquiv`; `Mathlib/CategoryTheory/Limits/IsLimit.lean::IsLimit.natIso`	P	Applying `C(-,X)` to a colimit yields the natural limit-of-homs isomorphism.
`FC03-C03-U052`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/IsLimit.lean::IsColimit.homEquiv`; `Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean::coprod.inl`; `coprod.inr`; `coprod.desc`; `coprod.hom_ext`	P	The coproduct universal property is exactly `C(X ⊔ Y,Z) ≃ C(X,Z) × C(Y,Z)`.
`FC03-C03-U053`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/Products.lean::Sigma.ι`; `Sigma.desc`; `Sigma.ι_desc`; `Sigma.hom_ext`; `Mathlib/CategoryTheory/Limits/Types/Coproducts.lean::Types.coproductIso`; `Equiv.sigmaEquivProd`	P	Constant coproducts give copowers/tensors; in `Type` the sigma coproduct is canonically equivalent to `I × A`.
`FC03-C03-U054`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean::PushoutCocone.isColimitYonedaEquiv`	P	Direct pushout-specific equivalence identifying the represented pushout universal property with a pullback of hom-types.
`FC03-C03-U055`	exact dual match	`mathlib`	`Mathlib/CategoryTheory/Limits/Yoneda.lean::yoneda_preservesLimit`; `coyonedaFunctor_preservesLimits`; `coyonedaFunctor_reflectsLimits`; `Limits.Cocone.isColimitYonedaEquiv`	P	Contravariant representables send colimits to limits, and the dual Yoneda embedding detects the colimit cone.
`FC03-C03-U056`	exact construction theorem	`mathlib`	`Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean::hasLimit_of_equalizer_and_product`; `has_limits_of_hasEqualizers_and_products`; `hasColimit_of_coequalizer_and_coproduct`; `has_colimits_of_hasCoequalizers_and_coproducts`	P	Every small (co)limit is constructed from products/equalizers or coproducts/coequalizers exactly as in the source.
`FC03-C03-U057`	exact generalized-element criterion	`mathlib`	`Mathlib/CategoryTheory/Yoneda.lean::Yoneda.fullyFaithful`; `yoneda_faithful`; `Mathlib/CategoryTheory/Limits/Yoneda.lean::Limits.Cone.isLimitCoyonedaEquiv`	P	Yoneda faithfulness detects equality on all generalized elements, and represented hom-set cones detect limiting cones.
`FC03-C03-U058`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Constructions/BinaryProducts.lean::isBinaryProductOfIsTerminalIsPullback`; `prodIsoPullback`; `prodIsoPullback_hom_fst`; `prodIsoPullback_hom_snd`	P	The pullback over a terminal object is canonically the binary product.
`FC03-C03-U059`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/Pullback/Equalizer.lean::isPullback_equalizer_prod`	P	Direct theorem realizing an equalizer as the pullback of `(f,g)` along the diagonal into `B × B`.
`FC03-C03-U060`	exact size interface	`mathlib`	`Mathlib/CategoryTheory/Comma/CardinalArrow.lean::Arrow.finite_iff`; `Mathlib/CategoryTheory/FinCategory/Basic.lean::FinCategory`; `Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean::HasFiniteLimits`; `HasFiniteColimits`	P	Finiteness of the total morphism type is equivalent to Mathlib’s finite-category interface, so finite diagrams match the source definition.
`FC03-C03-U061`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean::hasFiniteLimits_of_hasTerminal_and_pullbacks`; `hasFiniteColimits_of_hasInitial_and_pushouts`	P	Terminal plus pullbacks gives all finite limits, and initial plus pushouts gives all finite colimits.
`FC03-C03-U062`	exact concrete construction	`mathlib`	`Mathlib/CategoryTheory/Limits/Types/Colimits.lean::Types.hasColimitsOfShape`; `Types.hasColimitsOfSize`; `Mathlib/CategoryTheory/Limits/Types/Coproducts.lean::Types.coproductIso`; `Types/Coequalizers.lean::Types.coequalizerColimit`; `Types.coequalizerIso`	P	`Type` is cocomplete; coproducts are sigma/disjoint unions and coequalizers are the expected quotient by the generated equivalence relation.
`FC03-C03-U063`	exact concrete construction	`mathlib`	`Mathlib/Topology/Category/TopCat/Limits/Basic.lean::topCat_hasLimits`; `topCat_hasColimits`; `induced_of_isLimit`; `limit_topology`; `coinduced_of_isColimit`; `colimit_topology`; `forget_preservesLimits`; `forget_preservesColimits`	P	`TopCat` (co)limits use the underlying Type (co)limit with the initial/final topology, and the forgetful functor preserves them.
`FC03-C03-U064`	unmatched concrete example	`unmatched`	partial: `Mathlib/Topology/Category/TopCat/Limits/Basic.lean`	N	Generic topological limits are formalized, but no project/pinned/current/external declaration identifies the inverse limit of the p-th power maps of `S¹` with the p-adic solenoid.
`FC03-C03-U065`	unmatched concrete example	`unmatched`	partial: generic action-orbit colimit machinery in `Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean`	N	No searched declaration defines ordered/unordered configuration spaces `PConf_n(X)`/`Conf_n(X)` and realizes the latter as the orbit colimit of the symmetric-group action.
`FC03-C03-U066`	exact structural match	`mathlib`	`Mathlib/CategoryTheory/WithTerminal/Cone.lean` `HasLimitsOfSize (Over X)` and `HasColimitsOfSize (Under X)` instances; `Mathlib/CategoryTheory/Limits/Comma.lean::StructuredArrow.hasLimitsOfSize`; `CostructuredArrow.hasColimitsOfSize`	P	Applying the comma/slice instances to the identity functor gives completeness and cocompleteness of both slice orientations whenever the ambient category has them.
`FC03-C03-U067`	exact construction	`mathlib`	`Mathlib/CategoryTheory/Category/Cat/Limit.lean::Cat.HasLimits.homDiagram`; `limitConeX`; `limitCone`; `limitConeLift`; `limitConeIsLimit`; `HasLimits Cat`	P	Category limits are built objectwise on objects and morphisms; products and equalizers specialize to the source descriptions. Universe levels cover both `Cat` and `CAT`.
`FC03-C03-U068`	unmatched concrete pullback identification	`unmatched`	partial: `Mathlib/CategoryTheory/Elements.lean::Functor.Elements`; `Mathlib/CategoryTheory/Category/Cat/Limit.lean`	N	Categories of elements and categorical pullbacks in `Cat` both exist, but no searched declaration proves the specific pullback square `C → Set ← Set_*` whose apex is `∫F`.
`FC03-C03-U069`	unmatched concrete pushout examples	`unmatched`	partial: walking-arrow/isomorphism, `SingleObj`, free-category, and Cat-colimit infrastructure	N	No searched declaration computes the stated Cat pushouts as the one-object categories on the free monoid `ℕ` and free group `ℤ`.
`FC03-C03-U070`	exact invariance theorem	`mathlib`	`Mathlib/CategoryTheory/Adjunction/Limits.lean::hasLimitsOfShape_of_equivalence`; `has_limits_of_equivalence`; `hasColimitsOfShape_of_equivalence`; `has_colimits_of_equivalence`	P	Completeness and cocompleteness transport across categorical equivalence, shape-wise and globally.
`FC03-C03-U071`	exact order-categorical characterization	`mathlib`	`Mathlib/CategoryTheory/Limits/Preorder.lean::hasLimit_iff_hasGLB`; `hasColimit_iff_hasLUB`; `isLimitIInf`; `isColimitISup`; `Mathlib/CategoryTheory/Limits/Lattice.lean::CompleteLattice.hasLimits_of_completeLattice`; `hasColimits_of_completeLattice`; `limit_eq_iInf`; `colimit_eq_iSup`	P	Limits/colimits in a preorder are precisely infima/suprema, yielding the complete-lattice equivalence.
`FC03-C03-U072`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean::IsKernelPair`; `IsKernelPair.of_hasPullback`; `Mathlib/CategoryTheory/EquivalenceRelation.lean::IsKernelPair.equivalenceRelation`; `EffectiveEquivalenceRelation.isCoequalizer`	P	Kernel pairs are self-pullbacks, carry the internal equivalence-relation structure, and their effective quotient is the coequalizer.
`FC03-C03-U073`	exact chosen functors	`mathlib`	`Mathlib/CategoryTheory/Limits/HasLimits.lean::limMap`; `lim`; `colimMap`; `colim`	P	Choosing a (co)limit for each diagram gives the functors `lim_J` and `colim_J` exactly.
`FC03-C03-U074`	unmatched categorical factorization	`unmatched`	partial: `Mathlib/Topology/Connected/PathConnected.lean::pathSetoid`; `ZerothHomotopy`; `ZerothHomotopy.mk`; `lift`; `Mathlib/Topology/Homotopy/TopCat/ZerothHomotopy.lean::zerothHomotopyEquiv`	N	The quotient by path-connectedness is formalized, but no declaration realizes `π₀ : Top → Set` as the coequalizer of endpoint evaluation from the path-space diagram.
`FC03-C03-U075`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/HasLimits.lean::HasLimit.isoOfNatIso`; generated `HasColimit.isoOfNatIso`	P	A natural isomorphism of diagrams canonically induces an isomorphism of their chosen limits or colimits, with the expected leg compatibility.
`FC03-C03-U076`	unmatched concrete counterexample	`unmatched`	partial: `Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean::sectionsEquivFixedPoints`; `limitEquivFixedPoints`; `colimitTypeRel_iff_orbitRel`; `colimitEquivOrbitRelQuotient`	N	Fixed-point and orbit formulas are available generically, but no declaration realizes the source pair of objectwise-isomorphic `G`-sets whose fixed-point limits and orbit colimits differ.
`FC03-C03-U077`	unmatched species example	`unmatched`	—	N	No searched Lean implementation of the `Sym`/`Ord` species on `Fin_iso`, their objectwise cardinality comparison, or differing unlabeled orbit colimits was found.
`FC03-C03-U078`	unmatched noncanonicity theorem	`unmatched`	partial: `Mathlib/CategoryTheory/Limits/Shapes/Pullback/Pasting.lean`; `Mathlib/CategoryTheory/LocallyCartesianClosed/ChosenPullbacksAlong.lean`	N	Mathlib formalizes positive pullback pasting and chosen pullbacks, but no declaration proves the source impossibility of making both horizontal and vertical pasting strictly canonical.
`FC03-C03-U079`	exact natural associator	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean::prod.associator`; `prod.associator_naturality`; product hom-ext/projection lemmas	P	Exact unique natural product associativity isomorphism compatible with all projections.
`FC03-C03-U080`	unmatched Isbell example	`unmatched`	partial: `Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean::prod.associator`	N	No project/pinned/current/source-atlas/indexed declaration constructs Isbell’s skeletal category of sets in which product objects are literally equal but the canonical associator is nonidentity.
`FC03-C03-U081`	unmatched iff theorem	`unmatched`	partial: `Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean::coneOfDiagramInitial`; `limitOfDiagramInitial`	N	An initial object gives a limit of every diagram, hence the forward direction for `𝟭 C`, but no searched declaration proves the converse or packages the exact identity-functor iff.
`FC03-C03-U082`	exact cardinal interface	`mathlib`	`Mathlib/CategoryTheory/Comma/CardinalArrow.lean::Arrow.equivSigma`; `hasCardinalLT_of_hasCardinalLT_arrow`; `Mathlib/CategoryTheory/SmallRepresentatives.lean::SmallCategoryCardinalLT`; `SmallCategoryCardinalLT.hasCardinalLT`; `exists_equivalence`	P	`Arrow C` is equivalent to the sigma type of all source/target/morphism triples, so `HasCardinalLT (Arrow C) κ` is exactly the source cardinality condition; the representative interface packages κ-small index categories.
`FC03-C03-U083`	exact Freyd theorem specialization	`mathlib`	`Mathlib/CategoryTheory/Limits/SmallComplete.lean`, `Quiver.IsThin C` instance under `[SmallCategory C] [HasProducts.{u} C]`; dual via opposite	P	The file explicitly formalizes Freyd’s small-complete theorem: a small category with all same-universe products is thin. For a κ-small category the proof indexes by its κ-small morphism set, giving the source theorem and its colimit dual.
`FC03-C03-U084`	exact Fubini theorem	`mathlib`	`Mathlib/CategoryTheory/Limits/Fubini.lean::limitUncurryIsoLimitCompLim`; `colimitUncurryIsoColimitCompColim`; `limitFlipCompLimIsoLimitCompLim`; `colimitFlipCompColimIsoColimitCompColim`	P	Exact canonical isomorphisms between the two iterated (co)limits and the product-indexed (co)limit.
`FC03-C03-U085`	exact naturality strengthening	`mathlib`	`Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean::limIsoFlipCompWhiskerLim`; `limCompFlipIsoWhiskerLim`; `colimIsoFlipCompWhiskerColim`; `colimCompFlipIsoWhiskerColim`	P	These are natural isomorphisms of the chosen limit/colimit functors, exactly the source naturality statement.
`FC03-C03-U086`	exact comparison morphism	`mathlib`	`Mathlib/CategoryTheory/Limits/ColimitLimit.lean::colimitLimitToLimitColimit`; `colimitLimitToLimitColimitCone`; ι/π compatibility lemmas	P	Direct canonical morphism from a colimit of limits to the corresponding limit of colimits.
`FC03-C03-U087`	exact inequality	`mathlib`	`Mathlib/Order/CompleteLattice/Basic.lean::iSup_iInf_le_iInf_iSup`	P	The complete-lattice theorem is precisely `sup_x inf_y f(x,y) ≤ inf_y sup_x f(x,y)`; its ambient completeness is stronger than merely assuming the displayed extrema exist.
`FC03-C03-U088`	unmatched proof-identification remark	`unmatched`	partial: `Mathlib/CategoryTheory/Limits/ColimitLimit.lean::colimitLimitToLimitColimit`; `Mathlib/Order/CompleteLattice/Basic.lean::iSup_iInf_le_iInf_iSup`	N	Both the categorical comparison and minimax inequality are formalized, but no declaration identifies the ordinary order proof with the universal-property construction as asserted by this source remark.
`FC03-C03-U089`	exact order/categorical formulas	`mathlib`	`Mathlib/Data/EReal/Basic.lean::EReal` with `CompleteLinearOrder`; `Mathlib/CategoryTheory/Limits/Lattice.lean::limit_eq_iInf`; `colimit_eq_iSup`; `Mathlib/Order/LiminfLimsup.lean::liminf_eq_iSup_iInf_of_nat'`; `limsup_eq_iInf_iSup_of_nat'`; `liminf_le_limsup`	P	Extended reals are complete/cocomplete as a poset, limits/colimits are infima/suprema, and the source liminf/limsup tail formulas and inequality are explicit.
`FC03-C03-U090`	exact definition/criterion	`mathlib`	`Mathlib/CategoryTheory/Filtered/Basic.lean::IsFiltered`; `cocone_nonempty`; `of_cocone_nonempty`; `iff_cocone_nonempty`	P	`iff_cocone_nonempty` is exactly the characterization that every finite diagram admits a cone under it (Mathlib’s cocone terminology).
`FC03-C03-U091`	unmatched bundled examples	`unmatched`	partial: `Mathlib/CategoryTheory/Filtered/Basic.lean::isFiltered_of_semilatticeSup_nonempty`; `isFiltered_of_directed_le_nonempty`; `IsFiltered` criteria	N	Generic directed-order machinery covers ordinal-like categories, but no declaration realizes the complete source bundle, notably the one-object nonidentity-idempotent example and all stated parallel-pair/span/discrete nonexamples.
`FC03-C03-U092`	exact theorem	`mathlib`	`Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean::colimitLimitToLimitColimit_isIso`; `filtered_colim_preservesFiniteLimits_of_types`; `colimitLimitIso`	P	Exact theorem that filtered colimits in `Type`/Set commute with finite limits.
`FC03-C03-U093`	exact filtered-colimit construction	`mathlib`	`Mathlib/CategoryTheory/Limits/Types/Filtered.lean::FilteredColimit.Rel`; `rel_equiv`; `colimit_eq_iff`; `jointly_surjective_of_isColimit₂`; `Mathlib/CategoryTheory/Filtered/Basic.lean::cocone_nonempty`	P	`Rel` is literally equality after mapping two elements to a common later stage; `colimit_eq_iff` identifies this with colimit equality, while joint surjectivity and finite cocones supply simultaneous representatives at one stage.

Provenance contract for C04

Project search: LeanCategories/** outside .lake/.agents/.git was searched first for every C04 adjunction, concrete example, exactness theorem, reflective-subcategory construction, and adjoint-functor theorem. No project-owned C04 route was found; isolated definitions such as FieldCat or torsionFreeInclusion do not realize the source theorems by themselves.
Pinned Mathlib: project pin db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0, Lean v4.33.0), denoted P, was checked declaration-by-declaration. The core adjunction, Galois-connection, Kan-extension, parametrized-adjunction, closed-monoidal, exact-functor, reflective, weakly-initial, generator/subobject, and presentability APIs below are all present at that revision.
Current/open Mathlib: upstream 810b3888d0aa94294b18587c453466bc86c1f0fc (Apache-2.0, Lean v4.34.0-rc2) was rechecked 2026-09-06. Mathlib/CategoryTheory/Presentable/SolutionSetCondition.lean is post-pin and supplies SolutionSetCondition.of_isCardinalAccessible, but it does not prove the full locally-presentable adjoint-functor equivalence of U076. Current code also retains the explicit TODOs noted below for parametrized adjoint assembly, convenient Cartesian closure, transported Ab tensor structure, and noncommutative tensor right-exactness.
External search: rkirov/category-theory-in-context-lean@cae97fae75665bb93d36ff763c9243346806d12a is MIT, Lean v4.24.0-rc1 / Mathlib 4b9a202…, and covers only early Chapter 1. dagurtomas/LeanCondensed@50500fadbbfa205092dd7fb07a59a05eea23ce66 is Apache-2.0, Lean v4.32.0-rc1 / Mathlib 8231e3b…; LeanCondensed/Projects/AdjointFunctorTheorem.lean gives one locally-presentable adjoint direction but not U076’s full iff and later contains unfinished proofs, so it is not a route. Other targeted GitHub/Reservoir/source-atlas searches produced no complete C04 owner.
N denotes dated 2026-09-06 negative evidence after project-first search, pinned/current Mathlib, relevant open work, source-atlas repositories, Reservoir/GitHub, and Loogle/LeanSearch as feasible. Concrete bundles are not credited from generic ingredients unless declarations realize the stated example. Rows using Riehl’s stronger “strictly creates” or explicit arbitrary-subobject-intersection hypotheses are not silently weakened to Mathlib’s ordinary CreatesLimit or WellPowered formulations.

C04 — Adjunctions

FC03 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
`FC03-C04-U001`	exact match	`mathlib`	`Mathlib/CategoryTheory/Adjunction/Basic.lean::Adjunction`; `Adjunction.homEquiv`	P	Exact natural hom-set equivalence definition of `F ⊣ G`, including transpose maps.
`FC03-C04-U002`	exact match	`mathlib`	`Adjunction/Basic.lean::CoreHomEquiv`; `Adjunction.mkOfHomEquiv`; hom-equivalence naturality lemmas	P	The two naturality equations are exactly the source criterion for a family of hom-set equivalences to define an adjunction.
`FC03-C04-U003`	exact notation	`mathlib`	notation `F ⊣ G` in `Adjunction/Basic.lean`	P	Same left/right adjoint assertion; Riehl’s alternate right-facing glyph is only notation.
`FC03-C04-U004`	exact concrete adjunctions	`mathlib`	`Mathlib/Topology/Category/TopCat/Adjunctions.lean::TopCat.adj₁`; `TopCat.adj₂`; `discrete`; `trivial`; `forget`	P	Exact discrete-left-adjoint and indiscrete-right-adjoint to the underlying-set functor.
`FC03-C04-U005`	exact match	`mathlib`	`Mathlib/CategoryTheory/Category/GaloisConnection.lean::GaloisConnection.adjunction`; `Adjunction.gc`	P	A preorder adjunction is exactly a monotone Galois connection.
`FC03-C04-U006`	exact concrete example	`mathlib`	`Mathlib/Algebra/Order/Floor/Defs.lean::Int.gc_coe_floor`; `Int.gc_ceil_coe`; `Int.le_floor`; `Int.ceil_le`	P	Specializing to `ℝ` gives floor as right adjoint and ceiling as left adjoint to `ℤ ↪ ℝ`.
`FC03-C04-U007`	exact concrete example	`mathlib`	`Mathlib/Data/Set/Lattice/Image.lean::Set.image_preimage`; `Mathlib/Data/Set/Image.lean::Set.image_subset_iff`	P	Direct image is left adjoint to inverse image on powersets ordered by inclusion.
`FC03-C04-U008`	exact structural example	`mathlib`	`Set α = α → Prop`; pointwise order and complete Boolean-algebra instances	P	Propositional functions are predicates, with pointwise implication exactly the powerset order used in the source.
`FC03-C04-U009`	exact family of examples	`mathlib`	`GrpCat.adj`; `AddCommGrpCat.adj`; `CommRingCat.adj`; `ModuleCat.adj`; `MonCat.adj`; `AlgCat.adj`	P	Explicit free-forgetful adjunctions realize the source’s principal algebraic examples and terminology.
`FC03-C04-U010`	source specialization	`mathlib`	`Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean::restrictScalars`; `extendScalars`; `extendRestrictScalarsAdj`	P	Exact extension/restriction-of-scalars adjunction for commutative base rings. Riehl states a general ring map; Mathlib’s categorical extension construction currently imposes commutativity.
`FC03-C04-U011`	exact general mechanism plus concrete specialization	`mathlib`	`Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean::Functor.lanAdjunction`; `ranAdjunction`; `Mathlib/RepresentationTheory/Induced.lean::Rep.indResAdjunction`; `Coinduced.lean::Rep.resCoindAdjunction`	P	Precomposition/restriction has left/right Kan-extension adjoints when the needed (co)limits exist; the representation files give the group-action specialization explicitly.
`FC03-C04-U012`	unmatched nonexistence example	`unmatched`	—	N	No declaration proves the four forgetful functors from fields to rings/abelian groups/units/sets have neither adjoint; field infrastructure alone is insufficient.
`FC03-C04-U013`	exact match	`mathlib`	`Mathlib/CategoryTheory/Category/Quiv.lean::Cat.free`; `Quiv.forget`; `Quiv.adj`; `Quiv.pathsEquiv`	P	Exact free category on a directed graph/quiver with paths and concatenation.
`FC03-C04-U014`	unmatched concrete adjunction chain	`unmatched`	partial: `SimplexCategory.δ`; `SimplexCategory.σ`	N	Face and degeneracy maps are formalized, but no pinned/current declaration realizes Riehl’s `2n+1` chain of ordinal adjunctions/Galois connections.
`FC03-C04-U015`	unmatched two-sided example	`unmatched`	partial: `Grpd.free`; `Grpd.freeForgetAdjunction`; `CategoryTheory.Core`; `Core.inclusion`; `Functor.core`	N	The free-groupoid left adjoint is exact. The maximal core exists objectwise, but Mathlib explicitly lacks a functorial `Cat ⥤ Grpd` right adjoint to the inclusion, so the row’s pair of adjoints is incomplete.
`FC03-C04-U016`	exact match	`mathlib`	`Adjunction.unit`; `Adjunction.homEquiv_id`	P	Unit components are exactly the transposes of identities on `F c`.
`FC03-C04-U017`	exact match	`mathlib`	`Adjunction.counit`; `Adjunction.homEquiv_symm_id`	P	Counit components are exactly the inverse transposes of identities on `G d`.
`FC03-C04-U018`	exact concrete example	`mathlib`	`Mathlib/Algebra/Category/Grp/Adjunctions.lean::GrpCat.free`; `GrpCat.adj`; `Mathlib/GroupTheory/FreeGroup/Basic.lean::FreeGroup`; `FreeGroup.lift`	P	Exact free-group construction and free-forgetful adjunction.
`FC03-C04-U019`	exact universal-element interpretation	`mathlib`	`Adjunction.corepresentableBy`; `representableBy`; `homEquiv_id`; `homEquiv_symm_id`	P	Unit and counit are the universal elements representing the two adjunction hom functors.
`FC03-C04-U020`	exact equivalent definition	`mathlib`	`Adjunction.CoreUnitCounit`; `Adjunction.mkOfUnitCounit`; `Adjunction.unit`; `counit`	P	Exact unit/counit plus triangle-identity presentation of an adjunction.
`FC03-C04-U021`	exact equivalence of presentations	`mathlib`	`Adjunction.CoreHomEquiv`; `CoreUnitCounit`; `mkOfHomEquiv`; `mkOfUnitCounit`	P	Direct constructors between hom-equivalence data and unit/counit triangle data.
`FC03-C04-U022`	exact structural remark	`mathlib`	`Adjunction.CoreHomEquivUnitCounit`; `CoreHomEquiv`; `CoreUnitCounit`; constructors in `Adjunction/Basic.lean`	P	Mathlib exposes the same two equivalent complete presentations as explicit structures/conversions.
`FC03-C04-U023`	exact Galois formulas	`mathlib`	`Mathlib/Order/GaloisConnection/Defs.lean::GaloisConnection.le_u_l`; `l_u_le`; `u_l_u_eq_u`; `l_u_l_eq_l`	P	Exact closure/interior and fixed-point formulas for a preorder adjunction.
`FC03-C04-U024`	exact opposite-category encoding	`mathlib`	`Mathlib/CategoryTheory/Adjunction/Opposites.lean::Adjunction.op`; `unop`; `leftOp`; `rightOp`	P	Mutual contravariant adjoints are ordinary adjunctions after passing to opposites, exactly the source semantics.
`FC03-C04-U025`	exact concrete Galois connection	`mathlib`	`Mathlib/RingTheory/Nullstellensatz.lean::MvPolynomial.zeroLocus`; `vanishingIdeal`; `zeroLocus_vanishingIdeal_galoisConnection`; `le_zeroLocus_iff_le_vanishingIdeal`	P	Exact algebraic-set/ideal contravariant Galois connection; finite variables over an algebraically closed field specialize to Riehl.
`FC03-C04-U026`	exact syntax/semantics setup	`mathlib`	`Mathlib/ModelTheory/Basic.lean::FirstOrder.Language`; `Language.Structure`; `Syntax.lean::Language.Sentence`; `Language.Theory`; `Semantics.lean::Sentence.Realize`; `Theory.Model`	P	Direct formalization of first-order signatures, structures, theories, and satisfaction used in the source example.
`FC03-C04-U027`	unmatched bundled Galois connection	`unmatched`	partial: model-theory satisfaction and complete-theory APIs	N	No declaration packages sets of axioms and classes of structures as the stated Galois connection via satisfaction.
`FC03-C04-U028`	exact adjoint assembly theorem	`mathlib`	`Adjunction/Basic.lean::rightAdjointOfEquiv`; `adjunctionOfEquivRight`; dual `leftAdjointOfEquiv`; `adjunctionOfEquivLeft`	P	Given chosen representing objects and one-variable natural hom equivalences, Mathlib constructs the missing functor action and adjunction exactly.
`FC03-C04-U029`	explicit library TODO	`unmatched`	partial: `Mathlib/CategoryTheory/Adjunction/Parametrized.lean::ParametrizedAdjunction`	N	The file’s TODO is precisely this theorem: objectwise right adjoints should assemble into the parametrized right-adjoint bifunctor; it remains absent at P and H.
`FC03-C04-U030`	exact encoding	`mathlib`	`Adjunction/Parametrized.lean::ParametrizedAdjunction` (`F ⊣₂ G`)	P	The module documentation states that a two-variable adjunction is the third functor together with `F ⊣₂ G` and `F.flip ⊣₂ H`, exactly Riehl’s triple.
`FC03-C04-U031`	exact closed-monoidal interface	`mathlib`	`Mathlib/CategoryTheory/Monoidal/Closed/Basic.lean::Closed`; `MonoidalClosed`; `ihom.adjunction`; `MonoidalClosed.internalHom`; `internalHomAdjunction₂`	P	Exact left/right closure/internal-Hom formulation; braiding transports the second closure where appropriate.
`FC03-C04-U032`	exact Set/Type example	`mathlib`	`Mathlib/CategoryTheory/Monoidal/Closed/Types.lean::Types.tensorProductAdjunction`; `MonoidalClosed (Type v)`	P	Function types and currying give the Cartesian closed structure on the category of types.
`FC03-C04-U033`	exact definition	`mathlib`	`Mathlib/CategoryTheory/Monoidal/Closed/Cartesian.lean`; `CartesianMonoidalCategory`; `MonoidalClosed`	P	This is Mathlib’s current interface for Cartesian closed categories.
`FC03-C04-U034`	unmatched convenient-space example	`unmatched`	partial: `Topology/Convenient/Category.lean`; `Topology/Convenient/HomSpace.lean`; `Topology/Category/CompactlyGenerated.lean`	N	Completeness/cocompleteness and conditional currying infrastructure exist, but the relevant files still leave Cartesian/monoidal closure as TODO and do not bundle Steenrod’s Hausdorff convenient category with all stated properties.
`FC03-C04-U035`	unmatched concrete Ab tensor-Hom adjunction	`unmatched`	partial: `ModuleCat ℤ` is monoidal closed; `AddCommGrpCat ≌ ModuleCat ℤ`	N	Mathlib explicitly has not transported the tensor monoidal structure across the `ℤ`-module equivalence; existing `AddCommGrpCat` monoidal structure is Cartesian product, not tensor product.
`FC03-C04-U036`	unmatched convenient-topology specialization	`unmatched`	partial: generic convenient-space curry infrastructure	N	No category-level convenient `Top` closed structure or declaration packages `S¹ × - ⊣ Map(S¹,-)` with the path/loop interpretation.
`FC03-C04-U037`	unmatched smash-product construction	`unmatched`	—	N	No Lean4 monoidal smash-product structure for based topological spaces is present; current Mathlib still mentions the pointed-type smash monoidal structure only as a TODO.
`FC03-C04-U038`	exact uniqueness theorem	`mathlib`	`Mathlib/CategoryTheory/Adjunction/Unique.lean::Adjunction.leftAdjointUniq`; `unit_leftAdjointUniq_hom`; `leftAdjointUniq_hom_counit`	P	Exact unique natural isomorphism between two left adjoints to one right adjoint, compatible with the specified units/counits.
`FC03-C04-U039`	exact composition theorem	`mathlib`	`Mathlib/CategoryTheory/Adjunction/Basic.lean::Adjunction.comp`	P	The composite of left adjoints is left adjoint to the reverse composite of right adjoints.
`FC03-C04-U040`	exact adjointification theorem	`mathlib`	`Mathlib/CategoryTheory/Equivalence.lean::Equivalence.adjointifyη`; `Equivalence.mk`; `Mathlib/CategoryTheory/Adjunction/Basic.lean::Equivalence.toAdjunction`	P	Any equivalence can be adjusted to an adjoint equivalence satisfying triangle identities.
`FC03-C04-U041`	exact whiskering adjunction	`mathlib`	`Mathlib/CategoryTheory/Adjunction/Whiskering.lean::Adjunction.whiskerRight`; `whiskerLeft`	P	Post/precomposition with an adjoint pair induces the source adjunctions on functor categories.
`FC03-C04-U042`	exact bicategorical transfer	`mathlib`	`Mathlib/CategoryTheory/Bicategory/Adjunction/Basic.lean::Bicategory.Adjunction.comp`; `adjointifyCounit`; `Bicategory.Equivalence.mkOfAdjointifyCounit`; `Mathlib/CategoryTheory/Bicategory/Adjunction/Mate.lean::Adjunction.homEquiv₁`; `homEquiv₂`; `conjugateEquiv`; whiskering lemmas; `Mathlib/CategoryTheory/Bicategory/Adjunction/Adj.lean::lIso`; `rIso`	P	Mathlib internalizes the source adjunction manipulations in arbitrary bicategories: composition, adjointification, mate/conjugation equivalences, and unit/counit comparison isomorphisms realize the transfer content of the remark, distributed across the bicategorical API.
`FC03-C04-U043`	exact characterization	`mathlib`	`Mathlib/CategoryTheory/Limits/ConeCategory.lean::hasLimitsOfShape_iff_isLeftAdjoint_const`; `hasColimitsOfShape_iff_isRightAdjoint_const`; `HasLimits.lean::constLimAdj`; `colimConstAdj`	P	Exact equivalence between existence of all `J`-(co)limits and existence of the corresponding adjoint to the constant-diagram functor.
`FC03-C04-U044`	exact theorem	`mathlib`	`Mathlib/CategoryTheory/Adjunction/Limits.lean::Adjunction.rightAdjoint_preservesLimits`	P	Right adjoints preserve all existing limits.
`FC03-C04-U045`	exact theorem	`mathlib`	`Mathlib/CategoryTheory/Adjunction/Limits.lean::Adjunction.leftAdjoint_preservesColimits`	P	Left adjoints preserve all existing colimits.
`FC03-C04-U046`	exact concrete corollary	`mathlib`	`Mathlib/Data/Set/Lattice/Image.lean::Set.preimage_iUnion`; `preimage_iInter`; `image_iUnion`; `Mathlib/Data/Set/Image.lean::image_inter_subset`	P	Exact inverse-image preservation of unions/intersections, direct-image preservation of unions, and only inclusion for intersections.
`FC03-C04-U047`	exact concrete corollary	`mathlib`	`Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean::TensorProduct.directSum`; `directSumLeft`; `directSumRight`	P	Specializing the direct-sum tensor equivalence to two vector spaces gives `U ⊗ (V ⊕ W) ≅ (U ⊗ V) ⊕ (U ⊗ W)`.
`FC03-C04-U048`	exact canonical equivalences and arithmetic	`mathlib`	`Mathlib/Logic/Equiv/Sum.lean::Equiv.prodSumDistrib`; `Mathlib/Logic/Equiv/Prod.lean::Equiv.arrowProdEquivProdArrow`; `Equiv.sumArrowEquivProdArrow`; `Mathlib/SetTheory/Cardinal/Defs.lean::Cardinal.power_add`; cardinal commutative-semiring laws	P	The three stated set bijections are explicit canonical equivalences, and the resulting cardinal distributive/exponential laws are formalized directly.
`FC03-C04-U049`	exact free-product consequence	`mathlib`	`Mathlib/GroupTheory/CoprodI.lean::FreeGroupBasis.coprodI`; `Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean::FreeGroupBasis.repr`	P	A binary coproduct of free groups has basis the disjoint sum, giving the free group on `X ⊕ Y`.
`FC03-C04-U050`	unmatched noncommutative theorem	`unmatched`	partial: `Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean::LinearMap.lTensor_exact`; `rTensor_exact`	N	Riehl assumes an arbitrary `R`–`S` bimodule. Mathlib’s right-exact tensor theorem is commutative-base only and retains an explicit TODO for the noncommutative case; external candidates found were incomplete or stronger-specialized.
`FC03-C04-U051`	exact definitions	`mathlib`	`Mathlib/CategoryTheory/Limits/Preserves/Finite.lean::PreservesFiniteLimits`; `PreservesFiniteColimits`; `Mathlib/CategoryTheory/Limits/ExactFunctor.lean::LeftExactFunctor`; `RightExactFunctor`	P	Left/right exact are literally preservation of finite limits/colimits.
`FC03-C04-U052`	exact abelian criterion	`mathlib`	`Mathlib/CategoryTheory/Preadditive/LeftExact.lean::Functor.preservesFiniteLimits_of_preservesKernels`; `preservesBinaryProduct_of_preservesKernels`; `Functor.preservesFiniteLimits_tfae`; dual results	P	In the preadditive/abelian setting the finite-product/direct-sum and kernel conditions are equivalent to finite-limit preservation, exactly Riehl’s criterion.
`FC03-C04-U053`	exact adjoint exactness theorem	`mathlib`	`Adjunction/Limits.lean::rightAdjoint_preservesLimits`; `leftAdjoint_preservesColimits`; `Adjunction/Additive.lean::right_adjoint_additive`; `left_adjoint_additive`	P	Between abelian categories, the right adjoint is left exact, the left adjoint right exact, and both are additive.
`FC03-C04-U054`	exact definition/generalization	`mathlib`	`Mathlib/CategoryTheory/Adjunction/Reflective.lean::Reflective`; `reflector`; `reflectorAdjunction`; `Functor.fullyFaithfulOfReflective`	P	Mathlib generalizes a literal full-subcategory inclusion to a fully faithful functor equipped with a chosen left adjoint.
`FC03-C04-U055`	exact faithful/full criteria	`mathlib`	`Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean::counit_epi_of_R_faithful`; `faithful_R_of_epi_counit_app`; `counit_isSplitMono_of_R_full`; `full_R_of_isSplitMono_counit_app`; `counit_isIso_of_R_fully_faithful`; `fullyFaithfulROfIsIsoCounit`	P	Exact iff criteria for the right adjoint to be faithful, full, or fully faithful in terms of counit components.
`FC03-C04-U056`	exact concrete reflections	`mathlib`	`Mathlib/Topology/Category/CompHaus/Basic.lean::stoneCechEquivalence`; `topToCompHaus`; reflective instance; `Mathlib/Algebra/Category/Grp/Adjunctions.lean::GrpCat.abelianize`; `GrpCat.abelianizeAdj`	P	Exact Stone–Čech reflection `CompHaus ↪ Top` and abelianization reflection `CommGrp ↪ Grp`.
`FC03-C04-U057`	unmatched bundled examples	`unmatched`	partial: `GrpCat.abelianizeAdj`	N	Abelianization is realized, but no categorical commutativization reflector `CRing ↪ Ring` or torsion-free-abelian reflector `A ↦ A/TA` was found at P, H, project, or external search.
`FC03-C04-U058`	exact reflective-(co)limit theorem	`mathlib`	`Mathlib/CategoryTheory/Monad/Limits.lean::hasLimit_of_reflective`; `hasLimitsOfShape_of_reflective`; `hasLimits_of_reflective`; `hasColimitsOfShape_of_reflective`; `hasColimits_of_reflective`; `monadicCreatesLimits`	P	A reflective inclusion creates ambient limits, while colimits are obtained by applying the reflector to ambient colimits.
`FC03-C04-U059`	exact theorem	`mathlib`	`Mathlib/CategoryTheory/Category/Cat/Limit.lean` HasLimits instance; `Category/Cat/Colimit.lean` HasColimits instance	P	The universe-polymorphic category of categories is complete and cocomplete.
`FC03-C04-U060`	exact comma characterization	`mathlib`	`Mathlib/CategoryTheory/Adjunction/Comma.lean::leftAdjointOfStructuredArrowInitials`; `adjunctionOfStructuredArrowInitials` and converse structured-arrow initiality from an adjunction	P	Exact iff: a left adjoint exists precisely when every `s ↓ U` has an initial object.
`FC03-C04-U061`	exact standard interface	`mathlib`	`PreservesLimits`; `PreservesColimits`	P	Mathlib’s global preservation typeclasses are exactly continuous/cocontinuous in Riehl’s terminology.
`FC03-C04-U062`	unmatched strict-creation strengthening	`unmatched`	partial: `Mathlib/CategoryTheory/Limits/Comma.lean::StructuredArrow.createsLimit`; `createsLimitsOfShape`; `createsLimitsOfSize`	N	Riehl requires the projection to strictly create the preserved limit. Mathlib’s `CreatesLimit` only supplies a lifted cone whose image is isomorphic to the original cone (`LiftableCone.validLift : F.mapCone liftedCone ≅ c`), not an on-the-nose unique lift. No strict-creation interface/theorem for this comma projection was found in project, pinned/current Mathlib, or searched external Lean work as of 2026-09-06.
`FC03-C04-U063`	exact general adjoint-functor theorem	`mathlib`	`Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean::SolutionSetCondition`; `isRightAdjoint_of_preservesLimits_of_solutionSetCondition`; `solutionSetCondition_of_isRightAdjoint`	P	Exact solution-set criterion for a continuous functor from a complete locally-small domain to admit a left adjoint.
`FC03-C04-U064`	exact definitions	`mathlib`	`Mathlib/CategoryTheory/Limits/Constructions/WeaklyInitial.lean` weakly-initial APIs; object-property weak initial formulations in adjoint-functor code	P	Exact weakly initial and jointly weakly initial notions used by the source proof.
`FC03-C04-U065`	exact construction theorem	`mathlib`	`Mathlib/CategoryTheory/Limits/Constructions/WeaklyInitial.lean::has_weakly_initial_of_weakly_initial_set_and_hasProducts`; `hasInitial_of_weakly_initial_and_hasWideEqualizers`	P	Products turn a jointly weakly initial set into one weakly initial object; wide equalizers then produce an initial object, yielding the complete-category lemma.
`FC03-C04-U066`	unmatched worked solution-set example	`unmatched`	partial: free-group adjunction and generic solution-set theorem	N	No declaration realizes Riehl’s explicit cardinality-bounded jointly weakly initial family in `S ↓ Group`; generic free-group existence does not formalize this worked proof.
`FC03-C04-U067`	exact definitions	`mathlib`	`Mathlib/CategoryTheory/Generator/Basic.lean::ObjectProperty.IsSeparating`; `IsCoseparating`; `IsSeparator`; `IsCoseparator`	P	Exact separating/coseparating set and single-object notions.
`FC03-C04-U068`	exact definition	`mathlib`	`Mathlib/CategoryTheory/Subobject/Basic.lean::Subobject`; `Subobject.mk`; `equivMonoOver`	P	Subobjects are mono arrows modulo isomorphism, exactly the source convention.
`FC03-C04-U069`	unmatched source-hypothesis theorem	`unmatched`	partial: `AdjointFunctorTheorems.lean::isRightAdjoint_of_preservesLimits_of_isCoseparating`	N	Mathlib’s special adjoint-functor theorem assumes `WellPowered`; Riehl instead assumes arbitrary intersections of subobjects. Mathlib derives intersections from stronger hypotheses but no converse/equivalent theorem was found, so the source hypothesis set is not matched.
`FC03-C04-U070`	unmatched source-hypothesis lemma	`unmatched`	partial: `Mathlib/CategoryTheory/Generator/Basic.lean::hasInitial_of_isCoseparating`	N	The pinned lemma uses `WellPowered`; no theorem with exactly Riehl’s arbitrary-subobject-intersection assumption was found.
`FC03-C04-U071`	unmatched Stone–Čech SAFT construction	`unmatched`	partial: exact Stone–Čech adjunction and generic coseparator APIs	N	The reflection itself is formalized, but no declaration packages `[0,1]` as a `CompHaus` coseparator and carries out Riehl’s SAFT construction.
`FC03-C04-U072`	unmatched source-hypothesis corollary	`unmatched`	partial: `AdjointFunctorTheorems.lean` coseparating/WellPowered cocompleteness theorem	N	Mathlib proves cocompleteness from a small coseparating family under `WellPowered`, not from Riehl’s stated arbitrary-intersection hypothesis; no equivalence closing the gap was found.
`FC03-C04-U073`	unmatched source-hypothesis representability corollary	`unmatched`	partial: special AFT plus representability/adjunction APIs	N	The analogous result is derivable under Mathlib’s `WellPowered` hypothesis, but no declaration realizes Riehl’s exact intersection-of-subobjects assumptions.
`FC03-C04-U074`	exact solution-set representability criterion	`mathlib`	`Adjunction/AdjointFunctorTheorems.lean::isRightAdjoint_of_preservesLimits_of_solutionSetCondition`; `Adjunction/PartialAdjoint.lean::leftAdjointObjIsDefined`; `isRightAdjoint_iff_leftAdjointObjIsDefined_eq_top`; corepresentability APIs	P	Applying the general AFT to a Type-valued functor identifies the left-adjoint value at the singleton with a representing object, matching the source solution-set criterion.
`FC03-C04-U075`	exact definitions	`mathlib`	`Mathlib/CategoryTheory/Presentable/LocallyPresentable.lean::IsCardinalLocallyPresentable`; `IsLocallyPresentable`; `IsAccessibleCategory`; cardinal accessibility APIs	P	Exact locally-κ-presentable/local-presentable/accessibility framework, with regular-cardinal parameters and filtered-colimit preservation.
`FC03-C04-U076`	unmatched full locally-presentable iff	`unmatched`	partial: current-only `Presentable/SolutionSetCondition.lean::SolutionSetCondition.of_isCardinalAccessible`; external LeanCondensed partial theorem	N	Neither P nor H proves both source iff statements. Current Mathlib supplies accessibility ⇒ solution-set only, and the external LeanCondensed file proves one direction under compatible-style hypotheses but not the full equivalence and contains unfinished later proofs.

Provenance contract for C05

Project search: LeanCategories/** outside .lake/.agents/.git was searched first for monads/comonads, affine-space algebras, Kleisli/Eilenberg–Moore comparisons, Beck coequalizers, concrete monadicity examples, and monadic completeness/cocompleteness consequences. No project-owned C05 route was found.
Pinned Mathlib: project pin db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0, Lean v4.33.0), denoted P, was checked declaration-wise. Its dedicated CategoryTheory/Monad/** files cover monads/comonads, EM and Kleisli categories, comparison functors, Beck coequalizers/monadicity, and creation of limits/preserved colimits. Pinned topology, affine-space, p-adic, and Type (co)limit APIs supply the concrete rows credited below.
Current/open Mathlib: upstream 810b3888d0aa94294b18587c453466bc86c1f0fc (Apache-2.0, Lean v4.34.0-rc2) was rechecked 2026-09-06. The explicit TODO that forget CompHaus is monadic remains in Mathlib/Topology/Category/Compactum.lean; no current-only MonadicRightAdjoint owner for the concrete CompHaus/Module/Ring examples was found. No current theorem closes the finitary-monad cocompleteness or algebraic-theory-model gaps below.
External search: targeted GitHub/Reservoir/source-atlas searches for categorical powerset, CompHaus/Module/Ring monadicity, algebraic theories, affine monads, and Kleisli-to-EM comparison found no complete compatible Lean owner. Concrete programming-language Monad instances are not CategoryTheory.Monad routes. External partial developments with unfinished proofs are not credited.
N denotes dated 2026-09-06 negative evidence after project-first search, pinned/current Mathlib, relevant open work, source-atlas repositories, Reservoir/GitHub, and Loogle/LeanSearch as feasible. Bundled examples are credited only when all mathematical claims in the canonical unit have declaration-level owners. Riehl’s strictly creates assertions are not weakened to Mathlib’s ordinary CreatesColimit, whose lift is only identified up to isomorphism.

C05 — Monads and Their Algebras

FC03 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
`FC03-C05-U001`	exact match	`mathlib`	`Mathlib/CategoryTheory/Monad/Basic.lean::Monad`	P	Exact endofunctor, unit, multiplication, associativity, and two unit laws.
`FC03-C05-U002`	exact conceptual equivalence	`mathlib`	`Mathlib/CategoryTheory/Monad/EquivMon.lean::monadMonEquiv`	P	Explicit categorical equivalence `Monad C ≌ Mon (C ⥤ C)` for the composition monoidal structure.
`FC03-C05-U003`	exact match	`mathlib`	`Mathlib/CategoryTheory/Monad/Adjunction.lean::Adjunction.toMonad`; `adjToMonadIso`	P	Exact construction `T=F⋙U`, unit from the adjunction, and multiplication by the whiskered counit.
`FC03-C05-U004`	unmatched bundled examples	`unmatched`	partial: concrete pointed/free-monoid/free-module/free-group/free-category adjunctions and `Adjunction.toMonad`	N	Several of the seven familiar-adjunction monads are realized, but the unit also includes the Stone–Čech/ultrafilter and contravariant double-powerset monads; no complete declaration-level realization of the whole source bundle was found.
`FC03-C05-U005`	partial concrete case only	`unmatched`	partial: `Mathlib/CategoryTheory/Category/Pointed.lean::typeToPointed`; `typeToPointedForgetAdjunction`; `Adjunction.toMonad`	N	The Set case is exact (`typeToPointed.obj X = Option X`), but the canonical unit also asserts the analogous fixed-summand construction in an arbitrary category with coproducts. Dated 2026-09-06 project/P/H/external search found no generic categorical monad construction realizing that second clause, so the bundled unit is incomplete.
`FC03-C05-U006`	exact continuation-monad realization	`mathlib`	`Mathlib/Control/Monad/Cont.lean::ContT`; `Cont`; lawful `Monad` instance; `Mathlib/CategoryTheory/Monad/Types.lean::ofTypeMonad`	P	`Cont r α = (α → r) → r` is exactly the arbitrary-classifier double-dual/continuation endofunctor in the source; its lawful type-level monad is converted by `ofTypeMonad` to a categorical monad on `Type`.
`FC03-C05-U007`	exact bundled realization	`mathlib`	`Mathlib/Data/Set/Functor.lean::Set.monad`; `Set.instLawfulMonad`; `Mathlib/Algebra/Category/MonCat/Adjunctions.lean::AddCommMonCat.free`, `AddCommMonCat.adj`; `Mathlib/Control/Monad/Writer.lean::WriterT.monad` and `[Monoid ω]` lawful instance; `Mathlib/MeasureTheory/Category/MeasCat.lean::MeasCat.Giry`; `Mathlib/CategoryTheory/Monad/Types.lean::ofTypeMonad`	P	All four Example 5.1.5 monads are realized at the pin: covariant powerset (singleton/union), free commutative monoid, writer/product by a fixed monoid, and Giry. `ofTypeMonad` supplies the categorical packaging for the lawful type monads.
`FC03-C05-U008`	exact dual definition	`mathlib`	`Mathlib/CategoryTheory/Monad/Basic.lean::Comonad`; `Mathlib/CategoryTheory/Monad/Adjunction.lean::Adjunction.toComonad`	P	Exact comonad data/laws and the comonad induced by an adjunction.
`FC03-C05-U009`	unmatched preorder identification	`unmatched`	partial: `Monad`; order-theoretic closure/interior APIs	N	The ingredients exist separately, but no declaration identifies monads on preorder categories with closure operators and comonads with kernel operators, including the topological closure/interior example.
`FC03-C05-U010`	exact affine-space definition	`mathlib`	`Mathlib/LinearAlgebra/AffineSpace/Defs.lean::AffineSpace`; `AddTorsor`; `Equiv.vaddConst`	P	Mathlib takes the equivalent simply-transitive translation/torsor presentation as the primitive definition of affine space.
`FC03-C05-U011`	exact affine-combination realization	`mathlib`	`Mathlib/LinearAlgebra/AffineSpace/Combination.lean::Finset.affineCombination`; `affineCombination_apply_const`; `affineCombination_piSingle`; `map_affineCombination`	P	The origin-independent finite affine combinations with weights summing to one are implemented on every Mathlib affine space.
`FC03-C05-U012`	unmatched affine-monad algebra theorem	`unmatched`	partial: affine spaces and affine combinations	N	No categorical affine-combination monad on `Set` and no theorem identifying its Eilenberg–Moore algebras with affine spaces was found.
`FC03-C05-U013`	exact match	`mathlib`	`Mathlib/CategoryTheory/Monad/Algebra.lean::Monad.Algebra`; algebra category and hom structure	P	Exact Eilenberg–Moore algebra object/morphism equations and category.
`FC03-C05-U014`	unmatched bundled EM examples	`unmatched`	partial: pointed/module/free-monoid structures plus generic `Monad.Algebra`	N	No declaration set identifies all source concrete Eilenberg–Moore algebra examples with their familiar categories; generic algebra infrastructure is insufficient for this bundle.
`FC03-C05-U015`	unmatched concrete module-algebra identification	`unmatched`	partial: free-module adjunction; `Monad.Algebra`	N	No declaration proves that algebras for the free `R`-module monad on sets are precisely `R`-modules with the source scalar-action formulas.
`FC03-C05-U016`	exact canonical EM adjunction	`mathlib`	`Mathlib/CategoryTheory/Monad/Algebra.lean::Monad.free`; `Monad.forget`; `Monad.adj`	P	Exact free-algebra/forgetful Eilenberg–Moore adjunction inducing the original monad.
`FC03-C05-U017`	exact match	`mathlib`	`Mathlib/CategoryTheory/Monad/Kleisli.lean::Kleisli`; category structure	P	Morphisms `A ⟶ B` are exactly `A ⟶ T B`, with unit/multiplication defining identities/composition.
`FC03-C05-U018`	unmatched bundled Kleisli examples	`unmatched`	partial: `PartialFun`, Giry, free-monoid/state ingredients	N	No declaration-level realization of the complete source suite of maybe/list/state/Giry Kleisli categories was found; isolated constituent infrastructure does not realize the bundle.
`FC03-C05-U019`	exact canonical Kleisli adjunction	`mathlib`	`Mathlib/CategoryTheory/Monad/Kleisli.lean::Monad.toKleisli`; `fromKleisli`; `Kleisli.adj`; `toKleisliCompFromKleisliIsoSelf`	P	Exact Kleisli free/forgetful adjunction recovering the monad.
`FC03-C05-U020`	unmatched universal category of presentations	`unmatched`	partial: EM and Kleisli adjunctions	N	No category `Adj_T` of all adjunctions inducing `T` and no theorem that Kleisli is initial and Eilenberg–Moore terminal in it was found.
`FC03-C05-U021`	unmatched Kleisli-to-EM comparison theorem	`unmatched`	partial: `Monad.free`, Kleisli, EM categories	N	No canonical functor `C_T ⥤ C^T` with full-faithfulness and image exactly the free algebras was found in P or H.
`FC03-C05-U022`	exact match	`mathlib`	`Mathlib/CategoryTheory/Monad/Algebra.lean::Monad.free`; `free_obj_A`; `free_obj_a`	P	The free algebra on `c` is exactly `(T c, μ_c)`.
`FC03-C05-U023`	exact monadicity definition	`mathlib`	`Mathlib/CategoryTheory/Monad/Adjunction.lean::Monad.comparison`; `MonadicRightAdjoint`; `monadicAdjunction`	P	Exact comparison-functor/equivalence definition of a monadic right adjoint.
`FC03-C05-U024`	unmatched concrete maybe-monad comparison	`unmatched`	partial: `partialFunEquivPointed`; `typeToPointedForgetAdjunction`; generic comparison functor	N	Mathlib has `PartialFun ≌ Pointed`, but no theorem identifying the Kleisli comparison for the maybe monad with that equivalence or proving the source’s strict-monadicity comparison claim.
`FC03-C05-U025`	exact idempotent property	`mathlib`	predicate `[IsIso T.μ]`; `Mathlib/CategoryTheory/Monad/Adjunction.lean::μ_iso_of_reflective`	P	Mathlib expresses idempotence by invertibility of the multiplication and proves reflective adjunctions induce such monads.
`FC03-C05-U026`	exact theorem	`mathlib`	`Mathlib/CategoryTheory/Monad/Adjunction.lean::monadicOfReflective`	P	A reflective fully faithful right adjoint is monadic, exactly the source proposition.
`FC03-C05-U027`	exact Beck coequalizer	`mathlib`	`Mathlib/CategoryTheory/Monad/Coequalizer.lean::beckAlgebraCofork`; `beckAlgebraCoequalizer`	P	Exact coequalizer of free algebras `T²A ⇉ TA → A` for a `T`-algebra.
`FC03-C05-U028`	exact definition	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/SplitCoequalizer.lean::IsSplitCoequalizer`	P	Exact split-coequalizer maps and splitting identities.
`FC03-C05-U029`	exact theorem	`mathlib`	`IsSplitCoequalizer.isCoequalizer`; `IsSplitCoequalizer.map`	P	A split coequalizer is a coequalizer and remains one after every functor, i.e. is absolute.
`FC03-C05-U030`	exact Beck split diagram	`mathlib`	`Mathlib/CategoryTheory/Monad/Coequalizer.lean::beckSplitCoequalizer`; Beck splitting maps	P	Exact split coequalizer obtained by applying the EM forgetful functor to the algebra coequalizer diagram.
`FC03-C05-U031`	exact definition	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/SplitCoequalizer.lean::Functor.IsSplitPair`; `IsSplitPair` API	P	Exact notion of a pair whose image admits a split coequalizer.
`FC03-C05-U032`	unmatched strict-creation strengthening	`unmatched`	partial: `Mathlib/CategoryTheory/Monad/Monadicity.lean::CreatesColimitOfIsSplitPair`; `createsGSplitCoequalizersOfMonadic`	N	Riehl states that `U^T` strictly creates these coequalizers. Mathlib’s `CreatesColimit` lifts only up to a cone isomorphism, not an on-the-nose unique lift, and no strict-creation theorem was found.
`FC03-C05-U033`	exact monadic consequence	`mathlib`	`Mathlib/CategoryTheory/Monad/Monadicity.lean::createsGSplitCoequalizersOfMonadic`; `CreatesColimitOfIsSplitPair`	P	For a monadic adjunction, the right adjoint creates coequalizers of its split pairs in the ordinary categorical sense.
`FC03-C05-U034`	exact Beck monadicity theorem	`mathlib`	`Mathlib/CategoryTheory/Monad/Monadicity.lean::monadicOfCreatesGSplitCoequalizers`; `monadicOfHasPreservesReflectsGSplitCoequalizers`	P	Direct Beck characterization by creation/preservation/reflection of the required split coequalizers.
`FC03-C05-U035`	unmatched concrete algebraic-category theorem	`unmatched`	partial: free-forgetful adjunctions	N	No concrete `MonadicRightAdjoint` declarations establish the source list of familiar algebraic categories as monadic over `Set`; generic Beck machinery alone does not realize the examples.
`FC03-C05-U036`	exact finitary interface and implication	`mathlib`	`PreservesFilteredColimits`; `Adjunction.leftAdjoint_preservesColimits`; functor-composition preservation instances; `Adjunction.toMonad`	P	Finitary is represented by preservation of filtered colimits; if the right adjoint is finitary, the induced monad `F⋙U` is finitary (typeclass synthesis was checked at the project pin).
`FC03-C05-U037`	unmatched algebraic-theory definition	`unmatched`	—	N	No Mathlib/project definition identifies categories of models for algebraic theories with categories admitting a finitary monadic functor to `Set`.
`FC03-C05-U038`	explicit library TODO	`unmatched`	partial: Stone–Čech/CompHaus infrastructure	N	`Mathlib/Topology/Category/Compactum.lean` explicitly states as TODO that the underlying-set functor from compact Hausdorff spaces is monadic; P and H contain no proof/instance.
`FC03-C05-U039`	unmatched bundled monadic examples	`unmatched`	partial: Module/Ring/diagram forgetful functors and adjunctions	N	No declaration-level monadicity owners were found for the complete source bundle (`Mod_R→Ab`, `Ring→Ab`, restriction of diagrams, etc.).
`FC03-C05-U040`	exact crude Beck theorem	`mathlib`	`Mathlib/CategoryTheory/Monad/Monadicity.lean::monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms`; related crude variants	P	Exact reflexive-coequalizer + preservation + reflection-of-isomorphisms sufficient criterion.
`FC03-C05-U041`	unmatched contravariant-powerset monadicity	`unmatched`	partial: set image/preimage APIs	N	No categorical functor `P : Setᵒᵖ ⥤ Set` equipped with the source monadicity theorem was found.
`FC03-C05-U042`	unmatched pullback/direct-image lemma	`unmatched`	partial: `Set.preimage_comp_eq`; `Set.image_image`; `Set.preimage_image_eq`; pullback APIs	N	The set-theoretic ingredients are present, but no declaration realizes the source lemma that direct image and inverse image commute across an arbitrary pullback square of monomorphisms in the required form.
`FC03-C05-U043`	exact monadic reflection of isomorphisms	`mathlib`	`Mathlib/CategoryTheory/Monad/Adjunction.lean::MonadicRightAdjoint.eqv`; `Monad.comparisonForget`; `Mathlib/CategoryTheory/Monad/Algebra.lean::forget_reflects_iso`	P	The comparison equivalence followed by the EM forgetful functor makes every monadic right adjoint reflect isomorphisms; the instance was checked by Lean at the pin.
`FC03-C05-U044`	exact topological theorem	`mathlib`	`Mathlib/Topology/Homeomorph/Lemmas.lean::isHomeomorph_iff_continuous_bijective`	P	For compact source and Hausdorff target, a continuous bijection is exactly a homeomorphism.
`FC03-C05-U045`	unmatched proof-method example	`unmatched`	partial: U044 theorem; U038 monadicity missing	N	The claimed roundabout derivation through monadicity of `CompHaus→Set` cannot be formalized because that monadicity theorem itself remains unproved.
`FC03-C05-U046`	unmatched algebraic-theory corollary	`unmatched`	partial: generic monadic reflection of isomorphisms	N	The abstract monadic theorem exists, but the source’s category-of-models/algebraic-theory interface of U037 is absent, so this concrete corollary has no declaration-level owner.
`FC03-C05-U047`	exact creation theorem	`mathlib`	`Mathlib/CategoryTheory/Monad/Limits.lean::monadicCreatesLimits`; `monadicCreatesColimitOfPreservesColimit`; `monadicCreatesColimitsOfShapeOfPreservesColimitsOfShape`	P	A monadic right adjoint creates all limits and every colimit it preserves, exactly the source theorem.
`FC03-C05-U048`	exact reflective consequence	`mathlib`	`Mathlib/CategoryTheory/Monad/Adjunction.lean::monadicOfReflective`; `Mathlib/CategoryTheory/Monad/Limits.lean::monadicCreatesLimits`; reflective limit instances	P	Reflective inclusions are monadic and hence create all ambient limits; completeness descends.
`FC03-C05-U049`	exact generic consequence	`mathlib`	`monadicCreatesLimits`; `hasLimitsOfSize_of_hasLimitsOfSize_createsLimitsOfSize`	P	Any category monadic over `Set/Type` inherits completeness from `Type`, with limits created by the monadic forgetful functor.
`FC03-C05-U050`	exact p-adic limit universal property	`mathlib`	`Mathlib/NumberTheory/Padics/RingHoms.lean::PadicInt.toZModPow`; `zmod_cast_comp_toZModPow`; `PadicInt.lift`; `lift_spec`; `lift_unique`	P	These maps and uniqueness equations give the inverse-limit characterization of `ℤ_p` as compatible residue systems, including the ring structure.
`FC03-C05-U051`	exact match	`mathlib`	`Mathlib/CategoryTheory/Limits/Types/Colimits.lean::Types.hasColimitsOfSize`	P	`Type`/Set is cocomplete in the universe regime used by the source.
`FC03-C05-U052`	unmatched creation strengthening	`unmatched`	partial: `Mathlib/Algebra/Category/ModuleCat/Colimits.lean::ModuleCat.colimitCocone`; `forget₂_preservesColimits`	N	Mathlib explicitly constructs module colimits and proves the forgetful functor to abelian groups preserves them, but no `CreatesColimit(s)` instance/theorem for this forgetful functor was found at P or H. Preservation is weaker than the source’s creation claim.
`FC03-C05-U053`	unmatched cocompleteness iff	`unmatched`	partial: monadic creation of preserved colimits	N	No theorem was found that for a monadic `U:A→C` with cocomplete `C`, `A` is cocomplete iff it has coequalizers.
`FC03-C05-U054`	unmatched finitary-monad cocompleteness theorem	`unmatched`	partial: filtered-colimit and monad algebra infrastructure	N	No P/H theorem proves that algebras for a finitary monad on a complete+cocomplete locally small category are both complete and cocomplete.
`FC03-C05-U055`	unmatched bundled corollaries	`unmatched`	partial: `CompHaus` cocompleteness; generic monadic limit theory	N	Compact Hausdorff cocompleteness is formalized, but the algebraic-theory/model-category cocompleteness conclusion depends on missing U037/U054 infrastructure; the bundled source unit is therefore incomplete.

Provenance contract for C06

Project search: LeanCategories/** outside .lake/.agents/.git was searched first for every C06 Kan-extension, homotopical, derived-functor, density, and codensity unit. No project-owned C06 owner was found; generic syntax or infrastructure is not credited as a source-shaped realization.
Pinned Mathlib: project pin db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0, Lean v4.33.0) is denoted P. The local Mathlib worktree is exactly at this revision, and every positive declaration below was rechecked there.
Current Mathlib/open work: upstream 810b3888d0aa94294b18587c453466bc86c1f0fc (Apache-2.0, Lean v4.34.0-rc2) was refreshed/rechecked 2026-09-06. Post-pin declarations would be reference-port; no C06 row below depends on a current-only Mathlib declaration.
External/source-atlas search: relevant recorded source-atlas repositories, Reservoir/GitHub, Loogle/LeanSearch, and targeted current-web searches were rechecked where the pinned/current libraries lacked an owner. In particular, the available Riehl-in-Lean repositories do not extend to a usable C06 formalization, and no usable external owner was found for 2-of-6 homotopical categories, Riehl deformations, or the codensity examples.
N marks dated 2026-09-06 negative evidence after project-first search, pinned/current Mathlib, relevant source-atlas repositories, GitHub/Reservoir, and Loogle/LeanSearch as feasible. A generic construction is not credited for a concrete example or a stronger source theorem unless a declaration realizes that source-shaped claim.

C06 — All Concepts Are Kan Extensions

FC03 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
`FC03-C06-U001`	exact generic interface	`mathlib`	`Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean::Functor.IsLeftKanExtension`; `Functor.IsRightKanExtension`; `Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean::Functor.lanAdjunction`; `Functor.ranAdjunction`	P	Mathlib has the two universal extension notions and, when the corresponding extensions exist functorially, their adjunctions with precomposition, exactly realizing the source’s left/right and partial-adjoint viewpoint.
`FC03-C06-U002`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean::Functor.IsLeftKanExtension`; `Functor.IsRightKanExtension`; `Functor.leftKanExtensionUnique`; `Functor.rightKanExtensionUnique`	P	The classes encode the source universal factorization of the unit/counit extension data; the uniqueness isomorphisms are the expected universal uniqueness.
`FC03-C06-U003`	unmatched bundled remark	`unmatched`	partial: `Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean::LeftExtension.IsPointwiseLeftKanExtension.isIso_hom`; `RightExtension.IsPointwiseRightKanExtension.isIso_hom`	N	The fully-faithful pointwise restriction-back isomorphisms are formalized, but no source-shaped declaration also realizes the remark’s contrasting claim that an on-the-nose extension need not be a Kan extension. The complete remark is therefore not owned.
`FC03-C06-U004`	exact match	`mathlib`	`Mathlib/CategoryTheory/Yoneda.lean::coyonedaEquiv`; dual `yonedaEquiv`	P	`coyonedaEquiv` is exactly the bijection between elements of `F c` and natural transformations `C(c,-) ⟶ F`; the presheaf dual is also present.
`FC03-C06-U005`	unmatched concrete Kan-extension example	`unmatched`	partial: `Mathlib/CategoryTheory/Action/Basic.lean::Action.functorCategoryEquivalence`; generic Kan-extension API	N	Mathlib has categorical group actions and generic Kan extensions, but no declaration identifies the Kan extensions along `1 ⥤ BG` with the indexed coproduct/product formulas or packages the displayed natural-transformation correspondences for a general G-object.
`FC03-C06-U006`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean::Functor.lanAdjunction`; `Functor.ranAdjunction`	P	These are exactly the left and right adjunctions between Kan extension along `K` and precomposition by `K`, under the corresponding existence hypotheses.
`FC03-C06-U007`	exact representation-theoretic realization	`mathlib`	`Mathlib/RepresentationTheory/Induced.lean::Rep.indFunctor`; `Rep.indResAdjunction`; `Mathlib/RepresentationTheory/Coinduced.lean::Rep.coindFunctor`; `Rep.resCoindAdjunction`	P	Mathlib’s representation category and restriction functor have induction and coinduction as the left/right adjoints asserted by the source; this is the standard bundled realization of `Vect_k^{BG}`.
`FC03-C06-U008`	unmatched augmented-simplicial specialization	`unmatched`	partial: `Mathlib/AlgebraicTopology/SimplexCategory/Augmented/Basic.lean::AugmentedSimplexCategory.inclusion`; `Mathlib/AlgebraicTopology/SimplicialSet/PiZero.lean::SSet.π₀Functor`; `SSet.isColimitCoforkπ₀`	N	The inclusion, augmented-object infrastructure, and π₀ colimit exist, but no pinned/current declaration identifies the left/right Kan extensions along the augmentation inclusion with the π₀ augmentation and trivial augmentation adjoints.
`FC03-C06-U009`	exact pointwise construction	`mathlib`	`Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean::LeftExtension.coconeAt`; `LeftExtension.IsPointwiseLeftKanExtensionAt`; `RightExtension.coneAt`; `RightExtension.IsPointwiseRightKanExtensionAt`	P	The costructured/structured arrow categories are exactly `K↓d` and `d↓K`; Mathlib defines the pointwise extension data by the corresponding colimit/limit cone at each object.
`FC03-C06-U010`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean::LeftExtension.IsPointwiseLeftKanExtensionAt.isoColimit`; `RightExtension.IsPointwiseRightKanExtensionAt.isoLimit`; `Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean::Functor.leftKanExtensionObjIsoColimit`; `Functor.ranObjObjIsoLimit`	P	These isomorphisms are precisely the comma-colimit and comma-limit formulas for pointwise left and right Kan-extension values.
`FC03-C06-U011`	exact universe-aware realization	`mathlib`	`Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean::Functor.HasPointwiseLeftKanExtensionAt`; `Functor.HasPointwiseRightKanExtensionAt`; `Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean::Functor.leftKanExtensionObjIsoColimit`; `Functor.ranObjObjIsoLimit`	P	In Mathlib the existence conditions reduce to the required comma-category colimits/limits; cocompleteness/completeness plus the source size hypotheses supply those instances, and the displayed formulas are then exactly U010.
`FC03-C06-U012`	unmatched concrete real-exponential example	`unmatched`	—	N	No declaration was found formalizing `2^x` on the rationals as the left Kan extension to the reals with value the stated supremum. Generic order-completion and real-power infrastructure does not realize this example.
`FC03-C06-U013`	exact representation formulas	`mathlib`	`Mathlib/RepresentationTheory/Induced.lean::Representation.IndV`; `Representation.ind`; `Rep.indFunctor`; `Mathlib/RepresentationTheory/Coinduced.lean::Representation.coindV`; `Representation.coind`; `Rep.coindFunctor`	P	These declarations construct the induction and coinduction objects/functors for a subgroup homomorphism, giving the explicit adjoint constructions referenced by the source.
`FC03-C06-U014`	unmatched orbit-category example	`unmatched`	—	N	No pinned/current or external Lean declaration realizes Riehl’s orbit category `O_G` together with the `BGᵒᵖ ⥤ O_G` embedding at `G/e` and the stated endomorphism computation. Generic group-action infrastructure is insufficient for this concrete example.
`FC03-C06-U015`	exact match	`mathlib`	`Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean::SimplicialObject.truncation`; `SimplicialObject.skAdj`; `SimplicialObject.coskAdj`; `Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean::SSet.skAdj`; `SSet.coskAdj`	P	Mathlib’s truncation has skeleton and coskeleton as its left and right adjoints, and the simplicial-object file explicitly installs them as the corresponding Kan extensions.
`FC03-C06-U016`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/KanExtension/Preserves.lean::Functor.PreservesLeftKanExtension`; `Functor.PreservesRightKanExtension`	P	These classes say exactly that postcomposition by a functor carries a chosen left/right Kan extension to a left/right Kan extension.
`FC03-C06-U017`	exact match	`mathlib`	`Mathlib/CategoryTheory/Bicategory/Kan/Adjunction.lean::LeftExtension.isKanOfWhiskerLeftAdjoint`	P	The declaration states exactly that a left adjoint commutes with a left Kan extension; the right-handed dual is obtained by the standard opposite/dual bicategorical construction.
`FC03-C06-U018`	exact generic consequence	`mathlib`	`Mathlib/Topology/Category/TopCat/Adjunctions.lean::TopCat.adj₁`; `TopCat.adj₂`; `Mathlib/Topology/Category/TopCat/Limits/Basic.lean::TopCat.forget_preservesLimits`; `TopCat.forget_preservesColimits`; `Mathlib/CategoryTheory/Functor/KanExtension/Preserves.lean::preservesPointwiseLKEOfHasPointwiseAndPreservesPointwise`; `preservesPointwiseRKEOfHasPointwiseAndPreservesPointwise`	P	The underlying-set functor is both a left and right adjoint and preserves all colimits/limits; hence it preserves the pointwise induction/coinduction Kan extensions exactly as asserted.
`FC03-C06-U019`	unmatched concrete comparison	`unmatched`	partial: `Mathlib/Topology/Category/TopCat/Limits/Basic.lean::TopCat.forget_preservesLimits`; representation induction/coinduction APIs	N	General preservation results and the representation adjunctions exist, but no declaration proves the source’s concrete underlying-set comparison: induced representations do not agree with induced G-sets while coinduced representations do agree with coinduced G-sets.
`FC03-C06-U020`	unmatched source definition	`unmatched`	partial: `Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean::RightExtension.IsPointwiseRightKanExtension`; `RightExtension.IsPointwiseRightKanExtensionAt`	N	Mathlib takes the comma-limit criterion as the pointwise-right definition. No pinned/current declaration proves equivalence with Riehl’s defining condition of preservation by every representable `E(e,-)`, so the source definition itself is not matched.
`FC03-C06-U021`	unmatched source definition	`unmatched`	partial: `Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean::LeftExtension.IsPointwiseLeftKanExtension`; `LeftExtension.IsPointwiseLeftKanExtensionAt`	N	Mathlib takes the comma-colimit criterion as the pointwise-left definition. No pinned/current declaration proves equivalence with Riehl’s representable-based dual definition.
`FC03-C06-U022`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean::LeftExtension.IsPointwiseLeftKanExtensionAt`; `LeftExtension.IsPointwiseLeftKanExtensionAt.isoColimit`; `RightExtension.IsPointwiseRightKanExtensionAt`; `RightExtension.IsPointwiseRightKanExtensionAt.isoLimit`	P	Mathlib’s pointwise predicate is exactly the comma-(co)limit condition and supplies the value isomorphisms, so it realizes the theorem’s formula characterization directly.
`FC03-C06-U023`	unmatched natural-isomorphism lemma	`unmatched`	partial: `Mathlib/CategoryTheory/Limits/Yoneda.lean::Limits.coneOfSectionCompYoneda`; `Limits.coneOfSectionCompCoyoneda`; generic comma/Kan infrastructure	N	The relevant Yoneda/cone ingredients exist, but no declaration was found for the specific natural isomorphism between cones over `F Π_d` and natural transformations `D(d,K-) ⟶ E(e,F-)` used in Lemma 6.3.8.
`FC03-C06-U024`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean::LeftExtension.IsPointwiseLeftKanExtension.isIso_hom`; `RightExtension.IsPointwiseRightKanExtension.isIso_hom`	P	Under `Full` and `Faithful` hypotheses on `K`, these instances make the pointwise left unit and right counit isomorphisms on restriction, exactly Corollary 6.3.9.
`FC03-C06-U025`	unmatched restriction-adjoint iff	`unmatched`	partial: `Mathlib/CategoryTheory/WithTerminal/Basic.lean::WithTerminal.incl`; `WithInitial.incl`; `WithTerminal.equivComma`; `WithInitial.equivComma`; generic Kan-extension adjunctions	N	Mathlib has the cone/cocone shape categories and generic Kan adjunctions, but no declaration packages the source iff: all `J`-colimits exactly when restriction from `J▹` has the stated left adjoint `colim`, with the dual limit assertion.
`FC03-C06-U026`	unmatched 2-of-6 definition	`unmatched`	partial: `Mathlib/AlgebraicTopology/ModelCategory/CategoryWithCofibrations.lean::HomotopicalAlgebra.CategoryWithWeakEquivalences`; `HomotopicalAlgebra.weakEquivalences`	N	Mathlib’s category-with-weak-equivalences structure stores an arbitrary morphism property; model-category axioms later impose 2-of-3, not Riehl’s defining 2-of-6 condition. No 2-of-6 interface was found at P or H.
`FC03-C06-U027`	unmatched 2-of-6 consequence	`unmatched`	partial: `Mathlib/CategoryTheory/MorphismProperty/Basic.lean::MorphismProperty.isomorphisms`	N	No pinned/current theorem states that identities plus 2-of-6 force all isomorphisms into the class, because the requisite 2-of-6 structure itself is absent.
`FC03-C06-U028`	unmatched homotopical-category interface	`unmatched`	partial: `Mathlib/AlgebraicTopology/ModelCategory/CategoryWithCofibrations.lean::HomotopicalAlgebra.CategoryWithWeakEquivalences`; `HomotopicalAlgebra.weakEquivalences`	N	Mathlib has a weaker carrier for a chosen weak-equivalence property, but not Riehl’s 2-of-6-based homotopical-category structure nor a source-shaped bundled notion of homotopical functor preserving it.
`FC03-C06-U029`	exact localization universal property	`mathlib`	`Mathlib/CategoryTheory/Localization/Predicate.lean::Functor.IsLocalization`; `Functor.IsLocalization.lift`; `Functor.IsLocalization.fac`	P	`IsLocalization` is precisely the universal property of a functor that inverts the chosen morphism class, matching the source characterization of `Ho C`.
`FC03-C06-U030`	exact minimal localization	`mathlib`	`Mathlib/CategoryTheory/Localization/Predicate.lean::Functor.IsLocalization.for_id`; instance `(𝟭 C).IsLocalization (MorphismProperty.isomorphisms C)`	P	The identity functor is explicitly a localization at the isomorphisms, exactly the minimal homotopical structure/localization example.
`FC03-C06-U031`	unmatched source homotopical-structure claim	`unmatched`	partial: `Mathlib/Algebra/Homology/Homotopy.lean::HomologicalComplex.homotopyEquivalences`; `Mathlib/Algebra/Homology/QuasiIso.lean::HomologicalComplex.quasiIso`; `homotopyEquivalences_le_quasiIso`	N	Both morphism classes are formalized and have multiplicativity/2-of-3 APIs, but no declaration gives the 2-of-6 structure required by Riehl’s preceding definition; thus the stated examples as homotopical categories are not source-shaped matches.
`FC03-C06-U032`	unmatched topological homotopy-category example	`unmatched`	—	N	No pinned/current declaration packages both homotopy-equivalence and weak-homotopy-equivalence structures on `Top`, nor the source equivalence of the weak-homotopy localization with CW complexes and homotopy classes.
`FC03-C06-U033`	exact match	`mathlib`	`Mathlib/CategoryTheory/Functor/Derived/LeftDerived.lean::Functor.IsLeftDerivedFunctor`; `Functor.totalLeftDerived`; `Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean::Functor.IsRightDerivedFunctor`; `Functor.totalRightDerived`	P	Mathlib explicitly defines total left derived functors as right Kan extensions along a localization and total right derived functors as left Kan extensions, with the same variance as the source.
`FC03-C06-U034`	unmatched point-set-derived definition	`unmatched`	partial: total-derived API in `Mathlib/CategoryTheory/Functor/Derived/`; derivability structures in `Mathlib/CategoryTheory/Localization/DerivabilityStructure/`	N	The library has total and pointwise Kan-derived constructions, but no Riehl-style definition of a homotopical point-set derived functor on the original category whose localization induces the total derived functor.
`FC03-C06-U035`	unmatched deformation definition	`unmatched`	partial: `Mathlib/CategoryTheory/Localization/DerivabilityStructure/OfFunctorialResolutions.lean`	N	Functorial-resolution derivability structures are present, but no declaration defines Riehl’s left/right deformation `(Q,q)` with a natural weak equivalence to/from the identity and the stated deformability subcategory condition.
`FC03-C06-U036`	unmatched deformation theorem	`unmatched`	partial: `Mathlib/CategoryTheory/Localization/DerivabilityStructure/OfFunctorialResolutions.lean`; total-derived API	N	Without the source deformation interface there is no declaration proving that `FQ` with `Fq` is the corresponding point-set left derived functor, or its right dual.
`FC03-C06-U037`	unmatched absoluteness theorem	`unmatched`	partial: `Mathlib/CategoryTheory/Functor/Derived/PointwiseLeftDerived.lean`; `PointwiseRightDerived.lean`	N	Mathlib develops pointwise derived functors through localization/Kan criteria, but no theorem states Riehl’s deformation consequence that the total derived functor of a left-deformable functor is an absolute right Kan extension and hence pointwise.
`FC03-C06-U038`	exact derived-adjunction theorem	`mathlib`	`Mathlib/CategoryTheory/Functor/Derived/Adjunction.lean::Adjunction.derived`; `Adjunction.derivedη`; `Adjunction.derivedε`	P	Under the absolute-derived hypotheses encoded in the file, Mathlib constructs exactly the adjunction between total derived functors and its unit/counit.
`FC03-C06-U039`	unmatched uniqueness strengthening	`unmatched`	partial: `Mathlib/CategoryTheory/Functor/Derived/Adjunction.lean::Adjunction.derived`; `Adjunction.derivedη_fac_app`; `Adjunction.derivedε_fac_app`	N	Mathlib proves the derived adjunction and compatibility factor equations, but no declaration proves Riehl’s stronger remark that this is the unique adjunction compatible with the localization maps.
`FC03-C06-U040`	unmatched specialized iff	`unmatched`	partial: `Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean::Functor.isColimitCoconeOfIsLeftKanExtension`; `Functor.isLimitConeOfIsRightKanExtension`; generic Kan universal properties	N	The library proves how colimits/limits transport across Kan extensions, but no declaration packages the exact specialization that Kan extension along the unique `C ⥤ 1` is equivalent to `colim F` (and dually `lim F`) whenever either exists.
`FC03-C06-U041`	exact bicategorical characterization	`mathlib`	`Mathlib/CategoryTheory/Bicategory/Kan/Adjunction.lean::Adjunction.isAbsoluteLeftKan`; `LeftExtension.IsAbsKan.adjunction`; `LeftExtension.isLeftAdjoint_TFAE`; `Adjunction.isAbsoluteLeftKanLift`; `LeftLift.IsAbsKan.adjunction`; `LeftLift.isRightAdjoint_TFAE`	P	Specialized to `Cat`, these declarations give both directions: an adjunction presents its right/left adjoint as the relevant absolute Kan extension/lift of the identity, and the preserved Kan data reconstructs the adjunction.
`FC03-C06-U042`	unmatched Yoneda equalizer formula	`unmatched`	partial: Yoneda and product/equalizer APIs in `Mathlib/CategoryTheory/Yoneda.lean` and `Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean`	N	No declaration was found for the source’s canonical equalizer presentation of `F c` by the two products over arrows and composable pairs. Generic Yoneda and limit infrastructure does not realize this formula.
`FC03-C06-U043`	unmatched coYoneda coequalizer formula	`unmatched`	partial: coYoneda and coproduct/coequalizer APIs	N	No declaration was found for the dual canonical coequalizer presentation of `F c` by the two coproducts over arrows and composable pairs.
`FC03-C06-U044`	exact density theorem	`mathlib`	`Mathlib/CategoryTheory/Limits/Presheaf.lean::Presheaf.colimitOfRepresentable`; `Functor.Elements.coconeπOpCompShrinkYonedaFlip`; `Functor.Elements.isColimitCoconeπOpCompShrinkYonedaFlip`	P	Mathlib explicitly exhibits every presheaf as a colimit of representables indexed by its category of elements and every covariant Type-valued functor as the dual colimit of corepresentables.
`FC03-C06-U045`	exact existence theorem	`mathlib`	`Mathlib/CategoryTheory/Limits/Presheaf.lean::Presheaf.uliftYonedaAdjunction`; `Presheaf.uniqueExtensionAlongULiftYoneda`; generic `Functor.HasPointwiseLeftKanExtensionAt` inference under `HasColimitsOfSize`	P	For a small-domain functor into a cocomplete locally small target, the Yoneda left Kan extension exists pointwise; Mathlib constructs its adjunction and proves uniqueness, with universe lifts implementing the source size assumptions.
`FC03-C06-U046`	unmatched codensity-monad construction	`unmatched`	partial: generic `Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean::Functor.rightKanExtension`	N	Generic self-right-Kan extensions exist as functorial data when assumed, but no pinned/current declaration constructs the associated monad or names/identifies it as the codensity monad.
`FC03-C06-U047`	unmatched field-inclusion density example	`unmatched`	—	N	No Lean declaration was found for the inclusion `Field ⥤ CRing` carrying the source density/codensity-monad construction, nor for the full source example as stated.
`FC03-C06-U048`	unmatched ultrafilter codensity theorem	`unmatched`	partial: ultrafilter APIs in Mathlib; generic Kan-extension API	N	Mathlib formalizes ultrafilters, but no pinned/current or usable external declaration identifies the ultrafilter monad as the codensity monad of `Fin ⥤ Set` or proves the displayed limit characterization.
`FC03-C06-U049`	unmatched Giry codensity theorem	`unmatched`	partial: probability/Giry-style measure infrastructure from C05; generic Kan-extension API	N	No pinned/current or usable external declaration identifies the Giry monad, or the finitely-additive variant from finite powers of the interval, as the codensity monad of the source subcategory.

Provenance contract for the Epilogue

Project search: LeanCategories/** outside .lake/.agents/.git was searched first for symmetric-monoidal coherence, chain-complex braidings, interval/bipointed-space coalgebras, Grothendieck topoi/Giraud, and the abelian/exact-functor material below. No project-owned Epilogue route was found.
Pinned Mathlib: project pin db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0, Lean v4.33.0), denoted P, was checked declaration-wise. It already contains the symmetric-monoidal interface, the monoidal tensor totalization on homological complexes, sheafification as a left-exact reflection, the three Giraud-condition definitions in U009, the abelian-category interfaces, exact-functor equivalence, and Freyd–Mitchell.
Current/open Mathlib: upstream 810b3888d0aa94294b18587c453466bc86c1f0fc (Apache-2.0, Lean v4.34.0-rc2) was rechecked 2026-09-06. It still has no general symmetric Mac Lane–Kelly coherence theorem, no SymmetricCategory instance on HomologicalComplex/ChainComplex/CochainComplex, no topological bipointed interval terminal-coalgebra theorem, and no bundled Grothendieck-topos definition/Giraud characterization. Targeted open-PR searches found no exact owner of those gaps.
External search: TauCetiProject/TauCeti@e846d4b2028f14e1688a1ac4d0636510b6e98273 (Apache-2.0; current main rechecked 2026-09-06; Lean v4.34.0-rc2 / Mathlib 5fcc6656691ed31965746c369f41fa75e567ac9d) supplies the Koszul braiding and TauCeti.koszulSymmetricCategory on unbounded cochain complexes of modules, closing the missing complex-level symmetric structure only at an incompatible revision and therefore yielding a reference-port route for U002. Moonweave-AI/cantilune@784459c03ae766b4cf6596c8e1a7f32e3cbf65e0 was rechecked at its current main; its free-SMC quotient/universal-property development does not prove the full formal-diagram completeness statement of U003. jwiegley/category-theory@c490e6343af2038ea4fd387e3e0ab6a2dfdc6316 was rechecked at its current master; its independently verified Riehl E.2–E.4 coverage records the symmetric-coherence, interval/bipointed terminal-coalgebra, Grothendieck-topos equivalence, and Giraud theorem as absent/partial for the same declaration-level reasons. Broad GitHub/Reservoir/source-atlas searches found no later complete Lean owners.
N denotes dated 2026-09-06 negative evidence after project-first search, pinned/current Mathlib, relevant open work, source-atlas repositories, Reservoir/GitHub, and Loogle/LeanSearch as feasible. Generic ingredients are not promoted to source matches unless a declaration realizes the bundled source statement.

Epilogue — Further Topics

FC03 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
`FC03-CE-U001`	exact definition	`mathlib`	`Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean::SymmetricCategory`; `BraidedCategory`; `Mathlib/CategoryTheory/Monoidal/Category.lean::MonoidalCategory`	P	The bundled tensor/unit/associator/unitors and braiding/symmetry laws give exactly Riehl’s symmetric-monoidal data and coherence axioms; forgetting the braiding leaves the monoidal notion.
`FC03-CE-U002`	exact pinned examples plus incompatible complex completion	`reference-port`	P: `Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean::CartesianMonoidalCategory.ofHasFiniteProducts`; `CartesianMonoidalCategory.toSymmetricCategory`; `Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean::symmetricOfHasFiniteCoproducts`; `Algebra/Category/ModuleCat/Monoidal/Symmetric.lean::ModuleCat.symmetricCategory`; `Mathlib/Algebra/Homology/Monoidal.lean`; R: `TauCeti/Algebra/Homology/Monoidal/Braiding.lean::TauCeti.koszulSymmetricCategory` at `TauCetiProject/TauCeti@e846d4b2028f14e1688a1ac4d0636510b6e98273`	R	Products/coproducts and both module monoidal structures are pinned; pinned Mathlib also constructs the graded tensor totalization on homological complexes but no compatible braiding. TauCeti supplies the missing Koszul symmetric structure for unbounded cochain complexes, but only on Lean v4.34.0-rc2 / Mathlib `5fcc665…`, so the complete source example is a revision-specific reference port rather than pinned Mathlib.
`FC03-CE-U003`	unmatched symmetric coherence metatheorem	`unmatched`	partial: `Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean` ordinary monoidal coherence; Cantilune free-SMC infrastructure at `784459c03ae766b4cf6596c8e1a7f32e3cbf65e0`	N	Pinned/current Mathlib proves ordinary monoidal coherence but no theorem that every formal diagram using associators, unitors, and symmetries commutes. The current external free-SMC development provides syntax/quotient/universal properties but no completeness/unique-structural-map theorem matching Riehl E.2.2.
`FC03-CE-U004`	unmatched interval-wedge construction	`unmatched`	partial: `Mathlib/Topology/Category/TopCat/Monoidal.lean::TopCat.I`; `Mathlib/Topology/Homotopy/TopCat/Path.lean::TopCat.Path`; `Mathlib/Topology/Path.lean::Path.trans`	N	The unit interval and path concatenation are formalized, but no declaration identifies concatenation with a bipointed homeomorphism `I ≅ I ∨ I` followed by `p ∨ q` as in the source construction.
`FC03-CE-U005`	unmatched topological bipointed category	`unmatched`	partial: `Mathlib/CategoryTheory/Category/TwoP.lean::TwoP`; `Mathlib/CategoryTheory/Category/Bipointed.lean::Bipointed`	N	Mathlib has categories of two-pointed/bipointed types, including distinct points in `TwoP`, but no category of spaces with two distinct closed endpoints and the source wedge gluing operation.
`FC03-CE-U006`	unmatched Freyd–Leinster theorem	`unmatched`	partial: `Mathlib/CategoryTheory/Endofunctor/Algebra.lean::Endofunctor.Coalgebra`; `Endofunctor.Coalgebra.Terminal.str_isIso`	N	Generic endofunctor coalgebras and terminal-coalgebra theory exist, but no endofunctor `X ↦ X ∨ X` on the required bipointed spaces and no theorem that `(I,0,1)` is its terminal coalgebra was found.
`FC03-CE-U007`	unmatched Grothendieck-topos equivalence	`unmatched`	partial: `Mathlib/CategoryTheory/Sites/Sheafification.lean::GrothendieckTopology.sheafificationAdjunction`; reflective sheaf inclusion; `Mathlib/CategoryTheory/Sites/LeftExact.lean::GrothendieckTopology.preservesFiniteLimits_sheafification`	N	Pinned Mathlib proves that sheaves on a site form a left-exact reflective subcategory of presheaves, but has no bundled general Grothendieck-topos predicate and no equivalence between arbitrary left-exact reflective presheaf subcategories and sheaf categories on small sites.
`FC03-CE-U008`	unmatched Giraud characterization	`unmatched`	partial: finite-limit, disjoint-coproduct, universal-colimit, effective-equivalence-relation, and separating-object APIs	N	The individual condition interfaces largely exist, but neither P nor H nor searched external Lean work proves the stated iff characterization. Current `DisjointCoproduct.lean` still lists the infinitary/small version needed for Giraud as TODO.
`FC03-CE-U009`	exact definitions	`mathlib`	`Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean::CoproductDisjoint`; `Mathlib/CategoryTheory/Limits/VanKampen.lean::IsUniversalColimit`; `Mathlib/CategoryTheory/EquivalenceRelation.lean::EffectiveEquivalenceRelation`	P	These are exactly pairwise-initial pullbacks with monic coprojections, pullback-stable colimits, and internal equivalence relations realized as kernel pairs.
`FC03-CE-U010`	exact equivalent definition	`mathlib`	`Mathlib/CategoryTheory/Abelian/NonPreadditive.lean::NonPreadditiveAbelian`	P	The class assumes a zero object, kernels, cokernels, finite products/coproducts, and normal monos/epis, exactly Riehl’s non-preadditive axiom list; Mathlib then canonically recovers the preadditive structure.
`FC03-CE-U011`	exact structural consequences	`mathlib`	`Mathlib/CategoryTheory/Abelian/Basic.lean::Abelian.hasFiniteBiproducts`; `Mathlib/CategoryTheory/Abelian/NonPreadditive.lean::NonPreadditiveAbelian.preadditive`	P	Finite products and coproducts are biproducts/direct sums, while the recovered preadditive structure makes every hom-set an abelian group and composition bilinear.
`FC03-CE-U012`	exact image/exactness formulation	`mathlib`	`Mathlib/CategoryTheory/Abelian/Images.lean::Abelian.image`; `Abelian.coimage`; `Mathlib/CategoryTheory/Abelian/Basic.lean::Abelian.coimageIsoImage`; `Mathlib/CategoryTheory/Abelian/Exact.lean::ShortComplex.exact_iff_image_eq_kernel`	P	`image f = ker(coker f)`, `coimage f = coker(ker f)`, the canonical coimage-to-image map is an isomorphism in an abelian category, and exactness is equality of image and kernel subobjects.
`FC03-CE-U013`	exact iff	`mathlib`	`Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean::Functor.exact_tfae`; `Mathlib/CategoryTheory/Limits/ExactFunctor.lean::LeftExactFunctor`; `RightExactFunctor`	P	`exact_tfae` explicitly equates preservation of short exact sequences, preservation of all exact sequences, `PreservesHomology`, and simultaneous `PreservesFiniteLimits` plus `PreservesFiniteColimits`, exactly the source equivalence of exact with left-and-right exact.
`FC03-CE-U014`	exact theorem	`mathlib`	`Mathlib/CategoryTheory/Abelian/FreydMitchell.lean::Abelian.freyd_mitchell`; `FreydMitchell.functor`	P	Already at the project pin: for any small abelian category Mathlib constructs a ring and a full faithful functor to its module category preserving finite limits and colimits, hence exact.