-
Notifications
You must be signed in to change notification settings - Fork 298
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/subgroup/basic): Define characteristic subgroups #9921
Conversation
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.
Generally LGTM but I would wait for comments from one of our "algebra" maintainers.
attribute [class] characteristic | ||
|
||
@[priority 100] instance normal_of_characteristic [h : H.characteristic] : H.normal := | ||
⟨λ a ha b, (set_like.ext_iff.mp (h.fixed (mul_aut.conj b)) a).mpr ha⟩ |
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.
Can to_additive
generate this instance?
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.
I can't seem to get it to work :(
structure characteristic : Prop := | ||
(fixed : ∀ ϕ : G ≃* G, H.comap ϕ.to_monoid_hom = H) | ||
|
||
attribute [class] characteristic |
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.
You can use
structure characteristic : Prop := | |
(fixed : ∀ ϕ : G ≃* G, H.comap ϕ.to_monoid_hom = H) | |
attribute [class] characteristic | |
@[class] structure characteristic : Prop := | |
(fixed : ∀ ϕ : G ≃* G, H.comap ϕ.to_monoid_hom = H) |
to achieve the same goal.
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.
There is a slight difference. With the current setup, if [h : characteristic H]
, then you can write h.fixed
. With the proposed setup, you have to write characteristic.fixed
. This is especially painful if h
is not an instance (e.g., in characteristic_iff_comap_eq
).
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.
(I presume this is why subgroup.normal
does the same thing)
⟨characteristic.fixed, characteristic.mk⟩ | ||
|
||
@[to_additive] lemma characteristic_iff_comap_le : | ||
H.characteristic ↔ ∀ ϕ : G ≃* G, H.comap ϕ.to_monoid_hom ≤ H := |
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.
Please mention this and the next lemmas in the docstring.
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.
Done (assuming you mean the docstrings for the definitions)
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 merge
…9921) This PR defines characteristic subgroups and builds the basic API. Getting `@[to_additive]` to work correctly was a bit tricky, so I mostly just copied the setup for `subgroup.normal`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
…9921) This PR defines characteristic subgroups and builds the basic API. Getting `@[to_additive]` to work correctly was a bit tricky, so I mostly just copied the setup for `subgroup.normal`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
This PR defines characteristic subgroups and builds the basic API.
Getting
@[to_additive]
to work correctly was a bit tricky, so I mostly just copied the setup forsubgroup.normal
.