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 | ⊢ 𝐴 = ( Base ‘ 𝑉 ) | |
| mgcoval.2 | ⊢ 𝐵 = ( Base ‘ 𝑊 ) | ||
| mgcoval.3 | ⊢ ≤ = ( le ‘ 𝑉 ) | ||
| mgcoval.4 | ⊢ ≲ = ( le ‘ 𝑊 ) | ||
| mgcval.1 | ⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 ) | ||
| mgcval.2 | ⊢ ( 𝜑 → 𝑉 ∈ Proset ) | ||
| mgcval.3 | ⊢ ( 𝜑 → 𝑊 ∈ Proset ) | ||
| Assertion | mgcval | ⊢ ( 𝜑 → ( 𝐹 𝐻 𝐺 ↔ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mgcoval.1 | ⊢ 𝐴 = ( Base ‘ 𝑉 ) | |
| 2 | mgcoval.2 | ⊢ 𝐵 = ( Base ‘ 𝑊 ) | |
| 3 | mgcoval.3 | ⊢ ≤ = ( le ‘ 𝑉 ) | |
| 4 | mgcoval.4 | ⊢ ≲ = ( le ‘ 𝑊 ) | |
| 5 | mgcval.1 | ⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 ) | |
| 6 | mgcval.2 | ⊢ ( 𝜑 → 𝑉 ∈ Proset ) | |
| 7 | mgcval.3 | ⊢ ( 𝜑 → 𝑊 ∈ Proset ) | |
| 8 | 1 2 3 4 | mgcoval | ⊢ ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) → ( 𝑉 MGalConn 𝑊 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝑔 ‘ 𝑦 ) ) ) } ) |
| 9 | 6 7 8 | syl2anc | ⊢ ( 𝜑 → ( 𝑉 MGalConn 𝑊 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝑔 ‘ 𝑦 ) ) ) } ) |
| 10 | 5 9 | eqtrid | ⊢ ( 𝜑 → 𝐻 = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝑔 ‘ 𝑦 ) ) ) } ) |
| 11 | 10 | breqd | ⊢ ( 𝜑 → ( 𝐹 𝐻 𝐺 ↔ 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝑔 ‘ 𝑦 ) ) ) } 𝐺 ) ) |
| 12 | fveq1 | ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) | |
| 13 | 12 | adantr | ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) |
| 14 | 13 | breq1d | ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ‘ 𝑥 ) ≲ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ) ) |
| 15 | fveq1 | ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) | |
| 16 | 15 | adantl | ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑔 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) |
| 17 | 16 | breq2d | ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑥 ≤ ( 𝑔 ‘ 𝑦 ) ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ) |
| 18 | 14 17 | bibi12d | ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑓 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝑔 ‘ 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ) ) |
| 19 | 18 | 2ralbidv | ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝑔 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ) ) |
| 20 | eqid | ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝑔 ‘ 𝑦 ) ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝑔 ‘ 𝑦 ) ) ) } | |
| 21 | 19 20 | brab2a | ⊢ ( 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝑔 ‘ 𝑦 ) ) ) } 𝐺 ↔ ( ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐴 ↑m 𝐵 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ) ) |
| 22 | 2 | fvexi | ⊢ 𝐵 ∈ V |
| 23 | 1 | fvexi | ⊢ 𝐴 ∈ V |
| 24 | 22 23 | elmap | ⊢ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ↔ 𝐹 : 𝐴 ⟶ 𝐵 ) |
| 25 | 23 22 | elmap | ⊢ ( 𝐺 ∈ ( 𝐴 ↑m 𝐵 ) ↔ 𝐺 : 𝐵 ⟶ 𝐴 ) |
| 26 | 24 25 | anbi12i | ⊢ ( ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐴 ↑m 𝐵 ) ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ) |
| 27 | 26 | anbi1i | ⊢ ( ( ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐴 ↑m 𝐵 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ) ↔ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ) ) |
| 28 | 21 27 | bitr2i | ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ) ↔ 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝑔 ‘ 𝑦 ) ) ) } 𝐺 ) |
| 29 | 11 28 | bitr4di | ⊢ ( 𝜑 → ( 𝐹 𝐻 𝐺 ↔ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ) ) ) |