Zulip Chat Archive
Stream: Is there code for X?
Topic: Generalization of mul_eq_one_comm
Eric Wieser (Jan 11 2022 at 13:22):
Is there a generalized form of docs#matrix.mul_eq_one_comm that works for comm_monoid too?
Is there a name in general for monoids where x * y = 1 ↔ y * x = 1? (all left inverses are also right inverses and vice versa)
Riccardo Brasca (Jan 11 2022 at 13:27):
If left and right inverses exist they are always equal (in any monoid). The point with matrices is that the existence of a left inverse implies the existence of a right inverse
Alex J. Best (Jan 11 2022 at 13:28):
I think we spoke about this before right. The right generalization is something like dedekind_finite_monoid
Alex J. Best (Jan 11 2022 at 13:29):
I've cleaned up branch#alexjbest/dedekind-finite a little recently, its mainly focussed around rings and I'm not sure what parts hold for monoids only, but the definition certainly does
Eric Wieser (Jan 11 2022 at 13:29):
I think we spoke about this before right.
Yes, I'm sure we did, I just couldn't find the context
Alex J. Best (Jan 11 2022 at 13:29):
Riccardo Brasca (Jan 11 2022 at 13:31):
Wow, I've never about dedekind-finite monoids
Eric Wieser (Jan 11 2022 at 13:31):
Can you close #1822 and replace it with a new PR from branch#alexjbest/dedekind-finite?
Eric Wieser (Jan 11 2022 at 13:32):
The new one can still be please-adopt or whatever, but at least its in the right repo now
Eric Wieser (Jan 11 2022 at 13:36):
Are you ok with me PR'ing just the definition of is_dedekind_finite and a few instances?
Riccardo Brasca (Jan 11 2022 at 13:48):
@Alex J. Best Wow, the fact that this is true in any noetherian ring gives a very beautiful proof that it is true for matrices!
Alex J. Best (Jan 11 2022 at 13:49):
Yes! That was my original motivation for looking into this stuff in fact, I went down a rabbit hole of "why is it that matrix right inverses are left inverses"
Alex J. Best (Jan 11 2022 at 13:50):
Eric Wieser said:
Are you ok with me PR'ing just the definition of
is_dedekind_finiteand a few instances?
Sure go ahead!
Alex J. Best (Jan 11 2022 at 13:51):
Alex J. Best (Jan 11 2022 at 13:52):
Just to track the branch for now, a bit more work is needed to make some of the concepts there mathlib general I believe
Last updated: Dec 20 2023 at 11:08 UTC