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(linear_algebra): the direct sum of a submodule quotient is the quotient of the direct sum #17069
Conversation
…uotient of the direct sum This defines the linear equivalence `submodule.quotient_pi` which allows us to interchange taking the direct sum and taking the quotient. This result is useful for defining the ideal norm. Co-Authored-By: Alex J. Best <alex.j.best@gmail.com>
variables {N : Type*} [add_comm_group N] [module R N] | ||
variables {Ns : ι → Type*} [∀ i, add_comm_group (Ns i)] [∀ i, module R (Ns i)] | ||
|
||
/-- Lift a family of maps to the direct sum of quotients. -/ |
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.
Calling this a direct sum is maybe misleading in the presence of direct_sum
... But I don't have a better suggestion
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 don't think the presence of direct_sum
should change the informal meaning of "direct sum". :-)
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…t annoying timeouts due to the simp set not converging fast enough (?)
bors merge |
…uotient of the direct sum (#17069) This defines the linear equivalence `submodule.quotient_pi` which allows us to interchange taking the direct sum and taking the quotient. This result is useful for defining the ideal norm. Co-Authored-By: Alex J. Best <alex.j.best@gmail.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Build failed (retrying...): |
…uotient of the direct sum (#17069) This defines the linear equivalence `submodule.quotient_pi` which allows us to interchange taking the direct sum and taking the quotient. This result is useful for defining the ideal norm. Co-Authored-By: Alex J. Best <alex.j.best@gmail.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Pull request successfully merged into master. Build succeeded: |
This defines the linear equivalence
submodule.quotient_pi
which allows us to interchange taking the direct sum and taking the quotient. This result is useful for defining the ideal norm.Co-Authored-By: Alex J. Best alex.j.best@gmail.com