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

finite sums of ring elements #1959

Merged
merged 3 commits into from
May 18, 2024
Merged

finite sums of ring elements #1959

merged 3 commits into from
May 18, 2024

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented May 14, 2024

In this PR we define finite sums of ring elements and prove some basic properties about them. We also introduce the Kronecker delta function and prove some standard results about its interaction with sums.

Depends on #1956.

@Alizter Alizter marked this pull request as draft May 14, 2024 16:04
@Alizter Alizter mentioned this pull request May 17, 2024
Alizter added 2 commits May 18, 2024 01:39

Unverified

This commit is not signed, but one or more authors requires that any commit attributed to them is signed.
Signed-off-by: Ali Caglayan <[email protected]>
@Alizter
Copy link
Collaborator Author

Alizter commented May 18, 2024

I've rebased and split off the Kronecker delta stuff, generalising it to an arbitrary decidable type where applicable. I'll see about moving things about sums to abelian groups.

@Alizter Alizter marked this pull request as ready for review May 18, 2024 00:55
@Alizter
Copy link
Collaborator Author

Alizter commented May 18, 2024

@jdchristensen I've generalised sums from rings to abelian groups. However when the sum takes place in a ring, I've kept the lemma names as rng_sum. We could specialise ab_sum to rings with rng_sum however it doesn't seem to be a big issue reusing it for now.

@Alizter Alizter requested a review from jdchristensen May 18, 2024 16:49
@jdchristensen
Copy link
Collaborator

This looks better. It's actually possible to get rid of the ring assumption for most of the material on the Kronecker delta. It could be defined to land in nat, and then we could use the fact that in any abelian group you can multiply by a natural number (which we write as grp_pow). Also, there should be a coercion from nat to any ring R, and applying the coercion followed by multiplying in R is the same as grp_pow in the underlying abelian group. So then we'd be able to use lemmas like rng_sum_kronecker_delta_l in any abelian group. But maybe this would just make practical usage of this trickier?

@jdchristensen
Copy link
Collaborator

Feel free to either merge as is, or to try changing the Kronecker delta to land in nat, whichever you prefer.

@Alizter
Copy link
Collaborator Author

Alizter commented May 18, 2024

I'll leave generalising the Kronecker delta to a future PR. The only application I have in mind for this currently is for the identity matrix in #1965. The sum identities here allow us to show the identity matrix is a left and right identity.

@Alizter Alizter merged commit 34fa1d8 into HoTT:master May 18, 2024
23 checks passed
@Alizter Alizter deleted the finite-sums branch May 18, 2024 21:15
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.

2 participants