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 = ( Base ` V )
	mgcoval.2	|- B = ( Base ` W )
	mgcoval.3	|- .<_ = ( le ` V )
	mgcoval.4	|- .c_ = ( le ` W )
	mgcval.1	|- H = ( V MGalConn W )
	mgcval.2	|- ( ph -> V e. Proset )
	mgcval.3	|- ( ph -> W e. Proset )
Assertion	mgcval	|- ( 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 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mgcoval.1	|- A = ( Base ` V )
2		mgcoval.2	|- B = ( Base ` W )
3		mgcoval.3	|- .<_ = ( le ` V )
4		mgcoval.4	|- .c_ = ( le ` W )
5		mgcval.1	|- H = ( V MGalConn W )
6		mgcval.2	|- ( ph -> V e. Proset )
7		mgcval.3	|- ( ph -> W e. Proset )
8	1 2 3 4	mgcoval	|- ( ( 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 ) ) ) } )
9	6 7 8	syl2anc	|- ( 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 ) ) ) } )
10	5 9	syl5eq	|- ( 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 ) ) ) } )
11	10	breqd	|- ( 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 ) )
12		fveq1	|- ( f = F -> ( f ` x ) = ( F ` x ) )
13	12	adantr	|- ( ( f = F /\ g = G ) -> ( f ` x ) = ( F ` x ) )
14	13	breq1d	|- ( ( f = F /\ g = G ) -> ( ( f ` x ) .c_ y <-> ( F ` x ) .c_ y ) )
15		fveq1	|- ( g = G -> ( g ` y ) = ( G ` y ) )
16	15	adantl	|- ( ( f = F /\ g = G ) -> ( g ` y ) = ( G ` y ) )
17	16	breq2d	|- ( ( f = F /\ g = G ) -> ( x .<_ ( g ` y ) <-> x .<_ ( G ` y ) ) )
18	14 17	bibi12d	|- ( ( f = F /\ g = G ) -> ( ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) <-> ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) )
19	18	2ralbidv	|- ( ( 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 ) ) ) )
20		eqid	|- { <. 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 ) ) ) }
21	19 20	brab2a	|- ( 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 ) ) ) )
22	2	fvexi	|- B e. _V
23	1	fvexi	|- A e. _V
24	22 23	elmap	|- ( F e. ( B ^m A ) <-> F : A --> B )
25	23 22	elmap	|- ( G e. ( A ^m B ) <-> G : B --> A )
26	24 25	anbi12i	|- ( ( F e. ( B ^m A ) /\ G e. ( A ^m B ) ) <-> ( F : A --> B /\ G : B --> A ) )
27	26	anbi1i	|- ( ( ( 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 ) ) ) )
28	21 27	bitr2i	|- ( ( ( 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 )
29	11 28	bitr4di	|- ( 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 ) ) ) ) )