oalg-base-3.0.0.0: Algebraic structures on oriented entities and limits as a tool kit to solve algebraic problems.
Copyright(c) Erich Gut
LicenseBSD3
Maintainerzerich.gut@gmail.com
Safe HaskellNone
LanguageHaskell2010

OAlg.Adjunction.Definition

Description

definition of adjunctions between Multiplicative structures. We relay on the terms and notation as used in nLab

Synopsis

Adjunction

data Adjunction (h :: Type -> Type -> Type) d c where Source #

adjunction between two multiplicative structures d and c according two given multiplicative homomorphisms l :: h c d and r :: h d c. 

             l
         <------- 
       d          c
         -------->
             r

Property Let Adjunction l r u v be in Adjunction h d c where h is a Mlt-homomorphism, then holds:

  1. Naturality of the right unit u:

    1. For all x in Point c holds: orientation (u x) == x :> pmap r (pmap l x).
    2. For all f in c holds: u (end f) * f == amap r (amap l) f * u (start f).

  2. Naturality of the left unit v:

    1. For all y in Point d holds: orientation (v y) == pmap l (pmap r y) :> y.
    2. For all g in d holds: g * v (start g) == v (end g) * amap l (amap r) g.

  3. Triangle identities:

    1. For all x in Point c holds: one (pmap l x) == v (pmap l x) * amap l (u x).
    2. For all y in Point d holds: one (pmap r y) == amap r (v y) * u (pmap r y).

The following diagrams illustrate the above equations

naturality of the right unit u (Equations 1.1 and 1.2):

        u a
    a -------> pmap r (pmap l a)         
    |                |
  f |                | amap r (amap l f)
    v                v
    b -------> pmap r (pmap l b)
        u b

naturality of the left unit v (Equations 2.1 and 2.2):

        v a
   a <------- pmap l (pmap r a)
   |                |
 g |                | amap l (ampa r g)
   v                v
   b <------ pmap l (pmap r b)
        v b

the left adjoint of the right unit u is one (Equation 3.1, see adjl):

                                 pmap l x         x
                                /   |             |
                               /    |             |
                              /     |             |
                amap l (u x) /      | one  ~  u x |    
                            /       |             |
                           /        |             |
                          v         v             v
 pmap l (pmap r (pmap l x)) ---> pmap l x    pmap r (pmap l x)
                        v (pmap l x)

the right adjoint of the left unit v is one (Equation 3.2, see adjr):

                            u (pmap r y)
 pmap l (pmap r y)     pmap r y ---> pmap r (pmap l (pmap r y))
       |                  |         /
       |                  |        /
       | v y    ~     one |       / amap r (v y)
       |                  |      /
       |                  |     /
       v                  v    v
       y               pmap r y

Constructors

Adjunction 

Fields

  • :: forall (h :: Type -> Type -> Type) c d. h c d

    the homomorphism from right to left.

  • -> h d c

    the homomorphism from left to right.

  • -> (Point c -> c)

    the unit on the right side.

  • -> (Point d -> d)

    the unit on the left side.

  • -> Adjunction h d c
     

Instances

Instances details
(HomMultiplicative h, Entity2 h, XStandardPoint d, XStandard d, XStandardPoint c, XStandard c) => Validable (Adjunction h d c) Source # 
Instance details

Defined in OAlg.Adjunction.Definition

Methods

valid :: Adjunction h d c -> Statement Source #

unitr :: forall (h :: Type -> Type -> Type) d c. Adjunction h d c -> Point c -> c Source #

the unit on the right side.

unitl :: forall (h :: Type -> Type -> Type) d c. Adjunction h d c -> Point d -> d Source #

the unit on the left side.

adjl :: forall (h :: Type -> Type -> Type) d c. Hom Mlt h => Adjunction h d c -> Point d -> c -> d Source #

the left adjoint f' of a factor f in c.

Property Let y be in d and f in c with end f == pmap r y then the left adjoint f' of f is given by f' = v y * amap l f.

                     pmap l x           x
                      /   |             |
                     /    |             |
                    /     |             |
          amap l f /      | f'   ~    f |
                  /       |             |
                 /        |             |
                v         v             v
 pmap l (pmap r y) -----> y          pmap r y
                     v y

adjr :: forall (h :: Type -> Type -> Type) d c. Hom Mlt h => Adjunction h d c -> Point c -> d -> c Source #

the right adjoint g' of a factor in g in d

Property Let x be in c and g in d with start g == pmap l x then the right adjoint g' of g is given by g' = amap r g * u x.

                            u x
      pmap l x           x -----> pmap r (pmap l x)
         |               |       /
         |               |      /
         |               |     /
         | g     ~    g' |    / amap r g
         |               |   /
         |               |  /
         v               v v
         y            pmap r y

adjHomMlt :: forall (h :: Type -> Type -> Type) d c. Hom Mlt h => Adjunction h d c -> Homomorphous Mlt d c Source #

attest of being Multiplicative homomorphous.

adjHomDst :: forall (h :: Type -> Type -> Type) d c. HomDistributive h => Adjunction h d c -> Homomorphous Dst d c Source #

attest of being Distributive homomorphous.

adjHomDisj :: forall (h :: Type -> Type -> Type) s x y (o :: Type -> Type). (HomMultiplicative h, Transformable (ObjectClass h) s) => Adjunction h x y -> Adjunction (Variant2 'Covariant (HomDisj s o h)) x y Source #

the induce adjunction.

Map

adjMapCnt :: forall (h :: Type -> Type -> Type) x x' y y'. FunctorialOriented h => Variant2 'Contravariant (Inv2 h) x x' -> Variant2 'Contravariant (Inv2 h) y y' -> Adjunction (Variant2 'Covariant h) x y -> Adjunction (Variant2 'Covariant h) y' x' Source #

contravariant mapping of Adjunction.

coAdjunctionOp :: forall (h :: Type -> Type -> Type) x y. HomMultiplicative h => Adjunction h x y -> Adjunction (Variant2 'Covariant (HomDisj Mlt Op h)) (Op y) (Op x) Source #

the co-Adjunction according to Op.

Proposition

prpAdjunction :: forall (h :: Type -> Type -> Type) d c. (Hom Mlt h, Entity2 h) => Adjunction h d c -> X (Point d) -> X d -> X (Point c) -> X c -> Statement Source #

validity of an adjunction according to the properties of Adjunction.

prpAdjunctionRight :: forall (h :: Type -> Type -> Type) d c. (Hom Mlt h, Show2 h) => Adjunction h d c -> Point c -> c -> Statement Source #

validity of the unit on the right side.

prpAdjunctionLeft :: forall (h :: Type -> Type -> Type) d c. (Hom Mlt h, Show2 h) => Adjunction h d c -> Point d -> d -> Statement Source #

validity of the unit on the left side.