Quadratic forms with values in a larger ring

Stream: Is there code for X?

[Michael Stoll]

We have docs#QuadraticForm, which specifies quadratic forms on an R-module M with values in R.
However, I need quadratic forms that take values in a larger ring R' (think R = ℤ and R' = ℝ; I'd like to talk about (canonical) heights on abelian varieties eventually). The present set-up doesn't seem to allow that easily. How should I proceed?

[Kevin Buzzard]

Is this something to do with polynomial maps @María Inés de Frutos Fernández or @Antoine Chambert-Loir ?

[Eric Wieser]

There is a PR that generalizes to QuadraticMap, #7569, which would provide this for you

[Eric Wieser]

Its dependency was lost in the weeds due to a ring bug I think; I'll take another look and see if I can work it out

[Michael Stoll]

I was going to ask what held it up for so long...
Thanks for looking at it!

[Eric Wieser]

Ah nevermind, I fixed the ring bug and it was now stuck with elaboration issues

[Eric Wieser]

@Christopher Hoskin, can you clarify why this needs to be a dependency of the QuadraticMap PR? Is there some existing generalization we lose without it?

[Christopher Hoskin]

@Eric Wieser The problem is here: https://github.com/leanprover-community/mathlib4/pull/7569/files#diff-4b8a995fd51c4cb0a5d0ff6413fa1565f87f697d1b552327cfed2c98a4f62f49R1145

The proof of QuadraticMap.linMulLinSelfPosDef uses QuadraticMap.linMulLin so lean needs to know that the LinearOrderedCommSemiring A is a NonUnitalNonAssocCommSemiring. Adding the instance in LinearAlgebra/QuadraticForm/Basic works, but adding it in Algebra/Ring/Defswhere it belongs was failing.

[Antoine Chambert-Loir]

Kevin Buzzard said:

Is this something to do with polynomial maps María Inés de Frutos Fernández or Antoine Chambert-Loir ?

It has something to do with polynomial maps (which we may rename “polynomial law” to stick with more standard terminology), but it needs to be formalized independently, otherewise we won't be able to state that “the degree 2 part of the divided power algebra is the receptacle of the universal quadratic map.”

[Eric Wieser]

Can we make linMulLin take a CommSemiring for now, with a TODO?

[Christopher Hoskin]

Eric Wieser said:

Can we make linMulLin take a CommSemiring for now, with a TODO?

@Eric Wieser what about creating a file Mathlib/Algebra/Ring/Instances.lean and putting instance CommSemiring.toNonUnitalNonAssocCommSemiring in that as an interim measure?

[Yaël Dillies]

Forgetful inheritance instances being in obscure files is a recipe for unexpected behaviour

[Eric Wieser]

I think we want the instance where you currently have it, but we don't want to block the rest of quadratic maps while we work out how to fix the elaboration issues

[Christopher Hoskin]

Eric Wieser said:

Can we make linMulLin take a CommSemiring for now, with a TODO?

Done: https://github.com/leanprover-community/mathlib4/pull/7569/commits/d025c1c77f5bc1267683f338337128b529b1c5cb

[Christopher Hoskin]

Is there anything that can be done about the dot notation loss, or do we just have to live with that?

[Eric Wieser]

I think we live with it for now

[Christopher Hoskin]

Eric Wieser said:

I think we live with it for now

Okay, is there anything else I need to do to get the PR approved?

[Eric Wieser]

Christopher Hoskin said:

Eric Wieser The problem is here: https://github.com/leanprover-community/mathlib4/pull/7569/files#diff-4b8a995fd51c4cb0a5d0ff6413fa1565f87f697d1b552327cfed2c98a4f62f49R1145

The proof of QuadraticMap.linMulLinSelfPosDef uses QuadraticMap.linMulLin so lean needs to know that the LinearOrderedCommSemiring A is a NonUnitalNonAssocCommSemiring. Adding the instance in LinearAlgebra/QuadraticForm/Basic works, but adding it in Algebra/Ring/Defswhere it belongs was failing.

It turns out this is all a distraction, we don't need commutativity at all here

[Eric Wieser]

Okay, is there anything else I need to do to get the PR approved?

Just time from me, I think was the answer. I've set off a benchmark run; if it's not disastrous, then I think everything is ready to go

[Christopher Hoskin]

Eric Wieser said:

Just time from me, I think was the answer. I've set off a benchmark run; if it's not disastrous, then I think everything is ready to go

@Eric Wieser thanks very much! Whilst there's some attention on generalising forms to maps, is there any chance you could take a look at https://github.com/leanprover-community/mathlib4/pull/9334 please? I've been trying to get it merged for months.

