Library Combi.Basic.unitriginv: Uni-triangular Matrices

Triangular matrix with 1 on the diagonal

We deal with "matrices" which are triangular for a possibly partial order with 1 on the diagonal. The goal is to show that such a matrix is invertible on any ring and to give formulas for the inverse. The matrices are given as a function M : T -> T -> R for a finite partially ordered type T and a commutative unit ring R.

unitrig M == M is unitriangular where M.
Mat M == transform M to a usual mathcomp square matrix of order #|T|
Minv M == the inverse of the matrix M.

We show that such a matrix has determinant 1 (Lemma det_unitrig) and is therefore invertible. Moreover Lemma Minv_unitrig says that the inverse is unitriangular too.

Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrfun ssrbool eqtype ssrnat order.
From mathcomp Require Import fintype bigop ssralg.
From mathcomp Require Import finset fingroup perm matrix.

Require ordtype.

Set Implicit Arguments.

Import Order.TTheory.
Import GRing.Theory.
#[local] Open Scope ring_scope.

Section UniTriangular.

Variable R : comUnitRingType.
Variable disp : unit.
Variable T : finPOrderType disp.
Implicit Type M : T -> T -> R.
Implicit Types t u v : T.

Definition unitrig M :=
  [forall t, M t t == 1] && [forall t, [forall (u | M u t != 0), (t <= u)%O]].
Lemma unitrigP M :
  reflect ((forall t, M t t = 1) /\ (forall t u, M u t != 0 -> (t <= u)%O))
          (unitrig M).

Lemma unitrig1 : unitrig (fun x y => (x == y)%:R).

TODO : construct the group of unitriangular matrix

Lemma unitrig_suml M (Mod : lmodType R) (F : T -> Mod) u :
  unitrig M ->
  \sum_(t : T) M u t *: F t = \sum_(t | (t <= u)%O) M u t *: F t.

Lemma unitrig_sum1l M (Mod : lmodType R) (F : T -> Mod) u :
  unitrig M ->
  \sum_(t : T) M u t *: F t = F u + \sum_(t | (t < u)%O) M u t *: F t.

Lemma unitrig_sumr M (Mod : lmodType R) (F : T -> Mod) t :
  unitrig M ->
  \sum_(u : T) M u t *: F u = \sum_(u | (t <= u)%O) M u t *: F u.

Lemma unitrig_sum1r M (Mod : lmodType R) (F : T -> Mod) t :
  unitrig M ->
  \sum_(u : T) M u t *: F u = F t + \sum_(u | (t < u)%O) M u t *: F u.

Lemma unitrig_sumlV M (Mod : lmodType R) (F : T -> Mod) u :
  unitrig M ->
  \sum_(t : T) M t u *: F t = \sum_(t | (u <= t)%O) M t u *: F t.

Lemma unitrig_sum1lV M (Mod : lmodType R) (F : T -> Mod) u :
  unitrig M ->
  \sum_(t : T) M t u *: F t = F u + \sum_(t | (u < t)%O) M t u *: F t.

Lemma unitrig_sumrV M (Mod : lmodType R) (F : T -> Mod) t :
  unitrig M ->
  \sum_(u : T) M t u *: F u = \sum_(u | (u <= t)%O) M t u *: F u.

Lemma unitrig_sum1rV M (Mod : lmodType R) (F : T -> Mod) t :
  unitrig M ->
  \sum_(u : T) M t u *: F u = F t + \sum_(u | (u < t)%O) M t u *: F u.

End UniTriangular.

Section TriangularInv.

Variable R : comUnitRingType.
Variable disp : unit.
Variable T : finPOrderType disp.
Variable M : T -> T -> R.
Implicit Types t u v : T.

Hypothesis Munitrig : unitrig M.

#[local] Notation n := #|{: T }|.
Definition Mat : 'M[R]_n := \matrix_(i, j < n) M (enum_val i) (enum_val j).

Lemma det_unitrig : \det Mat = 1.

Definition Minv t u : R := invmx Mat (enum_rank t) (enum_rank u).

Lemma Minvl t u : \sum_(v : T) (Minv t v) * (M v u) = (u == t)%:R.

Lemma Minvr t u : \sum_(v : T) (M t v) * (Minv v u) = (u == t)%:R.

Lemma Minv_trig t u : Minv u t != 0 -> (t <= u)%O.

Lemma Minv_uni t : Minv t t = 1.

Lemma Minv_unitrig : unitrig Minv.

Lemma Minv_lincombl (Mod : lmodType R) (F G : T -> Mod) :
  (forall t, F t = \sum_u M t u *: G u ) ->
  (forall t, G t = \sum_u Minv t u *: F u ).

Lemma Minv_lincombr (Mod : lmodType R) (F G : T -> Mod) :
  (forall t, F t = \sum_u M u t *: G u ) ->
  (forall t, G t = \sum_u Minv u t *: F u ).

End TriangularInv.