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

the unit on the right side.

the unit on the left side.

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

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

attest of being Multiplicative homomorphous.

the dual adjunction.

validity of an adjunction according to the properties of Adjunction.

validity of the unit on the right side.

validity of the unit on the left side.