replace cyclic with cyclic'

[Alizter]

Actually, I misremembered. We don't use cyclic anywhere, so we are free to rename it. I was confused instead with the definition of the integers as a free group.

Fix #2051.

At some point we should move this definition of the integers to its own file or replace it. I opt for moving it since it is still of interest.

cc @ndcroos in case you are rebasing

[Alizter]

I wonder if while we are at it we might rename abgroup_Z to ab_Z and cyclic to ab_cyclic?

[jdchristensen]

I think we should use the same model for the infinite cyclic group as for its finite quotients. So if we want the new definition of cyclic n using abgroup_Z to be the official one, then we also should move Z1 out of the file Cyclic.v. Alternatively, the file could contain both definitions, one primed. But this PR leaves things in a mixed state.

[jdchristensen]

Maybe Z1 should be moved to Z.v as an alternate definition of the integers, with a TODO to prove that it is isomorphism to abgroup_Z? Edit: Then Cyclic.v could be focused on the finite cyclic groups, just using the new definition.

[Alizter]

I've moved the free group integer construction to FreeInt.v. Cylic.v looks a bit bare for now, but we will soon add lots of lemmas in other PRs.

[jdchristensen]

It shouldn't be hard to switch this file to use the new definition of cyclic groups. Do we know that multiplication by a non-zero integer is an injective map? And that the integers are projective? (Both regarding Spaces.Int.)

[Alizter]

I think I will leave this to a later cleanup. We are redefining cyclic' here using ab_cokernel_embedding. The cleanup in #2035 should clean up this situation, afterwards it would make sense to switch to cyclic.

[jdchristensen]

We should be able to define cyclic in this file using ab_cokernel_embedding as well. Is the fact that multiplication by a non-zero integer is an embedding already in the library? I don't see it, so that could be another "first issue" goal.

[Alizter]

We have it for nat but not for Int.

[jdchristensen]

I wonder if while we are at it we might rename abgroup_Z to ab_Z and cyclic to ab_cyclic?

We have other examples like abgroup_vector and abgroup_matrix, so maybe abgroup_Z is best? And maybe cyclic should be abgroup_cyclic?

[Alizter]

I think I'll hold off on any renaming. I like cyclic since it is short and otherwise it gets too verbose. Later we will have things like cyclic_ind_homotopy so you can see how sticking abgroup will get old quickly.