feat(Algebra/Algebra/Prod): add prodUnique and uniqueProd for LinearEquiv and AlgebraEquiv#9105
feat(Algebra/Algebra/Prod): add prodUnique and uniqueProd for LinearEquiv and AlgebraEquiv#9105
Conversation
…lib4 into LinearEquiv_AlgebraEquiv_prodUnique
Mathlib/Algebra/Algebra/Prod.lean
Outdated
|
|
||
| /-- Multiplying by the trivial algebra from the left does not change the structure. | ||
|
|
||
| This is the `AlgebraEquiv` version of `AddEquiv.uniqueProd`. -/ |
There was a problem hiding this comment.
Let's link the strongest weaker equivalence:
| This is the `AlgebraEquiv` version of `AddEquiv.uniqueProd`. -/ | |
| This is the `AlgebraEquiv` version of `LinearEquiv.uniqueProd`. -/ |
Ideally we'd mentionRingEquiv.uniqueProd too, but I assume that's also missing.
There was a problem hiding this comment.
RingEquiv.prodZeroRing and RingEquiv.zeroRingProd exist, but they use the condition [Subsingleton S] rather than [Unique S]. Any thoughts on whether we'd like these to be more consistent with one another? In any case, probably worth referencing them to one another for ease of use.
There was a problem hiding this comment.
The naming discrepancy sounds like a question for Zulip.
Using Subsingleton instead of Unique does seem sensible here.
There was a problem hiding this comment.
(I'm happy to merge as is with a reference to the inconsistent ring name, if you'd prefer to do this in two steps)
There was a problem hiding this comment.
Opened a Zulip thread about that here. I'll already commit a change to make them refer to one another tho
eric-wieser
left a comment
There was a problem hiding this comment.
bors d+
I pushed some cleanups. Let's leave the inconsistency to resolve in future, the cross-references are enough for now.
|
✌️ LukasMias can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Coming here from issue triage: it seems this PR is basically ready to go, except for merge conflicts. |
|
Coming here for PR triage: I recently created a PR with LinearEquiv.prodUnique - so I care about that getting merged. I'm very happy for your PR to merge first, though. Would you like to fix the merge conflicts, @LukasMias? (Or would you like me to do it?) |
Adds definitions of linear equivalences for modules M with their left-/right-product with a trivial module M \times 0 and 0 \times M, and analogous statements for Algebras. Rebased version of #9105. Co-authored-by: @LukasMias
|
This PR has been merged as #24168 now; hence, let me close this PR. Thanks for your work! |
Adds definitions of linear equivalences for modules M with their left-/right-product with a trivial module M \times 0 and 0 \times M, and analogous statements for Algebras. Rebased version of #9105. Co-authored-by: @LukasMias
Adds definitions of linear equivalences for modules M with their left-/right-product with a trivial module M \times 0 and 0 \times M, and analogous statements for Algebras. Rebased version of #9105. Co-authored-by: @LukasMias
This adds definitions of linear equivalences for modules
Mwith their left-/right-product with a trivial moduleM \times 0and0 \times M, and analogous statements for Algebras.