Tensor product of cyclic groups

[Alizter]

Now that we have tensor products of abelian groups in #2021, a nice exercise (and something useful for calculations) would be to show that

$$\mathbb{Z}/a\mathbb{Z} \otimes_{\mathbb{Z}} \mathbb{Z}/b\mathbb{Z}\cong \mathbb{Z}/(a,b)\mathbb{Z}$$

For this we will need some improvement to the material we have on cyclic groups. One important thing would be to have a multiplication formula for equivalence classes, i.e. $[xy]_a=[x]_a y$ for integers $x$ and $y$.

Once we have that the proof of the result is very straightforward. We have a bilinear (biadditive) map $f : \mathbb{Z}/a\mathbb{Z} \times \mathbb{Z}/b\mathbb{Z}\to \mathbb{Z}/(a,b)\mathbb{Z}$ given by $f ([x]_a ,[y]_{b})=[xy]_{(a,b)}$ and an inverse map $g : \mathbb{Z}/(a,b)\mathbb{Z} \to \mathbb{Z}/a\mathbb{Z} \otimes_{\mathbb{Z}} \mathbb{Z}/b\mathbb{Z}$ given by $g([x]_{(a,b)})=[x]_a \otimes [1]_b$. We only need show one direction is a homomorphism which seems easiest for $f$. Checking the inverses should then be a straightforward exercise.

[ndcroos]

Hi, I'd like to work on this issue, please.

[Alizter]

@ndcroos Great! I would start with introducing a new version of the cyclic group in AbGroups/Cyclic.v. The definition there is defined as a quotient of the free abelian group on one generator, but we have recently improved our own Int type so we should use that instead.

I think at some point we want to show that abgroup_Z (based on Int) is the free abelian group on one generator, but this is probably not the time to do it. Instead, I would suggest introducing an alternative cyclic' definition defined as the cokernel of the multiplication map which can be found in AbGroups/Z.v. You can just add it to the end of Cyclic.v

If you create a PR for that first, then I can help you set up the statement for this lemma.

Let me know if you need any help.

[ndcroos]

@Alizter A definition of cyclic as the cokernel of the multiplication map seems to be already present in Cyclic.v here:

Coq-HoTT/theories/Algebra/AbGroups/Cyclic.v

Line 78 in f367ba9

(** The [n]-th cyclic group is the cokernel of [Z1_mul_nat n]. *)

I also can't find the cokernel definition in AbGroups/Z.v here: https://github.com/HoTT/Coq-HoTT/blob/master/theories/Algebra/AbGroups/Z.v

[Alizter]

@ndcroos Yes, this is an older definition. There, the integers are defined as a free group on a single element, but this doesn't agree with the integers in Spaces/Int.v. The integers found in AbGroups/Z.v as an abelian group is based on Spaces/Int.v. You will need to define (just under in the file) cyclic' as the cokernel of the multiplication map. The multiplication map is called grp_pow_homo in AbGroups/Z.v, since in multiplicative notation in a group it would be a power, but since we are using additive notation in an abelian group it is a multiple.

The reason I suggest making a new cyclic type is so that you can use existing lemmas about the integers for the main result.

[jdchristensen]

ab_mul n is the thing to use, since it gives a group homomorphism from an abelian group A to itself defined by "multiplication" by n. grp_pow_homo g gives a group homomorphism from the integers to a group G sending n to g to the power n.

[Alizter]

@jdchristensen Yes of course. I'm still managing to get confused which is which. 😅

[Alizter]

The lemma I mentioned at the end of #2050 should look like:

Definition cyclic_in {n : nat} : abgroup_Z $-> cyclic' n
  := grp_quotient_map. 

Definition ab_mul_cyclic_in (n : nat) (x y : abgroup_Z)
  : ab_mul y (@cyclic_in n x) = cyclic_in (x * y)%int.
Proof.

You will need to import QuotientGroup at the top so that you can use grp_quotient_map.

Let me know if you need any hints on how to proceed.

[jdchristensen]

The RHS should be cyclic_in (y * x)%int, to avoid commuting x and y. And I think it's worth giving a hint here that the proof of this lemma just requires two lines, by combining two existing results. And all it uses is that cyclic_in is a group homomorphism with domain the integers. (I'm not sure if we're trying to withhold information here as a teaching mechanism. If not, I'll just give the proof in a comment.)

[jdchristensen]

