Base change for bilinear maps and quadratic forms

Stream: Is there code for X?

[Kevin Buzzard]

Am I reinventing the wheel here? Mathematically the set-up is: V is a vector space over a field K (or a module over a ring) and K -> K' is a morphism of fields, and then quadratic or bilinear forms on $V$ should push forward to quadratic or bilinear forms on $V\otimes_K K'$ (at least if 2 is invertible, in the quadratic form case).

import Mathlib

-- I want to do base change for quadratic forms.
-- How much of the below is re-inventing the wheel?

-- M and N are R-modules and A is an R-algebra and T is an A-module
variables (R A M N T : Type) [CommRing R] [CommRing A] [Algebra R A]
  [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]
  [AddCommGroup T] [Module A T]
  -- and I want to regard T as an R-module too, in the obvious way
  [Module R T] [IsScalarTower R A T]

open TensorProduct -- for notation

def LinearMap.baseChangeLeft (f : M →ₗ[R] T) : A ⊗[R] M →ₗ[A] T where
  toFun := TensorProduct.lift ({
    toFun := fun a ↦ a • f
    map_add' := sorry
    map_smul' := sorry
  } : A →ₗ[R] M →ₗ[R] T)
  map_add' := sorry
  map_smul' := sorry

def algebraMap' : R →ₗ[R] A where
  toFun := algebraMap R A
  map_add' := sorry
  map_smul' := sorry

