[Merged by Bors] - feat(Analysis/InnerProductSpace/MulOpposite): defines the inner product on opposite spaces by themathqueen · Pull Request #25951 · leanprover-community/mathlib4

themathqueen · 2025-06-16T10:34:09Z

This pr defines the inner product on opposite spaces.

Motivation for having the inner product structure on the opposite:
One application comes up in non-commutative graphs, which are defined on a finite-dimensional C*-algebra with a faithful and positive functional (a Hilbert space structure can be induced by the defined faithful and positive functional (will be added to a pr soon)). For example, we'd need the Hilbert space structure to be defined on the opposite space to define the isomorphism: (A →ₗ[ℂ] B) ≃ₗ[ℂ] TensorProduct ℂ B Aᵐᵒᵖ, where A, B are again finite-dimensional C*-algebras with faithful and positive functionals.

depends on: [Merged by Bors] - feat(LinearAlgebra/Basis/MulOpposite): basis of an opposite space #25949

github-actions · 2025-06-16T10:35:21Z

PR summary 85598ed4df

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Analysis.InnerProductSpace.MulOpposite` (new file)	2040

Declarations diff

+ _root_.Module.Basis.mulOpposite_is_orthonormal_iff
+ _root_.OrthonormalBasis.mulOpposite
+ inner_op
+ inner_unop
+ instance : InnerProductSpace 𝕜 Hᵐᵒᵖ
+ instance [Inner 𝕜 H] : Inner 𝕜 Hᵐᵒᵖ where inner x y := inner 𝕜 x.unop y.unop
+ isometry_opLinearEquiv
+ opLinearIsometryEquiv
+ toContinuousLinearEquiv_opLinearIsometryEquiv
+ toLinearEquiv_opLinearIsometryEquiv

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

j-loreaux · 2025-07-03T16:32:54Z

I'm not saying we can't have it, but why do you need this? I only see this being viable for H = \bbk or H = EuclideanSpace \bbk n.

themathqueen · 2025-07-03T17:23:30Z

@j-loreaux, also viable for H = Matrix n n \bbk or for finite-dimensional C*-algebras. Same goes for the pr that this one depends on.

j-loreaux · 2025-07-04T02:26:13Z

The Frobenius norm on Matrix makes sense, but I wouldn't expect to put an inner product structure on a generic finite dimensional C*-algebra.

But I guess the question is still: do you have a case in mind where you'll need the inner product structure on the opposite?

It seems like it would almost never be necessary.

themathqueen · 2025-07-12T14:16:14Z

-awaiting-author

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

…5949) This adds the definition of `Basis.mulOpposite` and shows finite-dimensionality and freeness of `Hᵐᵒᵖ`. For motivation, see #25951. Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

j-loreaux

Thanks!

bors d+

mathlib-bors · 2025-08-20T03:00:11Z

✌️ themathqueen can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

themathqueen · 2025-08-20T06:00:11Z

bors r+

…ct on opposite spaces (#25951) This pr defines the inner product on opposite spaces. Motivation for having the inner product structure on the opposite: One application comes up in non-commutative graphs, which are defined on a finite-dimensional C*-algebra with a faithful and positive functional (a Hilbert space structure can be induced by the defined faithful and positive functional (will be added to a pr soon)). For example, we'd need the Hilbert space structure to be defined on the opposite space to define the isomorphism: `(A →ₗ[ℂ] B) ≃ₗ[ℂ] TensorProduct ℂ B Aᵐᵒᵖ`, where `A`, `B` are again finite-dimensional C*-algebras with faithful and positive functionals. Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

themathqueen · 2025-08-20T06:05:43Z

bors r-

mathlib-bors · 2025-08-20T06:05:46Z

Canceled.

themathqueen · 2025-08-20T06:22:58Z

bors r+

…ct on opposite spaces (#25951) This pr defines the inner product on opposite spaces. Motivation for having the inner product structure on the opposite: One application comes up in non-commutative graphs, which are defined on a finite-dimensional C*-algebra with a faithful and positive functional (a Hilbert space structure can be induced by the defined faithful and positive functional (will be added to a pr soon)). For example, we'd need the Hilbert space structure to be defined on the opposite space to define the isomorphism: `(A →ₗ[ℂ] B) ≃ₗ[ℂ] TensorProduct ℂ B Aᵐᵒᵖ`, where `A`, `B` are again finite-dimensional C*-algebras with faithful and positive functionals. Co-authored-by: Monica Omar <2497250a@research.gla.ac.uk>

mathlib-bors · 2025-08-20T06:36:13Z

Pull request successfully merged into master.

Build succeeded:

CI Success

…ct on opposite spaces (leanprover-community#25951) This pr defines the inner product on opposite spaces. Motivation for having the inner product structure on the opposite: One application comes up in non-commutative graphs, which are defined on a finite-dimensional C*-algebra with a faithful and positive functional (a Hilbert space structure can be induced by the defined faithful and positive functional (will be added to a pr soon)). For example, we'd need the Hilbert space structure to be defined on the opposite space to define the isomorphism: `(A →ₗ[ℂ] B) ≃ₗ[ℂ] TensorProduct ℂ B Aᵐᵒᵖ`, where `A`, `B` are again finite-dimensional C*-algebras with faithful and positive functionals. Co-authored-by: Monica Omar <2497250a@research.gla.ac.uk>

themathqueen added 4 commits June 16, 2025 09:32

added Basis.mulOpposite

37771f7

doc string

7f67f27

instance name

888d355

inner product space of mulOpposite

d90739b

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jun 16, 2025

themathqueen added 5 commits June 18, 2025 20:47

fix style

4337078

fix

167887e

Merge branch 'basis_mulop' into inner_op

fe2a535

fix style

fde0983

Merge branch 'master' into inner_op

6b190ef

j-loreaux added awaiting-author A reviewer has asked the author a question or requested changes. blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Jul 3, 2025

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 3, 2025

j-loreaux added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 11, 2025

themathqueen mentioned this pull request Jul 12, 2025

[Merged by Bors] - feat(LinearAlgebra/Basis/MulOpposite): basis of an opposite space #25949

Closed

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 12, 2025

themathqueen and others added 6 commits July 20, 2025 23:44

finrank and rank

de00f24

add simp

d2c2e0c

fix

e12fb8b

Update Mathlib/LinearAlgebra/Basis/MulOpposite.lean

8069788

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

suggested changes

6e52161

Update MulOpposite.lean

3718f5b

themathqueen added 2 commits August 10, 2025 18:45

Merge branch 'master' into inner_op

f960ace

fix

8ed0fef

leanprover-community-bot-assistant assigned ADedecker Aug 12, 2025

j-loreaux reviewed Aug 19, 2025

View reviewed changes

Comment thread Mathlib/Analysis/InnerProductSpace/MulOpposite.lean Outdated

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 19, 2025

themathqueen added 2 commits August 19, 2025 21:03

Merge branch 'master' into inner_op

c3c589a

opLinearIsometryEquiv

57989ac

themathqueen removed the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 19, 2025

themathqueen and others added 2 commits August 19, 2025 21:17

docs

4c848c6

Update MulOpposite.lean

cb080ca

j-loreaux reviewed Aug 20, 2025

View reviewed changes

Comment thread Mathlib/Analysis/InnerProductSpace/MulOpposite.lean

Comment thread Mathlib/Analysis/InnerProductSpace/MulOpposite.lean

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Aug 20, 2025

Apply suggestions from code review

9e3d6fa

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

themathqueen added 2 commits August 20, 2025 06:08

Update MulOpposite.lean

d847dba

Update MulOpposite.lean

55cae1c

mathlib-bors Bot changed the title ~~feat(Analysis/InnerProductSpace/MulOpposite): defines the inner product on opposite spaces~~ [Merged by Bors] - feat(Analysis/InnerProductSpace/MulOpposite): defines the inner product on opposite spaces Aug 20, 2025

mathlib-bors Bot closed this Aug 20, 2025

themathqueen deleted the inner_op branch August 20, 2025 06:38

Conversation

themathqueen commented Jun 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jun 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 85598ed4df

Import changes for modified files

Declarations diff

Uh oh!

j-loreaux commented Jul 3, 2025

Uh oh!

themathqueen commented Jul 3, 2025

Uh oh!

j-loreaux commented Jul 4, 2025

Uh oh!

themathqueen commented Jul 12, 2025

Uh oh!

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

mathlib-bors Bot commented Aug 20, 2025

Uh oh!

themathqueen commented Aug 20, 2025

Uh oh!

themathqueen commented Aug 20, 2025

Uh oh!

mathlib-bors Bot commented Aug 20, 2025

Uh oh!

themathqueen commented Aug 20, 2025

Uh oh!

mathlib-bors Bot commented Aug 20, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

themathqueen commented Jun 16, 2025 •

edited

Loading

github-actions Bot commented Jun 16, 2025 •

edited

Loading