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 3A_3-space or commutative A 3A_3-algebra in homotopy types or commutative H-monoid consists of

  • A type AA,
  • A basepoint e:Ae:A
  • A binary operation μ:AAA\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 3A_3-spaces where commutativity is mere property rather than structure, which is a commutative A 3A_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)κ=bc_\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))κ=bc_\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 3A_3-spaces

A homomorphism of commutative A 3A_3-spaces between two commutative A 3A_3-spaces AA and BB consists of

  • A function ϕ:AB\phi:A \to B such that

    • The basepoint is preserved
      ϕ(e A)=e B\phi(e_A) = e_B
    • The binary operation is preserved
      (a:A) (b:A)ϕ(μ A(a,b))=μ B(ϕ(a),ϕ(b))\prod_{(a:A)} \prod_{(b:A)} \phi(\mu_A(a, b)) = \mu_B(\phi(a),\phi(b))
  • A function

ϕ λ:( (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 function
ϕ ρ:( (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 function
ϕ α:( (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 function
ϕ κ:( (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 3A_3-spaces

(…)

Examples

  • The integers are a commutative A 3A_3-space.

  • A commutative monoid is a 0-truncated commutative A 3A_3-space.

  • A H-rig? is a A 3A_3-algebra in commutative A 3A_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.