Documentation

Mathlib.CategoryTheory.Category.GaloisConnection

Galois connections between preorders are adjunctions. #

def GaloisConnection.adjunction {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] {l : XY} {u : YX} (gc : GaloisConnection l u) :
.functor .functor

A galois connection between preorders induces an adjunction between the associated categories.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem CategoryTheory.Adjunction.gc {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] {L : CategoryTheory.Functor X Y} {R : CategoryTheory.Functor Y X} (adj : L R) :
    GaloisConnection L.obj R.obj

    An adjunction between preorder categories induces a galois connection.