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): definition and properties of relative ideal norm #18299
Conversation
This PR/issue depends on:
|
This PR provides a definition of the relative ideal norm `ideal.span_norm R I` as the ideal spanned by the norms of elements in `I`. We also give some basic results on this definition. A follow-up PR will bundle this into a homomorphism `ideal.rel_norm`.
6f911b5
to
f67a978
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+
def span_norm (I : ideal S) : ideal R := | ||
ideal.span (algebra.norm R '' (I : set S)) | ||
|
||
@[simp] lemma span_norm_bot |
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 is false without nontrivial S
, right?
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.
Yes, then this would be ideal.span {algebra.norm 1} = ideal.span {1} = ⊤
(since norm
/det
breaks the tie between 0 = 1
in favour of 1).
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
…18299) This PR provides a definition of the relative ideal norm `ideal.span_norm R I` as the ideal spanned by the norms of elements in `I`. We also give some basic results on this definition. A follow-up PR will bundle this into a homomorphism `ideal.rel_norm`.
Pull request successfully merged into master. Build succeeded: |
This PR provides a definition of the relative ideal norm
ideal.span_norm R I
as the ideal spanned by the norms of elements inI
. We also give some basic results on this definition. A follow-up PR will bundle this into a homomorphismideal.rel_norm
.