Base change objects form a canonical dual pair

Open

QAlgorithms.Papers.Independent.Intakethird100.P60.base_change_dual_pair

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $\mathbb D$ be a framed bicategory and $f:A\to B$ a vertical arrow. Companion and conjoint objects $M=fB:A\rightsquigarrow B$ and $N=B_f:B\rightsquigarrow A$ exist. For every choice of their defining cells $u,c,v,d$ as in Theorem 4.1, set

\eta:U_A\xrightarrow{\lambda^{-1}}U_A\odot U_A \xrightarrow{u\odot v}M\odot N, \qquad \varepsilon:N\odot M\xrightarrow{d\odot c}U_B\odot U_B \xrightarrow{\lambda}U_B.

These maps satisfy both triangle identities, with the associator and unitors of $\mathbb D$ . Thus $(M,N)$ is a dual pair, with $M$ the left adjoint and $N$ the right adjoint under diagrammatic composition.

The explicit maps make the duality canonical relative to the chosen base change cells.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P60

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P60

open CategoryTheory

universe u v w x

/-- Proposition 5.3 (PDF pp. 20–21): the chosen companion and conjoint form
a dual pair with the displayed canonical evaluation and coevaluation. -/
theorem base_change_dual_pair {V : Type u} [Category.{v} V]
    (D : DoubleData.{u,v,w,x} V) (hD : DoubleCoherence D) (hFramed : IsFramed D)
    {A B : V} (f : A ⟶ B) :
    (∃ (M : D.H A B) (N : D.H B A),
      Nonempty (Companion D f M) ∧ Nonempty (Conjoint D f N)) ∧
    (∀ (M : D.H A B) (N : D.H B A) (c : Companion D f M) (j : Conjoint D f N),
      IsDualPair D M N (baseCoevaluation D c j) (baseEvaluation D c j)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P60

Source

Framed bicategories and monoidal fibrations, arXiv:0706.1286v2, PDF p. 20, Proposition 5.3: Base change objects form dual pairs

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $V$ be any category and $D$ any of the specified double data, with arbitrary universe sizes. Write $H(A,B)$ for horizontal-arrow types, $C_{f,g}(M,N)$ for square types with vertical boundaries $f,g$ , $U_A$ for horizontal units, $MN$ for horizontal products, $1_M$ for identity squares, $U_f$ for squares on horizontal units, $s;t$ for vertical composition in that order, and $s\otimes t$ for horizontal square composition; for identity-boundary squares, simplify composites of identity morphisms in $s;t$ . The specified identity-boundary squares are $\alpha_{M,N,P}:(MN)P\to M(NP)$ , its specified reverse $\bar\alpha_{M,N,P}$ , and the unit squares $\lambda_M:U_AM\to M$ , $\bar\lambda_M:M\to U_AM$ , $\rho_M:MU_B\to M$ , $\bar\rho_M:M\to MU_B$ . Assume the supplied coherence proof, meaning that universally over all well-typed configurations,

\begin{gathered} (a;b);c\doteq a;(b;c),\qquad 1_M;a\doteq a,\qquad a;1_N\doteq a,\\ U_{1_A}=1_{U_A},\qquad U_{g\circ f}=U_f;U_g,\qquad 1_M\otimes1_N=1_{MN},\\ (a\otimes b);(c\otimes d)=(a;c)\otimes(b;d),\\ \alpha_{M,N,P};\bar\alpha_{M,N,P}=1_{(MN)P},\qquad \bar\alpha_{M,N,P};\alpha_{M,N,P}=1_{M(NP)},\\ \lambda_M;\bar\lambda_M=1_{U_AM},\qquad \bar\lambda_M;\lambda_M=1_M,\qquad \rho_M;\bar\rho_M=1_{MU_B},\qquad \bar\rho_M;\rho_M=1_M,\\ ((a\otimes b)\otimes c);\alpha_{Q,R,S} \doteq\alpha_{M,N,P};(a\otimes(b\otimes c)),\\ (U_f\otimes a);\lambda_N\doteq\lambda_M;a,\qquad (a\otimes U_g);\rho_N\doteq\rho_M;a,\\ \bigl((\alpha_{M,N,P}\otimes1_Q);\alpha_{M,NP,Q}\bigr); (1_M\otimes\alpha_{N,P,Q}) =\alpha_{MN,P,Q};\alpha_{M,N,PQ},\\ \alpha_{M,U_B,N};(1_M\otimes\lambda_N) =\rho_M\otimes1_N. \end{gathered}

Here $\doteq$ is heterogeneous equality; in associativity naturality, $a:M\to Q$ , $b:N\to R$ , $c:P\to S$ have matching adjoining vertical boundaries, and in unit naturality $a:M\to N$ has boundaries $f,g$ . Also assume the following framing condition: for every $A_0,B_0,C_0,E_0$ , $p:A_0\to C_0$ , $q:B_0\to E_0$ , and $L\in H(C_0,E_0)$ , there exist $K\in H(A_0,B_0)$ and $a\in C_{p,q}(K,L)$ such that, for every $P,Q$ , $h:P\to A_0$ , $k:Q\to B_0$ , $T\in H(P,Q)$ , and $b\in C_{p\circ h,q\circ k}(T,L)$ , there exists exactly one $d\in C_{h,k}(T,K)$ with $d;a=b$ . A test type with no such $b$ imposes no factorization requirement. For any objects $A,B$ and any morphism $f:A\to B$ , including an identity, the theorem asserts a conjunction of two claims. First, there exist $M\in H(A,B)$ and $N\in H(B,A)$ for which both of the following structures are inhabited: a structure $c$ with squares $u_c\in C_{1_A,f}(U_A,M)$ , $e_c\in C_{f,1_B}(M,U_B)$ satisfying

u_c;e_c\doteq U_f,\qquad (\bar\lambda_M;(u_c\otimes e_c));\rho_M=1_M,

and a structure $j$ with squares $u_j\in C_{f,1_A}(U_A,N)$ , $e_j\in C_{1_B,f}(N,U_B)$ satisfying

u_j;e_j\doteq U_f,\qquad (\bar\rho_N;(e_j\otimes u_j));\lambda_N=1_N.

Second, for every $M\in H(A,B)$ , every $N\in H(B,A)$ , and every such supplied structures $c,j$ , set

\eta=\bar\lambda_{U_A};(u_c\otimes u_j) \in C_{1_A,1_A}(U_A,MN), \qquad \varepsilon=(e_j\otimes e_c);\lambda_{U_B} \in C_{1_B,1_B}(NM,U_B).

Then both equalities hold:

\begin{aligned} \Bigl(\Bigl(\bigl(\bar\lambda_M;(\eta\otimes1_M)\bigr); \alpha_{M,N,M}\Bigr);(1_M\otimes\varepsilon)\Bigr);\rho_M &=1_M,\\ \Bigl(\Bigl(\bigl(\bar\rho_N;(1_N\otimes\eta)\bigr); \bar\alpha_{N,M,N}\Bigr);(\varepsilon\otimes1_N)\Bigr);\lambda_N &=1_N. \end{aligned}

The universal second claim ranges over all choices of the structures, while the first claim asserts that appropriate choices exist for the given $f$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph