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 A A ,
A binary operation μ : A × A → A \mu : A \times A \to A
A binary power function ( − ) ( − ) : A × ℤ + → A {(-)}^{(-)}: A \times \mathbb{Z}_{+} \to A
Two families of dependent terms of identitiesa : A ⊢ i ( a ) : a 1 = a a:A \vdash i(a): a^1 = a m : ℤ + , n : ℤ + , a : A ⊢ c ( m , n , a ) : ( a m ) n = a m ⋅ n m:\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 identitiesa : A , m : ℤ + , n : ℤ + ⊢ π ( a , m , n ) : μ ( a m , a n ) = a m + n a: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 identitiesa : A , b : A ⊢ τ 0 ( a , b ) : isProp ( a = b ) a:A, b:A \vdash \tau_0(a,b):isProp(a=b)
representing that A A is a set .
The associative and commutative identities for powers of a : A a: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 A A
A term e : A e:A
A binary operation μ : A × A → A \mu : A \times A \to A
A binary power function ( − ) ( − ) : A × ℕ → A {(-)}^{(-)}: A \times \mathbb{N} \to A
Two families of dependent terms of identitiesa : A ⊢ i ( a ) : a 1 = a a:A \vdash i(a): a^1 = a m : ℕ , n : ℕ , a : A ⊢ c ( m , n , a ) : ( a m ) n = a m ⋅ n m:\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 identitiesa : A ⊢ z ( a ) : a 0 = e a:A \vdash z(a): a^0 = e
A family of dependent terms of identitiesa : A , m : ℕ , n : ℕ ⊢ π ( a , m , n ) : μ ( a m , a n ) = a m + n a: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 identitiesa : A , b : A ⊢ τ 0 ( a , b ) : isProp ( a = b ) a:A, b:A \vdash \tau_0(a,b):isProp(a=b)
representing that A A is a set .
The associative, commutative and unit identities for powers of a : A a: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 A A ,
A binary operation μ : A × A → A \mu : A \times A \to A
A binary power function ( − ) ( − ) : A × ℤ → A {(-)}^{(-)}: A \times \mathbb{Z} \to A
Two families of dependent terms of identitiesa : A ⊢ i ( a ) : a 1 = a a:A \vdash i(a): a^1 = a m : ℤ , n : ℤ , a : A ⊢ c ( m , n , a ) : ( a m ) n = a m ⋅ n m:\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 identitiesa : A , m : ℤ , n : ℤ ⊢ π ( a , m , n ) : μ ( a m , a n ) = a m + n a: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 identitiesa : A , b : A ⊢ τ 0 ( a , b ) : isProp ( a = b ) a:A, b:A \vdash \tau_0(a,b):isProp(a=b)
representing that A A is a set .
The associative, commutative, and inverse element identities for powers of a : A a:A follow from the associative, commutative, and inverse element identities of addition in ℤ \mathbb{Z} . In addition, the unit identities for powers of a : A a:A follow as well if A A 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.