Thanks.

[Kevin Buzzard]

The benchmarking doesn't look too promising right now :-(

[Eric Wieser]

I've made #14719 to continue with the topic of this thread, here generalizing .prod and .pi to larger rings

[Michael Stoll]

Can you also do Mathlib.LinearAlgebra.QuadraticForm.TensorProduct?
I'll need QuadraticMap.baseChange (compare docs#QuadraticForm.baseChange) and its properties to get from a real-valued quadratic map on a finitely generated abelian group to a quadratic form on the real vector space obtained by extending scalars... (and then to a euclidean space)

[Michael Stoll]

(and I hope this will work without the requirement that 2 is invertible in ℤ...)

[Christopher Hoskin]

Michael Stoll said:

(and I hope this will work without the requirement that 2 is invertible in ℤ...)

I'm not sure if this is what you're asking, but it's possible to extend quadratic maps to field extensions without requiring 2 to be invertible - although Mathlib assumes 2 to be invertible for a simpler proof. I can dig out a reference if you need it.

[Michael Stoll]

What I would need (at least with the proof that is currently there) is a version of docs#QuadraticMap.associatedHom that only requires that scalar multiplication by 2 is invertible on the target module (rather than in the base ring). It is not so clear to me how to state the condition in a nice way, though. Maybe we need another type class akin to docs#Invertible ?

[Michael Stoll]

Roughly like this:

class InvertibleSMul {R} (M) [Ring R] [AddCommGroup M] [Module R M] (r : R) where
  invSMul : M →ₗ[R] M
  invSMul_cancel_left : ∀ m : M, invSMul (r • m) = m
  invSMul_cancel_right : ∀ m : M, r • invSMul m = m

(perhaps?)

[Michael Stoll]

Then the assumption for QuadraticMap R M N would be [InvertibleSMul N (2 : R)].

[Eric Wieser]

Christopher Hoskin said:

Michael Stoll said:

(and I hope this will work without the requirement that 2 is invertible in ℤ...)

I'm not sure if this is what you're asking, but it's possible to extend quadratic maps to field extensions without requiring 2 to be invertible - although Mathlib assumes 2 to be invertible for a simpler proof. I can dig out a reference if you need it.

I have an open PR that has the proof of this

[Eric Wieser]

(Or at least, I think #14292 does all the work)

[Eric Wieser]

Christopher Hoskin said:

although Mathlib assumes 2 to be invertible for a simpler proof.

There's some discussion about this in Section 9.7 of my thesis

[Michael Stoll]

Eric Wieser said:

I have an open PR that has the proof of this

If I understand it correctly, this needs the source module to be free, so it would not work for my use case, where I have a (real-valued) quadratic map on a finitely generated (but not necessarily free) abelian group M that I want to base-change to the real vector space ℝ ⊗[ℤ] M.

[Eric Wieser]

Ah, indeed; but I think it covers the case of field extensions that Christopher was describing?

[Michael Stoll]

Probably; modules over fields are free.

[Christopher Hoskin]

The result I was thinking of is para 22 on p16 of https://www.math.uci.edu/~brusso/LecturesQuadJorAlg134pp.pdf

[Christopher Hoskin]

Presumably the next step would look something a bit like this?

open TensorProduct

variable {R : Type*} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]

variable {R' : Type*} [CommSemiring R'] [Algebra R R']

/-- Scalar extension of a basis of a free module -/
@[simps!]
noncomputable def Basis.scalarExtension (bm : Basis ι R M) :=
    Basis.tensorProduct (Basis.singleton (Fin 1) R') bm

namespace LinearMap

namespace BilinMap

/-- Scalar extension of a bilinear map on a free module -/
@[simps!]
noncomputable def scalarExtension (B : LinearMap.BilinMap R M N) (bm : Basis ι R M) :
    LinearMap.BilinMap R' (R' ⊗[R] M) (R' ⊗[R] N) :=
  bm.scalarExtension.constr (S := R) fun i =>
    bm.scalarExtension.constr (S := R) fun j =>
     (1 : R') ⊗ₜ B (bm i.2) (bm j.2)

theorem se_of_Bilin_apply' (B : LinearMap.BilinMap R M N) (bm : Basis ι R M) (i j : ι) :
    B.scalarExtension bm (bm.scalarExtension (1, i)) (bm.scalarExtension (1, j)) =
      (1 : R') ⊗ₜ B (bm i) (bm j) := by
  simp only [Fin.isValue, scalarExtension_apply, Basis.repr_self, Finsupp.total_single, one_smul,
    Basis.constr_basis]

end BilinMap

end LinearMap

variable [LinearOrder ι]

/-- Scalar extension of a Quadratic map on a free module -/
noncomputable def QuadraticMap.scalarExtension (Q : QuadraticMap R M N) (bm : Basis ι R M) :
    QuadraticMap R' (R' ⊗[R] M) (R' ⊗[R] N) := ((Q.toBilin bm).scalarExtension bm).toQuadraticMap

[Eric Wieser]

I think instead we should generalize docs#LinearMap.BilinMap.tmul to bilinear maps

[Christopher Hoskin]

Eric Wieser said:

I think instead we should generalize docs#LinearMap.BilinMap.tmul to bilinear maps

Presumably we need something like:

def tensorDistrib :
    BilinMap A M₁ N₁ ⊗[R] BilinMap R M₂ N₂ →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) := sorry

[Christopher Hoskin]

(I've hacked together the sorry bit for the above but will need to tidy it up to make a PR.)

[Eric Wieser]

Yes, that sounds right to me, and it shouldn't need a basis argument

[Eric Wieser]

I would imagine the existing construction is easy enough to adapt?

[Michael Stoll]

Can we replace the [Invertible (2 : R)] assumption by [Invertible (2 : Module.End R N)] wherever possible? (Where N is the target of the quadratic map.) I assume there can be an instance deriving this from Invertible (2 : R) so that previous use caes will continue to work. But this would make the extension of a quadratic map from a finitely generated abelian group M to the reals to ℝ ⊗[ℤ] M easy (I assume).

[Eric Wieser]

I don't think that's necessary for your use-case? The ring in the tensor product isn't the same as the one in the quadratic map I don't think, and you already have Invertible (2 : Real)

[Eric Wieser]

Either way, let's generalize the bilinear cases first; I suspect the quadratic form generalization you want will be easy after that, one way or another

[Michael Stoll]

My problem is that to go from the quadratic map to a bilinear form (involving division by 2) does not work as is since the base ring (before the base change) is ℤ. The way it's implemented is to first convert to the associated bilinear map (which needs [Invertible (2 : ℤ)], then base-change and then convert back to a quadratic map.

[Michael Stoll]

import Mathlib.Algebra.Algebra.Basic

variable {R M} [CommRing R] [AddCommGroup M] [Module R M]

instance [Invertible (2 : R)] : Invertible (2 : Module.End R M) := by
  convert Invertible.map (algebraMap R (Module.End R M)) 2
  ext
  simp only [Module.End.ofNat_apply, map_ofNat]

But I have the feeling that this should be easier... (Edited: see below.)

[Eric Wieser]

I guess you could make a PR that just generalizes docs#QuadraticMap.associated, to see what the fallout is

[Michael Stoll]

Later today...

[Eric Wieser]

I think the above follows directly from Invertible.map <| algebraMap _ _

[Michael Stoll]

Edited above.

[Christopher Hoskin]

How about this:

def tensorDistrib :
    BilinMap A M₁ N₁ ⊗[R] BilinMap R M₂ N₂ →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) :=
  (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)).symm.toLinearMap ∘ₗ
 ((LinearMap.llcomp A _ _ _).flip
   (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M₁ M₂ M₁ M₂).toLinearMap)
  ∘ₗ TensorProduct.AlgebraTensorModule.homTensorHomMap R _ _ _ _ _ _
  ∘ₗ (TensorProduct.AlgebraTensorModule.congr
    (TensorProduct.lift.equiv A M₁ M₁ N₁)
    (TensorProduct.lift.equiv R _ _ _)).toLinearMap

?

[Eric Wieser]

That looks exactly like what I had in mind

[Eric Wieser]

Regarding the Invertible 2 stuff; it seems we need some generalization that covers both free modules (where we can use toBilin) and https://ncatlab.org/nlab/show/dyadic+rational+module (where we can use associated)

[Eric Wieser]

I assume that not all dyadic modules are free modules.

[Michael Stoll]

Since docs#QuadraticMap.associatedHom is defined in terms of another ring S (s.t. R is an S-algebra), I wil need something along the lines of

import Mathlib

def Module.End.restrictScalars (S R M) [CommRing R] [AddCommGroup M] [Module R M] [CommRing S]
    [Algebra S R] [Module S M] [IsScalarTower S R M] :
    Module.End R M →+* Module.End S M where
  toFun := LinearMap.restrictScalars S
  map_one' := rfl
  map_mul' f g := by
    ext
    simp only [LinearMap.coe_restrictScalars, LinearMap.mul_apply]
  map_zero' := rfl
  map_add' f g := by
    ext
    simp only [LinearMap.restrictScalars_add, LinearMap.add_apply, LinearMap.coe_restrictScalars]

Does this look useful? (Some API would need to be added, I assume...)

[Eric Wieser]

It's an S-alg hom too, right?

[Eric Wieser]

Certainly we want that, though perhaps it's already hiding somewhere. I'm pretty sure we already have the linear version when the domain and codomain are different.

[Michael Stoll]

That would be docs#LinearMap.restrictScalars, I think (but without the compatibility with multiplication, which doesn't exist when domain and codomain are different). (But which is important when talking about invertibility, of course.)

[Eric Wieser]

I was thinking of LinearMap.restrictScalarsₗ

[Michael Stoll]

I'm trying to get Invertible (2 : Module.End S (QuadraticMap R M N →ₗ[S] (BilinMap R M N))) from Invertible (2 : Module.End R N) and find it quite hard.

[Eric Wieser]

Are you sure you need that instance?

[Michael Stoll]

The problem is the change from R-linear to S-linear maps and the simultaneous restriction of scalars.

[Michael Stoll]

I'm trying to replace the definition of docs#QuadraticMap.associatedHom by

  ⅟ (2 : Module.End S (QuadraticMap R M N →ₗ[S] (BilinMap R M N))) •
    { toFun := polarBilin
      map_add' := fun _x _y => LinearMap.ext₂ <| polar_add _ _
      map_smul' := fun _c _x => LinearMap.ext₂ <| polar_smul _ _ }

(trying to keep to the current version as much as possible).
Maybe it's easier to construct the hom in a more pedestrian way.

[Eric Wieser]

Can you make it work with just (2 : Module.End R N)?

[Michael Stoll]

failed to synthesize
  HSMul (Module.End R N) (QuadraticMap R M N →ₗ[S] BilinMap R M N) ?m.732428

[Eric Wieser]

Any luck with

#synth Module (Module.End R N) (QuadraticMap R M N →ₗ[S] BilinMap R M N)

[Eric Wieser]

Or the simpler

#synth Module (Module.End R N) (BilinMap R M N)

[Michael Stoll]

The second works, the first doesn't. (Edited!)

[Michael Stoll]

And I think the first one shouldn't, as there is no reason why the S-linear maps shoud carry an R-linear structure.
EDIT: That's wrong; the R-linear structure is inherited from the target.

[Eric Wieser]

docs#LinearMap.module

[Eric Wieser]

Does adding SMulCommClass S R N help?

[Michael Stoll]

This can be inferred from the IsScalarTower S R N instance that is floating around, so it should not make a difference.

[Michael Stoll]

I've now settled on

def associatedHom : QuadraticMap R M N →ₗ[S] (BilinMap R M N) :=
    { toFun := fun Q ↦ ⅟  (2 : Module.End R N) • polarBilin Q
      map_add' := fun _x _y ↦
        LinearMap.ext₂ fun _ _ ↦ by
          simp only [LinearMap.smul_apply, polarBilin_apply_apply, coeFn_add, polar_add,
            LinearMap.smul_def, LinearMap.map_add, LinearMap.add_apply]
      map_smul' := fun _c _x ↦
        LinearMap.ext₂ fun _ _ ↦ by
          simp only [LinearMap.smul_apply, polarBilin_apply_apply, coeFn_smul, polar_smul,
            LinearMap.smul_def, LinearMap.map_smul_of_tower, RingHom.id_apply] }

which avoids the struggle to get the instance mentioned earlier.

[Eric Wieser]

That's not too bad, but probably justifies defining associatedHom in terms of associated rather than vice versa

[Eric Wieser]

I'll grab a laptop and get to the bottom of why the instance isn't found

[Eric Wieser]

This works:

import Mathlib


instance {S R M} [Semiring R] [SMul S R] [AddCommMonoid M] [Module R M] [SMul S M] [IsScalarTower S R M] :
  SMulCommClass S (Module.End R M) M := ⟨fun s f n => (LinearMap.map_smul_of_tower f s n).symm⟩

variable {R S M N}
variable [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N]
variable [Module R M] [Module R N] [Module S N]
variable [Algebra S R] [IsScalarTower S R N]

open LinearMap (BilinMap)

#synth Module (Module.End R N) (QuadraticMap R M N →ₗ[S] BilinMap R M N)

[Eric Wieser]

The missing piece is that docs#LinearMap.apply_smulCommClass isn't general enough

[Michael Stoll]

#14986 (WIP for now) is a version that builds locally. You aare welcome to have a look.

[Christopher Hoskin]

I've opened a draft PR: https://github.com/leanprover-community/mathlib4/pull/14988

I'm unsure what to do about the results which use LinearMap.IsSymm defined as:

variable [CommSemiring R] [AddCommMonoid M] [Module R M] {I : R →+* R} {B : M →ₛₗ[I] M →ₗ[R] R}

/-- The proposition that a sesquilinear form is symmetric -/
def IsSymm (B : M →ₛₗ[I] M →ₗ[R] R) : Prop :=
  ∀ x y, I (B x y) = B y x

This doesn't directly make sense when R is replaced by a module N as the range. Possibly I should make N a star module?

The other thing I've been wondering about is recovering the original definition of LinearMap.BilinMap.tensorDistrib from the new one. The closest I've been able to get so far is:

def tensorDistrib' : BilinForm A M₁ ⊗[R] BilinForm R M₂ → BilinForm A (M₁ ⊗[R] M₂) :=
    fun B => LinearMap.compr₂ (tensorDistrib R A (M₁ := M₁) (N₁ := A) (M₂ := M₂) (N₂ := R) B)
    (TensorProduct.rid R A).toLinearMap

which doesn't quite work. I guess something like A ⊗[R] A ≃ₗ[A] A is true?

[Eric Wieser]

(TensorProduct.rid A A).restrictScalars R?

[Eric Wieser]

Eric Wieser said:

The missing piece is that docs#LinearMap.apply_smulCommClass isn't general enough

#14991

[Christopher Hoskin]

Eric Wieser said:

(TensorProduct.rid A A).restrictScalars R?

I think I probably want:

variable (R A) in
/-- The tensor product of two bilinear maps injects into bilinear maps on tensor products.

Note this is heterobasic; the bilinear map on the left can take values in a module over a
(commutative) algebra over the ring of the module in which the right bilinear map is valued. -/
def tensorDistrib :
    ((BilinMap A M₁ N₁) ⊗[R] (BilinMap R M₂ N₂)) →ₗ[A] ((BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))) :=
  (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)).symm.toLinearMap ∘ₗ
 ((LinearMap.llcomp A _ _ _).flip
   (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M₁ M₂ M₁ M₂).toLinearMap)
  ∘ₗ TensorProduct.AlgebraTensorModule.homTensorHomMap R _ _ _ _ _ _
  ∘ₗ (TensorProduct.AlgebraTensorModule.congr
    (TensorProduct.lift.equiv A M₁ M₁ N₁)
    (TensorProduct.lift.equiv R _ _ _)).toLinearMap

/- Want to recover
BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂)
-/

def conjecture1 : A ⊗[R] R ≃ₗ[A] A := AlgebraTensorModule.rid R A A

def conjecture2 : BilinMap A (M₁ ⊗[R] M₂) (A ⊗[R] R) ≃ₗ[A] BilinForm A (M₁ ⊗[R] M₂) := sorry

def tensorDistrib' : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) :=
  conjecture2.toLinearMap ∘ₗ (tensorDistrib R A)

Where conjecture2 is a special case of a more general result like LinearMap.BilinForm.congr but with the equivalence in the range.

[Christopher Hoskin]

This appears to work:

/-- This probably belongs somewhere else -/
def congrtmp (e : N₁ ≃ₗ[R] N₂) : BilinMap R M₁ N₁ ≃ₗ[R] BilinMap R M₁ N₂ where
  toFun B := LinearMap.compr₂ B e
  invFun B := LinearMap.compr₂ B e.symm
  left_inv B := ext₂ fun x => by
    simp only [compr₂_apply, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply, implies_true]
  right_inv B := ext₂ fun x => by
    simp only [compr₂_apply, LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply, implies_true]
  map_add' B B' := ext₂ fun x y => by
    simp only [compr₂_apply, add_apply, map_add, LinearEquiv.coe_coe]
  map_smul' B B' := ext₂ fun x y => by
    simp only [compr₂_apply, smul_apply, LinearMapClass.map_smul, LinearEquiv.coe_coe,
      RingHom.id_apply]

