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

[Merged by Bors] - feat(Algebra/Ring/Ext): prove extensionality lemmas for Ring and similar typeclasses #9511

Closed
wants to merge 43 commits into from

Conversation

raghuram-13
Copy link
Collaborator

@raghuram-13 raghuram-13 commented Jan 7, 2024

Add a file Algebra/Ring/Ext, proving ext lemmas for all of the ring-like classes (for example, anything from NonUnitalNonAssocSemiring to CommRing), stating that two instances of such a class are equal if they define the same addition and multiplication operations.
Also prove ext_iff variants for each class, and injectivity lemmas for projections from classes to parent classes.


Some notes:

  • Things I didn't do because they don't seem particularly necessary:

    • I skipped HasDistribNeg.
    • More injectivity lemmas could be proved between the Comm variants (currently it's just from Comm variant to non-Comm variant for each).
  • A natural next step would be to extend this to DivisionSemiring, DivisionRing, Semifield and Field.

  • I have introduced local notation to eliminate some boilerplate. I'm not sure if this is style-appropriate for Mathlib (although the notation is local to one file and (probably) never shows up when e.g. the types of lemmas are viewed, so that it's invisible to anyone not editing this file).

  • In another branch, I have used a (local) custom command to generate the ext and ext_iff lemmas, eliminating even more boilerplate.

    It should be possible to extend that command to be more general (such as allowing declModifiers and terminationSuffix clauses, allowing a custom theorem name defaulting to ext, specifying the type for which an ext lemma is being proved, specifying the arguments, and letting the names be inaccessible by default while allowing them to be specified with a "with" clause), in which case it could become a useful command for writing extensionality lemmas (admittedly partially overlapping in functionality with putting an @[ext] on the type definition).

  • I haven't written any tests — I'm not sure what to test or how to write tests.

Open in Gitpod

This is based on discussion in the Zulip thread
https://leanprover.zulipchat.com/stream/287929-mathlib4/topic/Ring.20is.20determined.20by.20Semiring.

Note that this commit introduce `sorry`s into the codebase. It is a WIP.
Prove `Semiring.ext` and `Semiring.ext_iff` lemmas, as well as that
`Semiring.toNonUnitalSemiring` and `Semiring.toNonAssocSemiring` are
injective.
Prove the injectivity lemma in terms of the `ext` lemma, as the former
goes through showing that `h_add` and `h_mul` hold anyway.
Prove that `NonAssocSemiring.toNonUnitalNonAssocSemiring` is
injective.
Prove an `ext` lemma and use it to show that
`NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` is injective as
well as an `ext_iff` lemma.
…emiring`

Show that `NonUnitalNonAssocSemiring.toDistrib` is injective.
One exception: leave the `h` in `fun h ↦` in `ext_iff` proofs,
for (marginally) more readability.
Prove that `Semiring.toNonAssocSemiring` is injective.
For each of the three typeclasses, state the `ext` lemma with a
sorried proof and prove the consequences (injectivity and `ext_iff`
lemmas).
Highlight the locations in the file where something mathematically
non-trivial is proved: namely that some operation is determined by
others. (There are essentially only two such.)
Change `a`, `b` to `x`, `y` in accordance with
https://leanprover-community.github.io/contribute/style.html#variable-conventions.

Additionally, remove an unnecessary `'` from a variable `inst`.
@Vierkantor Vierkantor added the awaiting-author A reviewer has asked the author a question or requested changes label Mar 28, 2024
@raghuram-13 raghuram-13 added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 8, 2024
Copy link
Contributor

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

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

Sorry for the late response, this dropped somewhat off my radar. The code looks good to me. Still have some small remarks about the comments.

bors d+

Mathlib/Algebra/Ring/Ext.lean Show resolved Hide resolved
Mathlib/Algebra/Ring/Ext.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/Ring/Ext.lean Outdated Show resolved Hide resolved
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Apr 22, 2024

✌️ raghuram-13 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@Vierkantor Vierkantor changed the title Prove extensionality lemmas for Ring and similar typeclasses feat(Algebra/Ring/Ext): prove extensionality lemmas for Ring and similar typeclasses Apr 22, 2024
@raghuram-13
Copy link
Collaborator Author

bors r+

mathlib-bors bot pushed a commit that referenced this pull request May 9, 2024
…lar typeclasses (#9511)

Add a file `Algebra/Ring/Ext`, proving `ext` lemmas for all of the ring-like classes (for example, anything from `NonUnitalNonAssocSemiring` to `CommRing`), stating that two instances of such a class are equal if they define the same addition and multiplication operations.
Also prove `ext_iff` variants for each class, and injectivity lemmas for projections from classes to parent classes.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 9, 2024

Build failed:

@raghuram-13
Copy link
Collaborator Author

bors r+

mathlib-bors bot pushed a commit that referenced this pull request May 9, 2024
…lar typeclasses (#9511)

Add a file `Algebra/Ring/Ext`, proving `ext` lemmas for all of the ring-like classes (for example, anything from `NonUnitalNonAssocSemiring` to `CommRing`), stating that two instances of such a class are equal if they define the same addition and multiplication operations.
Also prove `ext_iff` variants for each class, and injectivity lemmas for projections from classes to parent classes.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 9, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Ring/Ext): prove extensionality lemmas for Ring and similar typeclasses [Merged by Bors] - feat(Algebra/Ring/Ext): prove extensionality lemmas for Ring and similar typeclasses May 9, 2024
@mathlib-bors mathlib-bors bot closed this May 9, 2024
@mathlib-bors mathlib-bors bot deleted the raghuram-13/ext-for-rings branch May 9, 2024 04:39
apnelson1 pushed a commit that referenced this pull request May 12, 2024
…lar typeclasses (#9511)

Add a file `Algebra/Ring/Ext`, proving `ext` lemmas for all of the ring-like classes (for example, anything from `NonUnitalNonAssocSemiring` to `CommRing`), stating that two instances of such a class are equal if they define the same addition and multiplication operations.
Also prove `ext_iff` variants for each class, and injectivity lemmas for projections from classes to parent classes.
callesonne pushed a commit that referenced this pull request May 16, 2024
…lar typeclasses (#9511)

Add a file `Algebra/Ring/Ext`, proving `ext` lemmas for all of the ring-like classes (for example, anything from `NonUnitalNonAssocSemiring` to `CommRing`), stating that two instances of such a class are equal if they define the same addition and multiplication operations.
Also prove `ext_iff` variants for each class, and injectivity lemmas for projections from classes to parent classes.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
delegated new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

9 participants