Code

tensor products of abelian groups#2021

Code

Merged

Alizter merged 45 commits intoHoTT:masterHoTT/Coq-HoTT:masterfrom Alizter:ab-tensorAlizter/HoTT:ab-tensorCopy head branch name to clipboardJul 22, 2024

+1,110-248

Commits

Commits on Jul 11, 2024

• grp_pow_commutes

  Show description for 3c6ad57
  Alizter

  committed
  3c6ad57

  Copy full SHA for 3c6ad57

• tensor products of abelian groups

  Show description for d58355b
  Alizter

  committed
  d58355b

  Copy full SHA for d58355b

• more comments and simplify some proofs

  Show description for 5b89691
  Alizter

  committed
  5b89691

  Copy full SHA for 5b89691

• add universal property

  Show description for b733df5
  Alizter

  committed
  b733df5

  Copy full SHA for b733df5

Commits on Jul 12, 2024

• TensorProduct: fix typos in comments

  jdchristensen

  committed
  f9c589c

  Copy full SHA for f9c589c

• TensorProduct: drop (P 0) from induction principles

  jdchristensen

  committed
  df441c6

  Copy full SHA for df441c6

Commits on Jul 13, 2024

• Abelianization: rename ab map to abel_in

  Show description for 87afe85
  Alizter

  committed
  87afe85

  Copy full SHA for 87afe85

• fix abel_in negation lemma usage

  Show description for 4c9a8d2
  Alizter

  committed
  4c9a8d2

  Copy full SHA for 4c9a8d2

• Abelianization: inline proof of abel_unit

  jdchristensen

  committed
  4f84baf

  Copy full SHA for 4f84baf

• simplify induction principles

  Show description for 82b0feb
  Alizter

  committed
  82b0feb

  Copy full SHA for 82b0feb

• remove unneeded lemma

  Show description for b63352a
  Alizter

  committed
  b63352a

  Copy full SHA for b63352a

• small simplifications

  Show description for 5dee8c1
  Alizter

  committed
  5dee8c1

  Copy full SHA for 5dee8c1

• simplify induction hypothesis to +

  Show description for 8b88d03
  Alizter

  committed
  8b88d03

  Copy full SHA for 8b88d03

• cleanup names

  Show description for 08a26b1
  Alizter

  committed
  08a26b1

  Copy full SHA for 08a26b1

• TensorProduct: simplify proof of induction principle

  jdchristensen

  committed
  edc74fa

  Copy full SHA for edc74fa

• fix typo

  Show description for 9373e4d
  Alizter

  committed
  9373e4d

  Copy full SHA for 9373e4d

• TensorProduct: update comments

  jdchristensen

  committed
  baa3a89

  Copy full SHA for baa3a89

• Add grp_homo_op_agree, and use it in many places

  jdchristensen

  committed
  920db0c

  Copy full SHA for 920db0c

• TensorProduct: factor out defn of bilinear pairs to make goals small

  jdchristensen

  committed
  ee4daf5

  Copy full SHA for ee4daf5

Commits on Jul 16, 2024

• Simplifications involving grp_pow and ab_mul

  jdchristensen

  committed
  4758acc

  Copy full SHA for 4758acc

Commits on Jul 17, 2024

• Merge branch 'master' into ab-tensor

  Alizter

  authored
  4001f97

  Copy full SHA for 4001f97

• fix arguments of grp_homo_map

  Show description for 42207b7
  Alizter

  committed
  42207b7

  Copy full SHA for 42207b7

• bilinear -> biadditive for consistency

  Show description for 4d246eb
  Alizter

  committed
  4d246eb

  Copy full SHA for 4d246eb

Commits on Jul 18, 2024

• TensorProduct, QuotientGroup: some speed-ups

  jdchristensen

  committed
  5873da3

  Copy full SHA for 5873da3

• stagger definition of twist

  Show description for d5ba157
  Alizter

  committed
  d5ba157

  Copy full SHA for d5ba157

• simpl arg hint for ab_tensor_prod_twist_map

  Show description for afac23b
  Alizter

  committed
  afac23b

  Copy full SHA for afac23b

Commits on Jul 19, 2024

• make FreeGroup_rec o freegroup_in definitionally the identity

  Show description for 5b06920
  Alizter

  committed
  5b06920

  Copy full SHA for 5b06920

• FreeGroup, TensorProduct: some cleanups

  jdchristensen

  committed
  1589b71

  Copy full SHA for 1589b71

• remove reduction rules as they are definitional

  Show description for 0a58839
  Alizter

  committed
  0a58839

  Copy full SHA for 0a58839

• cleanup in FreeGroup.v

  Show description for 67e9b6c
  Alizter

  committed
  67e9b6c

  Copy full SHA for 67e9b6c

• add comment about words_rec

  Show description for 1d49f73
  Alizter

  committed
  1d49f73

  Copy full SHA for 1d49f73

• remove exact idpath

  Show description for 7c74b6e
  Alizter

  committed
  7c74b6e

  Copy full SHA for 7c74b6e

Commits on Jul 20, 2024

• FreeGroup: use a instead of x for a "letter" in A + A

  jdchristensen

  committed
  7ddd945

  Copy full SHA for 7ddd945

• use more list operations in FreeGroup.v

  Show description for 46c1bf0
  Alizter

  committed
  46c1bf0

  Copy full SHA for 46c1bf0

• write a little intro for tensor products

  Show description for e2f8d74
  Alizter

  committed
  e2f8d74

  Copy full SHA for e2f8d74

• small changes to comments

  Show description for f2c9ec7
  Alizter

  committed
  f2c9ec7

  Copy full SHA for f2c9ec7

• TensorProduct: update introductory comments

  jdchristensen

  committed
  1b5da89

  Copy full SHA for 1b5da89

Commits on Jul 22, 2024

• premetric.v: get rid of shadowed definition of uncurry

  jdchristensen

  committed
  b687878

  Copy full SHA for b687878

• fix typo

  Show description for a6873f0
  Alizter

  committed
  a6873f0

  Copy full SHA for a6873f0

• TensorProduct: simplify and/or speed up some proofs

  jdchristensen

  committed
  da27427

  Copy full SHA for da27427

• TensorProduct.v: updates to comments

  jdchristensen

  committed
  25a60a4

  Copy full SHA for 25a60a4

• Abelianization.v: minor stylistic changes

  jdchristensen

  committed
  aed0f0d

  Copy full SHA for aed0f0d

• TensorProduct: speed up some *ind_hprop* lines

  jdchristensen

  committed
  49c2b7e

  Copy full SHA for 49c2b7e

• remove redundant quotient_abgroup_map

  Show description for a2f3382
  Alizter

  committed
  a2f3382

  Copy full SHA for a2f3382

• fix wording in comment

  Show description for ade3c43
  Alizter

  committed
  ade3c43

  Copy full SHA for ade3c43