variable (R A) in
def tensorDistrib' : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) :=
  (congrtmp (AlgebraTensorModule.rid R A A)).toLinearMap ∘ₗ (tensorDistrib R A)

[Eric Wieser]

LinearEquiv.ofLinear should be a bit easier there

[Christopher Hoskin]

Eric Wieser said:

LinearEquiv.ofLinear

With LinearEquiv.ofLinear we have to prove that the functions in both directions are linear, but with where we need only prove it in one direction.

[Eric Wieser]

Ah, I mistook your maps for being LinearMaps already, but I now see they are not

[Michael Stoll]

Removed the WIP label from #14986 now. Reviews welcome!

[Christopher Hoskin]

I've got as far as I can get with https://github.com/leanprover-community/mathlib4/pull/14988 for the moment.

If @Eric Wieser could please take a look, I'd be very grateful.

[Michael Stoll]

(You can simply write #14988 to get the link to the PR: #14988 .)

[Christopher Hoskin]

@Eric Wieser did you have any further thoughts on https://github.com/leanprover-community/mathlib4/pull/14988 please?

[David Ang]

@Michael Stoll I missed this convo, but maybe something here is useful?

https://github.com/leanprover-community/mathlib4/pull/15786/files

[Michael Stoll]

@David Ang Thanks for the pointer; I'll have a look (but may take some time -- I have to deal with administation stuff today and will be traveling tomorrow).

[David Ang]

Basically I defined a "parallelogram map" (that which satisfies the parallelogram law) and got a quadratic map out of it.

[Christopher Hoskin]

Christopher Hoskin said:

The result I was thinking of is para 22 on p16 of https://www.math.uci.edu/~brusso/LecturesQuadJorAlg134pp.pdf

See also Meyberg's 1972 lecture notes, IX Lemma 1 (p78) https://www.math.uci.edu/~brusso/Meyberg(Reduced2).pdf

[Eric Wieser]

Which reads

If $Q : M \to M'$ is a quadratic map of $\phi$-modules, and $\Omega$ an extension of $\phi$, then $Q$ has a unique extension of $Q_\Omega : M_\Omega \to M'_\Omega$ such that

$$Q_\Omega (\sum w_i \otimes m_i) = \sum w_i ^2\otimes Q(m_i) - \sum_{i<j} w_iw_j \otimes Q(m_i, m_j)$$

[Eric Wieser]

This follows pretty straightforwardly from docs#QuadraticMap.toBilin and the tensor product of bilinear forms

[Eric Wieser]

But maybe the one in your reference doesn't need a free module

[Christopher Hoskin]

I think one takes a quotient to get from the general case to a free module.

[Christopher Hoskin]

It's next on my list of algebraic things to look at after #14988 gets merged.

[Eric Wieser]

Does mathlib know that every module is a quotient of a free module?

[Johan Commelin]

That's Finsupp.total right?

[Antoine Chambert-Loir]

Right, because docs#Finsupp.total applied with the identity map gives you a linear map from the free module with basis M to M, but a few things remain to be said.

[Johan Commelin]

Namely, that it is surjective, and that surjective maps are quotient maps. But I think mathlib also knows those two facts.

[Eric Wieser]

docs#Finsupp.linearCombination_id_surjective is that first result I guess

[Christopher Hoskin]

I presume scalar extensions of Bilinear maps should be defined as:

noncomputable def LinearMap.BilinMap.scalarExtension (B : LinearMap.BilinMap R M₁ N₁) :
  LinearMap.BilinMap A (A ⊗[R] M₁) (A ⊗[R] N₁) := LinearMap.BilinMap.tmul' (LinearMap.mul A A) B

[Eric Wieser]

I think we call that baseChange elsewhere, but that definition indeed looks correct

[Christopher Hoskin]

Eric Wieser said:

I think we call that baseChange elsewhere, but that definition indeed looks correct

Ah, yes - for linear maps here: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/RingTheory/TensorProduct/Basic.lean#L68

[Christopher Hoskin]

And we already have this for bilinear forms: https://github.com/leanprover-community/mathlib4/blob/cd1f49389b69f1e427def7a7c0ddc46f6a7da7dd/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean#L78

[Christopher Hoskin]

I'm trying to prove:

open LinearMap (BilinMap)

namespace QuadraticMap

variable {ι R M N} [LinearOrder ι]
variable [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]

lemma test (bm : Basis ι R M) (Q₁ Q₂ : QuadraticMap R M N) :
    (Q₁ + Q₂).toBilin bm = Q₁.toBilin bm + Q₂.toBilin bm := by
  ext x y
  simp [toBilin]
  simp_rw [polar_add]
  sorry

end QuadraticMap

I get to

(((bm.constr R) fun i ↦
        (bm.constr R) fun j ↦
          if i = j then Q₁ (bm i) + Q₂ (bm i)
          else if i < j then polar (⇑Q₁) (bm i) (bm j) + polar (⇑Q₂) (bm i) (bm j) else 0)
      x)
    y =
  (((bm.constr R) fun i ↦
          (bm.constr R) fun j ↦ if i = j then Q₁ (bm i) else if i < j then polar (⇑Q₁) (bm i) (bm j) else 0)
        x)
      y +
    (((bm.constr R) fun i ↦
          (bm.constr R) fun j ↦ if i = j then Q₂ (bm i) else if i < j then polar (⇑Q₂) (bm i) (bm j) else 0)
        x)
      y

but don't know what to do next?

[Eric Wieser]

lemma test (bm : Basis ι R M) (Q₁ Q₂ : QuadraticMap R M N) :
    (Q₁ + Q₂).toBilin bm = Q₁.toBilin bm + Q₂.toBilin bm := by
  refine bm.ext fun i => bm.ext fun j => ?_
  obtain h | rfl | h := lt_trichotomy i j
  · simp [h.ne, h, toBilin_apply, polar_add]
  · simp [toBilin_apply]
  · simp [h.ne', h.not_lt, toBilin_apply, polar_add]

[Christopher Hoskin]

@Eric Wieser thanks! https://github.com/leanprover-community/mathlib4/pull/18212

[Christopher Hoskin]

If we start with:

variable {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁}
  {N₂ : Type uN₂}

variable [CommRing R] [CommRing A]
variable [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N₁] [AddCommGroup N₂]
variable [Algebra R A] [Module R M₁] [Module A M₁] [Module R N₁] [Module A N₁]
variable [SMulCommClass R A M₁] [IsScalarTower R A M₁]
variable [SMulCommClass R A N₁] [IsScalarTower R A N₁]
variable [Module R M₂] [Module R N₂]

We can define a tensor product on free modules:

variable (R A) in
/-- The tensor product of two quadratic maps injects into quadratic maps on tensor products.

Note this is heterobasic; the quadratic map on the left can take values in a module over a larger
ring than the one on the right. -/
-- `noncomputable` is a performance workaround for mathlib4#7103
noncomputable def tensorDistribFree {ι₁ : Type uι} [LinearOrder ι₁] (bm₁ : Basis ι₁ A M₁)
    {ι₂ : Type uι} [LinearOrder ι₂] (bm₂ : Basis ι₂ R M₂) :
    QuadraticMap A M₁ N₁ ⊗[R] QuadraticMap R M₂ N₂ →ₗ[A] QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) :=
  -- while `letI`s would produce a better term than `let`, they would make this already-slow
  -- definition even slower.
  let toQ := BilinMap.toQuadraticMapLinearMap A A (M₁ ⊗[R] M₂)
  let tmulB := BilinMap.tensorDistrib R A (M₁ := M₁) (M₂ := M₂)
  let toB := AlgebraTensorModule.map
      (QuadraticMap.toBilinHom _ bm₁ : QuadraticMap A M₁ N₁ →ₗ[A] BilinMap A M₁ N₁)
      (QuadraticMap.toBilinHom _ bm₂ : QuadraticMap R M₂ N₂ →ₗ[R] BilinMap R M₂ N₂)
  toQ ∘ₗ tmulB ∘ₗ toB

Given quadratic maps

variable (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂)

We can extend Q₁ and Q₂ to quadratic maps of the free modules:

#check (Q₁.comp (Finsupp.linearCombination A (id : M₁ → M₁)) : QuadraticMap A (M₁ →₀ A) N₁)

#check (Q₂.comp (Finsupp.linearCombination R (id : M₂ → M₂)) : QuadraticMap R (M₂ →₀ R) N₂)

There are canonical bases for the free modules:

#check Basis.ofRepr (LinearEquiv.refl A (M₁ →₀ A))
#check Basis.ofRepr (LinearEquiv.refl R (M₂ →₀ R))

However, one cannot form:

#check tensorDistribFree R A (Basis.ofRepr (LinearEquiv.refl A (M₁ →₀ A)))
  (Basis.ofRepr (LinearEquiv.refl R (M₂ →₀ R)))

without also assuming

variable [LinearOrder M₁] [LinearOrder M₂]

Presumably I need to somehow invoke the Well-ordering theorem or something like that in order to
equip arbitary modules with a Linear Order?

[Eric Wieser]

This well-ordering is already used in docs#LinearMap.BilinMap.toQuadraticMap_surjective

[Eric Wieser]

So you can copy the approach there if you're mid-proof

[Antoine Chambert-Loir]

(Note: it's the canonical basis that you equip with a linear order, not the module itself.)

[Eric Wieser]

If you're making the caller pass in an explicit basis, then I'd argue it's best to also have them choose an explicit ordering with LinearOrder

[Christopher Hoskin]

Eric Wieser said:

If you're making the caller pass in an explicit basis

Presumably I can't put obtain ⟨ι, b⟩ := Module.Free.exists_basis (R := A) (M := (M₁ →₀ A)) in a def?

[Antoine Chambert-Loir]

If I understand things correctly, you don't need docs#Module.Free.exists_basis to get a basis of (M₁ →₀ A), you've got one under the eyes, docs#Finsupp.basis

[Eric Wieser]

If I understand correctly, the argument you're trying to make is "I can choose any order I like, it won't matter in the end because of docs#baseChange_ext or similar", in which case either you'll want to use the axiom of choice somehow (along with Module.Free) or work with Trunc (Basis _ _ _) and Trunc (LinearOrder _) if you feel super-constructive

[Eric Wieser]

(The constructive approach is somewhat disappointing because Basis is accidentally noncomputable, but that could eventually change)

[Antoine Chambert-Loir]

Another point is that a polar bilinear map of a quadratic form is not unique in general, but you have two ways of getting a reasonable representative: either 2 is invertible, and there is a unique symmetric one; or you choose some basis and a linear ordering of that basis, and you arrange so that the “matrix” is upper triangular. In your case, you chose the second option, and what you can prove is that the bilinear form you defined on the tensor products is of the same form for a linear ordering of the product basis (both lexicographic orderings will work). Anyway, and unless I'm mistaken, the tensorDistribFree quadratic map should not depend on those choices.

[Antoine Chambert-Loir]

Final remark: to define docs#QuadraticMap.toBilin, one does not really need a linear order on the chosen basis, it is only needed to be able to linearly order 2-element subsets.

[Eric Wieser]

Can you elaborate on that? You mean that only LinearOrder {(x, y) // x != y} is needed?

[Antoine Chambert-Loir]

You just need to be able to decide, for every two distinct elements $i,j$ in the basis index, whether $i<j$ or $j<i$, but transitivity does not seem to be useful. (And you will decide $b(e_i,e_j)=0$ if $i<j$ and put all the weight on $b(e_j,e_i)$, or the other way round.).

[Eric Wieser]

Right, I suppose Ord ι would suffice

[Eric Wieser]

It's not clear to me that the generality you talk about is useful though

[Antoine Chambert-Loir]

I think you need to have $$\all i,j (i<j) \xor (j<i)\xor (i=j)$$.

[Eric Wieser]

Yep, that's precisely what docs#Ord says

[Eric Wieser]

But I think your other message about not depending on the choice of order is the more interesting one!

[Antoine Chambert-Loir]

Of course, but you'll never know, it may help to have noticed that one day or another (the axiom of choice for 2-element sets is weaker than the full one).
The final remark came out when I thought about the ordering of the product basis indexed by $\iota_1 \times \iota_2$ of the tensor product $M_1\otimes M_2$; what linear ordering do you have here? you have two lexicographic ones, and when I thought about what happens, those remarks came out. (The matrix of the defined bilinear form has many zeroes!)

[Antoine Chambert-Loir]

I am wondering, but I should stop and go to bed, whether the freeness of the modules is necessary for this story to hold true. I suppose not, but I am not sure.

[Christopher Hoskin]

This is where I've got up to, if anyone is curious: #19432

[Christopher Hoskin]

Okay, progress! I think I've manged to prove the following:

$$Q_\Omega (\sum \alpha_i e_{i_1} \otimes f_{i_2}) = \sum_{i=j} \alpha_i^2 Q_1(e_{i_1}) \otimes Q_2(f_{i_2}) + \sum_{i_1 = j_1, i_2 \neq j_2} \alpha_i\alpha_j Q_1(e_{i_1}) \otimes Q_2(f_{i_2},f_{j_2}) + \sum_{i_1 \neq j_1, i_2 = j_2} \alpha_i\alpha_j Q_1(e_{i_1},e_{j_1}) \otimes Q_2(f_{i_2}) + \sum_{i_1 < j_1, i_2 < j_2} \alpha_i\alpha_j Q_1(e_{i_1},e_{j_1}) \otimes Q_2(f_{i_2},f_{j_2})$$

This is the general form of the equation quoted by @Eric Wieser in https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Quadratic.20forms.20with.20values.20in.20a.20larger.20ring/near/475131471

(put $Q_1$ equal to the square map to recover the special case).

The PR is here: #19432 and the result is provisionally called QuadraticMap.tensor_expansion`.

I know it still needs a lot of work, but it would be really useful if someone could give it an initial look to confirm that I'm heading in the right direction with this. Thanks.

[Christopher Hoskin]

Although now I think a bit more about it, I'm not sure the above helps with uniqueness arguments. Whilst it is a formula for $Q$ in terms of $Q_1$ and $Q_2$, it still depends on the choice of basis used to construct $Q$. :(

[Christopher Hoskin]

Oh! I missed this: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Base.20change.20for.20bilinear.20maps.20and.20quadratic.20forms/near/375115826 and #14285