# Galois connections between large posets

```agda
module order-theory.galois-connections-large-posets where
```

<details><summary>Imports</summary>

```agda
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.homotopies
open import foundation.logical-equivalences
open import foundation.universe-levels

open import order-theory.large-posets
open import order-theory.least-upper-bounds-large-posets
open import order-theory.order-preserving-maps-large-posets
open import order-theory.principal-lower-sets-large-posets
open import order-theory.principal-upper-sets-large-posets
open import order-theory.similarity-of-elements-large-posets
open import order-theory.similarity-of-order-preserving-maps-large-posets
```

</details>

## Idea

A **galois connection** between [large posets](order-theory.large-posets.md) `P`
and `Q` consists of
[order preserving maps](order-theory.order-preserving-maps-large-posets.md)
`f : hom-Large-Poset (λ l → l) P Q` and `hom-Large-Poset id Q P` such that the
adjoint relation

```text
  (f x ≤ y) ↔ (x ≤ g y)
```

holds for every two elements `x : P` and `y : Q`.

The following table lists the Galois connections that have been formalized in
the agda-unimath library

{{#include tables/galois-connections.md}}

## Definitions

### The adjoint relation between order preserving maps between large posets

```agda
module _
  {αP αQ γ δ : Level → Level} {βP βQ : Level → Level → Level}
  (P : Large-Poset αP βP) (Q : Large-Poset αQ βQ)
  (F : hom-Large-Poset γ P Q) (G : hom-Large-Poset δ Q P)
  where

  forward-implication-adjoint-relation-hom-Large-Poset : UUω
  forward-implication-adjoint-relation-hom-Large-Poset =
    {l1 l2 : Level}
    {x : type-Large-Poset P l1} {y : type-Large-Poset Q l2} →
    leq-Large-Poset Q (map-hom-Large-Poset P Q F x) y →
    leq-Large-Poset P x (map-hom-Large-Poset Q P G y)

  backward-implication-adjoint-relation-hom-Large-Poset : UUω
  backward-implication-adjoint-relation-hom-Large-Poset =
    {l1 l2 : Level}
    {x : type-Large-Poset P l1} {y : type-Large-Poset Q l2} →
    leq-Large-Poset P x (map-hom-Large-Poset Q P G y) →
    leq-Large-Poset Q (map-hom-Large-Poset P Q F x) y

  adjoint-relation-hom-Large-Poset : UUω
  adjoint-relation-hom-Large-Poset =
    {l1 l2 : Level}
    (x : type-Large-Poset P l1) (y : type-Large-Poset Q l2) →
    leq-Large-Poset Q (map-hom-Large-Poset P Q F x) y ↔
    leq-Large-Poset P x (map-hom-Large-Poset Q P G y)
```

### Galois connections between large posets

```agda
module _
  {αP αQ : Level → Level} {βP βQ : Level → Level → Level}
  (γ : Level → Level) (δ : Level → Level)
  (P : Large-Poset αP βP) (Q : Large-Poset αQ βQ)
  where

  record
    galois-connection-Large-Poset : UUω
    where
    constructor
      make-galois-connection-Large-Poset
    field
      lower-adjoint-galois-connection-Large-Poset :
        hom-Large-Poset γ P Q
      upper-adjoint-galois-connection-Large-Poset :
        hom-Large-Poset δ Q P
      adjoint-relation-galois-connection-Large-Poset :
        adjoint-relation-hom-Large-Poset P Q
          lower-adjoint-galois-connection-Large-Poset
          upper-adjoint-galois-connection-Large-Poset

  open galois-connection-Large-Poset public

module _
  {αP αQ : Level → Level} {βP βQ : Level → Level → Level}
  {γ : Level → Level} {δ : Level → Level}
  (P : Large-Poset αP βP) (Q : Large-Poset αQ βQ)
  (G : galois-connection-Large-Poset γ δ P Q)
  where

  map-lower-adjoint-galois-connection-Large-Poset :
    {l1 : Level} → type-Large-Poset P l1 → type-Large-Poset Q (γ l1)
  map-lower-adjoint-galois-connection-Large-Poset =
    map-hom-Large-Poset P Q
      ( lower-adjoint-galois-connection-Large-Poset G)

  preserves-order-lower-adjoint-galois-connection-Large-Poset :
    {l1 l2 : Level} (x : type-Large-Poset P l1) (y : type-Large-Poset P l2) →
    leq-Large-Poset P x y →
    leq-Large-Poset Q
      ( map-lower-adjoint-galois-connection-Large-Poset x)
      ( map-lower-adjoint-galois-connection-Large-Poset y)
  preserves-order-lower-adjoint-galois-connection-Large-Poset =
    preserves-order-hom-Large-Poset P Q
      ( lower-adjoint-galois-connection-Large-Poset G)

  map-upper-adjoint-galois-connection-Large-Poset :
    {l1 : Level} → type-Large-Poset Q l1 → type-Large-Poset P (δ l1)
  map-upper-adjoint-galois-connection-Large-Poset =
    map-hom-Large-Poset Q P
      ( upper-adjoint-galois-connection-Large-Poset G)

  preserves-order-upper-adjoint-galois-connection-Large-Poset :
    {l1 l2 : Level} (x : type-Large-Poset Q l1) (y : type-Large-Poset Q l2) →
    leq-Large-Poset Q x y →
    leq-Large-Poset P
      ( map-upper-adjoint-galois-connection-Large-Poset x)
      ( map-upper-adjoint-galois-connection-Large-Poset y)
  preserves-order-upper-adjoint-galois-connection-Large-Poset =
    preserves-order-hom-Large-Poset Q P
      ( upper-adjoint-galois-connection-Large-Poset G)

  forward-implication-adjoint-relation-galois-connection-Large-Poset :
    forward-implication-adjoint-relation-hom-Large-Poset P Q
      ( lower-adjoint-galois-connection-Large-Poset G)
      ( upper-adjoint-galois-connection-Large-Poset G)
  forward-implication-adjoint-relation-galois-connection-Large-Poset =
    forward-implication (adjoint-relation-galois-connection-Large-Poset G _ _)

  backward-implication-adjoint-relation-galois-connection-Large-Poset :
    backward-implication-adjoint-relation-hom-Large-Poset P Q
      ( lower-adjoint-galois-connection-Large-Poset G)
      ( upper-adjoint-galois-connection-Large-Poset G)
  backward-implication-adjoint-relation-galois-connection-Large-Poset =
    backward-implication (adjoint-relation-galois-connection-Large-Poset G _ _)
```

### Composition of Galois connections

```agda
module _
  {αP αQ αR : Level → Level} {βP βQ βR : Level → Level → Level}
  {γG γH : Level → Level} {δG δH : Level → Level}
  (P : Large-Poset αP βP)
  (Q : Large-Poset αQ βQ)
  (R : Large-Poset αR βR)
  (H : galois-connection-Large-Poset γH δH Q R)
  (G : galois-connection-Large-Poset γG δG P Q)
  where

  lower-adjoint-comp-galois-connection-Large-Poset :
    hom-Large-Poset (λ l → γH (γG l)) P R
  lower-adjoint-comp-galois-connection-Large-Poset =
    comp-hom-Large-Poset P Q R
      ( lower-adjoint-galois-connection-Large-Poset H)
      ( lower-adjoint-galois-connection-Large-Poset G)

  map-lower-adjoint-comp-galois-connection-Large-Poset :
    {l : Level} → type-Large-Poset P l → type-Large-Poset R (γH (γG l))
  map-lower-adjoint-comp-galois-connection-Large-Poset =
    map-comp-hom-Large-Poset P Q R
      ( lower-adjoint-galois-connection-Large-Poset H)
      ( lower-adjoint-galois-connection-Large-Poset G)

  preserves-order-lower-adjoint-comp-galois-connection-Large-Poset :
    preserves-order-map-Large-Poset P R
      map-lower-adjoint-comp-galois-connection-Large-Poset
  preserves-order-lower-adjoint-comp-galois-connection-Large-Poset =
    preserves-order-comp-hom-Large-Poset P Q R
      ( lower-adjoint-galois-connection-Large-Poset H)
      ( lower-adjoint-galois-connection-Large-Poset G)

  upper-adjoint-comp-galois-connection-Large-Poset :
    hom-Large-Poset (λ l → δG (δH l)) R P
  upper-adjoint-comp-galois-connection-Large-Poset =
    comp-hom-Large-Poset R Q P
      ( upper-adjoint-galois-connection-Large-Poset G)
      ( upper-adjoint-galois-connection-Large-Poset H)

  map-upper-adjoint-comp-galois-connection-Large-Poset :
    {l : Level} → type-Large-Poset R l → type-Large-Poset P (δG (δH l))
  map-upper-adjoint-comp-galois-connection-Large-Poset =
    map-comp-hom-Large-Poset R Q P
      ( upper-adjoint-galois-connection-Large-Poset G)
      ( upper-adjoint-galois-connection-Large-Poset H)

  preserves-order-upper-adjoint-comp-galois-connection-Large-Poset :
    preserves-order-map-Large-Poset R P
      map-upper-adjoint-comp-galois-connection-Large-Poset
  preserves-order-upper-adjoint-comp-galois-connection-Large-Poset =
    preserves-order-comp-hom-Large-Poset R Q P
      ( upper-adjoint-galois-connection-Large-Poset G)
      ( upper-adjoint-galois-connection-Large-Poset H)

  forward-implication-adjoint-relation-comp-galois-connection-Large-Poset :
    forward-implication-adjoint-relation-hom-Large-Poset P R
      lower-adjoint-comp-galois-connection-Large-Poset
      upper-adjoint-comp-galois-connection-Large-Poset
  forward-implication-adjoint-relation-comp-galois-connection-Large-Poset =
    forward-implication-adjoint-relation-galois-connection-Large-Poset P Q G ∘
    forward-implication-adjoint-relation-galois-connection-Large-Poset Q R H

  backward-implication-adjoint-relation-comp-galois-connection-Large-Poset :
    backward-implication-adjoint-relation-hom-Large-Poset P R
      lower-adjoint-comp-galois-connection-Large-Poset
      upper-adjoint-comp-galois-connection-Large-Poset
  backward-implication-adjoint-relation-comp-galois-connection-Large-Poset =
    backward-implication-adjoint-relation-galois-connection-Large-Poset Q R H ∘
    backward-implication-adjoint-relation-galois-connection-Large-Poset P Q G

  adjoint-relation-comp-galois-connection-Large-Poset :
    adjoint-relation-hom-Large-Poset P R
      lower-adjoint-comp-galois-connection-Large-Poset
      upper-adjoint-comp-galois-connection-Large-Poset
  pr1 (adjoint-relation-comp-galois-connection-Large-Poset x y) =
    forward-implication-adjoint-relation-comp-galois-connection-Large-Poset
  pr2 (adjoint-relation-comp-galois-connection-Large-Poset x y) =
    backward-implication-adjoint-relation-comp-galois-connection-Large-Poset

  comp-galois-connection-Large-Poset :
    galois-connection-Large-Poset (λ l → γH (γG l)) (λ l → δG (δH l)) P R
  lower-adjoint-galois-connection-Large-Poset
    comp-galois-connection-Large-Poset =
    lower-adjoint-comp-galois-connection-Large-Poset
  upper-adjoint-galois-connection-Large-Poset
    comp-galois-connection-Large-Poset =
    upper-adjoint-comp-galois-connection-Large-Poset
  adjoint-relation-galois-connection-Large-Poset
    comp-galois-connection-Large-Poset =
    adjoint-relation-comp-galois-connection-Large-Poset
```

### Homotopies of Galois connections

**Homotopies of Galois connections** are pointwise identifications between
either their lower adjoints or their upper adjoints. We will show below that
homotopies between lower adjoints induce homotopies between upper adjoints and
vice versa.

**Note:** We can only have homotopies between Galois connections with the same
universe level reindexing functions.

```agda
module _
  {αP αQ γ δ : Level → Level} {βP βQ : Level → Level → Level}
  (P : Large-Poset αP βP) (Q : Large-Poset αQ βQ)
  (G H : galois-connection-Large-Poset γ δ P Q)
  where

  lower-htpy-galois-connection-Large-Poset : UUω
  lower-htpy-galois-connection-Large-Poset =
    htpy-hom-Large-Poset P Q
      ( lower-adjoint-galois-connection-Large-Poset G)
      ( lower-adjoint-galois-connection-Large-Poset H)

  upper-htpy-galois-connection-Large-Poset : UUω
  upper-htpy-galois-connection-Large-Poset =
    htpy-hom-Large-Poset Q P
      ( upper-adjoint-galois-connection-Large-Poset G)
      ( upper-adjoint-galois-connection-Large-Poset H)
```

### Similarity of Galois connections

**Similarities of Galois connections** are pointwise
[similarities](order-theory.similarity-of-elements-large-posets.md) between
either their lower or their upper adjoints. We will show below that similarities
between lower adjoints induce similarities between upper adjoints and vice
versa.

**Note:** Since the notion of similarity applies to galois connections with not
necessarily the same universe level reindexing function, it is slightly more
flexible. For this reason, it may be easier to work with similarity of galois
connections.

```agda
module _
  {αP αQ γG γH δG δH : Level → Level} {βP βQ : Level → Level → Level}
  (P : Large-Poset αP βP) (Q : Large-Poset αQ βQ)
  (G : galois-connection-Large-Poset γG δG P Q)
  (H : galois-connection-Large-Poset γH δH P Q)
  where

  lower-sim-galois-connection-Large-Poset : UUω
  lower-sim-galois-connection-Large-Poset =
    sim-hom-Large-Poset P Q
      ( lower-adjoint-galois-connection-Large-Poset G)
      ( lower-adjoint-galois-connection-Large-Poset H)

  upper-sim-galois-connection-Large-Poset : UUω
  upper-sim-galois-connection-Large-Poset =
    sim-hom-Large-Poset Q P
      ( upper-adjoint-galois-connection-Large-Poset G)
      ( upper-adjoint-galois-connection-Large-Poset H)
```

### Lower universal objects of galois connections

Consider a Galois connection `G : P → Q` and an element `x : P`. An element
`x' : Q` is then said to satisfy the **lower universal property** with respect
to `x` if the logical equivalence

```text
  (x' ≤-Q y) ↔ (x ≤-P UG y)
```

holds for every element `y : Q`.

```agda
module _
  {αP αQ γ δ : Level → Level} {βP βQ : Level → Level → Level}
  (P : Large-Poset αP βP) (Q : Large-Poset αQ βQ)
  (G : galois-connection-Large-Poset γ δ P Q)
  {l1 l2 : Level} (x : type-Large-Poset P l1)
  (x' : type-Large-Poset Q l2)
  where

  is-lower-element-galois-connection-Large-Poset : UUω
  is-lower-element-galois-connection-Large-Poset =
    {l : Level} (y : type-Large-Poset Q l) →
    leq-Large-Poset Q x' y ↔
    leq-Large-Poset P x
      ( map-upper-adjoint-galois-connection-Large-Poset P Q G y)
```

### Upper universal objects of galois connections

Consider a Galois connection `G : P → Q` and an element `y : Q`. An element
`y' : P` is then said to satisfy the **upper universal property** with respect
to `y` if the logical equivalence

```text
  (LG x ≤-Q y) ↔ (x ≤-P y')
```

holds for every element `x : P`.

```agda
module _
  {αP αQ γ δ : Level → Level} {βP βQ : Level → Level → Level}
  (P : Large-Poset αP βP) (Q : Large-Poset αQ βQ)
  (G : galois-connection-Large-Poset γ δ P Q)
  {l1 l2 : Level} (y : type-Large-Poset Q l1)
  (y' : type-Large-Poset P l2)
  where

  is-upper-element-galois-connection-Large-Poset : UUω
  is-upper-element-galois-connection-Large-Poset =
    {l : Level} (x : type-Large-Poset P l) →
    leq-Large-Poset Q
      ( map-lower-adjoint-galois-connection-Large-Poset P Q G x)
      ( y) ↔
    leq-Large-Poset P x y'
```

## Properties

### A similarity between lower adjoints of a Galois connection induces a similarity between upper adjoints, and vice versa

**Proof:** Consider two Galois connections `LG ⊣ UG` and `LH ⊣ UH` between `P`
and `Q`, and suppose that `LG(x) ~ LH(x)` for all elements `x : P`. Then it
follows that

```text
  (x ≤ UG(y)) ↔ (LG(x) ≤ y) ↔ (LH(x) ≤ y) ↔ (x ≤ UH(y)).
```

Therefore it follows that `UG(y)` and `UH(y)` have the same lower sets, and
hence they must be equal.

```agda
module _
  {αP αQ γG γH δG δH : Level → Level} {βP βQ : Level → Level → Level}
  (P : Large-Poset αP βP) (Q : Large-Poset αQ βQ)
  (G : galois-connection-Large-Poset γG δG P Q)
  (H : galois-connection-Large-Poset γH δH P Q)
  where

  upper-sim-lower-sim-galois-connection-Large-Poset :
    lower-sim-galois-connection-Large-Poset P Q G H →
    upper-sim-galois-connection-Large-Poset P Q H G
  upper-sim-lower-sim-galois-connection-Large-Poset
    p x =
    sim-has-same-elements-principal-lower-set-element-Large-Poset P
      ( λ y →
        logical-equivalence-reasoning
          leq-Large-Poset P y
            ( map-upper-adjoint-galois-connection-Large-Poset P Q H x)
          ↔ leq-Large-Poset Q
              ( map-lower-adjoint-galois-connection-Large-Poset P Q H y)
              ( x)
            by inv-iff (adjoint-relation-galois-connection-Large-Poset H y x)
          ↔ leq-Large-Poset Q
              ( map-lower-adjoint-galois-connection-Large-Poset P Q G y)
              ( x)
            by
            inv-iff
              ( has-same-elements-principal-upper-set-element-sim-Large-Poset Q
                ( p y)
                ( x))
          ↔ leq-Large-Poset P y
              ( map-upper-adjoint-galois-connection-Large-Poset P Q G x)
            by adjoint-relation-galois-connection-Large-Poset G y x)

  lower-sim-upper-sim-galois-connection-Large-Poset :
    upper-sim-galois-connection-Large-Poset P Q H G →
    lower-sim-galois-connection-Large-Poset P Q G H
  lower-sim-upper-sim-galois-connection-Large-Poset
    p y =
    sim-has-same-elements-principal-upper-set-element-Large-Poset Q
      ( λ x →
        logical-equivalence-reasoning
          leq-Large-Poset Q
            ( map-lower-adjoint-galois-connection-Large-Poset P Q G y)
            ( x)
          ↔ leq-Large-Poset P y
              ( map-upper-adjoint-galois-connection-Large-Poset P Q G x)
            by adjoint-relation-galois-connection-Large-Poset G y x
          ↔ leq-Large-Poset P y
              ( map-upper-adjoint-galois-connection-Large-Poset P Q H x)
            by
            inv-iff
              ( has-same-elements-principal-lower-set-element-sim-Large-Poset P
                ( p x)
                ( y))
          ↔ leq-Large-Poset Q
              ( map-lower-adjoint-galois-connection-Large-Poset P Q H y)
              ( x)
            by inv-iff (adjoint-relation-galois-connection-Large-Poset H y x))
```

### A homotopy between lower adjoints of a Galois connection induces a homotopy between upper adjoints, and vice versa

**Proof:** Consider two Galois connections `LG ⊣ UG` and `LH ⊣ UH` between `P`
and `Q`, and suppose that `LG ~ LH`. Then there is a similarity `LG ≈ LH`, and
this induces a similarity `UG ≈ UH`. In other words, we obtain that

```text
  UG y ~ UH y
```

for any element `y : Q`. Since `UG y` and `UH y` are of the same universe level,
it follows that they are equal.

```agda
module _
  {αP αQ γ δ : Level → Level} {βP βQ : Level → Level → Level}
  (P : Large-Poset αP βP) (Q : Large-Poset αQ βQ)
  (G H : galois-connection-Large-Poset γ δ P Q)
  where

  upper-htpy-lower-htpy-galois-connection-Large-Poset :
    lower-htpy-galois-connection-Large-Poset P Q G H →
    upper-htpy-galois-connection-Large-Poset P Q G H
  upper-htpy-lower-htpy-galois-connection-Large-Poset p =
    htpy-sim-hom-Large-Poset Q P
      ( upper-adjoint-galois-connection-Large-Poset G)
      ( upper-adjoint-galois-connection-Large-Poset H)
      ( upper-sim-lower-sim-galois-connection-Large-Poset P Q H G
        ( sim-htpy-hom-Large-Poset P Q
          ( lower-adjoint-galois-connection-Large-Poset H)
          ( lower-adjoint-galois-connection-Large-Poset G)
          ( inv-htpy p)))

  lower-htpy-upper-htpy-galois-connection-Large-Poset :
    upper-htpy-galois-connection-Large-Poset P Q H G →
    lower-htpy-galois-connection-Large-Poset P Q G H
  lower-htpy-upper-htpy-galois-connection-Large-Poset p =
    htpy-sim-hom-Large-Poset P Q
      ( lower-adjoint-galois-connection-Large-Poset G)
      ( lower-adjoint-galois-connection-Large-Poset H)
      ( lower-sim-upper-sim-galois-connection-Large-Poset P Q G H
        ( sim-htpy-hom-Large-Poset Q P
          ( upper-adjoint-galois-connection-Large-Poset H)
          ( upper-adjoint-galois-connection-Large-Poset G)
          ( p)))
```

### An element `x' : Q` satisfies the lower universal property with respect to `x : P` if and only if it is similar to the element `LG x`

```agda
module _
  {αP αQ : Level → Level} {βP βQ : Level → Level → Level}
  {γ δ : Level → Level}
  (P : Large-Poset αP βP) (Q : Large-Poset αQ βQ)
  (G : galois-connection-Large-Poset γ δ P Q)
  {l1 l2 : Level} (x : type-Large-Poset P l1) (x' : type-Large-Poset Q l2)
  where

  is-lower-element-sim-galois-connection-Large-Poset :
    sim-Large-Poset Q
      ( map-lower-adjoint-galois-connection-Large-Poset P Q G x)
      ( x') →
    is-lower-element-galois-connection-Large-Poset P Q G x x'
  pr1 (is-lower-element-sim-galois-connection-Large-Poset s y) p =
    forward-implication-adjoint-relation-galois-connection-Large-Poset P Q G
      ( transitive-leq-Large-Poset Q _ x' y p (pr1 s))
  pr2 (is-lower-element-sim-galois-connection-Large-Poset s y) p =
    transitive-leq-Large-Poset Q x' _ y
      ( backward-implication-adjoint-relation-galois-connection-Large-Poset
        P Q G p)
      ( pr2 s)

  sim-is-lower-element-galois-connection-Large-Poset :
    is-lower-element-galois-connection-Large-Poset P Q G x x' →
    sim-Large-Poset Q
      ( map-lower-adjoint-galois-connection-Large-Poset P Q G x)
      ( x')
  sim-is-lower-element-galois-connection-Large-Poset l =
    sim-has-same-elements-principal-upper-set-element-Large-Poset Q
      ( λ y →
        logical-equivalence-reasoning
          leq-Large-Poset Q _ y
          ↔ leq-Large-Poset P x _
            by adjoint-relation-galois-connection-Large-Poset G x y
          ↔ leq-Large-Poset Q x' y
            by inv-iff (l y))
```

### An element `y' : P` satisfies the upper universal property with respect to `y : Q` if and only if it is similar to the element `UG y`

```agda
module _
  {αP αQ : Level → Level} {βP βQ : Level → Level → Level}
  {γ δ : Level → Level}
  (P : Large-Poset αP βP) (Q : Large-Poset αQ βQ)
  (G : galois-connection-Large-Poset γ δ P Q)
  {l1 l2 : Level} (y : type-Large-Poset Q l1) (y' : type-Large-Poset P l2)
  where

  is-upper-element-sim-galois-connection-Large-Poset :
    sim-Large-Poset P
      ( map-upper-adjoint-galois-connection-Large-Poset P Q G y)
      ( y') →
    is-upper-element-galois-connection-Large-Poset P Q G y y'
  pr1 (is-upper-element-sim-galois-connection-Large-Poset s x) p =
    transitive-leq-Large-Poset P x _ y'
      ( pr1 s)
      ( forward-implication-adjoint-relation-galois-connection-Large-Poset
        P Q G p)
  pr2 (is-upper-element-sim-galois-connection-Large-Poset s x) p =
    backward-implication-adjoint-relation-galois-connection-Large-Poset P Q G
      ( transitive-leq-Large-Poset P x y' _ (pr2 s) p)

  sim-is-upper-element-galois-connection-Large-Poset :
    is-upper-element-galois-connection-Large-Poset P Q G y y' →
    sim-Large-Poset P
      ( map-upper-adjoint-galois-connection-Large-Poset P Q G y)
      ( y')
  sim-is-upper-element-galois-connection-Large-Poset u =
    sim-has-same-elements-principal-lower-set-element-Large-Poset P
      ( λ x →
        logical-equivalence-reasoning
          leq-Large-Poset P x _
          ↔ leq-Large-Poset Q _ y
            by inv-iff (adjoint-relation-galois-connection-Large-Poset G x y)
          ↔ leq-Large-Poset P x y'
            by u x)
```

### The lower adjoint of a Galois connection preserves all existing joins

```agda
module _
  {αP αQ : Level → Level} {βP βQ : Level → Level → Level}
  {γ δ : Level → Level}
  (P : Large-Poset αP βP) (Q : Large-Poset αQ βQ)
  (G : galois-connection-Large-Poset γ δ P Q)
  where

  private
    _≤-P_ :
      {l1 l2 : Level} → type-Large-Poset P l1 → type-Large-Poset P l2 →
      UU (βP l1 l2)
    _≤-P_ = leq-Large-Poset P

    _≤-Q_ :
      {l1 l2 : Level} → type-Large-Poset Q l1 → type-Large-Poset Q l2 →
      UU (βQ l1 l2)
    _≤-Q_ = leq-Large-Poset Q

    hom-f : hom-Large-Poset _ P Q
    hom-f = lower-adjoint-galois-connection-Large-Poset G

    f : {l : Level} → type-Large-Poset P l → type-Large-Poset Q (γ l)
    f = map-hom-Large-Poset P Q hom-f

    hom-g : hom-Large-Poset _ Q P
    hom-g = upper-adjoint-galois-connection-Large-Poset G

    g : {l : Level} → type-Large-Poset Q l → type-Large-Poset P (δ l)
    g = map-hom-Large-Poset Q P hom-g

    adjoint-relation-G :
      {l1 l2 : Level}
      (x : type-Large-Poset P l1) (y : type-Large-Poset Q l2) →
      leq-Large-Poset Q (f x) y ↔
      leq-Large-Poset P x (g y)
    adjoint-relation-G = adjoint-relation-galois-connection-Large-Poset G

  preserves-join-lower-adjoint-galois-connection-Large-Poset :
    {l1 l2 l3 : Level} {U : UU l1} (x : U → type-Large-Poset P l2)
    (y : type-Large-Poset P l3) →
    is-least-upper-bound-family-of-elements-Large-Poset P x y →
    is-least-upper-bound-family-of-elements-Large-Poset Q
      ( λ α → f (x α))
      ( f y)
  preserves-join-lower-adjoint-galois-connection-Large-Poset x y H z =
    logical-equivalence-reasoning
      ((α : _) → f (x α) ≤-Q z)
      ↔ ((α : _) → (x α) ≤-P g z)
        by iff-Π-iff-family (λ α → adjoint-relation-G (x α) z)
      ↔ y ≤-P g z by H (g z)
      ↔ f y ≤-Q z by inv-iff (adjoint-relation-G y z)
```