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 | ||
mgcoval.2 | |||
mgcoval.3 | |||
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 | |||
mgcval.3 | |||
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 |- |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mgcoval.1 | ||
2 | mgcoval.2 | ||
3 | mgcoval.3 | ||
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 | ||
7 | mgcval.3 | ||
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 | ||
13 | 12 | adantr | |
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 | ||
16 | 15 | adantl | |
17 | 16 | breq2d | |
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 | |
23 | 1 | fvexi | |
24 | 22 23 | elmap | |
25 | 23 22 | elmap | |
26 | 24 25 | anbi12i | |
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 |- |