def TensorProduct.rid' : A ⊗[R] R ≃ₗ[A] A where
  toLinearMap := LinearMap.baseChangeLeft R A R A (algebraMap' R A)
  invFun := fun a ↦ a ⊗ₜ 1
  left_inv := sorry
  right_inv := sorry

def BilinForm.baseChange (F : BilinForm R M) : BilinForm A (A ⊗[R] M) := by
  let L := BilinForm.toLinHom R F
  let L' := L.baseChange A
  refine LinearMap.toBilin ?_
  refine LinearMap.comp ?_ L'
  apply LinearMap.baseChangeLeft
  refine LinearMap.comp ?_ (LinearMap.baseChangeHom R A _ _)
  apply LinearMap.restrictScalars R (S := A)
  refine LinearMap.llcomp A _ _ _ (?_ : A ⊗[R] R →ₗ[A] A)
  exact (TensorProduct.rid' R A).toLinearMap

def QuadraticForm.baseChange [Invertible (2 : R)] (F : QuadraticForm R M) : QuadraticForm A (A ⊗[R] M) := by
  let B : BilinForm R M := associatedHom R F
  let B' : BilinForm A (A ⊗[R] M) := B.baseChange R A M
  exact B'.toQuadraticForm

[Johan Commelin]

Do we have a characteristic predicate for base changes? Because we'll probably want them pretty soon

[Antoine Chambert-Loir]

Why would you need an assumption on the characteristic?

[Kevin Buzzard]

You shouldn't need this assumption but I was lazy

[Kevin Buzzard]

I didn't think carefully but I was worried about whether you could have a quadratic form on V which extends in more than one natural way to V tensor_K K' if char(K)=2. Can this happen?

[Scott Carnahan]

Any two extensions of a quadratic form are equal on pure tensors by quadratic homogeneity, and equal on finite sums thereof, since they have equal associated bilinear forms. (so I think the answer is no)

[Kevin Buzzard]

What is the "associated bilinear form" to a quadratic form in characteristic 2?

[Kevin Buzzard]

docs#QuadraticForm

[Kevin Buzzard]

OK got it

[Kevin Buzzard]

(I didn't even look at the definition when I wrote the base change code, I have used the wrong bilinear form in char 2, I didn't really think about the char 2 subtleties until now)

[Kevin Buzzard]

Oh wait. Given a quadratic form over K, I am assuming that by "associated bilinear form" the one being talked about here docs#QuadraticForm.exists_companion . I then base change this bilinear form to K'. And now what? I can't recover the quadratic form.

I was originally using docs#QuadraticForm.associatedHom (oh maybe this is the one you meant?) and this construction needs that 2 is invertible in mathlib.

[Eric Wieser]

Note that exists_companion is there only to permit the really weird corner case of quadratic forms over semirings (which at least one paper talked about)

[Eric Wieser]

So I'm pretty sure that's not what "associated" was intended to mean

[Eric Wieser]

https://leanprover-community.github.io/mathlib4_docs/Counterexamples/QuadraticForm.html is probably also relevant here

[Kevin Buzzard]

Right. Because these are distinct notions I am confused about deducing base change for quadratic forms from base change for bilinear forms. Given a quadratic form you can make a bilinear form by $B(x,y)=Q(x+y)-Q(x)-Q(y)$, and given a bilinear form you can make a quadratic form by $Q'(x)=B(x,x)$ and then $Q'=2Q$ so in characteristic 2 if you start with $Q$ then $Q'=0$, and you get a non-injective map from quadratic forms to bilinear forms, so you're losing information.

[Eric Wieser]

to_dual_prod in !3#18447 contains another example of something that ended up needing char != 2 (which is annoying because the source never mentioned it...)

[Kevin Buzzard]

I am a bit confused about why you can't just add an arbitrary additive group homomorphism $h:\frac{V\otimes_K K'}{V\otimes_K K}\to K'$ to $Q$ and get a different $Q$ which is also a candidate for "the base change". This is why I'm confused about what Hasse-Minkowski says. I think it might be a statement about symmetric bilinear forms, not quadratic forms?

[Kevin Buzzard]

mathlib#18447

[Kevin Buzzard]

Hmm, Wikipedia claims that Hasse-Minkowski is (a) a statement about quadratic forms and (b) valid for all global fields (no citation though). I am now a bit confused about whether it should really be a theorem about e.g. symmetric bilinear forms.

[Kevin Buzzard]

@Antoine Chambert-Loir what am I doing wrong?

[Scott Carnahan]

I'll try explaining with TeX. Let $Q_1$ and $Q_2$ be extensions of $Q$ to $V \otimes K'$. For elements of the form $v \otimes a$, we know that $Q_1(v \otimes a) = a^2Q(v) = Q_2(v \otimes a)$, so it suffices to show that $Q_1$ and $Q_2$ agree on finite sums. However, if we set $B_i(x,y) = Q_i(x+y)-Q_i(x)-Q_i(y)$, then we have $B_1 = B_2$ by bilinearity. Now, suppose we know $Q_1(x) = Q_2(x)$ and $Q_1(y) = Q_2(y)$. Then, $Q_1(x+y) = Q_1(x)+Q_1(y)+B_1(x,y) = Q_2(x) + Q_2(y) + B_2(x,y) = Q_2(x+y)$. One can then induct on number of pure summands.

[Heather Macbeth]

@Scott Carnahan Double $ !

[Scott Carnahan]

Thanks! I have fixed it.

[Antoine Chambert-Loir]

There are multiple definitions of quadratic forms (especially in characteristic two), but the classical one, when written in coordinates, exactly amounts to homogeneous polynomial maps of degree two. And you know how to base change them.

[Antoine Chambert-Loir]

You may ask: what if I have no coordinates, or quadratic forms from one module to another one, etc.

Given a commutative ring $k$ and $k$-modules $M,N$, there is a notion of polynomial map $f$ from $M$ to $N$: this is the datum of maps $f_R\colon M\otimes_k R\to N\otimes_k R$ for any $k$-algebra $R$ subject to a naturality condition. You can then prove that such a family of maps is naturally a polynomial in the sense that for every family $(m_1,m_2,\dots)$ of elements of $M$, there is a polynomial $c_m$ in indeterminates $T_1,T_2,\dots$ (valued in $N$) such that $f_R (a_1m_1+a_2m_2+\dots) = c_m(a_1,a_2,\dots)$ for all families $(a_1,a_2,\dots)$ in $R$. Homogeneous components give rise to multilinear maps, there are polarization identities, etc.

Polynomial maps form a graded $k$-module and there is a universal one (in each degree $n$): the… divided power algebra $\mathrm{DP}_n(M)$ in the sense that that there is homogeneous polynomial map $M\to \mathrm{DP}_n(M)$ — given by $m\mapsto m^{(n)}$, the $n$-th divided power of $m$ — so that any polynomial map $M\to N$ which is homogeneous of degree $n$ is of the form $m\mapsto \phi(m^ { (n) } )$ for a unique linear map $\mathrm{DP}_n(M)\to N$.

This will be in mathlib one day or another because this is needed to construct $B_{\mathrm{cris}}$… (Part of it is already formalized in our work with @María Inés de Frutos Fernández )

[Yury G. Kudryashov]

You can use double dollars for math: $\mathcal R$

[Kevin Buzzard]

Scott C aah I see! Thanks! I wasn't using the info that the forms agree on a*v for a not in K. Antoine I need to think longer about your reply :-)

[Eric Wieser]

Kevin and I discussed privately 6 months ago that the similar task of defining $Q_{12}(m_1 \otimes m_2) = Q_1(m_1)Q_2(m_2)$ didn't seem to work in characteristic 2; is this not a special case of that with $Q_1(a)=a^2$? Or maybe the base change fixes things.

[Eric Wieser]

Somehow despite reading this thread I managed to miss that it's exactly what I needed. I've *almost* managed to prove

def tensor_distrib' : bilin_form A M₁ ⊗[R] bilin_form R M₂ →ₗ[A] bilin_form A (M₁ ⊗[R] M₂) :=

the missing piece is

def tensor_tensor_tensor_comm :
  (M ⊗[R] N) ⊗[A] (P ⊗[R] Q) ≃ₗ[A] (M ⊗[A] P) ⊗[R] (N ⊗[R] Q) :=
sorry

@[simp] lemma tensor_tensor_tensor_comm_apply (m : M) (n : N) (p : P) (q : Q) :
  tensor_tensor_tensor_comm R A M N P Q ((m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q)) = (m ⊗ₜ p) ⊗ₜ (n ⊗ₜ q) :=
sorry

the full context is https://github.com/pygae/lean-ga/pull/31/, which shows all the other helper lemmas I needed in mathlib.

[Kevin Buzzard]

I filled in the sorrys in my earlier code BTW:

import Mathlib

variable (R A M N T : Type) [CommRing R] [CommRing A] [Algebra R A]
  [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]
  [AddCommGroup T] [Module A T] [Module R T] [IsScalarTower R A T]

open TensorProduct

def LinearMap.baseChangeLeft (f : M →ₗ[R] T) : A ⊗[R] M →ₗ[A] T where
  toFun := TensorProduct.lift ({
    toFun := fun a ↦ a • f
    map_add' := fun x y => add_smul x y f
    map_smul' := by
      intro r x
      simp only [smul_assoc, RingHom.id_apply]
  } : A →ₗ[R] M →ₗ[R] T)
  map_add' := map_add _
  map_smul' := by
    intro a x
    simp only [RingHom.id_apply]
    refine TensorProduct.induction_on x ?_ ?_ ?_
    · simp
    · intros b m
      simp [mul_smul a b (f m), show a • b ⊗ₜ[R] m = (a * b) ⊗ₜ[R] m from rfl]
    · intros x y hx hy
      simp [hx, hy]

def algebraMap' : R →ₗ[R] A where
  toFun := algebraMap R A
  map_add' := by simp
  map_smul' := by
    intros r s
    simp [Algebra.smul_def r ((algebraMap R A) s)]

def TensorProduct.rid' : A ⊗[R] R ≃ₗ[A] A where
  toLinearMap := LinearMap.baseChangeLeft R A R A (algebraMap' R A)
  invFun := fun a ↦ a ⊗ₜ 1
  left_inv := by
    intro x
    refine TensorProduct.induction_on x ?_ ?_ ?_
    · simp [LinearMap.baseChangeLeft, algebraMap']
    · intros a r
      simp [LinearMap.baseChangeLeft, algebraMap']
      rw [mul_comm]
      nth_rewrite 2 [show r = r • (1 : R) by simp]
      rw [← smul_tmul, _root_.Algebra.smul_def]
    · intros x y hx hy
      rw [AddHom.map_add']
      simp_all
      rw [add_tmul, hx, hy]
  right_inv := by
    intro a
    simp [LinearMap.baseChangeLeft, algebraMap']

but as Eric has pointed out to me already, there is probably a better approach to some of this stuff.

[Kevin Buzzard]

Re tensor_tensor_tensor_comm, what is an R-module and what is an A-module? I'm assuming A is an R-algebra and everything is commutative. Oh: I think it must be that M and P are A-modules and the other two are R-modules.

[Eric Wieser]

Yes, exactly. I tried to copy the approach we used to define tensor_tensor_tensor_comm, but it seems we're missing a lot of components

[Eric Wieser]

I've updated my message above to contain links to the source

[Eric Wieser]

The full (lean3, sorry) setup is

variables [comm_semiring R] [comm_semiring A] [algebra R A]
variables [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M]
variables [add_comm_monoid N] [module R N]
variables [add_comm_monoid P] [module R P] [module A P] [is_scalar_tower R A P]
variables [add_comm_monoid Q] [module R Q]

[Eric Wieser]

Now sorry-free :tada:!

[Eric Wieser]

"The algebraic theory of spinors" agrees with the claim that a base change of quadratic forms is possible in characteristic two over finite dimensional spaces, though the proof is just "we see that there exists only one quadratic form"...

image.png

[Kevin Buzzard]

You can't in general choose $B_0$ in char 2, right?

[Eric Wieser]

It seems to claim you can, just not uniquely (and it might not be symmetric)

[Kevin Buzzard]

Oh sorry you're right; I was only thinking about symmetric forms.

[Eric Wieser]

Should we redefine quadratic_form as the quotient of bilinear maps by equality on the diagonal?

[Eric Wieser]

Then at least we could pull out the B_0, compute with it, and prove that the computation was invariant to the choice

[Eric Wieser]

Maybe that's too constructive a question for you to care about

[Kevin Buzzard]

Yeah I can't comment on that, other than to say that it's not the definition in the books (but then again our definition of compactness is not the definition in the books either)

[Eric Wieser]

Our definition of docs#QuadraticForm is already not the one used by most books

[Antoine Chambert-Loir]

Why do you say it's not the def in the books? Aren't they defined as a map q such that there exists a bilinear form f such that q(x)=f(x,x) for all x?

[Antoine Chambert-Loir]

Anyway, there will be side cases, especially in char 2, where there are different notions of quadratic forms, whose goal is to provide a better understanding of the geometry of the orthogonal groups.

[Antoine Chambert-Loir]

I know B. has a tentative general definition which encompasses all known cases. The quadratic form and the bilinear form do not take their values in the same module, but there are two maps whose composition is multiplication by 2!

[Eric Wieser]

#6306 implements the base change of bilinear forms in mathlib4, though has some dependencies to clear up

[Eric Wieser]

The dependencies are now all clear on the above

[Antoine Chambert-Loir]

Is there a base change for linear forms?

[Antoine Chambert-Loir]

and for multilinear forms?

[Eric Wieser]

docs#LinearMap.baseChange ?

[Eric Wieser]

I guess you have to post-compose that with rid

[Eric Wieser]

Base change (and tensor product) of multilinear forms sounds like a fun project!

[Eric Wieser]

Alex J. Best said:

I think we found that we also need the lemma,

@[simp]
lemma QuadraticForm.baseChange_associated (F : QuadraticForm R₁ M) :
  (associated : _ →ₗ[A] _) (F.baseChange A) = ((associated : _ →ₗ[R₁] _) F).baseChange A :=

is that easy enough with your changes Eric?

It's in #6636