# Reflective Galois connections between large posets

Content created by Egbert Rijke, Fredrik Bakke and Maša Žaucer.

Created on 2023-06-08.

module order-theory.reflective-galois-connections-large-posets where

Imports
open import foundation.cartesian-product-types
open import foundation.universe-levels

open import order-theory.galois-connections-large-posets
open import order-theory.large-posets
open import order-theory.order-preserving-maps-large-posets


## Idea

A reflective galois connection between large posets P and Q is a Galois connection f : P ⇆ Q : g such that f ∘ g : Q → P is the identity map.

## Definitions

### The predicate of being a reflective Galois connection

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)
where

private
f = map-lower-adjoint-galois-connection-Large-Poset P Q G
g = map-upper-adjoint-galois-connection-Large-Poset P Q G

is-reflective-galois-connection-Large-Poset : UUω
is-reflective-galois-connection-Large-Poset =
{l : Level} (x : type-Large-Poset Q l) →
leq-Large-Poset Q (f (g x)) x ×
leq-Large-Poset Q x (f (g x))


### The type of reflective Galois connections

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

record reflective-galois-connection-Large-Poset : UUω
where
field
galois-connection-reflective-galois-connection-Large-Poset :
galois-connection-Large-Poset γ δ P Q
is-reflective-reflective-galois-connection-Large-Poset :
is-reflective-galois-connection-Large-Poset P Q
galois-connection-reflective-galois-connection-Large-Poset

open reflective-galois-connection-Large-Poset public

module _
(G : reflective-galois-connection-Large-Poset)
where