Transitivity of algebra norm

Suppose we have an R-algebra S with a finite basis. For each s : S, the determinant of the linear map given by multiplying by s gives information about the roots of the minimal polynomial of s over R.

References

• [Sil00] Silvester, Determinants of Block Matrices, The Mathematical Gazette (2000).

def Algebra.Norm.Transitivity.auxMat {S : Type u_2} {m : Type u_5} [CommRing S] (M : Matrix m m S) [DecidableEq m] (k : m) : Matrix m m S

Given a ((m-1)+1)x((m-1)+1) block matrix M = [[A,b],[c,d]], auxMat M k is the auxiliary matrix [[dI,0],[-c,1]]. k corresponds to the last row/column of the matrix.

Equations

• Algebra.Norm.Transitivity.auxMat M k = Matrix.of fun (i j : m) => if j = k then if i = k then 1 else 0 else if i = k then -M k j else if i = j then M k k else 0

theorem Algebra.Norm.Transitivity.auxMat_blockTriangular {S : Type u_2} {m : Type u_5} [CommRing S] (M : Matrix m m S) [DecidableEq m] (k : m) : (Algebra.Norm.Transitivity.auxMat M k).BlockTriangular fun (x : m) => x ≠ k

aux M k is lower triangular.

theorem Algebra.Norm.Transitivity.auxMat_toSquareBlock_ne {S : Type u_2} {m : Type u_5} [CommRing S] (M : Matrix m m S) [DecidableEq m] (k : m) : (Algebra.Norm.Transitivity.auxMat M k).toSquareBlock (fun (x : m) => x ≠ k) True = M k k • 1

theorem Algebra.Norm.Transitivity.auxMat_toSquareBlock_eq {S : Type u_2} {m : Type u_5} [CommRing S] (M : Matrix m m S) [DecidableEq m] (k : m) : (Algebra.Norm.Transitivity.auxMat M k).toSquareBlock (fun (x : m) => x ≠ k) False = 1

theorem Algebra.Norm.Transitivity.mul_auxMat_blockTriangular {S : Type u_2} {m : Type u_5} [CommRing S] (M : Matrix m m S) [DecidableEq m] (k : m) [Fintype m] : (M * Algebra.Norm.Transitivity.auxMat M k).BlockTriangular fun (x : m) => x = k

M * aux M k is upper triangular.

theorem Algebra.Norm.Transitivity.mul_auxMat_corner {S : Type u_2} {m : Type u_5} [CommRing S] (M : Matrix m m S) [DecidableEq m] (k : m) [Fintype m] : (M * Algebra.Norm.Transitivity.auxMat M k) k k = M k k

The lower-right corner of M * aux M k is the same as the corner of M.

theorem Algebra.Norm.Transitivity.mul_auxMat_toSquareBlock_eq {S : Type u_2} {m : Type u_5} [CommRing S] (M : Matrix m m S) [DecidableEq m] (k : m) [Fintype m] : (M * Algebra.Norm.Transitivity.auxMat M k).toSquareBlock (fun (x : m) => x = k) True = M k k • 1

def Algebra.Norm.Transitivity.termMulAuxMatBlock : Lean.ParserDescr

The upper-left block of M * aux M k.

Equations

