Skip to content
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

refactor(LinearAlgeba/BilinearMap): Weaken CommSemiring to SMulCommClass #7538

Closed
wants to merge 6 commits into from

Conversation

mans0954
Copy link
Collaborator

@mans0954 mans0954 commented Oct 5, 2023

The results in the CommSemiring section of LinearAlgeba/BilinearMap don't require the semirings to be commutative. It is sufficient that scalar multiplication in the modules is commutative.


Open in Gitpod

@mans0954
Copy link
Collaborator Author

mans0954 commented Oct 6, 2023

Build failing due to:

Error: No space left on device : '/home/lean/actions-runner/_work/_actions/dcarbone/install-jq-action/v1.0.1'

Not something I think I can fix?

@ADedecker
Copy link
Member

That's a thing that happens from time to time, the best you can do is ping maintainers on Zulip so that we can disable and fix the faulty runner. It's the case now so I've restarted the build for you.

@ADedecker
Copy link
Member

bors d+

@bors
Copy link

bors bot commented Oct 6, 2023

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

Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What's the motivation for this change? Are there any interesting actions of non-commuting elements whose actions commute? I think in various places we avoided this generalization because there was no clear use case, and we expected a performance impact.

!bench

@mans0954
Copy link
Collaborator Author

mans0954 commented Oct 7, 2023

What's the motivation for this change? Are there any interesting actions of non-commuting elements whose actions commute? I think in various places we avoided this generalization because there was no clear use case, and we expected a performance impact.

@eric-wieser I can explain what I'm trying to do, and you can tell me if I'm going about it in the right way.

When I defined Jordan algebras, I left out quadratic Jordan algebras which are more general as they work without restriction on the characteristic.

Now I've got a bit more used to working with Mathlib, I thought I'd see if I could give the quadratic definition, but that requires quadratic maps. Currently, I think Mathlib only has QuadraticForm, but defined over a non-commutative ring.

I started working on quadratic forms over commutative rings, but it was quickly apparent that it's almost identical to the quadratic forms theory, and we would end up with two files with almost exactly the same results in them. I started thinking about whether it might be possible to develop the theory of quadratic maps over commutative rings and quadratic forms over non-commutative rings simultaneously, and I came up with:

structure QuadraticForm (R : Type u) (M : Type v) (N : Type w) [Semiring R] [AddCommMonoid M]
    [Module R M] [Module Rᵐᵒᵖ M] [AddCommMonoid N] [Module R N] [Module Rᵐᵒᵖ N] [SMulCommClass Rᵐᵒᵖ R N] where
  toFun : M → N
  toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
  toFun_smulr : ∀ (a : Rᵐᵒᵖ) (x : M), toFun (a • x) = (a * a) • toFun x
  exists_companion' : ∃ B : M →ₗ[R] M →ₗ[Rᵐᵒᵖ] N, ∀ x y, toFun (x + y) = toFun x + toFun y + B x y

The idea here being that [SMulCommClass Rᵐᵒᵖ R R] will hold for an associative non-commutative ring as R is a left-module over R and a right-module over Rᵐᵒᵖ.

This seemed to be working, until I got to the SMul section where I needed to define scalar multiplication on QuadraticForm R M N which requires instance : SMul S (M →ₗ[R] M →ₗ[Rᵐᵒᵖ] N) for the bilinear map.

You can see my work-in-progress branch here: master...mans0954/quadratic-maps

So I guess the options are:

  • Merge this PR (if the performance is okay)
  • Develop quadratic maps over commutative rings and quadratic forms over non-commutative rings separately
  • Limit quadratic forms in Mathlib to only commutative rings
  • Only have (linear) Jordan algebras in Mathlib?

@eric-wieser
Copy link
Member

I'd envisaged that the correct statement was

toFun (a • x) = a • (op a • toFun x)

which corresponds to Q(ax) = aQ(x)a; does that sound right to you?

@eric-wieser
Copy link
Member

Note that to replace the existing quadratic forms with your definition, we are first going to need #7152.

1 similar comment
@eric-wieser
Copy link
Member

Note that to replace the existing quadratic forms with your definition, we are first going to need #7152.

@mans0954
Copy link
Collaborator Author

mans0954 commented Oct 7, 2023

I'd envisaged that the correct statement was

toFun (a • x) = a • (op a • toFun x)

which corresponds to Q(ax) = aQ(x)a; does that sound right to you?

That looks plausible - I think the bilinear map is still B : M →ₗ[R] M →ₗ[Rᵐᵒᵖ] N and we will still need to show that a • B is also M →ₗ[R] M →ₗ[Rᵐᵒᵖ] N?

@eric-wieser
Copy link
Member

Yes, I agree with the bilinear map form.

However, I don't think r • B is well-defined if r : R and R is not commutative. Better to define s • B for when the actions of R and S commute, which gives us the special case r • B for when R is commutative.

