[Merged by Bors] - feat(Algebra/Ring/Ext): prove extensionality lemmas for Ring and similar typeclasses #9511
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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`.
eric-wieser
reviewed
Jan 8, 2024
Vierkantor
added
the
awaiting-author
Co-authored-by: Anne Baanen <[email protected]>
WARNING: this commit is NOT error-free.
WARNING: this commit is NOT error-free.
WARNING: this commit is NOT error-free.
raghuram-13
added
awaiting-review
and removed
awaiting-author
Vierkantor
approved these changes
Apr 22, 2024
|
✌️ raghuram-13 can now approve this pull request. To approve and merge a pull request, simply reply with |
Vierkantor
changed the title
Ring and similar typeclassesBased on review suggestions https://github.com/leanprover-community/mathlib4/pull/9511/files#r1574231108, https://github.com/leanprover-community/mathlib4/pull/9511/files#r1574232858. Co-authored-by: Anne Baanen <[email protected]>
|
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.
|
Build failed: |
Specifically, replace `← Int.coe_nat_eq` with `Int.ofNat_eq_coe`.
|
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.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
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
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Add a file
Algebra/Ring/Ext, provingextlemmas for all of the ring-like classes (for example, anything fromNonUnitalNonAssocSemiringtoCommRing), stating that two instances of such a class are equal if they define the same addition and multiplication operations.Also prove
ext_iffvariants 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:
HasDistribNeg.Commvariants (currently it's just fromCommvariant to non-Commvariant for each).A natural next step would be to extend this to
DivisionSemiring,DivisionRing,SemifieldandField.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
extandext_ifflemmas, eliminating even more boilerplate.It should be possible to extend that command to be more general (such as allowing
declModifiersandterminationSuffixclauses, allowing a custom theorem name defaulting toext, 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.