Homotopy Type Theory biaction > history (Rev #2)

Idea

A ternary function which behaves as simultaneous actions on both the left and the right side:

 Definition

Given a set SS and monoids (M,e M,μ M)(M, e_M, \mu_M) and (N,e N,μ N)(N, e_N, \mu_N), a biaction is a ternary function α:M×S×NS\alpha:M \times S \times N \to S such that

  • for all s:Ss:S, α(e M,s,e N)=s\alpha(e_M, s, e_N) = s

  • for all s:Ss:S, a:Ma:M, b:Mb:M, c:Nc:N, and d:Nd:N, α(a,α(b,s,c),d)=α(μ M(a,b),s,μ N(c,d))\alpha(a, \alpha(b, s, c), d) = \alpha(\mu_M(a, b), s, \mu_N(c, d))

Left and right actions

The left $M$-action? is defined as

α M(a,s)α(a,s,e N)\alpha_M(a, s) \coloneqq \alpha(a, s, e_N)

for all a:Ma:M and s:Ss:S. It is a left action because

α M(e M,s)=α(e M,s,e N)=s\alpha_M(e_M, s) = \alpha(e_M, s, e_N) = s
α M(a,α L(b,s))=α(a,α(b,s,e N),e N)=α(μ M(a,b),s,μ N(e N,e N))=α(μ M(a,b),s,e N)=α M(μ M(a,b),s)\alpha_M(a, \alpha_L(b, s)) = \alpha(a, \alpha(b, s, e_N), e_N) = \alpha(\mu_M(a, b), s, \mu_N(e_N, e_N)) = \alpha(\mu_M(a, b), s, e_N) = \alpha_M(\mu_M(a, b), s)

The right $N$-action? is defined as

α N(s,c)α(e M,s,c)\alpha_N(s, c) \coloneqq \alpha(e_M, s, c)

for all c:Nc:N and s:Ss:S. It is a right action because

α N(s,e N)=α(e M,s,e N)=s\alpha_N(s, e_N) = \alpha(e_M, s, e_N) = s
α N(α N(s,c),d)=α(e M,α(e M,s,c),d)=α(μ M(e M,e M),s,μ N(c,d))=α(e M,s,μ N(c,d))=α N(s,μ N(c,d))\alpha_N(\alpha_N(s, c), d) = \alpha(e_M, \alpha(e_M, s, c), d) = \alpha(\mu_M(e_M, e_M), s, \mu_N(c, d)) = \alpha(e_M, s, \mu_N(c, d)) = \alpha_N(s, \mu_N(c, d))

The left MM-action and right NN-action satisfy the following identity:

  • for all s:Ss:S, a:Ma:M and c:Nc:N, α M(a,α N(s,c))=α N(α M(a,s),c)\alpha_M(a, \alpha_N(s, c)) = \alpha_N(\alpha_M(a, s), c).

This is because when expanded out, the identity becomes:

α(a,α(e M,s,c),e N)=α(e M,α(a,s,e N),c)\alpha(a, \alpha(e_M, s, c), e_N) = \alpha(e_M, \alpha(a, s, e_N), c)
α(μ M(a,e M),s,μ N(c,e N))=α(μ M(e M,a),s,μ N(e N,c))\alpha(\mu_M(a, e_M), s, \mu_N(c, e_N)) = \alpha(\mu_M(e_M, a), s, \mu_N(e_N, c))
α(a,s,c)=α(a,s,c)\alpha(a, s, c) = \alpha(a, s, c)

See also

Revision on May 25, 2022 at 03:20:18 by Anonymous?. See the history of this page for a list of all contributions to it.