Library minor

Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq path.
Require Import ssralg fintype perm choice finfun.
Require Import matrix bigop zmodp mxalgebra poly mxpoly.
Require Import ssrcomplements.

Import GRing.Theory.

Set Implicit Arguments.

Open Scope ring_scope.

Section submatrix_section.
Variable T : Type.

Definition submatrix m n p q
 (f : 'I_p -> 'I_m) (g : 'I_q -> 'I_n) (A: 'M[T]_(m,n)):=
    \matrix_(i < p, j < q) A (f i) (g j).

Lemma sub_submx k k' l l' m n (A : 'M[T]_(m,n)) (f' : 'I_k -> 'I_m)
 (f : 'I_k' -> 'I_k) (g' : 'I_l -> 'I_n) (g : 'I_l' -> 'I_l) :
  submatrix f g (submatrix f' g' A) = submatrix (f' \o f) (g' \o g) A.

End submatrix_section.

Section minor_def.
Variable R : ringType.

Definition minor (m n k : nat) (f1 : 'I_k -> 'I_m) (f2 : 'I_k -> 'I_n)
 (A: 'M[R]_(m,n)) := \det (submatrix f1 f2 A).

End minor_def.

Implicit Arguments minor [R m n].

Section minor_section.
Variable R : comRingType.

Lemma minor1 : forall (m n: nat) (A: 'M[R]_(m,n)) i j,
 minor 1 (fun _ => i) (fun _ => j) A = A i j.

Definition step_fun (n k:nat) (h : k <= n) : 'I_k -> 'I_n :=
  fun x => widen_ord h x.

Lemma step_fun_eq (n k : nat) (h h' : k <= n) : step_fun h =1 step_fun h'.

Definition lift_pred (n k:nat) (f: 'I_k -> 'I_n)
  : 'I_k.+1 -> 'I_n.+1 :=
fun (x: 'I_(1 + k)) => match split x with
           | inl _ => 0
           | inr j => lift 0 (f j)
         end.

Definition pminor (m n k:nat) (h: k.+1 <= m) (h': k.+1 <= n)
  (A: 'M[R]_(m,n)) := minor k.+1 (step_fun h) (step_fun h') A.

Lemma size_tool : forall n k, k <= n -> k.+1 <= n.+1.

Lemma lift_pred_step : forall (n k:nat) (h : k <= n) (x: 'I_k.+1),
  lift_pred (step_fun h) x = step_fun (size_tool h) x.

Lemma step0 : forall n (h: 1 <= n.+1) (x: 'I_1),
  step_fun h x = 0.

Lemma stepn: forall n (x: 'I_n) (h: n <= n),
  step_fun h x = x.

Lemma minorn : forall (n:nat) (A: 'M[R]_n),
  minor n id id A = \det A.

Lemma det2 : forall (A: 'M[R]_(2,2)),
  \det A = A 0 0 * A 1 1 - A 1 0 * A 0 1.

Lemma minor2 : forall (m n:nat) (A: 'M[R]_(m,n)) f1 f2,
  minor 2 f1 f2 A =
    A (f1 0) (f2 0) * A (f1 1) (f2 1) -
    A (f1 1) (f2 0) * A (f1 0) (f2 1).

Lemma minor_ltn_eq0l k m1 m2 n1 n2 x (f : 'I_k -> 'I_(m1 + m2)) g
  (M : 'M[R]_(m1,n1)) (N : 'M_(m1,n2)) :
  m1 < f x -> minor k f g (block_mx M N 0 0) = 0.

Lemma minor_ltn_eq0r k m1 m2 n1 n2 x f (g : 'I_k -> 'I_(n1 + n2))
  (M : 'M[R]_(m1,n1)) (N : 'M_(m2,n1)) :
  n1 < g x -> minor k f g (block_mx M 0 N 0) = 0.

End minor_section.

Section Theory.
Variable R: comRingType.

Lemma minor_alternate_f : forall (m n p:nat) f g (M: 'M[R]_(m,n)),
  (exists x, exists y, (x != y) /\ (f x == f y)) -> minor p f g M = 0.

Lemma minor_alternate_g : forall (m n p:nat) f g (M: 'M[R]_(m,n)),
  (exists x, exists y, (x != y) /\ (g x == g y)) -> minor p f g M = 0.

Lemma minor_f_not_injective : forall (m n p:nat) f g (M: 'M[R]_(m,n)),
   ~ injective f -> minor p f g M = 0.

Lemma minor_g_not_injective : forall (m n p:nat) f g (M: 'M[R]_(m,n)),
   ~ injective g -> minor p f g M = 0.

Lemma submatrix_eq : forall (m n p q :nat) (f1 f1': 'I_p -> 'I_m)
  (f2 f2' : 'I_q -> 'I_n) (M: 'M[R]_(m,n)),
    f1 =1 f1'-> f2 =1 f2' ->
 submatrix f1 f2 M = submatrix f1' f2' M.

Lemma minor_eq : forall (m n k:nat) f1 g1 f2 g2 (M: 'M[R]_(m,n)),
  (f1 =1 g1) -> (f2 =1 g2) -> minor k f1 f2 M = minor k g1 g2 M.

Lemma lift_pred0 : forall n k (f: 'I_k -> 'I_n),
  lift_pred f 0 = 0.

Lemma lift_predS : forall n k (f: 'I_k -> 'I_n) (x: 'I_k),
  lift_pred f (lift 0 x) = lift 0 (f x).

Lemma submatrix_lift_block : forall (m n p q:nat)
  (f1 : 'I_p -> 'I_m) (f2 : 'I_q -> 'I_n) a
  (M: 'M[R]_(m,n)) (c: 'cV[R]_m) (l: 'rV[R]_n),
  submatrix (lift_pred f1) (lift_pred f2)
    (block_mx a%:M l c M) =
  block_mx a%:M (submatrix id f2 l) (submatrix f1 id c)
    (submatrix f1 f2 M).

Lemma submatrix0 : forall n m p q (f1: 'I_p -> 'I_m) (f2 : 'I_q -> 'I_n),
  submatrix f1 f2 0 = 0 :> 'M[R]_(_,_).

Lemma minor_lift_block :
  forall (m n p :nat) f1 f2 a (M: 'M[R]_(m,n)) (l: 'rV[R]_n),
  minor p.+1 (lift_pred f1) (lift_pred f2) (block_mx a%:M l 0 M) =
  a * minor p f1 f2 M.

Lemma inj_lift : forall m n (f: 'I_n -> 'I_m),
  injective f -> injective (lift_pred f).

Lemma inj_step : forall n m (h: n <= m),
  injective (step_fun h).

Lemma submatrix_scale m n p k (A: 'M[R]_(m,n))
  (f : 'I_p -> 'I_m) (g : 'I_k -> 'I_n) a:
  submatrix f g (a *: A) = a *: submatrix f g A.

Lemma submatrix_add m n p k (A B : 'M[R]_(m,n))
  (f : 'I_p -> 'I_m) (g : 'I_k -> 'I_n):
  submatrix f g (A + B) = submatrix f g A + submatrix f g B.

Lemma submatrix_opp m n p k (A: 'M[R]_(m,n))
  (f : 'I_p -> 'I_m) (g : 'I_k -> 'I_n) :
  submatrix f g (- A ) = - submatrix f g A.

Lemma submatrix_mul m n p k l (A: 'M[R]_(m,n)) (B: 'M[R]_(n,p))
  (f : 'I_k -> 'I_m) (g : 'I_l -> 'I_p):
  submatrix f g (A *m B) = (submatrix f id A) *m (submatrix id g B).

Lemma submatrix_char_poly_mx : forall m p(M: 'M[R]_m)
  (f1: 'I_p -> 'I_m), injective f1 ->
  submatrix f1 f1 (char_poly_mx M) = char_poly_mx (submatrix f1 f1 M).

End Theory.