Homotopy Type Theory grouplike A3-space > history (changes)

Showing changes from revision #7 to #8: Added | Removed | Changed

Idea

The invertible version of the A3-space up to homotopy, without any higher coherences for inverses.

Definition

A grouplike A 3A_3-space or grouplike A 3A_3-algebra in homotopy types or H-group consists of

  • A type AA,
  • A basepoint e:Ae:A
  • A binary operation μ:AAA\mu : A \to A \to A
  • A unary operation ι:AA\iota: A \to A
  • A left unitor
    λ u: (a:A)μ(e,a)=a\lambda_u:\prod_{(a:A)} \mu(e,a)=a
  • A right unitor
    ρ u: (a:A)μ(a,e)=a\rho_u:\prod_{(a:A)} \mu(a,e)=a
  • An asssociator
    α: (a:A) (b:A) (c:A)μ(μ(a,b),c)=μ(a,μ(b,c))\alpha:\prod_{(a:A)} \prod_{(b:A)} \prod_{(c:A)} \mu(\mu(a, b),c)=\mu(a,\mu(b,c))
  • A left invertor
    l: (a:A)μ(ι(a),a)=el:\prod_{(a:A)} \mu(\iota(a), a)=e
  • A right invertor
    r: (a:A)μ(a,ι(a))=er:\prod_{(a:A)} \mu(a,\iota(a))=e

One could also speak of grouplike A 3A_3-spaces where the existence of left and right inverses are mere property rather than structure, which is a grouplike A 3A_3-space as defined above with additional structure specifying that the types (a:A)μ(ι(a),a)=e\prod_{(a:A)} \mu(\iota(a), a)=e and (a:A)μ(a,ι(a))=e\prod_{(a:A)} \mu(a,\iota(a))=e are contractible:

c l: l: (a:A)μ(ι(a),a)=e b: (a:A)μ(ι(a),a)=el=bc_l: \sum_{l:\prod_{(a:A)} \mu(\iota(a), a)=e} \prod_{b:\prod_{(a:A)} \mu(\iota(a), a)=e} l = b
c r: r: (a:A)μ(a,ι(a))=e b: (a:A)μ(a,ι(a))=er=bc_r: \sum_{r:\prod_{(a:A)} \mu(a,\iota(a))=e} \prod_{b:\prod_{(a:A)} \mu(a,\iota(a))=e} r = b

or equivalently,

c l: (a:A) (l:μ(ι(a),a)=e) (b:μ(ι(a),a)=e)l=bc_l:\prod_{(a:A)} \sum_{(l:\mu(\iota(a), a)=e)} \prod_{(b:\mu(\iota(a), a)=e)} l = b
c r: (a:A) (r:μ(a,ι(a))=e) (r:μ(a,ι(a))=e)r=bc_r:\prod_{(a:A)} \sum_{(r:\mu(a,\iota(a))=e)} \prod_{(r:\mu(a,\iota(a))=e)} r = b

Examples

  • The integers are an grouplike A 3A_3-space.

  • Every loop space is naturally an grouplike A 3A_3-space with path concatenation as the operation. In fact every loop space is a \infty-group.

  • A group is a 0-truncated grouplike A 3A_3-space.

See also

Last revised on June 9, 2022 at 14:44:15. See the history of this page for a list of all contributions to it.