Doctrinal Adjunction Skill

"An adjunction between T-algebras is precisely a lax T-morphism structure on the right adjoint, equivalently a colax T-morphism structure on the left adjoint." — G.M. Kelly (1974)

Trit: 0 (ERGODIC - coordinator) Color: #26D826 (Green) Status: Production Ready

Overview

A doctrinal adjunction is Kelly's 1974 theorem establishing a canonical bijection between:

• Lax T-morphism structures on a right adjoint u : B → A
• Colax T-morphism structures on the left adjoint f : A → B

Given a 2-monad T on a 2-category K, and an adjunction f ⊣ u in K, the mate correspondence lifts the adjunction to the world of T-algebras in a canonical way.

Mathematical Definition

Given:
  T = (T, η, μ)  a 2-monad on K
  (A, a) and (B, b)  strict T-algebras
  f ⊣ u : B → A  adjunction in K
  η_adj : 1 → uf   (unit)
  ε_adj : fu → 1   (counit)

Theorem (Kelly 1974):
  There is a bijection between:

  (i)  Lax T-morphism structures on u:
       ū : Tb ∘ Tu → u ∘ Ta   (lax cell)
       satisfying unit and associativity axioms

  (ii) Colax T-morphism structures on f:
       f̄ : f ∘ Ta → Tb ∘ Tf   (colax cell)
       satisfying unit and associativity axioms

  given by the mate correspondence:

       ū ↦ f̄ = (Tb ∘ Tε) ∘ (Tb ∘ T(ū) ∘ Tf) ∘ (Tη ∘ Tf)
       f̄ ↦ ū = (u ∘ Tε) ∘ (u ∘ T(f̄) ∘ Tu) ∘ (Tη ∘ Tu)

The Mate Correspondence

The key mechanism is the mate correspondence for 2-cells under adjunctions:

Given f ⊣ u with unit η and counit ε:

  ┌─────────────────────────────────────────────────┐
  │                                                 │
  │   2-cells  α : gf → h     (in left variable)   │
  │            ↕  bijection                         │
  │   2-cells  ᾱ : g → hu     (in right variable)  │
  │                                                 │
  │   α ↦ ᾱ = (hε) ∘ (αu) ∘ (gη)                   │
  │   ᾱ ↦ α = (hε) ∘ (ᾱf)                          │
  │                                                 │
  └─────────────────────────────────────────────────┘

Applied to the T-algebra structure cells, this produces the lax↔colax bijection.

GF(3) Mapping

The doctrinal adjunction is the coordinator that mediates between lax and colax — hence trit 0.

Why This Skill Was Missing

The concept of doctrinal adjunction was fragmented across existing skills:

1. synthetic-adjunctions

   handles adjunctions but not the T-algebra lifting

2. 2-monad

   defines the strictness grid but doesn't own the adjunction-lifting mechanism

3. bidirectional-lens-logic

   captures covariant/contravariant duality but not the specific Kelly bijection

4. open-games

   uses play/coplay (≈ lax/colax) but doesn't formalize the mate correspondence

Gap: No skill owned the canonical bijection between lax and colax T-morphism structures via mates, which is the mechanism that connects the GF(3) validator (-1, colax) to the generator (+1, lax) through the coordinator (0, mate).

Julia/Catlab Integration

using Catlab.CategoricalAlgebra

@present SchDoctrinalAdj(FreeSchema) begin
    Algebra::Ob
    Adjunction::Ob
    LaxCell::Ob
    ColaxCell::Ob

    adj_left::Hom(Adjunction, Algebra)     # f : A → B
    adj_right::Hom(Adjunction, Algebra)    # u : B → A
    lax_source::Hom(LaxCell, Adjunction)
    colax_source::Hom(ColaxCell, Adjunction)

    # Mate correspondence as morphism
    mate_lax_to_colax::Hom(LaxCell, ColaxCell)
    mate_colax_to_lax::Hom(ColaxCell, LaxCell)

    Strictness::AttrType
    lax_strictness::Attr(LaxCell, Strictness)    # always +1
    colax_strictness::Attr(ColaxCell, Strictness) # always -1
end

Canonical Examples

Bidirectional Neighbor Index

Edge-Scoped Propagator Table

scope:compose

scope:change

scope:compose

scope:change

scope:verify

scope:compose

scope:change

scope:verify

scope:compose

scope:change

scope:compose

scope:change

scope:verify

scope:verify

scope:compose

scope:change

scope:compose

scope:change

scope:verify

scope:verify

Mutual Awareness Summary

      synthetic-adj (+1)
            ↑ change
            │
kan-ext (0) ←── DOCTRINAL-ADJ (0) ──→ 2-monad (0)
            │           │
            ↓ compose   ↓ change
    open-games (0)   bidirectional (0)

+ 6 additional edges to existing skills

Total edges: 20 (10 bidirectional pairs) Propagator balance: 6 scope:change + 8 scope:compose + 6 scope:verify = balanced

GF(3) Triads

codescent (-1) ⊗ doctrinal-adjunction (0) ⊗ flexible-algebra (+1) = 0 ✓  [BKP Lifting]
sheaf-cohomology (-1) ⊗ doctrinal-adjunction (0) ⊗ synthetic-adjunctions (+1) = 0 ✓  [Adjunction-Monad]
linear-logic (-1) ⊗ doctrinal-adjunction (0) ⊗ free-monad-gen (+1) = 0 ✓  [Resource-Adjunction]
segal-types (-1) ⊗ doctrinal-adjunction (0) ⊗ operad-compose (+1) = 0 ✓  [Operadic-Lifting]
covariant-fibrations (-1) ⊗ doctrinal-adjunction (0) ⊗ discopy-operads (+1) = 0 ✓  [Fibered-Lifting]

Commands

just doctrinal-lift f u T          # Lift adjunction f ⊣ u through T
just doctrinal-mate lax-cell       # Compute mate of lax cell → colax cell
just doctrinal-verify adj T        # Verify doctrinal adjunction conditions
just doctrinal-examples T          # List known doctrinal adjunctions for T

References

• Kelly, G.M. (1974). "Doctrinal adjunction." LNM 420:257-280
• Blackwell, Kelly & Power (1989). "Two-dimensional monad theory." JPAA 59:1-41
• Lack, S. (2010). "A 2-categories companion." IMA Vol. Math. Appl. 152:105-191
• Kelly, G.M. & Street, R. (1974). "Review of the elements of 2-categories." LNM 420:75-103

SDF Interleaving

Primary Chapter: 5. Evaluation

Concepts: eval, apply, interpreter, environment

GF(3) Balanced Triad

doctrinal-adjunction (0) + SDF.Ch5 (0) + [balancer] (0) = 0

Skill Trit: 0 (ERGODIC - coordination)

Connection Pattern

Evaluation interprets expressions. Doctrinal adjunction interprets T-algebra structure through the mate correspondence, transporting between lax (evaluation) and colax (co-evaluation) modes.