Theorem cofidfth

Description: If " F is a section of G " in a category of small categories (in a universe), then F is faithful. Combined with cofidf1 , this theorem proves that F is an embedding (a faithful functor injective on objects, remark 3.28(1) of Adamek p. 34). (Contributed by Zhi Wang, 15-Nov-2025)

	Ref	Expression
Hypotheses	cofidfth.i	$$⊢I={id}_{\mathrm{func}}\left(D\right)$$
	cofidfth.f	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
	cofidfth.k	$$⊢\phi \to K\left(E\mathrm{Func}D\right)L$$
	cofidfth.o	$$⊢\phi \to ⟨K,L⟩{\circ }_{\mathrm{func}}⟨F,G⟩=I$$
Assertion	cofidfth	$$⊢\phi \to F\left(D\mathrm{Faith}E\right)G$$

Proof

Step	Hyp	Ref	Expression
1		cofidfth.i	$$⊢I={id}_{\mathrm{func}}\left(D\right)$$
2		cofidfth.f	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
3		cofidfth.k	$$⊢\phi \to K\left(E\mathrm{Func}D\right)L$$
4		cofidfth.o	$$⊢\phi \to ⟨K,L⟩{\circ }_{\mathrm{func}}⟨F,G⟩=I$$
5		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
6	2	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_D\wedge y\in {\mathrm{Base}}_D\right)\right)\to F\left(D\mathrm{Func}E\right)G$$
7	3	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_D\wedge y\in {\mathrm{Base}}_D\right)\right)\to K\left(E\mathrm{Func}D\right)L$$
8	4	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_D\wedge y\in {\mathrm{Base}}_D\right)\right)\to ⟨K,L⟩{\circ }_{\mathrm{func}}⟨F,G⟩=I$$
9		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
10		eqid	$$⊢\mathrm{Hom}\left(E\right)=\mathrm{Hom}\left(E\right)$$
11		simprl	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_D\wedge y\in {\mathrm{Base}}_D\right)\right)\to x\in {\mathrm{Base}}_D$$
12		simprr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_D\wedge y\in {\mathrm{Base}}_D\right)\right)\to y\in {\mathrm{Base}}_D$$
13	1 5 6 7 8 9 10 11 12	cofidf2	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_D\wedge y\in {\mathrm{Base}}_D\right)\right)\to \left(\left(xGy\right):x\mathrm{Hom}\left(D\right)y\underset{1-1}{⟶}F\left(x\right)\mathrm{Hom}\left(E\right)F\left(y\right)\wedge \left(F\left(x\right)LF\left(y\right)\right):F\left(x\right)\mathrm{Hom}\left(E\right)F\left(y\right)\underset{onto}{⟶}x\mathrm{Hom}\left(D\right)y\right)$$
14	13	simpld	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_D\wedge y\in {\mathrm{Base}}_D\right)\right)\to \left(xGy\right):x\mathrm{Hom}\left(D\right)y\underset{1-1}{⟶}F\left(x\right)\mathrm{Hom}\left(E\right)F\left(y\right)$$
15	14	ralrimivva	$$⊢\phi \to \forall x\in {\mathrm{Base}}_D\forall y\in {\mathrm{Base}}_D\left(xGy\right):x\mathrm{Hom}\left(D\right)y\underset{1-1}{⟶}F\left(x\right)\mathrm{Hom}\left(E\right)F\left(y\right)$$
16	5 9 10	isfth2	$$⊢F\left(D\mathrm{Faith}E\right)G\leftrightarrow \left(F\left(D\mathrm{Func}E\right)G\wedge \forall x\in {\mathrm{Base}}_D\forall y\in {\mathrm{Base}}_D\left(xGy\right):x\mathrm{Hom}\left(D\right)y\underset{1-1}{⟶}F\left(x\right)\mathrm{Hom}\left(E\right)F\left(y\right)\right)$$
17	2 15 16	sylanbrc	$$⊢\phi \to F\left(D\mathrm{Faith}E\right)G$$