refactor(algebra/star/*): Allow for star operation on non-associative algebras #17949
Conversation
…tar_add_monoid 100
…ar_add_monoid' 100
YaelDillies
changed the title
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
mans0954
added
the
awaiting-review
YaelDillies
added
the
modifies-synchronized-file
src/algebra/star/basic.lean
Outdated
| so `star (r * s) = star s * star r`. | ||
| -/ | ||
| class star_semigroup (R : Type u) [semigroup R] extends has_involutive_star R := | ||
| class star_magma (R : Type u) [has_mul R] extends has_involutive_star R := |
There was a problem hiding this comment.
We never really use magma as a word anywhere. Maybe this is better?
| class star_magma (R : Type u) [has_mul R] extends has_involutive_star R := | |
| class star_mul (R : Type u) [has_mul R] extends has_involutive_star R := |
There was a problem hiding this comment.
@YaelDillies Having a field with the same name as the class seems to be a source of confusion:
Error: /home/lean/actions-runner/_work/mathlib/mathlib/src/algebra/star/basic.lean:127:0:
invalid simplification lemma 'star_mul'
Should I rename the field to something else, like antihomomorphism?
|
What's the plan WRT mathlib 4 here? Once this is approved, are you happy to forward-port? |
@eric-wieser In principal yes - but what would the procedure be for forward-porting a PR when some of the files touched are in mathlib4 and others aren't? |
|
You only forward-port the changes to files that are already ported. |
|
Can't make sense of what's happened here. Where has |
|
I've renamed it to |
semorrison
added
the
too-late
|
@mans0954 even though this is marked as |
Yes - I came to the conclusion that trying to get it into mathlib and forward port it to mathlib4 was too much hard work, and it would be better to wait until I could just add it straight to mathlib4. Are we allowed to modify existing code in mathlib4 independent of mathlib now? |
@j-loreaux closing in favour of leanprover-community/mathlib4#6562 |
… algebras (#6562) Typically a * operation on a mathematical structure `R` equipped with a multiplication is an involutive anti-automorphism i.e. ``` ∀ r s : R, star (r * s) = star s * star r ``` Currently mathlib defines a class `StarSemigroup` to be a semigroup satisfying this property. However, the requirement for the multiplication to be associative is unnecessarily restrictive. There are important classes of star-algebra which are not associative (e.g. JB*-algebras). This PR removes the requirement for a `StarSemigroup` to be a semigroup, merely requiring it to have a multiplication. I've changed the name from `StarSemigroup` to `StarMul` since it's no longer a semigroup. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/non-associative.20*-algebras) Previously opened as a mathlib PR leanprover-community/mathlib#17949 Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Typically a * operation on a mathematical structure
Requipped with a multiplication is an involutive anti-automorphism i.e.Currently mathlib defines a class
star_semigroupto be a semigroup satisfying this property. However, the requirement for the multiplication to be associative is unnecessarily restrictive. There are important classes of star-algebra which are not associative (e.g. JB*-algebras).This PR removes the requirement for a
star_semigroupto be a semigroup, merely requiring it to have a multiplication.I've changed the name from
star_semigrouptostar_magmasince it's no longer a semigroup.Zulip discussion