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

• [silvester2000] 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) : (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) : (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) : (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 * 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 * 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 * 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 * 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 (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 (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)) ((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 * 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 = ((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} : (norm R) ((norm S) a) = (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}$.

theorem Algebra.isIntegral_norm {R : Type u_1} [CommRing R] {L : Type u_6} (K : Type u_7) [Field K] [Field L] [Algebra K L] [Algebra R L] [Algebra R K] [IsScalarTower R K L] {x : L} (hx : IsIntegral R x) : IsIntegral R ((norm K) x)

theorem Algebra.norm_eq_norm_adjoin {L : Type u_6} (K : Type u_7) [Field K] [Field L] [Algebra K L] (x : L) : (norm K) x = (norm K) (IntermediateField.AdjoinSimple.gen K x) ^ Module.finrank (↥K⟮x⟯) L

theorem Algebra.norm_eq_prod_roots {L : Type u_6} {K : Type u_7} [Field K] [Field L] [Algebra K L] (F : Type u_8) [Field F] [Algebra K F] {x : L} (hF : Polynomial.Splits (algebraMap K F) (minpoly K x)) : (algebraMap K F) ((norm K) x) = ((minpoly K x).aroots F).prod ^ Module.finrank (↥K⟮x⟯) L

theorem Algebra.norm_eq_prod_embeddings {L : Type u_6} (K : Type u_7) [Field K] [Field L] [Algebra K L] (E : Type u_9) [Field E] [Algebra K E] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsAlgClosed E] (x : L) : (algebraMap K E) ((norm K) x) = ∏ σ : L →ₐ[K] E, σ x

For L/K a finite separable extension of fields and E an algebraically closed extension of K, the norm (down to K) of an element x of L is equal to the product of the images of x over all the K-embeddings σ of L into E.

theorem Algebra.norm_eq_prod_automorphisms {L : Type u_6} (K : Type u_7) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (x : L) : (algebraMap K L) ((norm K) x) = ∏ σ : L ≃ₐ[K] L, σ x