Grace/Cumulus/Algebra/Ring/MatrixPolynomial.g17

Open in Workbench Download source

Imports

MatrixCramer · Bicommutant · Polynomial.BundledEvaluation

Declarations

Source

1-- Polynomials evaluated at a square matrix: the scalar matrices a · 1, the2-- commutative ring commutant(R, n, M) generated inside the matrix ring by M3-- and the scalars, and the evaluation evalAt(M) : polynomialRing(R, {0})4-- →+* commutant(R, n, M) sending X to M and the constants to the scalar5-- matrices; everything here is ZF6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Algebra.Ring.MatrixPolynomial12import MatrixCramer13import Bicommutant14import Polynomial.BundledEvaluation1516-- The scalar matrix a · 1, the embedding of R, and the commutative ring17-- of matrices commuting with everything that commutes with M.18def scalarMatrix (R n a : Set) : Set := scalarMultiple(R, n, a, oneMatrix(R, n))19def commutant (R n M : Set) : Set := bicommutantRing(matrixRing(R, n), {M})2021section Scalars22variable (R : Set) (n : Nat)23hypothesis comm : CommRing(R)2425theorem oneMatrix.guard26  shows oneMatrix(R, n) : R ^ n × n27proof28  have one := oneMatrix.matrix at R, n with *29  exact Matrix.of_square with one3031theorem scalarMatrix.entry (a : R) (i j : Set)32  requires row : i ∈ n33  requires column : j ∈ n34  shows scalarMatrix(R, n, a)[i, j] = a * singleValue(R.carrier, R.zero, R.one, j, i)35proof36  have one := oneMatrix.guard at R, n with *37  have entry := scalarMultiple.entry at R, n, a, oneMatrix(R, n), i, j with *38  have unit := oneMatrix.entry at R, n, i, j with *39  unfold scalarMatrix40  cc4142theorem scalarMatrix.guard (a : R)43  shows scalarMatrix(R, n, a) : R ^ n × n44proof45  have one := oneMatrix.guard at R, n with *46  unfold scalarMatrix47  exact scalarMultiple.matrix with *4849instance scalarMatrix.mem (a : R)50  shows scalarMatrix(R, n, a) ∈ Ring.carrier(matrixRing(R, n))51proof52  have guard := scalarMatrix.guard at R, n, a with *53  exact Matrix.mem_ring with guard5455-- Scalar matrices multiply every matrix entrywise, from either side.56theorem scalarMatrix.mul_left (a : R) (N : R ^ n × n)57  shows scalarMatrix(R, n, a) * N = scalarMultiple(R, n, a, N)58proof59  have parts := CommRing.parts with comm60  have finite := Finite.natural at n61  have scalar := scalarMatrix.guard at R, n, a with *62  have product := Matrix.of_mem at scalarMatrix(R, n, a) * N, R, n with (Ring.mul_mem with *)63  have scaled := scalarMultiple.matrix at R, n, a, N with *64  have aIn : a ∈ R by assumption65  apply Matrix.ext with product, scaled66  intros i hi j hj67  have entryN := Matrix.entry at N, R, n, i, j with *68  have entry := matrixRing.mul_entry at R, n, scalarMatrix(R, n, a), N, i, j with *69  have scale := scalarMultiple.entry at R, n, a, N, i, j with *70  have squareS := Matrix.square at scalarMatrix(R, n, a), R, n with *71  have squareN := Matrix.square at N, R, n with assumption72  have shapeS := squareMatrices.membership.forward with squareS73  have shapeN := squareMatrices.membership.forward with squareN74  have weights := matrixProductWeights.function at n, R.carrier, R.add, R.zero,75    R.neg, R.mul, R.one, scalarMatrix(R, n, a), N, i, j with *76  have selector := coefficientSingle.function at n, R.carrier, R.zero, a * N[i, j], i with *77  have values : ∀ k ∈ n, matrixProductWeights(n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, scalarMatrix(R, n, a), N, i, j)(k) =78      coefficientSingle(n, Ring.carrier(R), R.zero, a * N[i, j], i)(k)79    intros k hk80    have entryK := Matrix.entry at N, R, n, k, j with *81    have weight := matrixProductWeights.value at n, R.carrier, R.add, R.zero,82      R.neg, R.mul, R.one, scalarMatrix(R, n, a), N, i, j, k with *83    have scalarEntry := scalarMatrix.entry at R, n, a, i, k with *84    have alternatives : k = i ∨ k ≠ i by tauto85    cases alternatives with same | different86    . have equal : i = k by cc87      have delta := singleValue.same at R.carrier, R.zero, R.one, k, i with *88      have selected := coefficientSingle.same at n, R.carrier, R.zero, a * N[i, j], i with *89      rw [weight, scalarEntry, delta, same, selected]90      ring91    . have reverse : i ≠ k92        intro equal93        apply different94        cc95      have delta := singleValue.other at R.carrier, R.zero, R.one, k, i with *96      have selected := coefficientSingle.other at n, R.carrier, R.zero, a * N[i, j], i, k with *97      rw [weight, scalarEntry, delta, selected]98      ring99  have same := finiteRingSum.congr with values100  have single := finiteRingSum.single at n, R.carrier, R.add, R.zero, R.neg,101    R.mul, R.one, a * N[i, j], i with *102  unfold matrixProductEntry at entry103  cc104105theorem scalarMatrix.mul_right (a : R) (N : R ^ n × n)106  shows N * scalarMatrix(R, n, a) = scalarMultiple(R, n, a, N)107proof108  have parts := CommRing.parts with comm109  have finite := Finite.natural at n110  have scalar := scalarMatrix.guard at R, n, a with *111  have product := Matrix.of_mem at N * scalarMatrix(R, n, a), R, n with (Ring.mul_mem with *)112  have scaled := scalarMultiple.matrix at R, n, a, N with *113  have aIn : a ∈ R by assumption114  apply Matrix.ext with product, scaled115  intros i hi j hj116  have entryN := Matrix.entry at N, R, n, i, j with *117  have entry := matrixRing.mul_entry at R, n, N, scalarMatrix(R, n, a), i, j with *118  have scale := scalarMultiple.entry at R, n, a, N, i, j with *119  have squareS := Matrix.square at scalarMatrix(R, n, a), R, n with *120  have squareN := Matrix.square at N, R, n with assumption121  have shapeS := squareMatrices.membership.forward with squareS122  have shapeN := squareMatrices.membership.forward with squareN123  have weights := matrixProductWeights.function at n, R.carrier, R.add, R.zero,124    R.neg, R.mul, R.one, N, scalarMatrix(R, n, a), i, j with *125  have selector := coefficientSingle.function at n, R.carrier, R.zero, a * N[i, j], j with *126  have values : ∀ k ∈ n, matrixProductWeights(n, Ring.carrier(R), R.add, R.zero, R.neg, R.mul, R.one, N, scalarMatrix(R, n, a), i, j)(k) =127      coefficientSingle(n, Ring.carrier(R), R.zero, a * N[i, j], j)(k)128    intros k hk129    have entryK := Matrix.entry at N, R, n, i, k with *130    have weight := matrixProductWeights.value at n, R.carrier, R.add, R.zero,131      R.neg, R.mul, R.one, N, scalarMatrix(R, n, a), i, j, k with *132    have scalarEntry := scalarMatrix.entry at R, n, a, k, j with *133    have alternatives : k = j ∨ k ≠ j by tauto134    cases alternatives with same | different135    . have delta := singleValue.same at R.carrier, R.zero, R.one, j, k with *136      have selected := coefficientSingle.same at n, R.carrier, R.zero, a * N[i, j], j with *137      rw [weight, scalarEntry, delta, same, selected]138      ring139    . have delta := singleValue.other at R.carrier, R.zero, R.one, j, k with *140      have selected := coefficientSingle.other at n, R.carrier, R.zero, a * N[i, j], j, k with *141      rw [weight, scalarEntry, delta, selected]142      ring143  have same := finiteRingSum.congr with values144  have single := finiteRingSum.single at n, R.carrier, R.add, R.zero, R.neg,145    R.mul, R.one, a * N[i, j], j with *146  unfold matrixProductEntry at entry147  cc148149theorem scalarMatrix.central (a : R) (N : R ^ n × n)150  shows scalarMatrix(R, n, a) * N = N * scalarMatrix(R, n, a)151proof152  have left := scalarMatrix.mul_left at R, n, a, N with *153  have right := scalarMatrix.mul_right at R, n, a, N with *154  cc155156theorem scalarMatrix.add (a b : R)157  shows scalarMatrix(R, n, a + b) = scalarMatrix(R, n, a) + scalarMatrix(R, n, b)158proof159  have sumIn : a + b ∈ R := Ring.add_mem with *160  have guardA := scalarMatrix.guard at R, n, a with *161  have guardB := scalarMatrix.guard at R, n, b with *162  have guardSum := scalarMatrix.guard at R, n, a + b with *163  have total := Matrix.of_mem at scalarMatrix(R, n, a) + scalarMatrix(R, n, b), R, n with (Ring.add_mem with *)164  apply Matrix.ext with guardSum, total165  intros i hi j hj166  have zeroIn : R[0] ∈ R := Ring.zero_mem with *167  have oneIn : R[1] ∈ R := Ring.one_mem with *168  have delta := singleValue.closed at R.carrier, R.zero, R.one, j, i with *169  have entry := matrixRing.add_entry at R, n, scalarMatrix(R, n, a), scalarMatrix(R, n, b), i, j with *170  have left := scalarMatrix.entry at R, n, a, i, j with *171  have right := scalarMatrix.entry at R, n, b, i, j with *172  have both := scalarMatrix.entry at R, n, a + b, i, j with *173  rw [entry, left, right, both]174  ring175176theorem scalarMatrix.mul (a b : R)177  shows scalarMatrix(R, n, a * b) = scalarMatrix(R, n, a) * scalarMatrix(R, n, b)178proof179  have productIn : a * b ∈ R := Ring.mul_mem with *180  have guardB := scalarMatrix.guard at R, n, b with *181  have guardProduct := scalarMatrix.guard at R, n, a * b with *182  have scaled := scalarMultiple.matrix at R, n, a, scalarMatrix(R, n, b) with *183  have left := scalarMatrix.mul_left at R, n, a, scalarMatrix(R, n, b) with *184  rw left185  apply Matrix.ext with guardProduct, scaled186  intros i hi j hj187  have zeroIn : R[0] ∈ R := Ring.zero_mem with *188  have oneIn : R[1] ∈ R := Ring.one_mem with *189  have delta := singleValue.closed at R.carrier, R.zero, R.one, j, i with *190  have scale := scalarMultiple.entry at R, n, a, scalarMatrix(R, n, b), i, j with *191  have inner := scalarMatrix.entry at R, n, b, i, j with *192  have both := scalarMatrix.entry at R, n, a * b, i, j with *193  rw [scale, inner, both]194  ring195196theorem scalarMatrix.one197  shows scalarMatrix(R, n, R[1]) = matrixRing(R, n)[1]198proof199  have oneIn : R[1] ∈ R := Ring.one_mem with *200  have guard := scalarMatrix.guard at R, n, R[1] with *201  have one := Matrix.of_mem at matrixRing(R, n)[1], R, n with (Ring.one_mem with *)202  apply Matrix.ext with guard, one203  intros i hi j hj204  have zeroIn : R[0] ∈ R := Ring.zero_mem with *205  have delta := singleValue.closed at R.carrier, R.zero, R.one, j, i with *206  have entry := scalarMatrix.entry at R, n, R[1], i, j with *207  have unit := matrixRing.one_entry at R, n, i, j with *208  rw [entry, unit]209  ring210211end Scalars212213-- The embedding of R into its matrix ring.214defgraph scalarEmbedding (R n : Set) (a ∈ Ring.carrier(R)) : Ring.carrier(matrixRing(R, n)) :=215  scalarMatrix(R, n, a)216requires comm : CommRing(R)217requires natural : Nat(n)218proof219  exact scalarMatrix.mem with *220221-- Evaluation at M: the polynomials over R in the variable X(R, {0}, 0)222-- mapped into the commutant of M.223def matrixEvaluation (R n M : Set) : Set :=224  evaluationHom(R, commutant(R, n, M), {0}, scalarEmbedding(R, n),225    constantFunction({0}, Ring.carrier(commutant(R, n, M)), M))226227notation function "evalAt(M)" => matrixEvaluation(R, n, M) via hypothesis Matrix(M, R, m, n)228229section Commutants230variable (R : Set) (n : Nat)231hypothesis comm : CommRing(R)232233theorem commutant.carrierOf (M : R ^ n × n)234  shows Ring.carrier(commutant(R, n, M)) = bicommutant(matrixRing(R, n), {M})235proof236  unfold commutant237  exact bicommutantRing.carrierOf at matrixRing(R, n), {M}238239theorem commutant.generators (M : R ^ n × n)240  shows {M} ⊆ Ring.carrier(matrixRing(R, n))241proof242  intros s hs243  have equal := singleton.membership.forward with hs244  rw equal245  exact Matrix.mem_ring with assumption246247theorem commutant.generators_commute (M : R ^ n × n)248  shows {M} ⊆ ringCentralizer(matrixRing(R, n), {M})249proof250  have ring := matrixRing.ring at R, n with *251  have member := Matrix.mem_ring at M, R, n with assumption252  exact bicommutant.singleton_commuting at matrixRing(R, n), {M}, M with *253254instance commutant.comm_ring (M : R ^ n × n)255  shows CommRing(commutant(R, n, M))256proof257  have ring := matrixRing.ring at R, n with *258  have bounded := commutant.generators at R, n, M with *259  have commuting := commutant.generators_commute at R, n, M with *260  unfold commutant261  exact bicommutantRing.comm_ring with *262263theorem commutant.subset (M : R ^ n × n)264  shows Ring.carrier(commutant(R, n, M)) ⊆ Ring.carrier(matrixRing(R, n))265proof266  have ring := matrixRing.ring at R, n with *267  have bounded := commutant.generators at R, n, M with *268  rw commutant.carrierOf269  exact bicommutant.subset with *270271theorem commutant.mem_matrix (M : R ^ n × n) (N : Set)272  requires member : N ∈ Ring.carrier(commutant(R, n, M))273  shows N : R ^ n × n274proof275  have subset := commutant.subset at R, n, M with *276  have inRing := subset with N, member277  exact Matrix.of_mem with inRing278279instance commutant.self_mem (M : R ^ n × n)280  shows M ∈ Ring.carrier(commutant(R, n, M))281proof282  have ring := matrixRing.ring at R, n with *283  have bounded := commutant.generators at R, n, M with *284  have contains := bicommutant.contains at matrixRing(R, n), {M} with *285  have self : M ∈ {M} by simp [singleton.membership]286  rw commutant.carrierOf287  exact contains with M, self288289theorem commutant.scalar_mem (M : R ^ n × n) (a : R)290  shows scalarMatrix(R, n, a) ∈ Ring.carrier(commutant(R, n, M))291proof292  have ring := matrixRing.ring at R, n with *293  have bounded := commutant.generators at R, n, M with *294  have central := ringCentralizer.subset at matrixRing(R, n), {M} with *295  have element := scalarMatrix.mem at R, n, a with *296  have commutes : ∀ N ∈ ringCentralizer(matrixRing(R, n), {M}),297      call2(Ring.mul(matrixRing(R, n)), scalarMatrix(R, n, a), N) =298        call2(Ring.mul(matrixRing(R, n)), N, scalarMatrix(R, n, a))299    intros N hN300    have inRing := central with N, hN301    have guard := Matrix.of_mem with inRing302    exact scalarMatrix.central with *303  rw commutant.carrierOf304  unfold bicommutant305  exact ringCentralizer.mem at matrixRing(R, n), ringCentralizer(matrixRing(R, n), {M}), scalarMatrix(R, n, a) with *306307-- Sums, products, and negations in the commutant are those of the matrix ring.308theorem commutant.add_value (M : R ^ n × n) (N P : Set)309  requires memberN : N ∈ Ring.carrier(commutant(R, n, M))310  requires memberP : P ∈ Ring.carrier(commutant(R, n, M))311  shows call2(Ring.add(commutant(R, n, M)), N, P) = call2(Ring.add(matrixRing(R, n)), N, P)312proof313  have ring := matrixRing.ring at R, n with *314  have parts := Ring.parts with ring315  have bounded := commutant.generators at R, n, M with *316  have subring := bicommutant.subring at matrixRing(R, n), {M} with *317  have subset := IsSubring.subset_carrier with subring318  have closed := IsSubring.add_closed with subring319  have magma : IsMagma(Ring.carrier(matrixRing(R, n)), Ring.add(matrixRing(R, n)))320    simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]321  rw commutant.carrierOf at memberN322  rw commutant.carrierOf at memberP323  unfold commutant324  rw bicommutantRing.addOf325  exact restrictBinary.value with *326327theorem commutant.mul_value (M : R ^ n × n) (N P : Set)328  requires memberN : N ∈ Ring.carrier(commutant(R, n, M))329  requires memberP : P ∈ Ring.carrier(commutant(R, n, M))330  shows call2(Ring.mul(commutant(R, n, M)), N, P) = call2(Ring.mul(matrixRing(R, n)), N, P)331proof332  have ring := matrixRing.ring at R, n with *333  have parts := Ring.parts with ring334  have bounded := commutant.generators at R, n, M with *335  have subring := bicommutant.subring at matrixRing(R, n), {M} with *336  have subset := IsSubring.subset_carrier with subring337  have closed := IsSubring.mul_closed with subring338  have magma : IsMagma(Ring.carrier(matrixRing(R, n)), Ring.mul(matrixRing(R, n)))339    simp [IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]340  rw commutant.carrierOf at memberN341  rw commutant.carrierOf at memberP342  unfold commutant343  rw bicommutantRing.mulOf344  exact restrictBinary.value with *345346theorem commutant.neg_value (M : R ^ n × n) (N : Set)347  requires member : N ∈ Ring.carrier(commutant(R, n, M))348  shows Ring.neg(commutant(R, n, M))(N) = Ring.neg(matrixRing(R, n))(N)349proof350  have ring := matrixRing.ring at R, n with *351  have parts := Ring.parts with ring352  have bounded := commutant.generators at R, n, M with *353  have subring := bicommutant.subring at matrixRing(R, n), {M} with *354  have subset := IsSubring.subset_carrier with subring355  have closed := IsSubring.neg_closed with subring356  obtain ⟨addF, zeroIn, negF, mulF, oneIn⟩ := IsRing.typing_of_parts with parts357  rw commutant.carrierOf at member358  unfold commutant359  rw bicommutantRing.negOf360  exact restrictUnary.value with *361362theorem commutant.zero_value (M : R ^ n × n)363  shows Ring.zero(commutant(R, n, M)) = Ring.zero(matrixRing(R, n))364proof365  unfold commutant366  exact bicommutantRing.zeroOf at matrixRing(R, n), {M}367368theorem commutant.one_value (M : R ^ n × n)369  shows Ring.one(commutant(R, n, M)) = Ring.one(matrixRing(R, n))370proof371  unfold commutant372  exact bicommutantRing.oneOf at matrixRing(R, n), {M}373374-- The scalar embedding is a homomorphism into the commutant.375theorem scalarEmbedding.hom (M : R ^ n × n)376  shows scalarEmbedding(R, n) : R →+* commutant(R, n, M)377proof378  have natural : Nat(n) by typecheck379  have parts := CommRing.parts with comm380  have ring := CommRing.to_ring with comm381  have target := commutant.comm_ring at R, n, M with *382  have targetRing := CommRing.to_ring with target383  have targetParts := CommRing.parts with target384  have graph := scalarEmbedding.function at R, n with *385  have values : ∀ a ∈ R.carrier, scalarEmbedding(R, n)(a) ∈ Ring.carrier(commutant(R, n, M))386    intros a ha387    have value := scalarEmbedding.value at R, n, a with *388    rw value389    exact commutant.scalar_mem with *390  have function := FunctionBetween.codomain_of_values with graph, values391  have additive : ∀ a ∈ R.carrier, ∀ b ∈ R.carrier,392      scalarEmbedding(R, n)(call2(R.add, a, b)) =393        call2(Ring.add(commutant(R, n, M)), scalarEmbedding(R, n)(a), scalarEmbedding(R, n)(b))394    intros a ha b hb395    have sumIn : a + b ∈ R := Ring.add_mem with *396    have valueA := scalarEmbedding.value at R, n, a with *397    have valueB := scalarEmbedding.value at R, n, b with *398    have valueSum := scalarEmbedding.value at R, n, a + b with *399    have memberA := values with a, ha400    have memberB := values with b, hb401    have inner := commutant.add_value at R, n, M, scalarEmbedding(R, n)(a), scalarEmbedding(R, n)(b) with *402    have sum := scalarMatrix.add at R, n, a, b with *403    rw [inner, valueA, valueB, valueSum]404    exact sum405  have multiplicative : ∀ a ∈ R.carrier, ∀ b ∈ R.carrier,406      scalarEmbedding(R, n)(call2(R.mul, a, b)) =407        call2(Ring.mul(commutant(R, n, M)), scalarEmbedding(R, n)(a), scalarEmbedding(R, n)(b))408    intros a ha b hb409    have productIn : a * b ∈ R := Ring.mul_mem with *410    have valueA := scalarEmbedding.value at R, n, a with *411    have valueB := scalarEmbedding.value at R, n, b with *412    have valueProduct := scalarEmbedding.value at R, n, a * b with *413    have memberA := values with a, ha414    have memberB := values with b, hb415    have inner := commutant.mul_value at R, n, M, scalarEmbedding(R, n)(a), scalarEmbedding(R, n)(b) with *416    have product := scalarMatrix.mul at R, n, a, b with *417    rw [inner, valueA, valueB, valueProduct]418    exact product419  have unital : scalarEmbedding(R, n)(R.one) = Ring.one(commutant(R, n, M))420    have oneIn : R[1] ∈ R := Ring.one_mem with *421    have value := scalarEmbedding.value at R, n, R[1] with *422    have one := scalarMatrix.one at R, n with *423    rw [commutant.one_value, value]424    exact one425  have engine := IsRingHom.of_add_mul_one with parts, targetParts, function,426    additive, multiplicative, unital427  exact RingHom.of_projections with ring, targetRing, engine428429theorem matrixEvaluation.hom (M : R ^ n × n)430  shows evalAt(M) : polynomialRing(R, {0}) →+* commutant(R, n, M)431proof432  have target := commutant.comm_ring at R, n, M with *433  have hom := scalarEmbedding.hom at R, n, M with *434  have self := commutant.self_mem at R, n, M with *435  have assignment := constantFunction.function at {0}, Ring.carrier(commutant(R, n, M)), M with *436  unfold matrixEvaluation437  exact evaluationHom.hom with *438439theorem matrixEvaluation.map_X (M : R ^ n × n)440  shows evalAt(M)(X(R, {0}, 0)) = M441proof442  have target := commutant.comm_ring at R, n, M with *443  have hom := scalarEmbedding.hom at R, n, M with *444  have self := commutant.self_mem at R, n, M with *445  have assignment := constantFunction.function at {0}, Ring.carrier(commutant(R, n, M)), M with *446  have index : 0 ∈ {0} by simp [singleton.membership]447  have point := constantFunction.apply at {0}, Ring.carrier(commutant(R, n, M)), 0, M with *448  have mapped := evaluationHom.map_X at R, commutant(R, n, M), {0}, scalarEmbedding(R, n),449    constantFunction({0}, Ring.carrier(commutant(R, n, M)), M), 0 with *450  unfold matrixEvaluation451  cc452453theorem matrixEvaluation.map_constant (M : R ^ n × n) (a : R)454  shows evalAt(M)(polynomialConstant(R, {0})(a)) = scalarMatrix(R, n, a)455proof456  have natural : Nat(n) by typecheck457  have target := commutant.comm_ring at R, n, M with *458  have hom := scalarEmbedding.hom at R, n, M with *459  have self := commutant.self_mem at R, n, M with *460  have assignment := constantFunction.function at {0}, Ring.carrier(commutant(R, n, M)), M with *461  have mapped := evaluationHom.map_constant at R, commutant(R, n, M), {0}, scalarEmbedding(R, n),462    constantFunction({0}, Ring.carrier(commutant(R, n, M)), M), a with *463  have value := scalarEmbedding.value at R, n, a with *464  unfold matrixEvaluation465  cc466467end Commutants468