yoneda

Description: The Yoneda Lemma. There is a natural isomorphism between the functors Z and E , where Z ( F , X ) is the natural transformations from Yon ( X ) = Hom ( - , X ) to F , and E ( F , X ) = F ( X ) is the evaluation functor. Here we need two universes to state the claim: the smaller universe U is used for forming the functor category Q = C ^op -> SetCat ( U ) , which itself does not (necessarily) live in U but instead is an element of the larger universe V . (If U is a Grothendieck universe, then it will be closed under this "presheaf" operation, and so we can set U = V in this case.) (Contributed by Mario Carneiro, 29-Jan-2017)

	Ref	Expression
Hypotheses	yoneda.y	$⊢ Y = Yon (C)$
	yoneda.b	$⊢ B = {Base}_{C}$
	yoneda.1	$⊢ \underset{˙}{1} = Id (C)$
	yoneda.o	$⊢ O = oppCat (C)$
	yoneda.s	$⊢ S = SetCat (U)$
	yoneda.t	$⊢ T = SetCat (V)$
	yoneda.q	$⊢ Q = O FuncCat S$
	yoneda.h	$⊢ H = {Hom}_{F} (Q)$
	yoneda.r	$⊢ R = (Q \times_{c} O) FuncCat T$
	yoneda.e	$⊢ E = O {eval}_{F} S$
	yoneda.z	$⊢ Z = H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))$
	yoneda.c	$⊢ φ \to C \in Cat$
	yoneda.w	$⊢ φ \to V \in W$
	yoneda.u	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq U$
	yoneda.v	$⊢ φ \to ran {Hom}_{𝑓} (Q) \cup U \subseteq V$
	yoneda.m	$⊢ M = (f \in (O Func S), x \in B ⟼ (a \in (1^{st} (Y) (x) (O Nat S) f) ⟼ a (x) (\underset{˙}{1} (x))))$
	yoneda.i	$⊢ I = Iso (R)$
Assertion	yoneda	$⊢ φ \to M \in (Z I E)$

Proof

Step	Hyp	Ref	Expression
1		yoneda.y	$⊢ Y = Yon (C)$
2		yoneda.b	$⊢ B = {Base}_{C}$
3		yoneda.1	$⊢ \underset{˙}{1} = Id (C)$
4		yoneda.o	$⊢ O = oppCat (C)$
5		yoneda.s	$⊢ S = SetCat (U)$
6		yoneda.t	$⊢ T = SetCat (V)$
7		yoneda.q	$⊢ Q = O FuncCat S$
8		yoneda.h	$⊢ H = {Hom}_{F} (Q)$
9		yoneda.r	$⊢ R = (Q \times_{c} O) FuncCat T$
10		yoneda.e	$⊢ E = O {eval}_{F} S$
11		yoneda.z	$⊢ Z = H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))$
12		yoneda.c	$⊢ φ \to C \in Cat$
13		yoneda.w	$⊢ φ \to V \in W$
14		yoneda.u	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq U$
15		yoneda.v	$⊢ φ \to ran {Hom}_{𝑓} (Q) \cup U \subseteq V$
16		yoneda.m	$⊢ M = (f \in (O Func S), x \in B ⟼ (a \in (1^{st} (Y) (x) (O Nat S) f) ⟼ a (x) (\underset{˙}{1} (x))))$
17		yoneda.i	$⊢ I = Iso (R)$
18	9	fucbas	$⊢ (Q \times_{c} O) Func T = {Base}_{R}$
19		eqid	$⊢ Inv (R) = Inv (R)$
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	yonedalem1	$⊢ φ \to (Z \in ((Q \times_{c} O) Func T) \land E \in ((Q \times_{c} O) Func T))$
21	20	simpld	$⊢ φ \to Z \in ((Q \times_{c} O) Func T)$
22		funcrcl	$⊢ Z \in ((Q \times_{c} O) Func T) \to (Q \times_{c} O \in Cat \land T \in Cat)$
23	21 22	syl	$⊢ φ \to (Q \times_{c} O \in Cat \land T \in Cat)$
24	23	simpld	$⊢ φ \to Q \times_{c} O \in Cat$
25	23	simprd	$⊢ φ \to T \in Cat$
26	9 24 25	fuccat	$⊢ φ \to R \in Cat$
27	20	simprd	$⊢ φ \to E \in ((Q \times_{c} O) Func T)$
28		eqid	$⊢ (f \in (O Func S), x \in B ⟼ (u \in 1^{st} (f) (x) ⟼ (y \in B ⟼ (g \in (y Hom (C) x) ⟼ (x 2^{nd} (f) y) (g) (u))))) = (f \in (O Func S), x \in B ⟼ (u \in 1^{st} (f) (x) ⟼ (y \in B ⟼ (g \in (y Hom (C) x) ⟼ (x 2^{nd} (f) y) (g) (u)))))$
29	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 19 28	yonedainv	$⊢ φ \to M (Z Inv (R) E) (f \in (O Func S), x \in B ⟼ (u \in 1^{st} (f) (x) ⟼ (y \in B ⟼ (g \in (y Hom (C) x) ⟼ (x 2^{nd} (f) y) (g) (u)))))$
30	18 19 26 21 27 17 29	inviso1	$⊢ φ \to M \in (Z I E)$

Metamath Proof Explorer

Theorem yoneda

Proof