Matrices and determinants in tower bases

Let A be an R-algebra with an R-basis bA, and let M be an A-module with an A-basis c. The vectors bA a • c k form the R-basis bA.smulTower' c of M, indexed by pairs (k, a).

• LinearMap.toMatrix_restrictScalars: the matrix in tower bases of an A-linear map f : M → M', viewed as an R-linear map, is the block matrix whose (k, l) block is the matrix Algebra.leftMulMatrix bA x of multiplication by the entry x of the matrix of f in the A-bases. This generalizes LinearMap.restrictScalars_toMatrix from endomorphisms to maps between two modules.
• Module.Basis.det_smulTower': over commutative rings, the determinant in the basis bA.smulTower' c of the family bA a • v k is the norm Algebra.norm R (c.det v) of the determinant of v in the basis c.

The second statement is the form in which determinants over a finite extension are compared with determinants over the base, for instance for the torsion of a based chain complex after restricting its scalars.

theorem LinearMap.toMatrix_restrictScalars {R : Type u_1} {A : Type u_2} {M : Type u_3} {M' : Type u_4} {ι : Type u_5} {ι' : Type u_6} {κ : Type u_7} [Fintype ι] [Finite ι'] [Fintype κ] [DecidableEq ι] [DecidableEq κ] [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid M'] [Module R M'] [Module A M'] [IsScalarTower R A M'] (bA : Module.Basis ι R A) (c : Module.Basis κ A M) (c' : Module.Basis ι' A M') (f : M →ₗ[A] M') : (toMatrix (bA.smulTower' c) (bA.smulTower' c')) (↑R f) = (Matrix.comp ι' κ ι ι R) (((toMatrix c c') f).map ⇑(Algebra.leftMulMatrix bA))

The matrix in tower bases of an A-linear map f, viewed as an R-linear map, is the block matrix obtained by replacing each entry x of the matrix of f by the matrix of multiplication by x in the basis bA.

theorem Module.Basis.det_smulTower' {R : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_4} {κ : Type u_5} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] (bA : Basis ι R A) (c : Basis κ A M) (v : κ → M) : ((bA.smulTower' c).det fun (x : κ × ι) => bA x.2 • v x.1) = (Algebra.norm R) (c.det v)

The determinant, in the tower basis bA.smulTower' c, of the family of vectors bA a • v k is the norm of the determinant of the family v in the basis c.