Homotopy Type Theory abelian group > history (changes)

Showing changes from revision #16 to #17: Added | Removed | Changed

Definition

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 is the type Aut(Aut(G))\mathrm{Aut}(\mathrm{Aut}(G)) of automorphisms of automorphisms in GG.

As a group

An abelian group consists of

  • A type GG,
  • A basepoint e:Ge:G
  • A binary operation μ:GGG\mu : G \to G \to G
  • A unary operation ι:GG\iota: G \to G
  • A left unit identity
    c λ: a:Gμ(e,a)=ac_\lambda:\prod_{a:G} \mu(e,a)=a
  • A right unit identity
    c ρ: a:Gμ(a,e)=ac_\rho:\prod_{a:G} \mu(a,e)=a
  • A associative identity
    c α: a:G b:G c:Gμ(μ(a,b),c)=μ(a,μ(b,c))c_\alpha:\prod_{a:G} \prod_{b:G} \prod_{c:G} \mu(\mu(a, b),c)=\mu(a,\mu(b,c))
  • A left inverse identity
    c l: a:Gμ(ι(a),a)=ec_l:\prod_{a:G} \mu(\iota(a), a)=e
  • A right inverse identity
    c r: a:Gμ(a,ι(a))=ec_r:\prod_{a:G} \mu(a,\iota(a))=e
  • A commutative identity
    c κ: a:A b:Aμ(a,b)=μ(b,a)c_\kappa:\prod_{a:A} \prod_{b:A} \mu(a, b)=\mu(b, a)
  • A 0-truncator
    τ 0: a:A b:A c:(a=b) d:(a=b)c=d\tau_0: \prod_{a:A} \prod_{b:A} \prod_{c:(a = b)} \prod_{d:(a = b)} c = d

Examples

See also

References

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