Framing is exactly existence of companions and conjoints

Open

QAlgorithms.Papers.Independent.Intakethird100.P60.framed_iff_companions_and_conjoints

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

prove2quantum

Let $\mathbb D$ be a pseudo double category. A companion and a conjoint mean the typed cells and both vertical and horizontal identities of Definition A.1, with the horizontal identities interpreted using the specified unitors. Then

\mathbb D\text{ is a framed bicategory} \quad\Longleftrightarrow\quad \forall(f:A\to B),\ f\text{ has both a companion and a conjoint}.

Framing means that the joint frame functor $(L,R)$ is a fibration; its cartesian cells have the full factorization property over arbitrary further base arrows. All object and morphism universes are fixed independently, so categories may be large.

This is the companion/conjoint form of the framing criterion.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P60

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P60

open CategoryTheory

universe u v w x

/-- Theorem A.2 (PDF p. 72): both kinds of lift are required. -/
theorem framed_iff_companions_and_conjoints {V : Type u} [Category.{v} V]
    (D : DoubleData.{u,v,w,x} V) (hD : DoubleCoherence D) :
    IsFramed D ↔ HasCompanions D ∧ HasConjoints D := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P60

Source

Framed bicategories and monoidal fibrations, arXiv:0706.1286v2, PDF p. 72, Theorem A.2: Framing iff companions and conjoints

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 and $C_{f,g}(M,N)$ for squares, where $M\in H(A,B)$ , $N\in H(C,E)$ , $f:A\to C$ , and $g:B\to E$ . Write $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$ . Write $\alpha_{M,N,P}:(MN)P\to M(NP)$ , its specified reverse $\bar\alpha_{M,N,P}$ , and $\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$ for the specified squares with identity vertical boundaries. Assume the supplied coherence proof: 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$ means 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$ . The theorem asserts that the following condition holds if and only if both subsequent existence conditions hold: for every $A,B,C,E$ , $f:A\to C$ , $g:B\to E$ , and $N\in H(C,E)$ , there exist $M\in H(A,B)$ and $a\in C_{f,g}(M,N)$ such that, for every $P,Q$ , $h:P\to A$ , $k:Q\to B$ , $T\in H(P,Q)$ , and $b\in C_{f\circ h,g\circ k}(T,N)$ , there exists exactly one $c\in C_{h,k}(T,M)$ satisfying $c;a=b$ . The first existence condition is that for every $A,B$ and $f:A\to B$ , there exist $M\in H(A,B)$ and squares

u\in C_{1_A,f}(U_A,M),\qquad e\in C_{f,1_B}(M,U_B)

with proofs of

u;e\doteq U_f,\qquad (\bar\lambda_M;(u\otimes e));\rho_M=1_M.

The second existence condition is that for every $A,B$ and $f:A\to B$ , there exist $N\in H(B,A)$ and squares

u\in C_{f,1_A}(U_A,N),\qquad e\in C_{1_B,f}(N,U_B)

with proofs of

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

All morphisms, including identities, are included. The category may be empty, making these object-indexed conditions vacuous; likewise, a test square type with no $b$ contributes no requirement to the unique-factorization condition.

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