(BTW, I'm not sure why this lemma is highlighted as the next thing to do...)

[ndcroos]

@jdchristensen you can post the proof in a comment.

I have the following:

Definition ab_mul_cyclic_in (n : nat) (x y : abgroup_Z)
  : ab_mul y (@cyclic_in n x) = cyclic_in (y * x)%int.
Proof.
  unfold cyclic_in.
  exact (ab_mul_natural grp_quotient_map n).
Defined.

Naturalness seems one of the right properties to use.
But I get the error:

In environment
n : nat
x, y : abgroup_Z
The term "grp_quotient_map" has type "?A $-> QuotientGroup ?A ?N"
while it is expected to have type "GroupHomomorphism ?A ?B".

It looks like it's an error in usage and I should find a way to 'convert' the type grp_quotient_map to a GroupHomomorphism.

[jdchristensen]

@ndcroos ab_mul_natural gets you halfway, so that's a good first step. Then you need to use that the ab_mul structure on the integers coincides with ordinary multiplication of integers, which is abgroup_Z_ab_mul.

Definition ab_mul_cyclic_in (n : nat) (x y : abgroup_Z)
  : ab_mul y (@cyclic_in n x) = cyclic_in (y * x)%int.
Proof.
  lhs_V nrapply ab_mul_natural.
  apply ap, abgroup_Z_ab_mul.
Defined.

[Alizter]

Thanks for proving that lemma. I've done some more thinking and partial formalization to see which lemmas about cyclic we will need exactly. I have refined it down to the following list:

1. Recursion principle for cyclic. This should compute definitionally on cyclic_in n k giving grp_pow g k.

Definition cyclic_rec (n : nat) {G : Group} (g : G) (p : grp_pow g n = mon_unit)
  : GroupHomomorphism (cyclic n) G.

2. Induction principle for cyclic landing in a hprop "closed" under negation. The negation requirement comes from the fact that we are using nat and not int for the sections given by H1.

Definition cyclic_ind_hprop (n : nat) (P : cyclic n -> Type)
  `{forall x, IsHProp (P x)}
  (H1 : forall (x : nat), P (cyclic_in n x)) (H2 : forall x, P x -> P (negate x))
  : forall x, P x.

3. Induction principle for cyclic landing in a homotopy of group homomorphisms. This will be a useful lemma as the sections of the equivalence of the tensor of cyclic groups will be of this form. It is a special case of cyclic_ind_hprop.

Definition cyclic_ind_homotopy (n : nat) {G : Group}
  (f g : GroupHomomorphism (cyclic n) G)
  (p : forall (k : nat), f (cyclic_in n k) = g (cyclic_in n k))
  : f == g.

4. A specialised version of cyclic_ind_homotopy for addition of morphisms on the right. This is needed when checking bilinearity of the map from the tensor product.

Definition cyclic_ind_homotopy_op (n : nat) {A : AbGroup}
  (f f' f'' : (cyclic n) $-> A)
  (p : forall (k : nat), f (cyclic_in n k) = f' (cyclic_in n k) + f'' (cyclic_in n k))
  : forall x, f x = f' x + f'' x
  := cyclic_ind_homotopy n _ (ab_homo_add f' f'') p.

Note that ab_homo_add comes from AbGroups.AbHom and unlike cyclic_ind_homotopy, the codomain is now an abelian group instead of a group. Note that you also might have to do Local Open Scope mc_scope and Local Open Scope mc_add_scope at the top of Cyclic.v in order to get the + notation for abelian groups.

5. A lemma showing invariance of cyclic_in under nat_mod.

Definition cyclic_in_mod (n : nat) (x : nat)
  : cyclic_in n x = cyclic_in n (x mod n)%nat.

6. This should allow for the following useful lemma which will appear often in the tensor equivalence:

Definition cyclic_in_divides n m : (n | m)%nat -> cyclic_in n m = mon_unit.

I have the proofs of all these lemmas already, but I thought it would be instructional for you to attempt to prove them yourself. Let me know if you need any hints or if you get stuck. You can do these all in one PR or one-by-one however you like.

[jdchristensen]

@Alizter That's a helpful list. About item 2, the hypothesis H2 shouldn't be needed, since every element of the cyclic group is represented by a natural number. (For example, for any natural number x, [n.+1 * x - x] + [x] equals 0 in cyclic n, where I'm using square brackets for cyclic_in n, so [n.+1 * x - x] represents the negation of [x]. If we know x < n, then [n - x] also works, but the formula I gave should work for all n and x.)

[ndcroos]

@Alizter

• in item 1, 'compute definitionally' means something of the form := ... . ?
• in item 2, are you sure this should be cyclic and not cyclic'?

[Alizter]

@ndcroos When I say "compute definitionally" I mean that if you have a term like cyclic_rec n g p (cyclic_in n k) then this can be reduced to grp_pow g k. You can check this is the case by taking the first term and writing Eval simpl in term. or having a lemma like

Definition cyclic_rec_beta_in (n k : nat) {G : Group} (g : G)
  (p : grp_pow g n = mon_unit)
  : cyclic_rec n g p (cyclic_in n k) = grp_pow g k
  := idpath.

And yes, I am talking about cyclic since cyclic' replaced it in #2053.

[ndcroos]

@Alizter for item 1, I have for the first line:
snrapply Build_GroupHomomorphism.
Is this correct?

[Alizter]

You can use grp_quotient_map to create the homomorphism out of a quotient. You will just have to show that the map is well defined w.r.t equivalence classes which is what p will ensure.

[ndcroos]

This is what I have at the moment for item 1. However, it doesn't use grp_quotient_map. (I also needed to add ``{Funext}`).

