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
refactor(linear_algebra/smodeq): Relax smodeq to accept arbitrary add_subgroups. #15915
Conversation
erdOne
commented
Aug 7, 2022
@@ -14,66 +15,99 @@ import ring_theory.ideal.quotient | |||
open submodule | |||
open_locale polynomial | |||
|
|||
variables {R : Type*} [ring R] | |||
variables {M : Type*} [add_comm_group M] [module R M] (U U₁ U₂ : submodule R M) | |||
variables {M X : Type*} [add_comm_group M] [set_like X M] [add_subgroup_class X M] (U U₁ U₂ : X) |
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.
Do you intentionally not generalize this to [add_group M]
?
def smodeq (x y : M) : Prop := | ||
(submodule.quotient.mk x : M ⧸ U) = submodule.quotient.mk y |
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.
Another solution here would be to eliminate the distinction between submodule.quotient
and add_subgroup.quotient
; they're now defined in terms of each other which they didn't use to be.
Did you attempt that at all @Vierkantor?
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 think I tried that a while ago before the redefinition of the quotients, and it was quite a bit of straightforward work so not too bad if you have some time. We did get the ⧸
notation out of that attempt though.
Closed for now. Maybe revisit in mathlib4. |