Theorem mgcval

Description: Monotone Galois connection between two functions F and G . If this relation is satisfied, F is called the lower adjoint of G , and G is called the upper adjoint of F .

Technically, this is implemented as an operation taking a pair of structures V and W , expected to be posets, which gives a relation between pairs of functions F and G .

If such a relation exists, it can be proven to be unique.

Galois connections generalize the fundamental theorem of Galois theory about the correspondence between subgroups and subfields. (Contributed by Thierry Arnoux, 23-Apr-2024)

	Ref	Expression
Hypotheses	mgcoval.1	$$⊢A={\mathrm{Base}}_V$$
	mgcoval.2	$$⊢B={\mathrm{Base}}_W$$
	mgcoval.3	$$⊢\underset{\dot{}}{\le }={\le }_V$$
	mgcoval.4	No typesetting found for |- .c_ = ( le ` W ) with typecode |-
	mgcval.1	No typesetting found for |- H = ( V MGalConn W ) with typecode |-
	mgcval.2	$$⊢\phi \to V\in \mathrm{Proset}$$
	mgcval.3	$$⊢\phi \to W\in \mathrm{Proset}$$
Assertion	mgcval	Could not format assertion : No typesetting found for |- ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mgcoval.1	$$⊢A={\mathrm{Base}}_V$$
2		mgcoval.2	$$⊢B={\mathrm{Base}}_W$$
3		mgcoval.3	$$⊢\underset{\dot{}}{\le }={\le }_V$$
4		mgcoval.4	Could not format .c_ = ( le ` W ) : No typesetting found for |- .c_ = ( le ` W ) with typecode |-
5		mgcval.1	Could not format H = ( V MGalConn W ) : No typesetting found for |- H = ( V MGalConn W ) with typecode |-
6		mgcval.2	$$⊢\phi \to V\in \mathrm{Proset}$$
7		mgcval.3	$$⊢\phi \to W\in \mathrm{Proset}$$
8	1 2 3 4	mgcoval	Could not format ( ( V e. Proset /\ W e. Proset ) -> ( V MGalConn W ) = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) : No typesetting found for |- ( ( V e. Proset /\ W e. Proset ) -> ( V MGalConn W ) = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) with typecode |-
9	6 7 8	syl2anc	Could not format ( ph -> ( V MGalConn W ) = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) : No typesetting found for |- ( ph -> ( V MGalConn W ) = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) with typecode |-
10	5 9	syl5eq	Could not format ( ph -> H = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) : No typesetting found for |- ( ph -> H = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) with typecode |-
11	10	breqd	Could not format ( ph -> ( F H G <-> F { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } G ) ) : No typesetting found for |- ( ph -> ( F H G <-> F { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } G ) ) with typecode |-
12		fveq1	$$⊢f=F\to f\left(x\right)=F\left(x\right)$$
13	12	adantr	$$⊢\left(f=F\wedge g=G\right)\to f\left(x\right)=F\left(x\right)$$
14	13	breq1d	Could not format ( ( f = F /\ g = G ) -> ( ( f ` x ) .c_ y <-> ( F ` x ) .c_ y ) ) : No typesetting found for |- ( ( f = F /\ g = G ) -> ( ( f ` x ) .c_ y <-> ( F ` x ) .c_ y ) ) with typecode |-
15		fveq1	$$⊢g=G\to g\left(y\right)=G\left(y\right)$$
16	15	adantl	$$⊢\left(f=F\wedge g=G\right)\to g\left(y\right)=G\left(y\right)$$
17	16	breq2d	$$⊢\left(f=F\wedge g=G\right)\to \left(x\underset{\dot{}}{\le }g\left(y\right)\leftrightarrow x\underset{\dot{}}{\le }G\left(y\right)\right)$$
18	14 17	bibi12d	Could not format ( ( f = F /\ g = G ) -> ( ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) <-> ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) : No typesetting found for |- ( ( f = F /\ g = G ) -> ( ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) <-> ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) with typecode |-
19	18	2ralbidv	Could not format ( ( f = F /\ g = G ) -> ( A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) <-> A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) : No typesetting found for |- ( ( f = F /\ g = G ) -> ( A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) <-> A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) with typecode |-
20		eqid	Could not format { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } : No typesetting found for |- { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } with typecode |-
21	19 20	brab2a	Could not format ( F { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } G <-> ( ( F e. ( B ^m A ) /\ G e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) : No typesetting found for |- ( F { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } G <-> ( ( F e. ( B ^m A ) /\ G e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) with typecode |-
22	2	fvexi	$$⊢B\in \mathrm{V}$$
23	1	fvexi	$$⊢A\in \mathrm{V}$$
24	22 23	elmap	$$⊢F\in \left(B^A\right)\leftrightarrow F:A⟶B$$
25	23 22	elmap	$$⊢G\in \left(A^B\right)\leftrightarrow G:B⟶A$$
26	24 25	anbi12i	$$⊢\left(F\in \left(B^A\right)\wedge G\in \left(A^B\right)\right)\leftrightarrow \left(F:A⟶B\wedge G:B⟶A\right)$$
27	26	anbi1i	Could not format ( ( ( F e. ( B ^m A ) /\ G e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) <-> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) : No typesetting found for |- ( ( ( F e. ( B ^m A ) /\ G e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) <-> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) with typecode |-
28	21 27	bitr2i	Could not format ( ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) <-> F { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } G ) : No typesetting found for |- ( ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) <-> F { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } G ) with typecode |-
29	11 28	bitr4di	Could not format ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) ) : No typesetting found for |- ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) ) with typecode |-