[Merged by Bors] - feat: unit equivalences #6526
Conversation
ericrbg
added
awaiting-review
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Mathlib/Algebra/Ring/UnitEquivs.lean
Outdated
| /-- The stabilizer of `Dˣ` acting on itself by conjugation at `x : Dˣ` is exactly the | ||
| units of the centralizer of `x : D`. -/ | ||
| def unitsCentralizerEquiv [Monoid D] (x : Dˣ) : | ||
| MulAction.stabilizer (ConjAct Dˣ) x ≃* (Submonoid.centralizer ({↑x} : Set D))ˣ where |
There was a problem hiding this comment.
I assume there's not a more general results hiding here for MulDistribMulActions?
There was a problem hiding this comment.
I'm not even sure what it'd look like
Mathlib/Algebra/Ring/UnitEquivs.lean
Outdated
| @@ -0,0 +1,69 @@ | |||
| /- | |||
| Copyright (c) 2021 Johan Commelin. All rights reserved. | |||
There was a problem hiding this comment.
Is this a copy-paste error?
| Copyright (c) 2021 Johan Commelin. All rights reserved. | |
| Copyright (c) 2023 Eric Rodriguez. All rights reserved. |
Same remark for Authors field on line 4, though maybe this is co-authored?
There was a problem hiding this comment.
This was written by Johan in Lean3 for little wedderburn so I wanted to carry on his attribution
Mathlib/Algebra/Ring/UnitEquivs.lean
Outdated
| /-- `unitsCentralizerEquiv` for a `Ring`. Restated for Wedderburn's little theorem. -/ | ||
| def unitsCentralizerEquivSubring [Ring D] (x : Dˣ) : | ||
| MulAction.stabilizer (ConjAct Dˣ) x ≃* (Subring.centralizer ({↑x} : Set D))ˣ := | ||
| unitsCentralizerEquiv x | ||
|
|
There was a problem hiding this comment.
I don't understand why we need this. Can you not just use what you have for Monoids?
Mathlib/Algebra/Ring/UnitEquivs.lean
Outdated
| /-- `centerUnitsEquivUnitsCenter` but instead for `Subring.center`. This is convenient for | ||
| Wedderburn's little theorem. -/ | ||
| def centerUnitsEquivUnitsRingCenter [DivisionRing D] : | ||
| Subgroup.center (Dˣ) ≃* (Subring.center D)ˣ := centerUnitsEquivUnitsCenter D |
There was a problem hiding this comment.
Same question here: it's not clear to me why you need this.
Mathlib/Algebra/Ring/UnitEquivs.lean
Outdated
| Authors: Eric Rodriguez, Johan Commelin | ||
| -/ | ||
| import Mathlib.GroupTheory.GroupAction.ConjAct | ||
| import Mathlib.RingTheory.Subring.Basic |
There was a problem hiding this comment.
This import is only necessary because of unitsCentralizerEquivSubring and centerUnitsEquivUnitsRingCenter about which I have doubts.
If it turns out we don't need those lemmas then I think these results could go in the GroupTheory.GroupAction.ConjAct file.
ocfnash
added
awaiting-author
ericrbg
added
awaiting-review
|
The reason I want the ring versions are to do with the proof of little wedderburn; you can see the WIP here. I tried messing around with the proof to change things, and it should be fine but minorly annoying; some slight motive issues as we'd need to rewrite in |
|
I think treating various bundled versions of the same thing as defeq doesn't count as abuse |
|
Alright, I'll change it to that version then |
|
✌️ ericrbg can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
|
bors r+ |
Useful for Wedderburn's little theorem. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.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. |
bors
bot
changed the title
Useful for Wedderburn's little theorem.