Change of basis for matrices of bilinear and sesquilinear maps

Mathlib's LinearMap.toMatrix₂_mul_basis_toMatrix records how the matrix of a bilinear map responds to a change of basis, but it is stated for B : M₁ →ₗ[R] M₂ →ₗ[R] R, whose values are the scalars themselves. A bilinear map valued in an R-algebra S has no such lemma, because its matrix has entries in S while a change-of-basis matrix has entries in R; the two are related only after pushing the latter along algebraMap R S. That is what this file supplies, for LinearMap.toMatrix₂Aux, the combinator whose target is the map's own codomain.

The file also supplies the semilinear analogue of Mathlib's theorem: when the codomain is the scalar ring, each coordinate matrix is first mapped by the ring homomorphism governing its argument. This gives the involution-transpose formula for a sesquilinear form.

Main results

• LinearMap.toMatrix₂Aux_comp_index: precomposing the index families takes a submatrix, of which reindexing a basis is the special case. Stated at the full sesquilinear generality LinearMap.toMatrix₂Aux accepts, since the equality is definitional.
• LinearMap.toMatrix₂Aux_mul_map_basis_toMatrixₛₗ: the change-of-basis law for a sesquilinear map into a commutative semiring, with each coordinate matrix transformed by the ring homomorphism governing the corresponding argument.
• LinearMap.toMatrix₂Aux_mul_map_basis_toMatrix: the change-of-basis law, oriented as Mathlib's is, with the change-of-basis matrices pushed into the codomain. The codomain need only be a possibly noncommutative semiring.
• LinearMap.det_toMatrix₂Aux_eq_det_toMatrix₂Aux: for a map on a single ℤ-module, the signed determinant of the matrix is independent of the basis, and of its index type. An integral change-of-basis matrix has determinant ±1, so the congruence above multiplies the determinant by its square, namely 1. This needs CommRing S and no order; the absolute-value statement is congrArg abs away and is left to the caller.

The statements differ in what they ask of the codomain. toMatrix₂Aux_comp_index needs only an additive commutative monoid carrying the required actions. The sesquilinear change-of-basis law allows distinct source scalar rings and has values in a commutative semiring. The bilinear law allows values in an R-algebra, which may be a noncommutative semiring: the proof uses only that the images of algebraMap are central. The determinant result needs a commutative ring, and ℤ as the scalars.

Implementation notes

TauCeti/LinearAlgebra/IntegralLattice/Gram.lean carries the same mathematics for an integral form — gramMatrix, gramMatrix_reindex, gramDet_eq_gramDet, determinant, discriminant — with the same argument about integral change-of-basis matrices having determinant ±1. That development is ℤ-valued: its Gram matrix has entries in the scalars, so it cannot serve a map valued in a larger codomain, which is the gap filled here.

@[simp]

theorem LinearMap.toMatrix₂Aux_comp_index {R : Type u_1} {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [CommSemiring R] [Semiring R₁] [Semiring S₁] [Semiring R₂] [Semiring S₂] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] [AddCommMonoid N₂] [Module R N₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] {σ₁ : R₁ →+* S₁} {σ₂ : R₂ →+* S₂} (B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) (v₁ : n → M₁) (v₂ : m → M₂) (e₁ : n' → n) (e₂ : m' → m) : (toMatrix₂Aux R (v₁ ∘ e₁) (v₂ ∘ e₂)) B = ((toMatrix₂Aux R v₁ v₂) B).submatrix e₁ e₂

Precomposing the index families with any maps takes a submatrix. Reindexing a basis is the special case where the maps are the inverses of equivalences, since Module.Basis.coe_reindex puts b.reindex σ into the form b ∘ σ.symm. Stated for the sesquilinear maps LinearMap.toMatrix₂Aux accepts, the equality being definitional.

@[simp]

theorem LinearMap.toMatrix₂Aux_mul_map_basis_toMatrixₛₗ {R₁ : Type u_1} {R₂ : Type u_2} {S : Type u_3} {M₁ : Type u_4} {M₂ : Type u_5} {ι₁ : Type u_6} {ι₂ : Type u_7} {ι₁' : Type u_8} {ι₂' : Type u_9} [CommSemiring R₁] [CommSemiring R₂] [CommSemiring S] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁ : R₁ →+* S} {σ₂ : R₂ →+* S} [Fintype ι₁] [Fintype ι₂] (B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] S) (b₁ : Module.Basis ι₁ R₁ M₁) (b₂ : Module.Basis ι₂ R₂ M₂) (c₁ : Module.Basis ι₁' R₁ M₁) (c₂ : Module.Basis ι₂' R₂ M₂) : ((b₁.toMatrix ⇑c₁).map ⇑σ₁).transpose * (toMatrix₂Aux S ⇑b₁ ⇑b₂) B * (b₂.toMatrix ⇑c₂).map ⇑σ₂ = (toMatrix₂Aux S ⇑c₁ ⇑c₂) B

Change of basis for a sesquilinear map. If the first and second arguments are semilinear for σ₁ and σ₂, respectively, then their coordinate matrices enter the change-of-basis formula after applying those ring homomorphisms entrywise.

For a Laurent-sesquilinear pairing, σ₁ is the involution q ↦ q⁻¹ and σ₂ is the identity, so the first factor is the involution-transpose of the change-of-basis matrix.

@[simp]

theorem LinearMap.toMatrix₂Aux_mul_map_basis_toMatrix {R : Type u_1} {S : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {ι₁ : Type u_5} {ι₂ : Type u_6} {ι₁' : Type u_7} {ι₂' : Type u_8} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [Semiring S] [Algebra R S] [Fintype ι₁] [Fintype ι₂] (B : M₁ →ₗ[R] M₂ →ₗ[R] S) (b₁ : Module.Basis ι₁ R M₁) (b₂ : Module.Basis ι₂ R M₂) (c₁ : Module.Basis ι₁' R M₁) (c₂ : Module.Basis ι₂' R M₂) : ((b₁.toMatrix ⇑c₁).map ⇑(algebraMap R S)).transpose * (toMatrix₂Aux R ⇑b₁ ⇑b₂) B * (b₂.toMatrix ⇑c₂).map ⇑(algebraMap R S) = (toMatrix₂Aux R ⇑c₁ ⇑c₂) B

The change-of-basis law for the matrix of a bilinear map valued outside the scalars. The change-of-basis matrices enter through algebraMap R S, since the matrix of B has entries in S. Compare LinearMap.toMatrix₂_mul_basis_toMatrix, which is the case S = R. The codomain need not be commutative: the images of algebraMap are central, which is all the proof uses.

theorem LinearMap.det_toMatrix₂Aux_eq_det_toMatrix₂Aux {S : Type u_1} {M : Type u_2} {ι : Type u_3} {ι' : Type u_4} [CommRing S] [AddCommGroup M] [Module ℤ M] [Fintype ι] [DecidableEq ι] [Fintype ι'] [DecidableEq ι'] (B : M →ₗ[ℤ] M →ₗ[ℤ] S) (b : Module.Basis ι ℤ M) (b' : Module.Basis ι' ℤ M) : ((toMatrix₂Aux ℤ ⇑b' ⇑b') B).det = ((toMatrix₂Aux ℤ ⇑b ⇑b) B).det

Over ℤ, the determinant of the matrix is basis-independent, and independent of the index type too. An integral change-of-basis matrix has determinant ±1, so the congruence of toMatrix₂Aux_mul_map_basis_toMatrix multiplies the determinant by its square, namely 1.