Homotopy Type Theory
commutative A3-space > history (Rev #12, changes)
Showing changes from revision #11 to #12:
Added | Removed | Changed
Idea
The commutative version of the A3-space up to homotopy, without any higher commutative coherences.
Definition
A commutative A 3 A_3 -space or commutative A 3 A_3 -algebra in homotopy types or commutative H-monoid consists of
A type A A ,
A basepoint e : A e:A
A binary operation μ : A → A → A \mu : A \to A \to A
A left unitorλ : ∏ ( a : A ) μ ( e , a ) = a \lambda:\prod_{(a:A)} \mu(e,a)=a
A right unitorρ : ∏ ( a : A ) μ ( a , e ) = a \rho:\prod_{(a:A)} \mu(a,e)=a
An asssociatorα : ∏ ( a 1 : A ) ∏ ( a 2 : A ) ∏ ( a 3 : A ) μ ( μ ( a 1 , a 2 ) , a 3 ) = μ ( a 1 , μ ( a 2 , a 3 ) ) \alpha:\prod_{(a_1:A)} \prod_{(a_2:A)} \prod_{(a_3:A)} \mu(\mu(a_1, a_2),a_3)=\mu(a_1,\mu(a_2,a_3))
A commutatorκ : ∏ ( a 1 : A ) ∏ ( a 2 : A ) μ ( a 1 , a 2 ) = μ ( a 2 , a 1 ) \kappa:\prod_{(a_1:A)} \prod_{(a_2:A)} \mu(a_1, a_2)=\mu(a_2, a_1)
One could also speak of commutative A 3 A_3 -spaces where commutativity is mere property rather than structure, which is a commutative A 3 A_3 -space as defined above with additional structure specifying that the type ∏ ( a 1 : A ) ∏ ( a 2 : A ) μ ( a 1 , a 2 ) = μ ( a 2 , a 1 ) \prod_{(a_1:A)} \prod_{(a_2:A)} \mu(a_1, a_2)=\mu(a_2, a_1) is contractible :
c κ : ∑ κ : ∏ ( a 1 : A ) ∏ ( a 2 : A ) μ ( a 1 , a 2 ) = μ ( a 2 , a 1 ) ∏ b : ∏ ( a 1 : A ) ∏ ( a 2 : A ) μ ( a 1 , a 2 ) = μ ( a 2 , a 1 ) κ = b c_\kappa: \sum_{\kappa:\prod_{(a_1:A)} \prod_{(a_2:A)} \mu(a_1, a_2)=\mu(a_2, a_1)} \prod_{b:\prod_{(a_1:A)} \prod_{(a_2:A)} \mu(a_1, a_2)=\mu(a_2, a_1)} \kappa = b
or equivalently
c κ : ∏ ( a 1 : A ) ∏ ( a 2 : A ) ∑ ( κ : μ ( a 1 , a 2 ) = μ ( a 2 , a 1 ) ) ∏ ( b : μ ( a 1 , a 2 ) = μ ( a 2 , a 1 ) ) κ = b c_\kappa:\prod_{(a_1:A)} \prod_{(a_2:A)} \sum_{(\kappa:\mu(a_1, a_2)=\mu(a_2, a_1))} \prod_{(b:\mu(a_1, a_2)=\mu(a_2, a_1))} \kappa = b
or
c κ : ∏ ( a 1 : A ) ∏ ( a 2 : A ) isContr ( μ ( a 1 , a 2 ) = μ ( a 2 , a 1 ) ) c_\kappa:\prod_{(a_1:A)} \prod_{(a_2:A)} isContr(\mu(a_1, a_2)=\mu(a_2, a_1))
Homomorphisms of commutative A 3 A_3 -spaces
A homomorphism of commutative A 3 A_3 -spaces between two commutative A 3 A_3 -spaces A A and B B consists of
ϕ λ : ( ∏ ( a : A ) μ ( e A , a ) = a ) → ( ∏ ( b : B ) μ ( e B , b ) = b ) \phi_\lambda:\left(\prod_{(a:A)} \mu(e_A,a)=a\right) \to \left(\prod_{(b:B)} \mu(e_B,b)=b\right)
such that the left unitor is preserved:
ϕ λ ( λ A ) = λ B \phi_\lambda(\lambda_A) = \lambda_B
ϕ ρ : ( ∏ ( a : A ) μ ( a , e A ) = a ) → ( ∏ ( b : B ) μ ( b , e B ) = b ) \phi_\rho:\left(\prod_{(a:A)} \mu(a, e_A)=a\right) \to \left(\prod_{(b:B)} \mu(b, e_B)=b\right)
such that the right unitor is preserved:
ϕ ρ ( ρ A ) = ρ B \phi_\rho(\rho_A) = \rho_B
ϕ α : ( ∏ ( a 1 : A ) ∏ ( a 2 : A ) ∏ ( a 3 : A ) μ ( μ ( a 1 , a 2 ) , a 3 ) = μ ( a 1 , μ ( a 2 , a 3 ) ) ) → ( ∏ ( b 1 : B ) ∏ ( b 2 : B ) ∏ ( b 3 : B ) μ ( μ ( b 1 , b 2 ) , b 3 ) = μ ( b 1 , μ ( b 2 , b 3 ) ) ) \phi_\alpha:\left(\prod_{(a_1:A)} \prod_{(a_2:A)} \prod_{(a_3:A)} \mu(\mu(a_1, a_2),a_3)=\mu(a_1,\mu(a_2,a_3))\right) \to \left(\prod_{(b_1:B)} \prod_{(b_2:B)} \prod_{(b_3:B)} \mu(\mu(b_1, b_2),b_3)=\mu(b_1,\mu(b_2,b_3))\right)
such that the associator is preserved:
ϕ α ( α A ) = α B \phi_\alpha(\alpha_A) = \alpha_B
ϕ κ : ( ∏ ( a 1 : A ) ∏ ( a 2 : A ) μ ( a 1 , a 2 ) = μ ( a 2 , a 1 ) ) → ( ∏ ( b 1 : B ) ∏ ( b 2 : B ) μ ( b 1 , b 2 ) = μ ( b 2 , b 1 ) ) \phi_\kappa:\left(\prod_{(a_1:A)} \prod_{(a_2:A)} \mu(a_1, a_2)=\mu(a_2, a_1)\right) \to \left(\prod_{(b_1:B)} \prod_{(b_2:B)} \mu(b_1, b_2)=\mu(b_2, b_1)\right)
such that the commutator is preserved:
ϕ κ ( κ A ) = κ B \phi_\kappa(\kappa_A) = \kappa_B
Tensor product of commutative A 3 A_3 -spaces
(…)
Examples
The integers are a commutative A 3 A_3 -space.
A commutative monoid is a 0-truncated commutative A 3 A_3 -space.
A H-rig? is a A 3 A_3 -algebra in commutative A 3 A_3 -spaces.
See also
Revision on June 9, 2022 at 14:48:46 by
Anonymous? .
See the history of this page for a list of all contributions to it.