-
Notifications
You must be signed in to change notification settings - Fork 297
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(ring_theory/ideal): simp
lemmas for ideal.quotient.mk
+ algebra_map
#9829
Conversation
@[simp] lemma quotient.mk_comp_algebra_map (I : ideal A) : | ||
(quotient.mk I).comp (algebra_map R A) = algebra_map R I.quotient := | ||
rfl | ||
|
||
@[simp] lemma quotient.mk_algebra_map (I : ideal A) (x : R) : | ||
quotient.mk I (algebra_map R A x) = algebra_map R I.quotient x := | ||
rfl |
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 chose for simp
to go in this direction for these two lemmas since it makes working with alg_hom
s a bit easier, and the RHS is shorter. Flipping the direction is also fine with me, since there are quite a few ideal.quotient.mk
-specific lemmas in this file.
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.
Are we missing an alg_hom.commute_of_tower
lemma or something to make it less annoying to have these in the other direction?
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.
If I understand your question correctly, they do exist, as alg_hom.map_algebra_map
and alg_hom.comp_algebra_map_of_tower
. The issue is that quotient.mk
is only a ring_hom
, not an alg_hom
, so we need to reprove all the algebra_map
-related things anyway.
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
…ebra_map` (#9829) Some `simp` lemmas I needed for combining `algebra_map` with `ideal.quotient.mk`. This also allowed me to golf two existing proofs.
bors r+ |
…ebra_map` (#9829) Some `simp` lemmas I needed for combining `algebra_map` with `ideal.quotient.mk`. This also allowed me to golf two existing proofs.
Pull request successfully merged into master. Build succeeded: |
simp
lemmas for ideal.quotient.mk
+ algebra_map
simp
lemmas for ideal.quotient.mk
+ algebra_map
…ebra_map` (#9829) Some `simp` lemmas I needed for combining `algebra_map` with `ideal.quotient.mk`. This also allowed me to golf two existing proofs.
Some
simp
lemmas I needed for combiningalgebra_map
withideal.quotient.mk
. This also allowed me to golf two existing proofs.