centrosymmetric matrices

theories/Algebra/Rings/Matrix.v

@@ -89,6 +89,16 @@
   exact (H i j Hi Hj).
 Defined.
 
+Definition path_entry_matrix {R : Type} {m n} {M M' : Matrix R m n}
+  (p : M = M') {i i' j j' : nat} (q : i = i') (r : j = j')
+  (Hi : (i < m)%nat) (Hj : (j < n)%nat)
+  (Hi' : (i' < m)%nat) (Hj' : (j' < n)%nat)
+  : entry M i j = entry M' i' j'.
+Proof.
+  snrapply path_entry_vector; trivial.
+  by snrapply path_entry_vector.
+Defined.
+
 (** ** Addition and module structure *)
 
 (** Here we define the abelian group of (n x m)-matrices over a ring. This follows from the abelian group structure of the underlying vectors. We are also able to derive a left module strucutre when the entries come from a left module. *)
@@ -102,6 +112,14 @@
 
 Definition matrix_zero (A : AbGroup) m n : Matrix A m n
   := @mon_unit (abgroup_matrix A m n) _.
+
+Definition entry_matrix_zero {A : AbGroup} {m n} (i j : nat)
+  (Hi : (i < m)%nat) (Hj : (j < n)%nat)
+  : entry (matrix_zero A m n) i j = 0.
+Proof.
+  unfold entry, matrix_zero.
+  by rewrite 2 entry_Build_Vector.
+Defined.
 
 Definition matrix_negate {A : AbGroup} {m n}
   : Matrix A m n -> Matrix A m n
@@ -1018,6 +1036,267 @@
 
 (** Skew-symmetric matrices degenerate to symmetric matrices in rings with characteristic 2. In odd characteristic the module of matrices can be decomposed into the direct sum of symmetric and skew-symmetric matrices. *)
 
