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(group_theory/group_action): Extract a smaller typeclass out of mul_semiring_action
#8918
Conversation
…mul_semiring_action` This new typeclass, `mul_distrib_mul_action`, is satisfied by conjugation actions.
c81f48f
to
4074614
Compare
5a80cf5
to
ef8eabc
Compare
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 d+
@@ -2311,6 +2311,10 @@ S.to_submonoid.has_faithful_scalar | |||
instance [add_monoid α] [distrib_mul_action G α] (S : subgroup G) : distrib_mul_action S α := | |||
S.to_submonoid.distrib_mul_action | |||
|
|||
/-- The action by a subgroup is the action by the underlying group. -/ |
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.
/-- The action by a subgroup is the action by the underlying group. -/ | |
/-- The action by a subgroup is the action by the ambient group. -/ |
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.
This docstring is copied from lots of other places, so I'd prefer to leave it as is rather than finding all occurences in this PR.
@@ -855,6 +855,10 @@ lemma smul_def [mul_action M' α] {S : submonoid M'} (g : S) (m : α) : g • m | |||
instance [add_monoid α] [distrib_mul_action M' α] (S : submonoid M') : distrib_mul_action S α := | |||
distrib_mul_action.comp_hom _ S.subtype | |||
|
|||
/-- The action by a submonoid is the action by the underlying monoid. -/ |
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.
/-- The action by a submonoid is the action by the underlying monoid. -/ | |
/-- The action by a submonoid is the action by the ambient monoid. -/ |
@@ -960,6 +960,10 @@ S.to_subsemiring.has_faithful_scalar | |||
instance [add_monoid α] [distrib_mul_action R α] (S : subring R) : distrib_mul_action S α := | |||
S.to_subsemiring.distrib_mul_action | |||
|
|||
/-- The action by a subsemiring is the action by the underlying semiring. -/ |
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.
/-- The action by a subsemiring is the action by the underlying semiring. -/ | |
/-- The action by a subsemiring is the action by the ambient semiring. -/ |
@@ -819,6 +819,11 @@ S.to_submonoid.has_faithful_scalar | |||
instance [add_monoid α] [distrib_mul_action R' α] (S : subsemiring R') : distrib_mul_action S α := | |||
S.to_submonoid.distrib_mul_action | |||
|
|||
/-- The action by a subsemiring is the action by the underlying semiring. -/ |
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.
/-- The action by a subsemiring is the action by the underlying semiring. -/ | |
/-- The action by a subsemiring is the action by the ambient semiring. -/ |
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.
idem
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
…mul_semiring_action` (#8918) This new typeclass, `mul_distrib_mul_action`, is satisfied by conjugation actions. This PR provides instances for: * `mul_aut` * `prod` of two types with a `mul_distrib_mul_action` * `pi` of types with a `mul_distrib_mul_action` * `units` of types with a `mul_distrib_mul_action` * `ulift` of types with a `mul_distrib_mul_action` * `opposite` of types with a `mul_distrib_mul_action` * `sub(monoid|group|semiring|ring)`s of types with a `mul_distrib_mul_action` * anything already satisfying a `mul_semiring_action`
Pull request successfully merged into master. Build succeeded: |
mul_semiring_action
mul_semiring_action
This new typeclass,
mul_distrib_mul_action
, is satisfied by conjugation actions. This PR provides instances for:mul_aut
prod
of two types with amul_distrib_mul_action
pi
of types with amul_distrib_mul_action
units
of types with amul_distrib_mul_action
ulift
of types with amul_distrib_mul_action
opposite
of types with amul_distrib_mul_action
sub(monoid|group|semiring|ring)
s of types with amul_distrib_mul_action
mul_semiring_action
This typeclass was one I suggested in #8592, and is discussed briefly here on Zulip.