(** Recursion principle for `cyclic`. *)
Definition cyclic_rec `{Funext} (n : nat) {G : Group} (g : G) (p : grp_pow g n = mon_unit)
  : GroupHomomorphism (cyclic n) G.
Proof.
  snrapply Build_GroupHomomorphism.
  1: trivial.
  1: unfold IsSemiGroupPreserving.
  intros x1 x2.
  unfold sg_op.
  induction n.
  - simpl.
Defined.

1 goal
H : Funext
G : Group
g : G
p : grp_pow g 0%nat = mon_unit
x1, x2 : cyclic 0
______________________________________(1/1)
g = group_sgop g g

It seems like one should find a way to use p to prove the goal.
The goal is essentially to prove g = g * g
p states that g^n = mon_unit
Using this assumption, one can rewrite g^n in terms of mon_unit.
Can you give some hints for item 1? Should I use induction?

[Alizter]

When you create a group homomorphism, the first goal will be the underlying map. For that, you have used trivial which typically does reflexivity, intros behind the scenes. Using trivial for this goal is not a good idea as it is not obvious what the term should be. The goal looks like cyclic n -> G and trivial ends up proving the goal G using the available term g : G that we have. If you think about this, you will not be able to show this is a group homomorphism as you just have a constant map at the element g. For instance, group homomorphisms should preserve the group unit, but cyclic_in n 0 : cyclic n will be mapped to g : G rather than mon_unit : G. If you want to see exactly the terms constructed from the goals so far you can use Show Proof.

It's maybe best to take a step back and explain what we are trying to construct with cyclic_rec. The idea is that all elements of the cyclic group are some power of a generator (if you are thinking additively, then they are all some multiple of a generator). Knowing that group homomorphisms preserve powers, we see that we only need to specify how our homomorphism acts on the generator of the cyclic group, this is g : G and if it satisfies the same equations as the generator of the cyclic group, this is p : grp_pow g n = mon_unit. The generator of the cyclic group is cyclic_in n 1%nat. So we are asking for a group homomoprhism such that grp_pow (f (cyclic_in n 1%nat)) n.

My suggestion to use grp_quotient_rec. When you use it, Coq will ask for abgroup_Z $-> G which is a map we already have, look in AbGroups/Z.v.

The second part will be to show that the equivalence class is respected. To see the goal more clearly, we need to import some more things which are available (from the transitive nature of Require) but we just haven't imported the modules. If you add Basics.Trunc to see truncation levels more clearly and Truncations.Core to see the truncation type, together with simpl you will see that the goal looks like

forall n0 : Int, Tr (-1) {a : Int & grp_pow a n = n0} -> grp_pow g n0 = mon_unit

Introducing two hypotheses, the second hypothesis will look like y : Tr (-1) ... which you can't do anything until you "strip" the truncation off of the term. In order to do this we have a tactic strip_truncations which will turn this into y : .... Behind the scenes it is just applying Trunc_ind.

Now you should have all the pieces that you need to show the final goal.

[Alizter]

@ndcroos Also, the fact that you had to add funext, indicates that you still have the old cyclic around. I'm guessing you've already rebased, so make sure you've recompiled the library with the new updates. CoqIDE is likely finding the old compiled files and giving you the old definition.

[ndcroos]

For (1), I have now:

(** Recursion principle for `cyclic`. *)

Definition cyclic_rec (n : nat) {G : Group} (g : G) (p : grp_pow g n = mon_unit)
  : GroupHomomorphism (cyclic n) G.
Proof.
  snrapply grp_quotient_rec.
  1: apply grp_pow_homo; assumption.
  1: simpl. 
  intros x y.
  strip_truncations.
  destruct y as [a H].
Defined.

And

1 goal
n : nat
G : Group
g : G
p : grp_pow g n = mon_unit
x, a : Int
H : grp_pow a n = x
______________________________________(1/1)
grp_pow g x = mon_unit

The proof p is for n : nat, while the goal is for x : Int.

For (2), I have a somewhat similar issue:

(** Induction principle for `cyclic`. *)
Definition cyclic_ind_hprop (n : nat) (P : cyclic n -> Type)
  `{forall x, IsHProp (P x)}
  (H1 : forall (x : nat), P (cyclic_in n x))
  : forall x, P x.
