free abelian groups #2020
free abelian groups #2020
Conversation
Signed-off-by: Ali Caglayan <[email protected]> <!-- ps-id: 12288780-47db-4924-a830-f1ece95f8878 -->
|
I've noticed that in |
| Definition isequiv_group_precomp_isabelianization `{Funext} | ||
| {G : Group} {G_ab : AbGroup} (eta : GroupHomomorphism G G_ab) | ||
| `{!IsAbelianization G_ab eta} (A : AbGroup) | ||
| : IsEquiv (group_precomp A eta). | ||
| Proof. | ||
| snrapply isequiv_adjointify. | ||
| - intros g. | ||
| rapply (surjinj_inv (group_precomp A eta) g). | ||
| - intros f. | ||
| snrapply equiv_path_grouphomomorphism. | ||
| exact (eisretr0gpd_inv (group_precomp A eta) f). | ||
| - intros f. | ||
| snrapply equiv_path_grouphomomorphism. | ||
| exact (eissect0gpd_inv (group_precomp A eta) f). | ||
| Defined. |
There was a problem hiding this comment.
The proof of this looks like it can be abstracted out as a general lemma. Maybe it would say something like: If A is a wild category with MorExt and f : Hom a b -> Hom c d is a map of zero groupoids that satisfies IsSurjInj, then it is an equivalence on the underlying types?
But really it should be a bit more general. We could say that a zero groupoid is "extensional" if the 1-cells are equivalent to the paths in the underlying type. Then the lemma would say that if G and H are extensional zero groupoids and f : G -> H is a map of zero groupoids that satisfies IsSurjInj, then it is an equivalence on the underlying types. And we'd have a typeclass instance that says that if A is a wild category that satisfies MorExt, then its Hom zero groupoids are extensional.
(I'm not sure if "extensional" is the right word. It's vague.)
There was a problem hiding this comment.
Alternatively, we wouldn't need this at all if we removed funext from the free group universal property. I haven't had a look at that in detail yet.
|
This PR is fairly short and sweet (and I just pushed a commit making it a bit shorter), so I'm ok with merging it and leaving the cleanup of Funext for a future PR. My comment above could also be left as a TODO item in the file, or could be handled. I'm fine either way. |
In this PR we:
This construction will be important in the theory of modules as we will be taking quotients of free abelian groups to produce constructions such as tensor products of abelian groups.
I had a bit of trouble managing funext. I tried to see if it was possible to stay funext free but I didn't see a way.
Classically, the free abelian group is defined as a fucntion from the generating set into Z together with a finite support. This definition is very appealing for us but would also require a lot of funext in order to equate terms. It is also not clear how to constructively reason about finite supports as their definition contains an awkward negation that means basic lemmas require decidablility or LEM in general.