Commit 2023-08-17 14:45 433c2755

feat(LinearAlgebra/BilinearForm/TensorProduct): base change of bilinear forms (#6306) This generalizes the existing BilinForm.tensorDistrib to be heterogenous in the rings it uses, such that a base change,

protected def baseChange (B : BilinForm R M₂) :
  BilinForm A (A ⊗[R] M₂) :=

falls out as a special case. I do not attempt to generalize BilinForm.tensorDistribEquiv. Unfortunately, this changes the defeq as

-(B₁.tmul B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' * B₂ m₂ m₂'
+(B₁.tmul B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₂ m₂ m₂' • B₁ m₁ m₁'

We could fix this by using the right action instead, but that's a lot of work for a very minorly annoying defeq. This also breaks the defeq of tensorDistribEquiv B = tensorDistrib B; though the reason is more complicated than the scalar action issue above. It would be fixed if we defined all the homogenous operations on tensor products as special cases of the heterogenous ones, but that's also a lot of work for a very small win. This is a port of work from https://github.com/pygae/lean-ga/pull/31, and almost at the end of the path to a base change of quadratic forms and clifford algebras. This was independently developed at the Leiden workshop as BilinForm.baseChange, though the results there are not sorry-free.