Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

free abelian groups take products to tensor products #2068

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented Aug 30, 2024

We show that the tensor product of free abelian groups is the free abelian group on the cartesian product of the generating sets.

The proof could be prettier. It was quite difficult to get right due to the subtle distinction between Hom (A:=Group) and Hom (A:=AbGroup).

Verified

This commit was signed with the committer’s verified signature.
Alizter Ali Caglayan
<!-- ps-id: eb86e734-3b10-4189-90f0-3ee3047f1b25 -->

Signed-off-by: Ali Caglayan <[email protected]>
@Alizter Alizter requested a review from jdchristensen August 30, 2024 10:00
Definition equiv_ab_tensor_prod_freeabgroup X Y
: FreeAbGroup (X * Y) $<~> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y).
Proof.
srefine (let f:=_ in let g:=_ in cate_adjointify f g _ _).
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This trick avoids needing to state the types of f and g, but still makes them available for use later.

@jdchristensen
Copy link
Collaborator

The proof could be prettier. It was quite difficult to get right due to the subtle distinction between Hom (A:=Group) and Hom (A:=AbGroup).

Yes, it would be nice if there was an easier way to handle that...

Verified

This commit was signed with the committer’s verified signature.
Alizter Ali Caglayan
Signed-off-by: Ali Caglayan <[email protected]>
@Alizter Alizter merged commit 7f008c7 into HoTT:master Sep 6, 2024
20 checks passed
@Alizter Alizter deleted the ps/rr/free_abelian_groups_take_products_to_tensor_products branch September 6, 2024 22:52
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants