Homotopy Type Theory abelian group > history (Rev #9, changes)

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


As a twice-delooping of a pointed simply connected 2-groupoid

A pointed simply connected 2-groupoid consists of

  • A type GG
  • A basepoint e:Ge:G
  • A 1-connector
    ΞΊ 1:∏ f:Gβ†’πŸ™βˆ a:πŸ™isContr([fiber(f,a)] 1)\kappa_1:\prod_{f:G \to \mathbb{1}} \prod_{a:\mathbb{1}} \mathrm{isContr}(\left[\mathrm{fiber}(f, a)\right]_{1})
  • A 2-truncator:
    Ο„ 2:isTwoGroupoid(G)\tau_2:\mathrm{isTwoGroupoid}(G)

An abelian group or β„€\mathbb{Z}-module is the type Aut(Aut(G))\mathrm{Aut}(\mathrm{Aut}(G)) of automorphisms of automorphisms in GG.

As a group

An abelian group or β„€\mathbb{Z}-module consists of

  • A type GG,
  • A basepoint e:Ge:G
  • A binary operation ΞΌ:Gβ†’Gβ†’G\mu : G \to G \to G
  • A unary operation ΞΉ:Gβ†’G\iota: G \to G
  • A contractible left unit identity
    c λ:∏ (a:G)isContr(μ(e,a)=a)c_\lambda:\prod_{(a:G)} isContr(\mu(e,a)=a)
  • A contractible right unit identity
    c ρ:∏ (a:G)isContr(μ(a,e)=a)c_\rho:\prod_{(a:G)} isContr(\mu(a,e)=a)
  • A contractible associative identity
    c α:∏ (a:G)∏ (b:G)∏ (c:G)isContr(μ(μ(a,b),c)=μ(a,μ(b,c)))c_\alpha:\prod_{(a:G)} \prod_{(b:G)} \prod_{(c:G)} isContr(\mu(\mu(a, b),c)=\mu(a,\mu(b,c)))
  • A contractible left inverse identity
    c l:∏ (a:G)isContr(μ(ι(a),a)=e)c_l:\prod_{(a:G)} isContr(\mu(\iota(a), a)=e)
  • A contractible right inverse identity
    c r:∏ (a:G)isContr(μ(a,ι(a))=e)c_r:\prod_{(a:G)} isContr(\mu(a,\iota(a))=e)
  • A contractible commutative identity
    c κ:∏ (a:A)∏ (b:A)isContr(μ(a,b)=μ(b,a))c_\kappa:\prod_{(a:A)} \prod_{(b:A)} isContr(\mu(a, b)=\mu(b, a))
  • A 0-truncator
    Ο„ 0:∏ (a:G)∏ (b:G)isProp(a=b)\tau_0: \prod_{(a:G)} \prod_{(b:G)} isProp(a=b)

As a module

An abelian group or β„€\mathbb{Z}-module is a set SS with a term 0:S0:S and a binary function (βˆ’)+(βˆ’):SΓ—Sβ†’S(-)+(-):S \times S \to S, and a left multiplicative β„€\mathbb{Z}-action (βˆ’)β‹… l(βˆ’):β„€Γ—Sβ†’S(-)\cdot_l(-):\mathbb{Z} \times S \to S, such that

∏ a:S∏ b:Sa+b=b+a\prod_{a:S} \prod_{b:S} a + b = b + a
∏ a:S∏ b:S∏ c:Sa+(b+c)=(a+b)+c\prod_{a:S} \prod_{b:S} \prod_{c:S} a + (b + c) = (a + b) + c
∏ a:S1β‹… la=a\prod_{a:S} 1 \cdot_l a = a
∏ a:β„€βˆ b:β„€βˆ c:S(aβ‹…b)β‹… lc=aβ‹… l(bβ‹… lc)\prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}} \prod_{c:S} (a \cdot b) \cdot_l c = a \cdot_l (b \cdot_l c)
∏ a:S0β‹… la=0\prod_{a:S} 0 \cdot_l a = 0
∏ a:β„€βˆ b:S∏ c:Saβ‹… l(b+c)=aβ‹… lb+aβ‹… lc\prod_{a:\mathbb{Z}} \prod_{b:S} \prod_{c:S} a \cdot_l (b + c) = a \cdot_l b + a \cdot_l c
∏ a:β„€βˆ b:β„€βˆ c:S(a+b)β‹… lc=aβ‹… lc+bβ‹… lc\prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}} \prod_{c:S} (a + b) \cdot_l c = a \cdot_l c + b \cdot_l c

We define the functions βˆ’:Sβ†’S-:S \to S and (βˆ’)β‹… r(βˆ’):SΓ—β„€β†’S(-)\cdot_r(-):S \times \mathbb{Z} \to S to be

βˆ’a≔(βˆ’1)β‹… la-a \coloneqq (-1) \cdot_l a
aβ‹… rb≔bβ‹… laa \cdot_r b \coloneqq b \cdot_l a

and SS is an abelian group and a β„€\mathbb{Z}-bimodule

a=1β‹… 1a=(1+0)β‹… 1a=(1β‹… 1a)+(0β‹… 1a)=a+0a = 1 \cdot_1 a = (1 + 0) \cdot_1 a = (1 \cdot_1 a) + (0 \cdot_1 a) = a + 0
a=1β‹… 1a=(0+1)β‹… 1a=(0β‹… 1a)+(1β‹… 1a)=0+aa = 1 \cdot_1 a = (0 + 1) \cdot_1 a = (0 \cdot_1 a) + (1 \cdot_1 a) = 0 + a
0=0β‹… 1a=(1+βˆ’1)β‹… 1a=(1β‹… 1a)+(βˆ’1β‹… 1a)=a+βˆ’a0 = 0 \cdot_1 a = (1 + -1) \cdot_1 a = (1 \cdot_1 a) + (-1 \cdot_1 a) = a + -a
0=0β‹… 1a=(βˆ’1+1)β‹… 1a=(βˆ’1β‹… 1a)+(1β‹… 1a)=βˆ’a+a0 = 0 \cdot_1 a = (-1 + 1) \cdot_1 a = (-1 \cdot_1 a) + (1 \cdot_1 a) = -a + a


  • Every contractible magma (M,ΞΌ)(M, \mu) with a function f:Mβ†’Mf:M \to M is an abelian group.

  • The integers are an abelian group.

See also


Revision on May 2, 2022 at 01:45:04 by Anonymous?. See the history of this page for a list of all contributions to it.