adjunction.cppm File Reference

Adjoint functors (the Free / Forgetful axis). More...

#include <concepts>
#include <functional>
#include <type_traits>
#include <utility>
import dedekind.category:logic;

Include dependency graph for adjunction.cppm:

Classes
struct	dedekind::category::adjunction_witness< Left, Right, Unit, Counit >
	Typed unit/counit data for an adjunction witness. More...
struct	dedekind::category::is_adjoint< F, G, Op >
	The adjunction law \(f(x) \le y \iff x \le g(y)\) as an opt-in leaf fact, with the one theorem derived here: a monotone isomorphism is adjoint to its inverse ( \(f(x) \le y \iff x \le f^{-1}(y)\), both legs monotone). Other adjunctions register their fact where their theorem is stated (Δ ⊣ ∧ per glb in :cartesian_bicategory, S ⊣ P on the saturating ℤ in numbers:integer, the antitone involution's self-adjunction in algebra:ordered_algebra). More...

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::HasAdjunctionShape
	Structural shape: F and U have the categorical signature of an adjoint pair F ⊣ U — F : 𝒟 → 𝒞 (left, free) and U : 𝒞 → 𝒟 (right, forgetful).
concept	dedekind::category::IsFreeFunctor
	Directional alias: F is the left adjoint of an adjunction F ⊣ U. Names the free direction — F sends an object d : 𝒟 to its free construction F(d) : 𝒞 (the universal recipient under U).
concept	dedekind::category::IsForgetfulFunctor
	Directional alias: U is the right adjoint of an adjunction F ⊣ U. Names the forgetful direction — U drops the structure that distinguishes 𝒞 from 𝒟 (e.g., U_Ring→Rig forgets that you can do −).
concept	dedekind::category::IsUnitOfAdjunction
	Structural shape: η is the unit of an adjunction F ⊣ U — a natural transformation id_𝒟 ⇒ U ∘ F.
concept	dedekind::category::IsCounitOfAdjunction
	Structural shape: ε is the counit of an adjunction F ⊣ U — a natural transformation F ∘ U ⇒ id_𝒞. Dual of IsUnitOfAdjunction.
concept	dedekind::category::IsAdjunction
	A typed unit/counit witness relating a left and right functor.
concept	dedekind::category::IsCovariantFunctor
	A covariant functor between posetal categories: an order-PRESERVING arrow. This is IsMonotone read categorically (a monotone map is a functor of posets that preserves the direction of composition), the documented covariant pole of functor variance (#908).
concept	dedekind::category::IsContravariantFunctor
	A contravariant functor between posetal categories: an order-REVERSING arrow (IsAntiMonotone read categorically). The contravariant pole; inhabited by the negation NegationArrow ¬ and any Compose that mixes one covariant with one contravariant leg.
concept	dedekind::category::IsVariantFunctor
	A functor between posetal categories with a definite variance: covariant or contravariant. This is the "@c IsFunctor parametrized with @c IsVariant" umbrella whose poles are IsCovariantFunctor and IsContravariantFunctor, and exactly the leg-shape a Galois connection's adjoints must share (matched variance, below).
concept	dedekind::category::IsOrderEmbedding
	An order-preserving embedding: a monic, order-preserving arrow of one ordered set into another. Such an embedding is a covariant functor between the two posetal categories, so IsCovariantFunctor is a conjunct — the classification is derived from the two legs (IsEmbeddingFunctor && IsMonotone), not re-declared per carrier (#908).
concept	dedekind::category::IsGaloisConnection
	Structural shape: F and G form a Galois connection F ⊣ G in a posetal setting — the simplest adjunction. Both are monotone arrows; F : P → Q and G : Q → P with the source/target carriers crossed (so F's Codomain matches G's Domain and vice versa). The universal-property test, for monotone legs
concept	dedekind::category::IsClosureOperator
	Structural shape: C is a closure operator on a poset P — an arrow C : P → P that is idempotent (C(C(x)) = C(x)), monotone (x ≤ y ⇒ C(x) ≤ C(y)), and extensive (x ≤ C(x)) for all x.

Functions
template<typename Left, typename Right, typename Unit, typename Counit> requires IsAdjunction<std::remove_cvref_t<Left>, std::remove_cvref_t<Right>, std::remove_cvref_t<Unit>, std::remove_cvref_t<Counit>>
constexpr auto	dedekind::category::make_adjunction (Left left, Right right, Unit unit, Counit counit)
	Factory for adjunction witnesses.

Variables
template<typename F, typename G, typename Op = std::less_equal<>>
constexpr bool	dedekind::category::is_adjoint_v = is_adjoint<F, G, Op>::value
template<typename F, typename G, typename Op>
constexpr bool	dedekind::category::is_adjoint_v< F, G, Op > = true

Detailed Description

Adjoint functors (the Free / Forgetful axis).

@partition :adjunction

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

adjunction__Adjunctions

An adjunction F ⊣ U is a pair of functors F : 𝒟 → 𝒞 (the free / left adjoint) and U : 𝒞 → 𝒟 (the forgetful / right adjoint), with a natural isomorphism Hom_𝒞(F(d), c) ≅ Hom_𝒟(d, U(c)) between the two hom-sets. Equivalently: a unit η : id_𝒟 ⇒ U ∘ F and a counit ε : F ∘ U ⇒ id_𝒞 satisfying the triangle identities (Mac Lane Ch. IV; Pierce gives adjunctions their own section because the structure recurs everywhere a free construction does).

adjunction__In_this_codebase

Concrete carrier-side instances:

• F : Rig → Ring (the Grothendieck construction): SignedCardinality = F(Cardinality), Cardinality = U(SignedCardinality).
• F : IntegralDomain → Field (the field of fractions): Rational<Z> = F(Z) for Z = SignedExtensionalCardinal<>.
• F : OrderedField → CompleteOrderedField (the Cauchy completion): Real = F(Rational).
• F : Field → AlgebraicallyClosedField (the algebraic closure): Complex = F(Real).

Each step in the carrier lattice ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ is a free construction in its respective category. The closure-forcing operators (-Cardinality → SignedCardinality, etc.) are the unit's components made operational at the operator level — see docs/design/carrier-lattice.md.

adjunction__Two_concept_tiers

The partition exposes two conceptually distinct surfaces:

• HasAdjunctionShape<F, U> — structural-only 2-parameter form. Names just the categorical signatures of the adjoint pair; the unit / counit are unspecified. Used in the directional aliases IsFreeFunctor / IsForgetfulFunctor where the directional reading is what's load-bearing.

• IsAdjunction<Left, Right, Unit, Counit> — stronger 4-parameter witness form. Requires explicit unit and counit arrows and exercises the typed triangle-identity surface. Used where the actual unit / counit components are concretely available (e.g. for monad-style derivations).

The split mirrors a recurring project pattern: the 2-param shape concept (cheap, deducible) anchors the textbook vocabulary and gates downstream uses; the n-param witness concept binds the operational evidence.

Note

"Adjoint functors arise everywhere." — Saunders Mac Lane, Categories for the Working Mathematician (1971), as quoted in Benjamin C. Pierce, Basic Category Theory for Computer Scientists (1991), §2.6.