+(** ** Exchange matrix *)
+
+(** The exchange matrix is the matrix with ones on the anti-diagonal and zeros elsewhere. It will play an important role in defining classes of matrices with certain symmetric properties. *)
+Definition exchange_matrix (R : Ring) n : Matrix R n n
+  := Build_Matrix R n n (fun i j Hi Hj
+      => kronecker_delta (R:=R) (i + j) (pred n))%nat.
+
+(** The exchange matrix is invariant under transpose. *)
+Definition exchange_matrix_transpose {R n}
+  : matrix_transpose (exchange_matrix R n) = exchange_matrix R n.
+Proof.
+  apply path_matrix.
+  intros i j Hi Hj.
+  rewrite 3 entry_Build_Matrix.
+  by rewrite nat_add_comm.
+Defined.
+
+(** The exchange matrix is symmetric. *)
+Global Instance issymmetric_exchange {R : Ring} {n : nat}
+  : IsSymmetric (exchange_matrix R n)
+  := exchange_matrix_transpose.
+
+(** This gets used in a couple of places below, so we add it to [typeclass_instances] to simplify the proofs. It says that [i < j -> i <= pred j]. *)
+#[local] Hint Immediate lt_implies_pred_geq : typeclass_instances.
+
+(** An alternate way to write the exchange matrix. *)
+Definition exchange_matrix_sub {R n}
+  (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat)
+  : entry (exchange_matrix R n) i j = kronecker_delta (R:=R) i (pred n - j)%nat.
+Proof.
+  lhs nrapply entry_Build_Matrix.
+  rhs_V nrapply (kronecker_delta_map_inj _ _ (fun m => m + j)).
+  2: nrapply isinj_nat_add_r.
+  apply ap.
+  symmetry; rapply natminuspluseq.
+Defined.
+
+(** And another way to write the exchange matrix. *)
+Definition exchange_matrix_sub' {R n}
+  (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat)
+  : entry (exchange_matrix R n) i j = kronecker_delta (R:=R) (pred n - i)%nat j.
+Proof.
+  rewrite <- exchange_matrix_transpose.
+  lhs nrapply entry_Build_Matrix.
+  lhs nrapply exchange_matrix_sub.
+  apply kronecker_delta_symm.
+Defined.
+
+(** A lemma that is needed to ensure that [pred n - i] is a valid matrix index.  The hypothesis [i < n] is only used to force that [0 < n], and matches what we have when we use this. *)
+Local Definition nat_pred_sub_lt (n i : nat) (Hi : (i < n)%nat) : (pred n - i < n)%nat.
+Proof.
+  (* We prove this using mixed transitivity: [pred n - i <= pred n < n]. *)
+  apply (mixed_trans1 _ (pred n) _).
+  1: apply sub_less.
+  by apply leq_implies_pred_lt with (i:=i).
+Defined.
+
+#[local] Hint Immediate nat_pred_sub_lt : typeclass_instances.
+
+(** Multiplying a matrix by the exchange matrix on the left reverses the order of the rows. Similarly multiplying on the right reverses the order of the columns, but we don't prove this. *)
+Definition entry_matrix_mult_exchange_l {R : Ring} {n : nat} (M : Matrix R n n)
+  (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat)
+  : entry (matrix_mult (exchange_matrix R n) M) i j
+      = entry M (pred n - i) j.
+Proof.
+  lhs nrapply entry_Build_Matrix.
+  lhs rapply (path_ab_sum (g:=fun k Hk => kronecker_delta (pred n - i)%nat k * entry M k j)).
+  2: nrapply rng_sum_kronecker_delta_l.
+  intros k Hk.
+  apply (ap (.* _)).
+  apply exchange_matrix_sub'.
+Defined.
+
+(* TODO: if we keep this, clean it up like the _l version. *)
+Definition entry_matrix_mult_exchange_r {A : Ring} {n : nat} (M : Matrix A n n)
+  (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat)
+  : let Hj' := natpmswap1 _ _ _ (lt_implies_pred_geq _ _ _)
+      (leq_implies_pred_lt _ _ _ Hj (n_leq_add_n_k' n j)) in
+    entry (matrix_mult M (exchange_matrix A n)) i j
+      = entry M i (pred n - j).
+Proof.
+  assert (r : (j <= pred n)%nat) by auto with nat.
+  lhs nrapply entry_Build_Matrix.
+  lhs nrapply path_ab_sum.
+  { intros k Hk.
+    rewrite entry_Build_Matrix.
+    rewrite <- (nat_add_sub_eq _ r).
+    rewrite <- nat_add_comm.
+    unshelve erewrite (kronecker_delta_map_inj _ _ (fun x => j + x)).
+    2: reflexivity.
+    intros x y H; exact (isinj_nat_add_l j x y H). }
+  nrapply rng_sum_kronecker_delta_r'.
+Defined.
+
+(** The exchange matrix has order 2. This proof is only long because of arithmetic. *)
+Definition exchange_matrix_square {R : Ring} {n : nat}
+  : matrix_mult (exchange_matrix R n) (exchange_matrix R n) = identity_matrix R n.
+Proof.
+  apply path_matrix.
+  intros i j Hi Hj.
+  lhs nrapply entry_matrix_mult_exchange_l.
+  lhs nrapply entry_Build_Matrix.
+  rhs nrapply entry_Build_Matrix.
+  (* We hide this [pred n] in [t] so that the rewrite below changes the other [pred n]. *)
+  set (t := (pred n - i + j)%nat);
+    rewrite <- (natminuspluseq i (pred n) _);
+    unfold t; clear t.
+  unshelve erewrite (kronecker_delta_map_inj j i (fun x => pred n - i + x)%nat).
+  2: apply kronecker_delta_symm.
+  nrapply isinj_nat_add_l.
+Defined.
+
+(** ** Centrosymmetric matrices *)
+
+(** A centrosymmetric matrix is symmetric about its center. We propositionally truncate this statement to avoid funext. *)
+Class IsCentrosymmetric {A : Type@{i}} {n : nat} (M : Matrix@{i} A n n) : Type@{i}
+  := iscentrosymmetric
+    : merely (
+        forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
+        entry M i j = entry M (pred n - i) (pred n - j)).
+
+(** The characterizing property of centrosymmetric matrices is that they commute with the exchange matrix. *)
+Definition exchange_matrix_iscentrosymmetric {R : Ring@{i}} {n : nat}
+  (M : Matrix@{i} R n n) `{!IsCentrosymmetric M}
+  (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat)
+  : matrix_mult (exchange_matrix R n) M = matrix_mult M (exchange_matrix R n).
+Proof.
+  apply path_matrix.
+  intros k l Hk Hl.
+  lhs nrapply entry_matrix_mult_exchange_l.
+  rhs nrapply entry_matrix_mult_exchange_r.
+  pose proof (p := iscentrosymmetric).
+  strip_truncations.
+  lhs nrapply p.
+  apply path_entry_matrix; trivial.
+  apply ineq_sub.
+  eauto with nat.
+Defined.
+
+Global Instance ishprop_iscentrosymmetric {A : Type@{i}} {n : nat}
+  (M : Matrix A n n)
+  : IsHProp (IsCentrosymmetric M).
+Proof.
+  unfold IsCentrosymmetric; exact _.
+Defined.
+
+(** The zero matrix is centrosymmetric. *)
+Global Instance iscentrosymmetric_matrix_zero {A : AbGroup@{i}} {n : nat}
+  : IsCentrosymmetric (matrix_zero A n n).
+Proof.
+  apply tr; intros i j Hi Hj.
+  lhs nrapply entry_matrix_zero.
+  by rhs nrapply entry_matrix_zero.
+Defined.
+
+Local Open Scope nat_scope.
+Definition isinj_nat_sub_leq@{}(n x y : nat)
+  : x <= n -> y <= n -> n - x = n - y
+  -> x = y.
+Proof.
+  intros H1 H2 p.
+  rewrite <- (ineq_sub _ _ H1) in H1 |- *.
+  rewrite <- (ineq_sub _ _ H2) in H2 |- *.
+  set (x' := (n - x)%nat) in *.
+  set (y' := (n - y)%nat) in *.
+  clearbody x' y'; clear x y.
+  by destruct p.
+Defined.
+Local Close Scope nat_scope.
+
+(** The identity matrix is centrosymmetric. *)
+Global Instance iscentrosymmetric_matrix_identity {R : Ring@{i}} {n : nat}
+  : IsCentrosymmetric (identity_matrix R n).
+Proof.
+  apply tr; intros i j Hi Hj.
+  lhs nrapply entry_Build_Matrix.
+  rhs nrapply entry_Build_Matrix.
+  symmetry.
+  nrapply (kronecker_delta_map_inj _ _ (fun m => pred n - m)%nat).
+  intros x y p.
+  nrapply (isinj_nat_sub_leq (pred n) _ _ _ _ p).
+  (* Doesn't work because injectivity needed here is more general.... *)
+Admitted.
+
+(** The sum of two centrosymmetric matrices is centrosymmetric. *)
+Global Instance iscentrosymmetric_matrix_plus {R : Ring@{i}} {n : nat}
+  (M N : Matrix R n n) {H1 : IsCentrosymmetric M} {H2 : IsCentrosymmetric N}
+  : IsCentrosymmetric (matrix_plus M N).
+Proof.
+  unfold IsCentrosymmetric.
+  strip_truncations; apply tr; intros i j Hi Hj.
+  rewrite 2 entry_Build_Matrix.
+  apply ap011.
+  - apply H1.
+  - apply H2.
+Defined.
+
+(** The negation of a centrosymmetric matrix is centrosymmetric. *)
+Global Instance iscentrosymmetric_matrix_negate {R : Ring@{i}} {n : nat}
+  (M : Matrix R n n) {H : IsCentrosymmetric M}
+  : IsCentrosymmetric (matrix_negate M).
+Proof.
+  unfold IsCentrosymmetric.
+  strip_truncations; apply tr; intros i j Hi Hj.
+  rewrite 2 entry_Build_Matrix.
+  apply ap, H.
+Defined.
+
+(** A scalar multiple of a centrosymmetric matrix is centrosymmetric. *)
+Global Instance iscentrosymmetric_matrix_scale {R : Ring@{i}} {n : nat}
+  (r : R) (M : Matrix R n n) {H : IsCentrosymmetric M}
+  : IsCentrosymmetric (matrix_lact r M).
+Proof.
+  unfold IsCentrosymmetric.
+  strip_truncations; apply tr; intros i j Hi Hj.
+  rewrite 2 entry_Build_Matrix.
+  apply ap, H.
+Defined.
+
+(** A centrosymmetric matrix is also centrosymmetric when considered over the opposite ring. *)
+Global Instance iscentrosymmetric_rng_op {R : Ring@{i}} {n : nat} (M : Matrix R n n)
+  `{!IsCentrosymmetric M}
+  : IsCentrosymmetric (A := rng_op R) M.
+Proof.
+  assumption.
+Defined.
+
+(** The transpose of a centrosymmetric matrix is centrosymmetric. *)
+Global Instance iscentrosymmetric_matrix_transpose {R : Ring@{i}} {n : nat}
+  (M : Matrix R n n) {H : IsCentrosymmetric M}
+  : IsCentrosymmetric (matrix_transpose M).
+Proof.
+  unfold IsCentrosymmetric.
+  strip_truncations; apply tr; intros i j Hi Hj.
+  rewrite 2 entry_Build_Matrix.
+  apply H.
+Defined.
+
+(** The product of two centrosymmetric matrices is centrosymmetric. *)
+Global Instance iscentrosymmetric_matrix_mult {R : Ring@{i}} {n : nat}
+  (M N : Matrix R n n) {H1 : IsCentrosymmetric M} {H2 : IsCentrosymmetric N}
+  : IsCentrosymmetric (matrix_mult M N).
+Proof.
+  lhs nrapply (rng_mult_assoc (A:=matrix_ring R n)).
+  rhs_V nrapply (rng_mult_assoc (A:=matrix_ring R n)).
+  hnf in H1, H2; cbn.
+  rewrite H1.
+  lhs_V nrapply (rng_mult_assoc (A:=matrix_ring R n)); f_ap.
+Defined.
+
+(** Centrosymmetric matrices form a subring of the matrix ring. *)
+Definition centrosymmetric_matrix_ring (R : Ring@{i}) (n : nat)
+  : Subring (matrix_ring R n).
+Proof.
+  nrapply (Build_Subring' (fun M : matrix_ring R n => IsCentrosymmetric M)).
+  - exact _.
+  - intros x y ? ?; exact (iscentrosymmetric_matrix_plus x (-y)).
+  - exact iscentrosymmetric_matrix_mult.
+  - exact iscentrosymmetric_matrix_identity.
+Defined.
+
 Section MatrixCat.
 
   (** The wild category [MatrixCat R] of [R]-valued matrices. This category has natural numbers as objects and m x n matrices as the arrows between [m] and [n]. *)

theories/Algebra/Rings/Vector.v

@@ -66,11 +66,11 @@ Proof.
   1, 2: apply nth'_nth'.
 Defined.
 
-Definition path_entry_vector {A : Type} {n : nat} (v : Vector A n)
-  (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat) (p : i = j)
-  : entry v i = entry v j.
+Definition path_entry_vector {A : Type} {n : nat} {v v' : Vector A n} (p : v = v')
+  {i j : nat} {Hi : (i < n)%nat} {Hj : (j < n)%nat} (q : i = j)
+  : entry v i = entry v' j.
 Proof.
-  destruct p.
+  destruct p, q.
   apply nth'_nth'.
 Defined.