diagciso

Description: The diagonal functor is an isomorphism from a category C to the category of functors from a terminal category to C .

It is provable that the inverse of the diagonal functor is the mapped object by the transposed curry of ( D evalF C ) , i.e., U. ran ( 1st( <. D , Q >. curryF ( ( D evalF C ) o.func ( D swapF Q ) ) ) ) .

	Ref	Expression
Hypotheses	diagffth.c	$⊢ φ \to C \in Cat$
	diagffth.d	No typesetting found for \|- ( ph -> D e. TermCat ) with typecode \|-
	diagffth.q	$⊢ Q = D FuncCat C$
	diagciso.e	$⊢ E = CatCat (U)$
	diagciso.u	$⊢ φ \to U \in V$
	diagciso.c	$⊢ φ \to C \in U$
	diagciso.1	$⊢ φ \to Q \in U$
	diagciso.i	$⊢ I = Iso (E)$
	diagciso.l	$⊢ L = C Δ_{func} D$
Assertion	diagciso	$⊢ φ \to L \in (C I Q)$

Proof

Step	Hyp	Ref	Expression
1		diagffth.c	$⊢ φ \to C \in Cat$
2		diagffth.d	Could not format ( ph -> D e. TermCat ) : No typesetting found for \|- ( ph -> D e. TermCat ) with typecode \|-
3		diagffth.q	$⊢ Q = D FuncCat C$
4		diagciso.e	$⊢ E = CatCat (U)$
5		diagciso.u	$⊢ φ \to U \in V$
6		diagciso.c	$⊢ φ \to C \in U$
7		diagciso.1	$⊢ φ \to Q \in U$
8		diagciso.i	$⊢ I = Iso (E)$
9		diagciso.l	$⊢ L = C Δ_{func} D$
10	1 2 3 9	diagffth	$⊢ φ \to L \in ((C Full Q) \cap (C Faith Q))$
11		eqid	$⊢ {Base}_{C} = {Base}_{C}$
12	11 2 1 9	diag1f1o	$⊢ φ \to 1^{st} (L) : {Base}_{C} \underset{1-1 onto}{⟶} D Func C$
13		eqid	$⊢ {Base}_{E} = {Base}_{E}$
14	3	fucbas	$⊢ D Func C = {Base}_{Q}$
15	6 1	elind	$⊢ φ \to C \in (U \cap Cat)$
16	4 13 5	catcbas	$⊢ φ \to {Base}_{E} = U \cap Cat$
17	15 16	eleqtrrd	$⊢ φ \to C \in {Base}_{E}$
18	2	termccd	$⊢ φ \to D \in Cat$
19	3 18 1	fuccat	$⊢ φ \to Q \in Cat$
20	7 19	elind	$⊢ φ \to Q \in (U \cap Cat)$
21	20 16	eleqtrrd	$⊢ φ \to Q \in {Base}_{E}$
22	4 13 11 14 5 17 21 8	catciso	$⊢ φ \to (L \in (C I Q) \leftrightarrow (L \in ((C Full Q) \cap (C Faith Q)) \land 1^{st} (L) : {Base}_{C} \underset{1-1 onto}{⟶} D Func C))$
23	10 12 22	mpbir2and	$⊢ φ \to L \in (C I Q)$

Metamath Proof Explorer

Theorem diagciso

Proof