Framing: three equivalent characterizations

Open

QAlgorithms.Papers.Independent.Intakethird100.P60.framing_three_characterizations

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

prove2quantum

Let $\mathbb D$ be a pseudo double category, with strict vertical category $\mathbb D_0$ , weak horizontal composition $\odot$ , and specified coherent globular associators and unitors. Let $L,R$ send a horizontal arrow or square to its left and right frame. Then

(L,R)\text{ is a fibration}\quad\Longleftrightarrow\quad (L,R)\text{ is an opfibration}\quad\Longleftrightarrow\quad \text{every vertical arrow has both a companion and a conjoint}.

For a vertical arrow $f:A\to B$ , a companion is $M:A\rightsquigarrow B$ with cells $u:U_A\Rightarrow M$ over $(1_A,f)$ and $c:M\Rightarrow U_B$ over $(f,1_B)$ . A conjoint is $N:B\rightsquigarrow A$ with cells $v:U_A\Rightarrow N$ over $(f,1_A)$ and $d:N\Rightarrow U_B$ over $(1_B,f)$ . Their vertical composites equal $U_f$ . Their horizontal composites, conjugated by the indicated unitors, are the identity cells of $M$ and $N$ . The lifting properties quantify over every pair of further frame arrows and require unique factorization.

This characterizes nonalgebraic framing by typed companion and conjoint data, including all equations (4.3)–(4.4).

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 4.1 (PDF p. 15): all three conditions, with both vertical and
horizontal identities included in the companion and conjoint data. -/
theorem framing_three_characterizations {V : Type u} [Category.{v} V]
    (D : DoubleData.{u,v,w,x} V) (hD : DoubleCoherence D) :
    (IsFrameFibration D ↔ IsFrameOpfibration D) ∧
    (IsFrameFibration D ↔ HasCompanions D ∧ HasConjoints D) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P60

Source

Framed bicategories and monoidal fibrations, arXiv:0706.1286v2, PDF p. 15, Theorem 4.1: Three equivalent characterizations of framing

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 square types, 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)$ , $\bar\alpha_{M,N,P}:M(NP)\to(MN)P$ , $\lambda_M:U_AM\to M$ , $\bar\lambda_M:M\to U_AM$ , $\rho_M:MU_B\to M$ , and $\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 objects, morphisms, horizontal arrows, and squares,

\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$ , and $c:P\to S$ have matching adjoining vertical boundaries; in unit naturality, $a:M\to N$ has boundaries $f,g$ . Define the following four conditions locally. Condition $F$ says that 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$ . Condition $O$ says that for every $A,B,C,E$ , $f:A\to C$ , $g:B\to E$ , and $M\in H(A,B)$ , there exist $N\in H(C,E)$ and $a\in C_{f,g}(M,N)$ such that, for every $P,Q$ , $h:C\to P$ , $k:E\to Q$ , $T\in H(P,Q)$ , and $b\in C_{h\circ f,k\circ g}(M,T)$ , there exists exactly one $c\in C_{h,k}(N,T)$ satisfying $a;c=b$ . Condition $C$ says 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)$ , $e\in C_{f,1_B}(M,U_B)$ , with proofs that $u;e\doteq U_f$ and $(\bar\lambda_M;(u\otimes e));\rho_M=1_M$ . Condition $J$ says 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)$ , $e\in C_{1_B,f}(N,U_B)$ , with proofs that $u;e\doteq U_f$ and $(\bar\rho_N;(e\otimes u));\lambda_N=1_N$ . The theorem asserts

(F\iff O)\ \land\ \bigl(F\iff(C\land J)\bigr).

All quantified morphisms include identities, and $V$ may be empty. In either unique-factorization condition, a test square type containing no $b$ contributes no requirement; whenever a test square $b$ exists, its stated factor must exist uniquely.

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