# 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).

source
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

Instances For

source
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.

source
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
source
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
source
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.

source
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`.

source
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
source
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")

Instances For

source
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
source
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

Instances For

source
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
source
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
source
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
source
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
source
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
source
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.

source
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)
source
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}$.

source
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)
source
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
source
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
source
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`.

source
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) = ∏ σ : Gal(L/K), σ x