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: TwoUniqueProds #7169
Conversation
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
This PR/issue depends on:
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Very nice! I left just a couple of small comments.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
+ Introduce `TwoUniqueProds/Sums`: let `R[G]` be a monoid algebra over a semiring `R` without zero-divisors. A natural sufficient condition for `R[G]` to have no zero-divisors is that `G` has `UniqueProds`, as is shown by [MonoidAlgebra.instNoZeroDivisorsOfUniqueProds](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.html#MonoidAlgebra.instNoZeroDivisorsOfUniqueProds). Similarly, a natural sufficient condition for `R[G]` to have only trivial units (of the form `rg` with `r` a unit in `R` and `g` a unit in `G`) is that `G` has `TwoUniqueProds`, but we don't prove this yet in this PR. `TwoUniqueProds G` is also a natural sufficient condition in order for factors of a homogeneous element in an algebra graded by `G` without zero-divisors to themselves be homogeneous. + Show `TwoUniqueProds` implies `UniqueProds`: `TwoUniqueProds.toUniqueProds` + Strengthen `of_Covariant_right/left` to have `TwoUniqueProds` as conclusion + Extract `of_image_filter` from the proof of the instance `UniqueProds (∀ i, G i)` and use it also in the proof of `TwoUniqueProds (∀ i, G i)` + Use some private defs (starting from `private abbrev I`) to transfer `(Two)UniqueProds (∀ i, G i)` instances to `(Two)UniqueProds (G × H)` + Move the `[Module ℚ G] : UniqueSums G` instance from NoZeroDivisors.lean to UniqueProds.lean and strengthen to `TwoUniqueSums` New lemmas about UniqueMul: + `of_card_le_one`, `iff_card_le_one`, `UniqueMul_of_TwoUniqueMul` Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
+ Introduce `TwoUniqueProds/Sums`: let `R[G]` be a monoid algebra over a semiring `R` without zero-divisors. A natural sufficient condition for `R[G]` to have no zero-divisors is that `G` has `UniqueProds`, as is shown by [MonoidAlgebra.instNoZeroDivisorsOfUniqueProds](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.html#MonoidAlgebra.instNoZeroDivisorsOfUniqueProds). Similarly, a natural sufficient condition for `R[G]` to have only trivial units (of the form `rg` with `r` a unit in `R` and `g` a unit in `G`) is that `G` has `TwoUniqueProds`, but we don't prove this yet in this PR. `TwoUniqueProds G` is also a natural sufficient condition in order for factors of a homogeneous element in an algebra graded by `G` without zero-divisors to themselves be homogeneous. + Show `TwoUniqueProds` implies `UniqueProds`: `TwoUniqueProds.toUniqueProds` + Strengthen `of_Covariant_right/left` to have `TwoUniqueProds` as conclusion + Extract `of_image_filter` from the proof of the instance `UniqueProds (∀ i, G i)` and use it also in the proof of `TwoUniqueProds (∀ i, G i)` + Use some private defs (starting from `private abbrev I`) to transfer `(Two)UniqueProds (∀ i, G i)` instances to `(Two)UniqueProds (G × H)` + Move the `[Module ℚ G] : UniqueSums G` instance from NoZeroDivisors.lean to UniqueProds.lean and strengthen to `TwoUniqueSums` New lemmas about UniqueMul: + `of_card_le_one`, `iff_card_le_one`, `UniqueMul_of_TwoUniqueMul` Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Introduce
TwoUniqueProds/Sums
: letR[G]
be a monoid algebra over a semiringR
without zero-divisors. A natural sufficient condition forR[G]
to have no zero-divisors is thatG
hasUniqueProds
, as is shown by MonoidAlgebra.instNoZeroDivisorsOfUniqueProds. Similarly, a natural sufficient condition forR[G]
to have only trivial units (of the formrg
withr
a unit inR
andg
a unit inG
) is thatG
hasTwoUniqueProds
, but we don't prove this yet in this PR.TwoUniqueProds G
is also a natural sufficient condition in order for factors of a homogeneous element in an algebra graded byG
without zero-divisors to themselves be homogeneous.Show
TwoUniqueProds
impliesUniqueProds
:TwoUniqueProds.toUniqueProds
Strengthen
of_Covariant_right/left
to haveTwoUniqueProds
as conclusionExtract
of_image_filter
from the proof of the instanceUniqueProds (∀ i, G i)
and use it also in the proof ofTwoUniqueProds (∀ i, G i)
Use some private defs (starting from
private abbrev I
) to transfer(Two)UniqueProds (∀ i, G i)
instances to(Two)UniqueProds (G × H)
Move the
[Module ℚ G] : UniqueSums G
instance from NoZeroDivisors.lean to UniqueProds.lean and strengthen toTwoUniqueSums
New lemmas about UniqueMul:
of_card_le_one
,iff_card_le_one
,UniqueMul_of_TwoUniqueMul