Proof.
  srapply grp_quotient_ind_hprop.
  unfold cyclic_in in H1.
Defined.

And

1 goal
n : nat
P : cyclic n -> Type
H : forall x : cyclic n, IsHProp (P x)
H1 : forall x : nat, P (grp_quotient_map x)
______________________________________(1/1)
forall x : abgroup_Z, P (grp_quotient_map x)

H1 is for x : nat, while the goal is for x : abgoup_Z.

[Alizter]

For (1), you are on the right track. Recall that H : grp_pow a n is definitionally equal to ab_mul n a. Therefore you can use

change (ab_mul n a) in H.

to write it that way. Now see if you can use rewrite and abgroup_Z_ab_mul to turn q into an equation that can be used to rewrite x in the goal.

At that point, we should notice we need one of the lemmas in #2015. So it would be good to address that issue too.

[Alizter]

For (2), I would suggest that you continue with my proposal with H2. What @jdchristensen suggests will work when n >= 1 however when n = 0 we should get the integers again rather than any finite cyclic group. In this case it is not immediately clear that we can drop H2. Let's leave the question of if H2 can be dropped to a later date as it shouldn't affect anything else we want to do here.

[jdchristensen]

Yes, @Alizter is right that H2 will be needed if n = 0. So it's probably best to just keep it in general. We could have a variant that works with cyclic n.+1 and avoids the H2 hypothesis, but that's a separate thing that can be done later if needed. Sorry for introducing some confusion here!

[ndcroos]

@Alizter and @jdchristensen, thanks both for your feedback. I am going to try to address also #2015.

[Alizter]

@ndcroos I think it would be best if you addressed that in its own PR. For the record, I did #2054 but closed it because it should follow what was outlined in #2015.

[ndcroos]

@Alizter For (1) I get the follow error:

In environment
n : nat
G : Group
g : G
p : grp_pow g n = mon_unit
x, a : Int
H : grp_pow a n = x
The term "a" has type "Int"
while it is expected to have type
 "group_type ?A".

For:

(** Recursion principle for `cyclic`. *)
Definition cyclic_rec (n : nat) {G : Group} (g : G) (p : grp_pow g n = mon_unit)
  : GroupHomomorphism (cyclic n) G.
Proof.
  snrapply grp_quotient_rec.
  1: apply grp_pow_homo; assumption.
  1: simpl. 
  intros x y.
  strip_truncations.
  destruct y as [a H].
  change (ab_mul n a) in H.

[Alizter]

You need to help Coq along a little. It doesn't see that Int is the underlying type of a group, so you need to write (a : abgroup_Z) instead.

[ndcroos]

What is the correct way to do such a type conversion in this case? I tried to do something like this:

Definition int_to_abgroup_Z (a : Int) : abgroup_Z := a.

Definition cyclic_rec (n : nat) {G : Group} (g : G) (p : grp_pow g n = mon_unit)
  : GroupHomomorphism (cyclic n) G.
  ... (previous code)
  destruct y as [a H].
  set (a' := int_to_abgroup_Z a).
  change (ab_mul n a') in H.

Sorry for the late response.

[Alizter]

You can write change abgroup_Z in a. before you use a or you can cast it by writing (ab_nul n (a : abgroup_Z)).

[ndcroos]

Thanks. I get the error Not a type. for both variants. I have not been able to resolve this.

[Alizter]

Here is my proof for you to compare with:

Click me

Definition cyclic_rec' (n : nat) {G : Group} (g : G) (p : grp_pow g n = mon_unit)
  : GroupHomomorphism (cyclic n) G.
Proof.
  snrapply grp_quotient_rec.
  1: snrapply (grp_pow_homo g).
  intros x.
  apply Trunc_rec.
  intros [y q].
  rewrite abgroup_Z_ab_mul in q.
  destruct q.
  simpl.
  lhs nrapply grp_pow_int_mul.
  rewrite p.
  apply grp_pow_unit.
Defined.

You're welcome to ask me any questions about why I've done things this way. You can see why I asked you to prove the laws in #2015 before.

[ndcroos]

@Alizter I have been quiet here the last few weeks, but this weekend I have time to attempt the remaining items in the list.

Edit: I did not have time this weekend, but starting from the beginning of November I should have time then.

[Alizter]

@ndcroos Did you get another chance to look at this? Is there anything I can help with?