@eric-wieser
Copy link
Member

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 05a2cf5.
There were significant changes against commit 8ec1ec7:

  Benchmark                                        Metric         Change
  ======================================================================
- ~Mathlib.LinearAlgebra.BilinearMap               instructions    12.2%
+ ~Mathlib.LinearAlgebra.DirectSum.TensorProduct   instructions    -7.8%
- ~Mathlib.LinearAlgebra.TensorPower               instructions     6.6%

@mans0954
Copy link
Collaborator Author

mans0954 commented Oct 7, 2023

However, I don't think r • B is well-defined if r : R and R is not commutative. Better to define s • B for when the actions of R and S commute, which gives us the special case r • B for when R is commutative.

Exactly - which brings us back to the purpose of this PR.

@eric-wieser
Copy link
Member

eric-wieser commented Oct 7, 2023

Do you have an example in mind (a choice of R and M) where R is non-commutative but its action on M is commutative?

@mans0954
Copy link
Collaborator Author

mans0954 commented Oct 7, 2023

I'd envisaged that the correct statement was

toFun (a • x) = a • (op a • toFun x)

which corresponds to Q(ax) = aQ(x)a; does that sound right to you?

@eric-wieser Do you also need:

toFun (op a • x) = op a • (a • toFun x)

i.e. Q(xa) = aQ(x)a e.g. to get B(x,ya) = B(x,y)a?

@eric-wieser
Copy link
Member

eric-wieser commented Oct 7, 2023

No, that feels like a bad assumption to me as it means $$x \mapsto x^2$$ doesn't count as a quadratic form over a non-commutative ring.

Edit: hmm, that seems troublesome anyway...

@mans0954
Copy link
Collaborator Author

mans0954 commented Oct 7, 2023

No, that feels like a bad assumption to me as it means x↦x2 doesn't count as a quadratic form over a non-commutative ring.

Edit: hmm, that seems troublesome anyway...

@eric-wieser I don't see that $$x \mapsto x^2$$ satisfies Q(ax) = aQ(x)a either? So I think we're back to $$Q(ax) = a^2Q(x)$$ and $$Q(xa) = Q(x)a^2$$

@eric-wieser
Copy link
Member

You're right, and that was what my edit was intended to convey.

I think the important question here is my earlier message:

Do you have an example in mind (a choice of R and M) where R is non-commutative but its action on M is commutative?

@mans0954
Copy link
Collaborator Author

mans0954 commented Oct 8, 2023

I think the important question here is my earlier message:

Do you have an example in mind (a choice of R and M) where R is non-commutative but its action on M is commutative?

Yes, sorry, I got a bit lost in all of this earlier and had my wires crossed. I agree now that I don't need this PR to get a scalar multiplication on instance : SMul S (QuadraticForm R M N) - I just need the appropriate SMulCommClass as hypothesis.

However, the next place I get stuck is in composition of a quadratic map with a linear map. Specifically LinearMap.compl₁₂ doesn't work because it expects the rings to be commutative (https://github.com/leanprover-community/mathlib4/pull/7569/files#diff-4b8a995fd51c4cb0a5d0ff6413fa1565f87f697d1b552327cfed2c98a4f62f49R609). What I was hoping for from this PR was to have a version of LinearMap.compl₁₂ that works with SMulCommClass instead of commutative rings.

I've opened a draft PR #7569 for the quadratic maps in case it's easier to discuss this there?

@eric-wieser
Copy link
Member

Specifically LinearMap.compl₁₂ doesn't work because it expects the rings to be commutative

Well worse, doesn't it require the rings to be the same?

Note that in the short term you can use ((f ∘ₗ g).flip ∘ₗ h).flip); but it would be great to generalize LinearMap.compl₁₂ to make it work here.

I think we should close this PR; I don't think there is anything worth merging here, and the conversation is still useful even if this PR is closed.

@eric-wieser eric-wieser closed this Oct 8, 2023
mathlib-bors bot pushed a commit that referenced this pull request Jan 6, 2024
Remove unused commutativity hypothesis:

* Removes the requirement for the Semirings to be commutative in `LinearMap.ext_basis` and `LinearMap.sum_repr_mul_repr_mulₛₗ` in `LinearAlgebra/Basis/Bilinear`
* Remove the requirement for some Semirings to be commutative in `AuxToLinearMap`, `CommSemiring` and `CommRing` in `LinearAlgebra/Matrix/SesquilinearForm`
* In addition, the rings in `CommRing` can just be `Semiring`

No changes to the proofs are required.

It would also be possible to weaken commutativity from `Rₗ` in `LinearMap.sum_repr_mul_repr_mul` to `[SMulCommClass Rₗ Rₗ Pₗ]` in order to make `sum_repr_mul_repr_mulₛₗ` and `sum_repr_mul_repr_mul` consistent, but I have not done that in this PR because there might be a performance impact (see #7538 (review)).



Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants