Homotopy Type Theory power-associative magma > history (changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Contents

< power-associative magma

Definition

In any magma

Let +\mathbb{Z}_{+} be the type of all positive integers:

+ n:n>0\mathbb{Z}_{+} \coloneqq \sum_{n:\mathbb{Z}} n \gt 0

A power-associative magma consists of

  • A type AA,
  • A binary operation μ:A×AA\mu : A \times A \to A
  • A binary power function () ():A× +A{(-)}^{(-)}: A \times \mathbb{Z}_{+} \to A
  • Two families of dependent terms of identities
    a:Ai(a):a 1=aa:A \vdash i(a): a^1 = a
    m: +,n: +,a:Ac(m,n,a):(a m) n=a mnm:\mathbb{Z}_{+}, n:\mathbb{Z}_{+}, a:A \vdash c(m, n, a): (a^m)^n = a^{m \cdot n}

    stating that the power is a right multiplicative +\mathbb{Z}_{+}-action.

  • A family of dependent terms of identities
    a:A,m: +,n: +π(a,m,n):μ(a m,a n)=a m+na:A, m:\mathbb{Z}_{+}, n:\mathbb{Z}_{+} \vdash \pi(a, m, n):\mu(a^m, a^n)=a^{m+n}

    representing the law of exponents for the magma.

  • A family of dependent terms of identities
    a:A,b:Aτ 0(a,b):isProp(a=b)a:A, b:A \vdash \tau_0(a,b):isProp(a=b)

    representing that AA is a set.

The associative and commutative identities for powers of a:Aa:A follow from the associative and commutative identities of addition in +\mathbb{Z}_{+}.

In a unital magma

There is a definition of a power-associative unital magma with two-sided inverses, without using explicit unit identites:

A power-associative unital magma consists of

  • A type AA
  • A term e:Ae:A
  • A binary operation μ:A×AA\mu : A \times A \to A
  • A binary power function () ():A×A{(-)}^{(-)}: A \times \mathbb{N} \to A
  • Two families of dependent terms of identities
    a:Ai(a):a 1=aa:A \vdash i(a): a^1 = a
    m:,n:,a:Ac(m,n,a):(a m) n=a mnm:\mathbb{N}, n:\mathbb{N}, a:A \vdash c(m, n, a): (a^m)^n = a^{m \cdot n}

    stating that the power is a right multiplicative \mathbb{N}-action.

  • A family of dependent terms of identities
    a:Az(a):a 0=ea:A \vdash z(a): a^0 = e
  • A family of dependent terms of identities
    a:A,m:,n:π(a,m,n):μ(a m,a n)=a m+na:A, m:\mathbb{N}, n:\mathbb{N} \vdash \pi(a, m, n):\mu(a^m, a^n)=a^{m+n}

    representing the law of exponents for the magma.

  • A family of dependent terms of identities
    a:A,b:Aτ 0(a,b):isProp(a=b)a:A, b:A \vdash \tau_0(a,b):isProp(a=b)

    representing that AA is a set.

The associative, commutative and unit identities for powers of a:Aa:A follow from the associative, commutative, and unit identities of addition in \mathbb{N}.

In a magma with two-sided inverses

There is a definition of a power-associative magma with two-sided inverses, without using explicit inverses as structure or property:

A power-associative magma with two-sided inverses consists of

  • A type AA,
  • A binary operation μ:A×AA\mu : A \times A \to A
  • A binary power function () ():A×A{(-)}^{(-)}: A \times \mathbb{Z} \to A
  • Two families of dependent terms of identities
    a:Ai(a):a 1=aa:A \vdash i(a): a^1 = a
    m:,n:,a:Ac(m,n,a):(a m) n=a mnm:\mathbb{Z}, n:\mathbb{Z}, a:A \vdash c(m, n, a): (a^m)^n = a^{m \cdot n}

    stating that the power is a right multiplicative \mathbb{Z}-action.

  • A family of dependent terms of identities
    a:A,m:,n:π(a,m,n):μ(a m,a n)=a m+na:A, m:\mathbb{Z}, n:\mathbb{Z} \vdash \pi(a, m, n):\mu(a^m, a^n)=a^{m+n}

    representing the law of exponents for the magma.

  • A family of dependent terms of identities
    a:A,b:Aτ 0(a,b):isProp(a=b)a:A, b:A \vdash \tau_0(a,b):isProp(a=b)

    representing that AA is a set.

The associative, commutative, and inverse element identities for powers of a:Aa:A follow from the associative, commutative, and inverse element identities of addition in \mathbb{Z}. In addition, the unit identities for powers of a:Aa:A follow as well if AA is inhabited.

See also

Last revised on June 13, 2022 at 21:57:40. See the history of this page for a list of all contributions to it.