[Merged by Bors] - feat(analysis/inner_product_space/basic): orthogonal submodules #18705
Conversation
eric-wieser
added
awaiting-review
mathlib-dependent-issues-bot
added
the
blocked-by-other-PR
eric-wieser
changed the base branch from
master
to
eric-wieser/split-inner-basic
github-actions
bot
removed
the
awaiting-CI
mathlib-dependent-issues-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
| (self_is_ortho_orthogonal U).symm | ||
|
|
||
| @[simp] | ||
| lemma is_ortho_top_right {U : submodule 𝕜 E} : U ⟂ ⊤ ↔ U = ⊥ := |
There was a problem hiding this comment.
Okay, this reads funny!
There was a problem hiding this comment.
I think I derived this name from disjoint_top_right, though I might be imagining things
There was a problem hiding this comment.
This is even worse: lemma is_ortho_bot_left {V : submodule 𝕜 E} : ⊥ ⟂ V. Is there any reason why we use ⊥ (the submodule, not the orthogonality sign) instead of 0?
There was a problem hiding this comment.
Yes, we more often care about its order properties than its algebraic ones (which only come in handy when doing pointwise operations).
There was a problem hiding this comment.
If these are really objectionable I could either write is_ortho ⊥ V or (⊥ : submodule 𝕜 E) ⟂ V here
There was a problem hiding this comment.
I think it's alright. My remark was inconsequential.
The splitting plan already happened, this all used to be in |
Co-authored-by: Yaël Dillies <[email protected]>
| @@ -1885,6 +1885,7 @@ open_locale direct_sum | |||
| The simple way to express this concept would be as a condition on `V : ι → submodule 𝕜 E`. We | |||
| We instead implement it as a condition on a family of inner product spaces each equipped with an | |||
| isometric embedding into `E`, thus making it a property of morphisms rather than subobjects. | |||
| The connection to the subobject spelling is shown in `orthogonal_family_iff_pairwise`. | |||
There was a problem hiding this comment.
Oh hmm, if you've already split out orthogonality, why is this still here?
There was a problem hiding this comment.
I left behind the orthogonal family stuff since it's not about submodules at all.
There was a problem hiding this comment.
I'm not opposed to a further split / reshuffle, but I think it's out of scope for this PR.
There was a problem hiding this comment.
Ah I see. The file names are currently misleading.
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
1 similar comment
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
Thanks! bors r+ |
github-actions
bot
added
ready-to-merge
This adds `submodule.is_ortho U V`, with notation `U ⟂ V`, as a shorthand for `U ≤ Vᗮ`. To make this useful, this also adds about 30 lemmas of basic API. Some downstream proofs are golfed using the new API.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
This adds `submodule.is_ortho U V`, with notation `U ⟂ V`, as a shorthand for `U ≤ Vᗮ`. To make this useful, this also adds about 30 lemmas of basic API. Some downstream proofs are golfed using the new API.
This adds
submodule.is_ortho U V, with notationU ⟂ V, as a shorthand forU ≤ Vᗮ.To make this useful, this also adds about 30 lemmas of basic API.
Some downstream proofs are golfed using the new API.
submodule.orthogonalto a new file #18706This acts upon a discussion in #18230.
I've tried to add all the obvious API, but there are almost certainly some useful results I've missed. I am happy to add more to this PR.