• Algebra.Norm.Transitivity.termMulAuxMatBlock = Lean.ParserDescr.node `Algebra.Norm.Transitivity.termMulAuxMatBlock 1024 (Lean.ParserDescr.symbol "mulAuxMatBlock")

theorem Algebra.Norm.Transitivity.det_mul_corner_pow {S : Type u_2} {m : Type u_5} [CommRing S] (M : Matrix m m S) [DecidableEq m] (k : m) [Fintype m] : M.det * M k k ^ (Fintype.card m - 1) = M k k * ((M * Algebra.Norm.Transitivity.auxMat M k).toSquareBlock (fun (x : m) => x = k) False).det

noncomputable def Algebra.Norm.Transitivity.cornerAddX {S : Type u_2} {m : Type u_5} [CommRing S] (M : Matrix m m S) [DecidableEq m] (k : m) : Matrix m m (Polynomial S)

A matrix with X added to the corner.

Equations

• Algebra.Norm.Transitivity.cornerAddX M k = (Matrix.diagonal fun (i : m) => if i = k then Polynomial.X else 0) + M.map ⇑Polynomial.C

theorem Algebra.Norm.Transitivity.polyToMatrix_cornerAddX {R : Type u_1} {S : Type u_2} {n : Type u_4} {m : Type u_5} [CommRing R] [CommRing S] (M : Matrix m m S) [DecidableEq m] [DecidableEq n] (k : m) [Fintype n] (f : S →+* Matrix n n R) : f.polyToMatrix (Algebra.Norm.Transitivity.cornerAddX M k k k) = (-f (M k k)).charmatrix

theorem Algebra.Norm.Transitivity.eval_zero_det_det {R : Type u_1} {S : Type u_2} {n : Type u_4} {m : Type u_5} [CommRing R] [CommRing S] (M : Matrix m m S) [DecidableEq m] [DecidableEq n] (k : m) [Fintype m] [Fintype n] (f : S →+* Matrix n n R) : Polynomial.eval 0 (f.polyToMatrix (Algebra.Norm.Transitivity.cornerAddX M k).det).det = (f M.det).det

theorem Algebra.Norm.Transitivity.eval_zero_comp_det {R : Type u_1} {S : Type u_2} {n : Type u_4} {m : Type u_5} [CommRing R] [CommRing S] (M : Matrix m m S) [DecidableEq m] [DecidableEq n] (k : m) [Fintype m] [Fintype n] (f : S →+* Matrix n n R) : Polynomial.eval 0 ((Matrix.comp m m n n (Polynomial R)) ((Algebra.Norm.Transitivity.cornerAddX M k).map ⇑f.polyToMatrix)).det = ((Matrix.comp m m n n R) (M.map ⇑f)).det

theorem Algebra.Norm.Transitivity.comp_det_mul_pow {R : Type u_1} {S : Type u_2} {n : Type u_4} {m : Type u_5} [CommRing R] [CommRing S] (M : Matrix m m S) [DecidableEq m] [DecidableEq n] (k : m) [Fintype m] [Fintype n] (f : S →+* Matrix n n R) : ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) = (f (M k k)).det * ((Matrix.comp { a : m // (a = k) = False } { a : m // (a = k) = False } n n R) (((M * Algebra.Norm.Transitivity.auxMat M k).toSquareBlock (fun (x : m) => x = k) False).map ⇑f)).det

theorem Algebra.Norm.Transitivity.det_det_aux {R : Type u_1} {S : Type u_2} {n : Type u_4} {m : Type u_5} [CommRing R] [CommRing S] {M : Matrix m m S} [DecidableEq m] [DecidableEq n] (k : m) [Fintype m] [Fintype n] {f : S →+* Matrix n n R} (ih : ∀ (M : Matrix { a : m // (a = k) = False } { a : m // (a = k) = False } S), (f M.det).det = ((Matrix.comp { a : m // (a = k) = False } { a : m // (a = k) = False } n n R) (M.map ⇑f)).det) : ((f M.det).det - ((Matrix.comp m m n n R) (M.map ⇑f)).det) * (f (M k k)).det ^ (Fintype.card m - 1) = 0

theorem Matrix.det_det {R : Type u_1} {S : Type u_2} {n : Type u_4} {m : Type u_5} [CommRing R] [CommRing S] (M : Matrix m m S) [DecidableEq m] [DecidableEq n] [Fintype m] [Fintype n] (f : S →+* Matrix n n R) : (f M.det).det = ((Matrix.comp m m n n R) (M.map ⇑f)).det

The main result in Silvester's paper Determinants of Block Matrices: the determinant of a block matrix with commuting, equal-sized, square blocks can be computed by taking determinants twice in a row: first take the determinant over the commutative ring generated by the blocks (S here), then take the determinant over the base ring.

theorem LinearMap.det_restrictScalars {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Module.Free R S] [AddCommGroup A] [Module R A] [Module S A] [IsScalarTower R S A] [Module.Free S A] {f : A →ₗ[S] A} : LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

theorem Algebra.norm_norm {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Free R S] {A : Type u_6} [Ring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Module.Free S A] {a : A} : (Algebra.norm R) ((Algebra.norm S) a) = (Algebra.norm R) a

Let A/S/R be a tower of finite free tower of rings (with R and S commutative). Then $\text{Norm}_{A/R} = \text{Norm}_{A/S} \circ \text{Norm}_{S/R}$.