diff --git a/Cubical/Algebra/Determinat/Minor.agda b/Cubical/Algebra/Determinat/Minor.agda new file mode 100644 index 000000000..521477bb6 --- /dev/null +++ b/Cubical/Algebra/Determinat/Minor.agda @@ -0,0 +1,195 @@ +{-# OPTIONS --cubical #-} + +module Minor where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Algebra.Matrix +open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ + ; +-comm to +ℕ-comm + ; +-assoc to +ℕ-assoc + ; ·-assoc to ·ℕ-assoc) +open import Cubical.Data.Vec.Base using (_∷_; []) +open import Cubical.Foundations.Structure using (⟨_⟩) +open import Cubical.Data.FinData +open import Cubical.Data.FinData.Order using (_<'Fin_; _≤'Fin_) +open import Cubical.Algebra.Ring +open import Cubical.Algebra.Ring.Base +open import Cubical.Algebra.Ring.BigOps +open import Cubical.Algebra.Monoid.BigOp +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommRing.Base +open import Cubical.Data.Nat.Order +open import Cubical.Tactics.CommRingSolver + +module Minor (ℓ : Level) where + + -- definition and properties to remove one Index, i.e. (removeIndex i) is the monoton ebbeding from {0,...,n-1} to {0,...,n} ommiting i. + + removeIndex : {n : ℕ} → Fin (suc n) → Fin n → Fin (suc n) + removeIndex zero k = suc k + removeIndex (suc i) zero = zero + removeIndex (suc i) (suc k) = suc (removeIndex i k) + + -- On {0,...,i-1} the map (removeIndex i) is the identity. + removeIndexId : {n : ℕ} → (i : Fin (suc n)) → (k : Fin n) → (suc k) ≤'Fin i → (removeIndex i k) ≡ weakenFin k + removeIndexId (suc i) zero le = refl + removeIndexId (suc i) (suc k) (s≤s le) = cong (λ a → suc a) (removeIndexId i k le) + + -- On {i,...,n-1} the map (removeIndex i) is the successor function. + removeIndexSuc : {n : ℕ} → (i : Fin (suc n)) → (k : Fin n) → i ≤'Fin weakenFin k → (removeIndex i k) ≡ suc k + removeIndexSuc zero k le = refl + removeIndexSuc (suc i) (suc k) (s≤s le) = cong (λ a → suc a) (removeIndexSuc i k le) + + -- A formula for commuting removeIndex maps + removeIndexComm : {n : ℕ} → (i j : Fin (suc n)) → (k : Fin n) → i ≤'Fin j → + removeIndex (suc j) (removeIndex i k) ≡ removeIndex (weakenFin i) (removeIndex j k) + removeIndexComm zero j k le = refl + removeIndexComm (suc i) (suc j) zero le = refl + removeIndexComm (suc i) (suc j) (suc k) (s≤s le) = cong (λ a → suc a) (removeIndexComm i j k le) + + -- remove the j-th column of a matrix + + remove-column : {A : Type ℓ} {n m : ℕ} (j : Fin (suc m)) (M : FinMatrix A n (suc m)) → FinMatrix A n m + remove-column j M k l = M k (removeIndex j l) + + remove-column-comm : {A : Type ℓ} {n m : ℕ} (i : Fin (suc m)) (j : Fin (suc m)) (M : FinMatrix A n (suc (suc m))) (k : Fin n) (l : Fin m) → + j ≤'Fin i → + remove-column j (remove-column (suc i) M) k l ≡ remove-column i (remove-column (weakenFin j) M) k l + remove-column-comm i j M k l le = + remove-column j (remove-column (suc i) M) k l + ≡⟨ refl ⟩ + M k (removeIndex (suc i) (removeIndex j l)) + ≡⟨ cong (λ a → M k a) ( removeIndexComm j i l le) ⟩ + M k (removeIndex (weakenFin j) (removeIndex i l)) + ≡⟨ refl ⟩ + remove-column i (remove-column (weakenFin j) M) k l + ∎ + + -- remove the i-th row of a matrix + remove-row : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n)) (M : FinMatrix A (suc n) m) → FinMatrix A n m + remove-row i M k l = M (removeIndex i k) l + + remove-row-comm : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n)) (j : Fin (suc n)) (M : FinMatrix A (suc (suc n)) m) (k : Fin n) (l : Fin m) → + j ≤'Fin i → + remove-row j (remove-row (suc i) M) k l ≡ remove-row i (remove-row (weakenFin j) M) k l + remove-row-comm i j M k l le = + remove-row j (remove-row (suc i) M) k l + ≡⟨ refl ⟩ + M (removeIndex (suc i) (removeIndex j k)) l + ≡⟨ cong (λ a → M a l) ( removeIndexComm j i k le) ⟩ + M (removeIndex (weakenFin j) (removeIndex i k)) l + ≡⟨ refl ⟩ + remove-row i (remove-row (weakenFin j) M) k l + ∎ + + remove-column-row-comm : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n)) (j : Fin (suc m)) (M : FinMatrix A (suc n) (suc m)) (k : Fin n) (l : Fin m) → (remove-row i (remove-column j M)) k l ≡ (remove-column j (remove-row i M)) k l + remove-column-row-comm i j M k l = refl + + -- Calculating of the minor. + minor : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n)) (j : Fin (suc m)) (M : FinMatrix A (suc n) (suc m)) → FinMatrix A n m + minor i j M = remove-column j (remove-row i M) + + -- Compatability of the minor with the equality. + minorComp : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n)) (j : Fin (suc m)) (M N : FinMatrix A (suc n) (suc m)) → ((i : Fin (suc n)) → (j : Fin (suc m)) → M i j ≡ N i j ) → (k : Fin n) → (l : Fin m) → minor i j M k l ≡ minor i j N k l + minorComp {n = suc n} {suc m} i j M N f k l = f (removeIndex i k) (removeIndex j l) + + -- Formulas to commute minors + minorComm0 : {A : Type ℓ} {n m : ℕ} (i₁ i₂ : Fin (suc n)) (j₁ j₂ : Fin (suc m)) (k : Fin n) (l : Fin m) (M : FinMatrix A (suc (suc n)) (suc (suc m))) → + i₂ ≤'Fin i₁ → j₂ ≤'Fin j₁ → + minor i₂ j₂ (minor (suc i₁) (suc j₁) M) k l ≡ minor i₁ j₁ (minor (weakenFin i₂) (weakenFin j₂) M) k l + minorComm0 i₁ i₂ j₁ j₂ k l M lei lej = + M (removeIndex (suc i₁) (removeIndex i₂ k)) + (removeIndex (suc j₁) (removeIndex j₂ l)) + ≡⟨ cong (λ a → M a (removeIndex (suc j₁) (removeIndex j₂ l))) (removeIndexComm i₂ i₁ k lei) ⟩ + M (removeIndex (weakenFin i₂) (removeIndex i₁ k)) + (removeIndex (suc j₁) (removeIndex j₂ l)) + ≡⟨ cong (λ a → M (removeIndex (weakenFin i₂) (removeIndex i₁ k)) a ) ((removeIndexComm j₂ j₁ l lej)) ⟩ + M (removeIndex (weakenFin i₂) (removeIndex i₁ k)) + (removeIndex (weakenFin j₂) (removeIndex j₁ l)) + ∎ + + minorComm1 : {A : Type ℓ} {n m : ℕ} (i₁ i₂ : Fin (suc n)) (j₁ j₂ : Fin (suc m)) (k : Fin n) (l : Fin m) (M : FinMatrix A (suc (suc n)) (suc (suc m))) → + i₂ ≤'Fin i₁ → j₁ ≤'Fin j₂ → + minor i₂ j₂ (minor (suc i₁) (weakenFin j₁) M) k l ≡ minor i₁ j₁ (minor (weakenFin i₂) (suc j₂) M) k l + + minorComm1 i₁ i₂ j₁ j₂ k l M lei lej = + M (removeIndex (suc i₁) (removeIndex i₂ k)) + (removeIndex (weakenFin j₁) (removeIndex j₂ l)) + ≡⟨ cong (λ a → M a (removeIndex (weakenFin j₁) (removeIndex j₂ l))) ((removeIndexComm i₂ i₁ k lei)) ⟩ + M (removeIndex (weakenFin i₂) (removeIndex i₁ k)) + (removeIndex (weakenFin j₁) (removeIndex j₂ l)) + ≡⟨ cong (λ a → M (removeIndex (weakenFin i₂) (removeIndex i₁ k)) a) (sym ((removeIndexComm j₁ j₂ l lej))) ⟩ + M (removeIndex (weakenFin i₂) (removeIndex i₁ k)) + (removeIndex (suc j₂) (removeIndex j₁ l)) + ∎ + + minorComm2 : {A : Type ℓ} {n m : ℕ} (i₁ i₂ : Fin (suc n)) (j₁ j₂ : Fin (suc m)) (k : Fin n) (l : Fin m) (M : FinMatrix A (suc (suc n)) (suc (suc m))) → + i₁ ≤'Fin i₂ → j₂ ≤'Fin j₁ → + minor i₂ j₂ (minor (weakenFin i₁) (suc j₁) M) k l ≡ minor i₁ j₁ (minor (suc i₂) (weakenFin j₂) M) k l + + minorComm2 i₁ i₂ j₁ j₂ k l M lei lej = + M (removeIndex (weakenFin i₁) (removeIndex i₂ k)) + (removeIndex (suc j₁) (removeIndex j₂ l)) + ≡⟨ cong (λ a → M a (removeIndex (suc j₁) (removeIndex j₂ l))) (sym ((removeIndexComm i₁ i₂ k lei))) ⟩ + M (removeIndex (suc i₂) (removeIndex i₁ k)) + (removeIndex (suc j₁) (removeIndex j₂ l)) + ≡⟨ cong (λ a → M (removeIndex (suc i₂) (removeIndex i₁ k)) a) ((removeIndexComm j₂ j₁ l lej)) ⟩ + M (removeIndex (suc i₂) (removeIndex i₁ k)) + (removeIndex (weakenFin j₂) (removeIndex j₁ l)) + ∎ + + minorSemiCommR : {A : Type ℓ} {n m : ℕ} (i₁ : Fin (suc (suc n))) (i₂ : Fin (suc n)) (j₁ j₂ : Fin (suc m)) (k : Fin n) (l : Fin m) (M : FinMatrix A (suc (suc n)) (suc (suc m))) → + j₂ ≤'Fin j₁ → + minor i₂ j₂ (minor i₁ (suc j₁) M) k l ≡ minor i₂ j₁ (minor i₁ (weakenFin j₂) M) k l + minorSemiCommR i₁ i₂ j₁ j₂ k l M lej = + cong + (λ a → M (removeIndex i₁ (removeIndex i₂ k)) a) + (removeIndexComm j₂ j₁ l lej) + + + --Formulas to compute compute the entries of the minor. + minorIdId : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n))(j : Fin (suc m)) (k : Fin n)(l : Fin m) (M : FinMatrix A (suc n) (suc m)) → + suc k ≤'Fin i → suc l ≤'Fin j → + minor i j M k l ≡ M (weakenFin k) (weakenFin l) + minorIdId i j k l M lei lej = + M (removeIndex i k) (removeIndex j l) + ≡⟨ cong (λ a → M a (removeIndex j l)) (removeIndexId i k lei) ⟩ + M (weakenFin k) (removeIndex j l) + ≡⟨ cong (λ a → M (weakenFin k) a) (removeIndexId j l lej) ⟩ + M (weakenFin k) (weakenFin l) + ∎ + + minorSucSuc : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n))(j : Fin (suc m)) (k : Fin n)(l : Fin m) (M : FinMatrix A (suc n) (suc m)) → + i ≤'Fin weakenFin k → j ≤'Fin weakenFin l → + minor i j M k l ≡ M (suc k) (suc l) + minorSucSuc i j k l M lei lej = + M (removeIndex i k) (removeIndex j l) + ≡⟨ cong (λ a → M a (removeIndex j l)) (removeIndexSuc i k lei) ⟩ + M (suc k) (removeIndex j l) + ≡⟨ cong (λ a → M (suc k) a) (removeIndexSuc j l lej) ⟩ + M (suc k) (suc l) + ∎ + + minorIdSuc : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n))(j : Fin (suc m)) (k : Fin n)(l : Fin m) (M : FinMatrix A (suc n) (suc m)) → + suc k ≤'Fin i → j ≤'Fin weakenFin l → + minor i j M k l ≡ M (weakenFin k) (suc l) + minorIdSuc i j k l M lei lej = + M (removeIndex i k) (removeIndex j l) + ≡⟨ cong (λ a → M a (removeIndex j l)) (removeIndexId i k lei) ⟩ + M (weakenFin k) (removeIndex j l) + ≡⟨ cong (λ a → M (weakenFin k) a) (removeIndexSuc j l lej) ⟩ + M (weakenFin k) (suc l) + ∎ + + minorSucId : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n))(j : Fin (suc m)) (k : Fin n)(l : Fin m) (M : FinMatrix A (suc n) (suc m)) → + i ≤'Fin weakenFin k → suc l ≤'Fin j → + minor i j M k l ≡ M (suc k) (weakenFin l) + minorSucId i j k l M lei lej = + M (removeIndex i k) (removeIndex j l) + ≡⟨ cong (λ a → M a (removeIndex j l)) (removeIndexSuc i k lei) ⟩ + M (suc k) (removeIndex j l) + ≡⟨ cong (λ a → M (suc k) a) (removeIndexId j l lej) ⟩ + M (suc k) (weakenFin l) + ∎ + diff --git a/Cubical/Algebra/Determinat/RingSum.agda b/Cubical/Algebra/Determinat/RingSum.agda new file mode 100644 index 000000000..f95ce43c4 --- /dev/null +++ b/Cubical/Algebra/Determinat/RingSum.agda @@ -0,0 +1,348 @@ +{-# OPTIONS --cubical #-} + +module RingSum where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ + ; +-comm to +ℕ-comm + ; +-assoc to +ℕ-assoc + ; ·-assoc to ·ℕ-assoc) +open import Cubical.Data.Vec.Base using (_∷_; []) +open import Cubical.Foundations.Structure using (⟨_⟩) +open import Cubical.Data.FinData +open import Cubical.Algebra.Ring +open import Cubical.Algebra.Ring.Base +open import Cubical.Algebra.Ring.BigOps +open import Cubical.Algebra.Monoid.BigOp +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommRing.Base +open import Cubical.Data.Nat.Order +open import Cubical.Tactics.CommRingSolver + +module RingSum (ℓ : Level) (P' : CommRing ℓ) where + + R' = CommRing→Ring P' + + open RingStr (snd (CommRing→Ring P')) renaming ( is-set to isSetR) + + ∑ = Sum.∑ (CommRing→Ring P') + + R : Type ℓ + R = ⟨ P' ⟩ + + open MonoidBigOp (Ring→AddMonoid R') + + + + -- Compatability theorems + ∑Compat : {n : ℕ} → (U V : FinVec R n) → + ((i : Fin n) → U i ≡ V i) → ∑ U ≡ ∑ V + ∑Compat U V f = bigOpExt f + + ∑∑Compat : {n m : ℕ} → (U V : FinVec (FinVec R m) n) → + ((i : Fin n) → (j : Fin m) → U i j ≡ V i j) → + ∑ (λ i → ∑ (λ j → U i j)) ≡ ∑ (λ i → ∑ (λ j → V i j)) + ∑∑Compat U V Eq = + ∑ (λ i → ∑ (U i)) + ≡⟨ + ∑Compat + (λ i → ∑ (U i)) + (λ i → ∑ (V i)) + (λ i → ∑Compat (U i) (V i) (Eq i)) + ⟩ + ∑ (λ i → ∑ (V i)) + ∎ + + -- Spliting a sum in the sum: + ∑Split = Sum.∑Split R' + + ∑∑Split : {n m : ℕ} → (U V : Fin n → Fin m → R) → + ∑ (λ i → ∑ (λ j → U i j + V i j)) + ≡ + ∑ (λ i → ∑ (λ j → U i j)) + + ∑ (λ i → ∑ (λ j → V i j)) + ∑∑Split U V = + ∑ (λ i → ∑ (λ j → U i j + V i j)) + ≡⟨ + ∑Compat + (λ i → ∑ (λ j → U i j + V i j)) + (λ i → ∑ (λ j → U i j) + ∑ ( λ j → V i j)) + (λ i → ∑Split (λ j → U i j) ( λ j → V i j)) + ⟩ + ∑ (λ i → ∑ (λ j → U i j) + ∑ (λ j → V i j)) + ≡⟨ ∑Split (λ i → ∑ (λ j → U i j)) (λ i → ∑ (λ j → V i j)) ⟩ + (∑ (λ i → ∑ (U i)) + ∑ (λ i → ∑ (V i))) + ∎ + + -- Distributivity of the sum + ∑DistR = Sum.∑Mulrdist (CommRing→Ring P') + + ∑DistL = Sum.∑Mulldist (CommRing→Ring P') + + -- Sum of Zeros is Zero + ∑Zero : {n : ℕ} → (U : FinVec R n) → ((i : Fin n) → U i ≡ 0r) → ∑ U ≡ 0r + ∑Zero {zero} U f = refl + ∑Zero {suc n} U f = + ∑ U + ≡⟨ refl ⟩ + (U zero + ∑ (λ i → U (suc i)) ) + ≡⟨ cong (λ a → a + ∑ (λ i → U (suc i))) (f zero) ⟩ + (0r + ∑ (λ i → U (suc i))) + ≡⟨ +Comm 0r (∑ (λ i → U (suc i))) ⟩ + ∑ (λ i → U (suc i)) + 0r + ≡⟨ +IdR (∑ (λ i → U (suc i))) ⟩ + ∑ (λ i → U (suc i)) + ≡⟨ ∑Zero {n} ((λ i → U (suc i))) (λ i → f (suc i)) ⟩ + 0r ∎ + + -- Summs are commutative + ∑Comm : {n m : ℕ} → (U : FinVec (FinVec R m) n) → + ∑ (λ i → ∑ (λ j → U i j )) ≡ ∑ (λ j → ∑ (λ i → U i j)) + ∑Comm {zero} {zero} U = refl + ∑Comm {zero} {m} U = + 0r + ≡⟨ sym (∑Zero (λ (j : Fin m) → 0r) (λ (j : Fin m) → refl)) ⟩ + ∑ (λ (j : Fin m) → 0r) + ≡⟨ ∑Compat (λ j → 0r) (λ j → ∑ (λ i → U i j )) (λ j → refl) ⟩ + ( (∑ λ j → ∑ (λ i → U i j ))) + ∎ + ∑Comm {n} {zero} U = + ∑ (λ (i : Fin n) → 0r) + ≡⟨ ∑Zero ( (λ (i : Fin n) → 0r)) ( (λ i → refl)) ⟩ + 0r + ∎ + ∑Comm {suc n} {suc m} U = + ∑ (λ i → ∑ (U i)) + ≡⟨ refl ⟩ + ( ∑ (λ i → (U i zero + ∑ λ j → (U i (suc j)))) ) + ≡⟨ bigOpSplit +Comm (λ i → U i zero) (λ i → ∑ λ j → (U i (suc j))) ⟩ + (∑ (λ i → (U i zero)) + ∑ λ i → (∑ λ j → (U i (suc j)))) + ≡⟨ cong (λ a → ∑ (λ i → (U i zero)) + a) (∑Comm λ i → ( λ j → (U i (suc j) ))) ⟩ + (∑ (λ i → U i zero) + ∑ (λ j → ∑ (λ i → U i (suc j)))) + ≡⟨ refl ⟩ + ∑ (λ j → ∑ (λ i → U i j)) + ∎ + + -- Indikator function: ind> i j = 1r if i>j and ind> i j = 0r else + ind> : (i j : ℕ) → R + ind> zero j = 0r + ind> (suc i) zero = 1r + ind> (suc i) (suc j) = ind> i j + + ind>prop : {n m : ℕ} → (A B : FinVec (FinVec R m) n) → + ((i : Fin n) → (j : Fin m) → (toℕ j) <' (toℕ i) → A i j ≡ B i j) → + (i : Fin n) → (j : Fin m) → + (ind> (toℕ i) (toℕ j) · A i j) ≡ (ind> (toℕ i) (toℕ j) · B i j) + ind>prop {m = suc m} A B f zero j = solve! P' + ind>prop {m = suc m} A B f (suc i) zero = + cong + (λ a → 1r · a) + (f (suc i) zero (s≤s z≤)) + ind>prop {m = suc m} A B f (suc i) (suc j) = + ind>prop + (λ i j → A (suc i) (suc j)) + (λ i j → B (suc i) (suc j)) + (λ i₁ j₁ le → f (suc i₁) (suc j₁) + (s≤s le)) + i + j + + ind>anti : {n m : ℕ} → (A B : FinVec (FinVec R m) n) → + ((i : Fin n) (j : Fin m) → (toℕ i) ≤' (toℕ j) → A i j ≡ B i j) → + (i : Fin n) → (j : Fin m) → + (1r + (- ind> (toℕ i) (toℕ j))) · A i j ≡ (1r + - (ind> (toℕ i) (toℕ j))) · B i j + ind>anti {m = suc m} A B f zero j = + cong + (λ a → (1r + - 0r) · a) + (f zero j z≤) + ind>anti {m = suc m} A B f (suc i) zero = solve! P' + ind>anti {m = suc m} A B f (suc i) (suc j) = + ind>anti + (λ i j → A (suc i) (suc j)) + (λ i j → B (suc i) (suc j)) + (λ i₁ j₁ le → f (suc i₁) (suc j₁) (s≤s le)) i j + + ind>Neg : (i j : ℕ) → (1r + - ind> (suc i) j) ≡ ind> j i + ind>Neg i zero = +InvR 1r + ind>Neg zero (suc j) = solve! P' + ind>Neg (suc i) (suc j) = ind>Neg i j + + ind>Suc : (i j : ℕ) → ind> (suc i) j ≡ (1r + - ind> j i) + ind>Suc i zero = solve! P' + ind>Suc zero (suc j) = solve! P' + ind>Suc (suc i) (suc j) = ind>Suc i j + + --Index Shift-- + ∑∑ShiftSuc : {n : ℕ} → (A : Fin (suc n) → Fin n → R) → + ∑ (λ (i : Fin (suc n)) → ∑ ( λ j → ind> (toℕ i) (toℕ j) · A i j)) + ≡ + ∑ (λ (i : Fin n) → ∑ ( λ j → ind> (toℕ (suc i)) (toℕ j) · A (suc i) j)) + ∑∑ShiftSuc {zero} A = ∑Zero {one} (λ j → 0r) (λ j → refl) + ∑∑ShiftSuc {suc n} A = + ∑ {suc (suc n)} + (λ i → + ∑ (λ j → ind> (toℕ i) (toℕ j) · A i j)) + ≡⟨ refl ⟩ + ∑ {suc n} + (λ j → ind> zero (toℕ j) · A zero j) + + ∑ (λ i → + ∑ (λ j → + ind> (toℕ (suc i)) (toℕ j) · A (suc i) j)) + ≡⟨ + cong + (λ a → a + ∑ (λ i → + ∑ (λ j → ind> (toℕ (suc i)) (toℕ j) · A (suc i) j))) + (∑Compat + (λ j → ind> zero (toℕ j) · A zero j) + (λ j → 0r) + (λ j → solve! P')) + ⟩ + ∑ {suc n} (λ j → 0r) + + ∑ (λ i → ∑ (λ j → ind> (toℕ (suc i)) (toℕ j) · A (suc i) j)) + ≡⟨ + cong + (λ a → a + ∑ (λ i → ∑ (λ j → ind> (toℕ (suc i)) (toℕ j) · A (suc i) j))) + (∑Zero {suc n} (λ j → 0r) (λ j → refl)) ⟩ + 0r + ∑ (λ i → ∑ (λ j → ind> (toℕ (suc i)) (toℕ j) · A (suc i) j)) + ≡⟨ + +Comm + 0r + (∑ (λ i → ∑ (λ j → ind> (toℕ (suc i)) (toℕ j) · A (suc i) j))) + ⟩ + ∑ (λ i → ∑ (λ j → ind> (toℕ (suc i)) (toℕ j) · A (suc i) j)) + 0r + ≡⟨ + +IdR + (∑ (λ i → ∑ (λ j → ind> (toℕ (suc i)) (toℕ j) · A (suc i) j))) + ⟩ + ∑ (λ i → ∑ (λ j → ind> (toℕ (suc i)) (toℕ j) · A (suc i) j)) + ∎ + + ∑∑ShiftWeak : {n : ℕ} → (A : Fin (suc n) → Fin n → R) → + ∑ (λ (i : Fin (suc n)) → ∑ ( λ j → (1r + - ind> (toℕ i) (toℕ j)) · A i j)) + ≡ + ∑ (λ (i : Fin n) → + ∑ ( λ j → + (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) · A (weakenFin i) j)) + ∑∑ShiftWeak {zero} A = + ∑Zero {one} + (λ i → ∑ ( λ j → (1r + - ind> (toℕ i) (toℕ j)) · A i j)) + (λ i → refl) + ∑∑ShiftWeak {suc n} A = + (∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) + + ∑ + (λ i → ∑ (λ j → (1r + - ind> (toℕ (suc i)) (toℕ j)) · A (suc i) j))) + ≡⟨ + cong + (λ a → ∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) + a) + (∑Compat + (λ i → ∑ (λ j → (1r + - ind> (toℕ (suc i)) (toℕ j)) · A (suc i) j)) + (λ i → + (1r + - ind> (toℕ (suc i)) zero) · A (suc i) zero + + ∑ (λ j → (1r + - ind> (toℕ (suc i)) (toℕ (suc j))) · A (suc i) (suc j))) + (λ i → refl)) + ⟩ + ∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) + + ∑ (λ i → + (1r + - ind> (toℕ (suc i)) zero) · A (suc i) zero + + ∑ (λ j → + (1r + - ind> (toℕ (suc i)) (toℕ (suc j))) · A (suc i) (suc j))) + ≡⟨ + cong + (λ a → ∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) + a) + (∑Split + (λ i → + (1r + - ind> (toℕ (suc i)) zero) · A (suc i) zero) + (λ i → + ∑ (λ j → + (1r + - ind> (toℕ (suc i)) (toℕ (suc j))) + · A (suc i) (suc j)))) + ⟩ + (∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) + + (∑ (λ i → (1r + - ind> (toℕ (suc i)) zero) · A (suc i) zero) + + ∑ + (λ i → + ∑ (λ j → (1r + - ind> (toℕ i) (toℕ j)) · A (suc i) (suc j))))) + ≡⟨ + cong + (λ a → + ∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) + + (∑ (λ i → + (1r + - ind> (toℕ (suc i)) zero) · + A (suc i) zero) + a)) + (∑∑ShiftWeak (λ i j → A (suc i) (suc j))) + ⟩ + (∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) + + (∑ (λ i → (1r + - ind> (toℕ (suc i)) zero) · A (suc i) zero) + + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ (suc (weakenFin i))) (toℕ (suc j))) + · A (suc (weakenFin i)) (suc j))))) + ≡⟨ + cong + (λ a → + (∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) + + (a + + ∑ (λ i → + ∑ (λ j → + (1r + - ind> (toℕ (suc (weakenFin i))) (toℕ (suc j))) + · A (suc (weakenFin i)) (suc j)))))) + ( + ∑ (λ i → (1r + - ind> (toℕ (suc i)) zero) · A (suc i) zero) + ≡⟨ refl ⟩ + ∑ (λ i → + (1r + - 1r) · A (suc i) zero) + ≡⟨ ∑Compat ( + λ i → (1r + - 1r) · A (suc i) zero) + (λ i → 0r) + (λ i → solve! P') + ⟩ + ∑ (λ (i : Fin (suc n)) → 0r) + ≡⟨ + ∑Zero + (λ (i : Fin (suc n)) → 0r) + (λ i → refl) + ⟩ + 0r + ≡⟨ sym (∑Zero (λ (i : Fin n) → 0r) (λ i → refl)) ⟩ + ∑ (λ (i : Fin n) → 0r) + ≡⟨ ∑Compat + (λ (i : Fin n) → 0r) + (λ i → (1r + - 1r) · A (suc (weakenFin i)) zero) + (λ i → solve! P') + ⟩ + ∑ (λ i → (1r + - 1r) · A (suc (weakenFin i)) zero)∎ + )⟩ + (∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) + + (∑ + (λ i → + (1r + - ind> (toℕ (suc (weakenFin i))) zero) · + A (suc (weakenFin i)) zero) + + + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ (suc (weakenFin i))) (toℕ (suc j))) · + A (suc (weakenFin i)) (suc j))))) + ≡⟨ + cong + (λ a → ∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) + a) + (sym + (∑Split + (λ i → + (1r + - ind> (toℕ (suc (weakenFin i))) zero) · + A (suc (weakenFin i)) zero) + (λ i → ∑ (λ j → + (1r + - ind> (toℕ (suc (weakenFin i))) (toℕ (suc j))) · + A (suc (weakenFin i)) (suc j))))) + ⟩ + ∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) + + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ (suc (weakenFin i))) (toℕ j)) · + A (suc (weakenFin i)) j)) ∎ diff --git a/Cubical/Algebra/Determinat/adjugate.agda b/Cubical/Algebra/Determinat/adjugate.agda new file mode 100644 index 000000000..a2f31ab3d --- /dev/null +++ b/Cubical/Algebra/Determinat/adjugate.agda @@ -0,0 +1,1925 @@ +{-# OPTIONS --cubical #-} + +module adjugate where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Algebra.Matrix +open import Cubical.Algebra.Matrix.CommRingCoefficient +open import Cubical.Functions.FunExtEquiv +open import Cubical.Data.Bool +open import Cubical.Data.Sum +open import Cubical.Foundations.Structure using (⟨_⟩) +open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ + ; +-comm to +ℕ-comm + ; +-assoc to +ℕ-assoc + ; ·-assoc to ·ℕ-assoc) +open import Cubical.Data.FinData +open import Cubical.Data.FinData.Order using (_<'Fin_; _≤'Fin_) +open import Cubical.Algebra.Ring +open import Cubical.Algebra.Ring.Base +open import Cubical.Algebra.Ring.BigOps +open import Cubical.Algebra.Monoid.BigOp +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommRing.Base +open import Cubical.Algebra.Semiring +open import Cubical.Data.Int.Base using (pos; negsuc) +open import Cubical.Data.Vec.Base using (_∷_; []) +open import Cubical.Data.Nat.Order +open import Cubical.Tactics.CommRingSolver + +open import Minor +open import RingSum +open import det + +module adjugate (ℓ : Level) (P' : CommRing ℓ) where + open Minor.Minor ℓ + open RingSum.RingSum ℓ P' + open RingStr (snd (CommRing→Ring P')) renaming ( is-set to isSetR ) + open Determinat ℓ P' + open Coefficient (P') + + _∘_ : {n m : ℕ} → R → FinMatrix R n m → FinMatrix R n m + (a ∘ M) i j = a · (M i j) + + deltaProp : {n : ℕ} → (k l : Fin n) → toℕ k <' toℕ l → δ k l ≡ 0r + deltaProp {suc n} zero (suc l) (s≤s le) = refl + deltaProp {suc n} (suc k) (suc l) (s≤s le) = deltaProp {n} k l le + + deltaPropSym : {n : ℕ} → (k l : Fin n) → toℕ l <' toℕ k → δ k l ≡ 0r + deltaPropSym {suc n} (suc k) (zero) (s≤s le) = refl + deltaPropSym {suc n} (suc k) (suc l) (s≤s le) = deltaPropSym {n} k l le + + ==Refl : {n : ℕ} → (k : Fin n) → k == k ≡ true + ==Refl {n} zero = refl + ==Refl {suc n} (suc k) = ==Refl {n} k + + ==Sym : {n : ℕ} → (k l : Fin n) → k == l ≡ l == k + ==Sym {suc n} zero zero = refl + ==Sym {suc n} zero (suc l) = refl + ==Sym {suc n} (suc k) zero = refl + ==Sym {suc n} (suc k) (suc l) = ==Sym {n} k l + + deltaPropEq : {n : ℕ} → (k l : Fin n) → k ≡ l → δ k l ≡ 1r + deltaPropEq k l e = + δ k l + ≡⟨ cong (λ a → δ a l) e ⟩ + δ l l + ≡⟨ cong (λ a → if a then 1r else 0r) (==Refl l) ⟩ + 1r + ∎ + + deltaComm : {n : ℕ} → (k l : Fin n) → δ k l ≡ δ l k + deltaComm k l = cong (λ a → if a then 1r else 0r) (==Sym k l) + + + -- Definition of the cofactor matrix + cof : {n : ℕ} → FinMatrix R n n → FinMatrix R n n + cof {suc n} M i j = (MF (toℕ i +ℕ toℕ j)) · det {n} (minor i j M) + + cofTransp : {n : ℕ} → (M : FinMatrix R n n) → (i j : Fin n) → cof (M ᵗ) i j ≡ cof M j i + cofTransp {suc n} M i j = + MF (toℕ i +ℕ toℕ j) · det (minor i j (M ᵗ)) + ≡⟨ cong (λ a → MF (toℕ i +ℕ toℕ j) · a) (detTransp ((minor j i M ᵗ))) ⟩ + (MF (toℕ i +ℕ toℕ j) · det (minor j i M)) + ≡⟨ + cong + (λ a → MF (a) · det (minor j i M)) (+ℕ-comm (toℕ i) (toℕ j)) ⟩ + (MF (toℕ j +ℕ toℕ i) · det (minor j i M)) + ∎ + + -- Definition of the adjugate matrix + adjugate : {n : ℕ} → FinMatrix R n n → FinMatrix R n n + adjugate M i j = cof M j i + + adjugateTransp : {n : ℕ} → (M : FinMatrix R n n) → (i j : Fin n) → adjugate (M ᵗ) i j ≡ adjugate M j i + adjugateTransp M i j = cofTransp M j i + + + weakenPredFinLt : {n : ℕ} → (k l : Fin (suc (suc n))) → toℕ k <' toℕ l → k ≤'Fin weakenFin (predFin l) + weakenPredFinLt {zero} zero one (s≤s z≤) = z≤ + weakenPredFinLt {zero} one one (s≤s ()) + weakenPredFinLt {zero} one (suc (suc ())) (s≤s le) + weakenPredFinLt {suc n} zero one (s≤s z≤) = z≤ + weakenPredFinLt {suc n} zero (suc (suc l)) (s≤s le) = z≤ + weakenPredFinLt {suc n} (suc k) (suc (suc l)) (s≤s (s≤s le)) = s≤s ( weakenPredFinLt {n} k (suc l) (s≤s le)) + + sucPredFin : {n : ℕ} → (k l : Fin (suc (suc n))) → toℕ k <' toℕ l → suc (predFin l) ≡ l + sucPredFin {zero} zero one le = refl + sucPredFin {zero} (suc k) (suc l) le = refl + sucPredFin {suc n} zero (suc l) le = refl + sucPredFin {suc n} (suc k) (suc l) (s≤s le) = refl + + adjugatePropAux1a : {n : ℕ} → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → (k l : Fin (suc (suc n))) → toℕ k <' toℕ l → + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M)))))) + ≡ + ∑ + (λ i → + ∑ + (λ z → + ind> (toℕ i) (toℕ z) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ z) · M l (weakenFin z)) + · det (minor (predFin l) z (minor k i M))))) + adjugatePropAux1a M k l le = + ∑∑Compat + (λ i j → + ind> (toℕ i) (toℕ j) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M))))) + (λ z z₁ → + ind> (toℕ z) (toℕ z₁) · + (M l z · MF (toℕ k +ℕ toℕ z) · + (MF (toℕ (predFin l) +ℕ toℕ z₁) · M l (weakenFin z₁)) + · det (minor (predFin l) z₁ (minor k z M)))) + (ind>prop + (λ z z₁ → + M l z · MF (toℕ k +ℕ toℕ z) · + (MF (toℕ (predFin l) +ℕ toℕ z₁) · minor k z M (predFin l) z₁ · + det (minor (predFin l) z₁ (minor k z M)))) + (λ z z₁ → + M l z · MF (toℕ k +ℕ toℕ z) · + (MF (toℕ (predFin l) +ℕ toℕ z₁) · M l (weakenFin z₁)) + · det (minor (predFin l) z₁ (minor k z M))) + (λ i j lf → + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M)))) + ≡⟨ + cong + (λ a → M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · a · + det (minor (predFin l) j (minor k i M)))) + (minorSucId + k + i + (predFin l) + j + M + (weakenPredFinLt k l le) + lf) + ⟩ + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · M (suc (predFin l)) (weakenFin j) + · det (minor (predFin l) j (minor k i M)))) + ≡⟨ ·Assoc _ _ _ ⟩ + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · M (suc (predFin l)) (weakenFin j)) + · det (minor (predFin l) j (minor k i M))) + ≡⟨ cong + (λ a → (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · M a (weakenFin j)) + · det (minor (predFin l) j (minor k i M)))) + (sucPredFin + k + l + le + ) + ⟩ + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · M l (weakenFin j)) + · det (minor (predFin l) j (minor k i M))) + ∎ + ) + ) + + adjugatePropAux1b : {n : ℕ} → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → (k l : Fin (suc (suc n))) → toℕ k <' toℕ l → + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ i) (toℕ j)) · + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l) +ℕ toℕ j) · + minor k (weakenFin i) M (predFin l) j + · det (minor (predFin l) j (minor k (weakenFin i) M)))))) + ≡ + ∑ + (λ i → + ∑ + (λ z → + (1r + - ind> (toℕ i) (toℕ z)) · + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc z))) · M l (suc z) · + det (minor (predFin l) i (minor k (suc z) M)))))) + + adjugatePropAux1b M k l le = + ∑∑Compat + (λ i j → + (1r + - ind> (toℕ i) (toℕ j)) · + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l) +ℕ toℕ j) · + minor k (weakenFin i) M (predFin l) j + · det (minor (predFin l) j (minor k (weakenFin i) M))))) + (λ z z₁ → + (1r + - ind> (toℕ z) (toℕ z₁)) · + (M l (weakenFin z) · MF (toℕ k +ℕ toℕ (weakenFin z)) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc z₁))) · M l (suc z₁) · + det (minor (predFin l) z (minor k (suc z₁) M))))) + λ i j → + ind>anti + (λ i j → (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l) +ℕ toℕ j) · + minor k (weakenFin i) M (predFin l) j + · det (minor (predFin l) j (minor k (weakenFin i) M))))) + (λ z z₁ → + M l (weakenFin z) · MF (toℕ k +ℕ toℕ (weakenFin z)) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc z₁))) · M l (suc z₁) · + det (minor (predFin l) z (minor k (suc z₁) M)))) + (λ i j lf → + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l) +ℕ toℕ j) · + minor k (weakenFin i) M (predFin l) j + · det (minor (predFin l) j (minor k (weakenFin i) M)))) + ≡⟨ + cong + (λ a → M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l) +ℕ toℕ j) · a + · det (minor (predFin l) j (minor k (weakenFin i) M)))) + (minorSucSuc + k (weakenFin i) (predFin l) j M (weakenPredFinLt k l le) (weakenweakenFinLe i j lf)) + ⟩ + M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l) +ℕ toℕ j) · M (suc (predFin l)) (suc j) · + det (minor (predFin l) j (minor k (weakenFin i) M))) + ≡⟨ + cong + (λ a → + M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l) +ℕ toℕ j) · M (a) (suc j) · + det (minor (predFin l) j (minor k (weakenFin i) M)))) + (sucPredFin k l le) + ⟩ + M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l) +ℕ toℕ j) · M l (suc j) · + det (minor (predFin l) j (minor k (weakenFin i) M))) + ≡⟨ + cong + (λ a → M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l) +ℕ toℕ j) · M l (suc j) · a)) + (detComp + (minor (predFin l) j (minor k (weakenFin i) M)) + (minor (predFin l) i (minor k (suc j) M)) + (λ i₁ j₁ → + (sym (minorSemiCommR k (predFin l) j i i₁ j₁ M lf)))) + ⟩ + M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l) +ℕ toℕ j) · M l (suc j) · + det (minor (predFin l) i (minor k (suc j) M))) + ≡⟨ cong + (λ a → + M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (a · M l (suc j) · + det (minor (predFin l) i (minor k (suc j) M)))) + (sumMF (toℕ (predFin l)) (toℕ j)) + ⟩ + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (suc j) · + det (minor (predFin l) i (minor k (suc j) M)))) + ≡⟨ + cong + (λ a → (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l)) · a · M l (suc j) · + det (minor (predFin l) i (minor k (suc j) M))))) + (sucMFRev (toℕ j)) + ⟩ + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc j))) · M l (suc j) · + det (minor (predFin l) i (minor k (suc j) M)))) + ∎) + i + j + + adjugatePropAux2a : {n : ℕ} → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → (k l : Fin (suc (suc n))) → + toℕ k <' toℕ l → + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · M l (weakenFin j)) + · det (minor (predFin l) j (minor k i M))))) + ≡ + ∑ + (λ i → + ∑ + (λ z → + 1r · + (ind> (toℕ i) (toℕ z) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ z) · M l (weakenFin z) · + det (minor (predFin l) z (minor k i M))))))) + adjugatePropAux2a M k l le = + ∑∑Compat + (λ i j → + ind> (toℕ i) (toℕ j) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · M l (weakenFin j)) + · det (minor (predFin l) j (minor k i M)))) + (λ z z₁ → + 1r · + (ind> (toℕ z) (toℕ z₁) · + (M l z · (MF (toℕ k) · MF (toℕ z)) · + (MF (toℕ (predFin l)) · MF (toℕ z₁) · M l (weakenFin z₁) · + det (minor (predFin l) z₁ (minor k z M)))))) + (λ i j → + (ind> (toℕ i) (toℕ j) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · M l (weakenFin j)) + · det (minor (predFin l) j (minor k i M)))) + ≡⟨ + cong + (λ a → (ind> (toℕ i) (toℕ j) · + (M l i · a · + (MF (toℕ (predFin l) +ℕ toℕ j) · M l (weakenFin j)) + · det (minor (predFin l) j (minor k i M))))) + (sumMF (toℕ k) (toℕ i)) ⟩ + (ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l) +ℕ toℕ j) · M l (weakenFin j)) + · det (minor (predFin l) j (minor k i M)))) + ≡⟨ + cong + (λ a → (ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (a · M l (weakenFin j)) + · det (minor (predFin l) j (minor k i M))))) + (sumMF (toℕ (predFin l)) (toℕ j)) + ⟩ + (ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j)) + · det (minor (predFin l) j (minor k i M)))) + ≡⟨ cong + (λ a → (ind> (toℕ i) (toℕ j) · a)) + (sym (·Assoc _ _ _)) + ⟩ + ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) · + det (minor (predFin l) j (minor k i M)))) + ≡⟨ sym (·IdL _) ⟩ + (1r · (ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) · + det (minor (predFin l) j (minor k i M)))))) + ∎ ) + + adjugatePropAux2b : {n : ℕ} → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → (k l : Fin (suc (suc n))) → + toℕ k <' toℕ l → + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · MF (toℕ k +ℕ toℕ (weakenFin j)) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i · + det (minor (predFin l) j (minor k i M)))))) + ≡ + ∑ + (λ i → + ∑ + (λ z → + - 1r · + (ind> (toℕ i) (toℕ z) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ z) · M l (weakenFin z) · + det (minor (predFin l) z (minor k i M))))))) + adjugatePropAux2b M k l le = + ∑∑Compat + (λ i j → + ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · MF (toℕ k +ℕ toℕ (weakenFin j)) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i · + det (minor (predFin l) j (minor k i M))))) + (λ z z₁ → + - 1r · + (ind> (toℕ z) (toℕ z₁) · + (M l z · (MF (toℕ k) · MF (toℕ z)) · + (MF (toℕ (predFin l)) · MF (toℕ z₁) · M l (weakenFin z₁) · + det (minor (predFin l) z₁ (minor k z M)))))) + (λ i j → + (ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · MF (toℕ k +ℕ toℕ (weakenFin j)) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i · + det (minor (predFin l) j (minor k i M))))) + ≡⟨ + cong + (λ a → + (ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · a · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i · + det (minor (predFin l) j (minor k i M)))))) + (sumMF (toℕ k) (toℕ (weakenFin j))) + ⟩ + (ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · (MF (toℕ k) · MF (toℕ (weakenFin j))) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i · + det (minor (predFin l) j (minor k i M))))) + ≡⟨ + cong + (λ a → + (ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · (MF (toℕ k) · MF a) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i · + det (minor (predFin l) j (minor k i M)))))) + (toℕweakenFin j) ⟩ + (ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i · + det (minor (predFin l) j (minor k i M))))) + ≡⟨ + cong + (λ a → ind> (toℕ i) (toℕ j) · a) + (sym (·Assoc _ _ _)) + ⟩ + (ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · + (MF (toℕ k) · MF (toℕ j) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i · + det (minor (predFin l) j (minor k i M)))))) + ≡⟨ + cong + (λ a → + ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · a)) + (sym (·Assoc _ _ _)) + ⟩ + (ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · + (MF (toℕ k) · + (MF (toℕ j) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i · + det (minor (predFin l) j (minor k i M))))))) + ≡⟨ + cong + (λ a → + (ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · + (MF (toℕ k) · a)))) + (·Assoc _ _ _) + ⟩ + (ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · + (MF (toℕ k) · + (MF (toℕ j) · (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i) + · det (minor (predFin l) j (minor k i M)))))) + ≡⟨ + cong + (λ a → ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · a)) + (·Assoc _ _ _) + ⟩ + (ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · + (MF (toℕ k) · + (MF (toℕ j) · (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i)) + · det (minor (predFin l) j (minor k i M))))) + ≡⟨ cong + (λ a → ind> (toℕ i) (toℕ j) · a) + (·Assoc _ _ _) + ⟩ + (ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · + (MF (toℕ k) · + (MF (toℕ j) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i))) + · det (minor (predFin l) j (minor k i M)))) + ≡⟨ + cong + (λ a → ind> (toℕ i) (toℕ j) · (a · det (minor (predFin l) j (minor k i M)))) + (solve! P') + ⟩ + ind> (toℕ i) (toℕ j) · + (- 1r · M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j)) + · det (minor (predFin l) j (minor k i M))) + ≡⟨ ·Assoc _ _ _ ⟩ + (ind> (toℕ i) (toℕ j) · + (- 1r · M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j))) + · det (minor (predFin l) j (minor k i M))) + ≡⟨ + cong + (λ a → a · det (minor (predFin l) j (minor k i M))) + (·Assoc _ _ _) + ⟩ + (ind> (toℕ i) (toℕ j) · (- 1r · M l i · (MF (toℕ k) · MF (toℕ i))) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j)) + · det (minor (predFin l) j (minor k i M))) + ≡⟨ cong + (λ a → a · (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j)) + · det (minor (predFin l) j (minor k i M))) + (solve! P') + ⟩ + (- 1r) · ind> (toℕ i) (toℕ j) · (M l i · (MF (toℕ k) · MF (toℕ i))) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j)) + · det (minor (predFin l) j (minor k i M)) + ≡⟨ sym (·Assoc _ _ _) ⟩ + - 1r · ind> (toℕ i) (toℕ j) · (M l i · (MF (toℕ k) · MF (toℕ i))) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) · + det (minor (predFin l) j (minor k i M))) + ≡⟨ sym (·Assoc _ _ _) ⟩ + (- 1r · ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) · + det (minor (predFin l) j (minor k i M))))) + ≡⟨ sym (·Assoc _ _ _) ⟩ + - 1r · + (ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) · + det (minor (predFin l) j (minor k i M))))) + ∎) + + adjugatePropRG : {n : ℕ} → (M : FinMatrix R (suc n) (suc n)) → (k l : Fin (suc n)) → toℕ k <' toℕ l → + ∑ (λ i → (M l i · (MF (toℕ k +ℕ toℕ i) · det (minor k i M)))) ≡ 0r + adjugatePropRG {zero} M zero zero () + adjugatePropRG {zero} M zero (suc ()) (s≤s le) + adjugatePropRG {suc n} M k l le = + ∑ (λ i → M l i · (MF (toℕ k +ℕ toℕ i) · det (minor k i M))) + ≡⟨ ∑Compat + (λ i → M l i · (MF (toℕ k +ℕ toℕ i) · det (minor k i M))) + (λ i → M l i · MF (toℕ k +ℕ toℕ i) · det (minor k i M)) + (λ i → ·Assoc _ _ _) ⟩ + ∑ (λ i → M l i · MF (toℕ k +ℕ toℕ i) · det (minor k i M)) + ≡⟨ ∑Compat + (λ i → M l i · MF (toℕ k +ℕ toℕ i) · det (minor k i M)) + (λ i → M l i · MF (toℕ k +ℕ toℕ i) · detR (predFin l) (minor k i M)) + (λ i → + cong + (λ a → M l i · MF (toℕ k +ℕ toℕ i) · a) + (sym (DetRow (predFin l) (minor k i M)))) + ⟩ + ∑ + (λ i → + M l i · MF (toℕ k +ℕ toℕ i) · detR (predFin l) (minor k i M)) + ≡⟨ refl ⟩ + ∑ + (λ i → + M l i · MF (toℕ k +ℕ toℕ i) · + ∑ + (λ j → + MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M)))) + ≡⟨ ∑Compat + (λ i → + M l i · MF (toℕ k +ℕ toℕ i) · + ∑ + (λ j → + MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M)))) + (λ i → + ∑ + (λ j → M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M))))) + (λ i → + ∑DistR + (M l i · MF (toℕ k +ℕ toℕ i)) + (λ j → MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M)))) + ⟩ + ∑ + (λ i → + ∑ + (λ j → + M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M))))) + ≡⟨ ∑∑Compat + (λ i j → + M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M)))) + (λ z z₁ → + ind> (toℕ z) (toℕ z₁) · + (M l z · MF (toℕ k +ℕ toℕ z) · + (MF (toℕ (predFin l) +ℕ toℕ z₁) · minor k z M (predFin l) z₁ · + det (minor (predFin l) z₁ (minor k z M)))) + + + (1r + - ind> (toℕ z) (toℕ z₁)) · + (M l z · MF (toℕ k +ℕ toℕ z) · + (MF (toℕ (predFin l) +ℕ toℕ z₁) · minor k z M (predFin l) z₁ · + det (minor (predFin l) z₁ (minor k z M))))) + (λ i j → + DetRowAux2 + (ind> (toℕ i) (toℕ j)) + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M)))) + ) + ⟩ + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M)))) + + + (1r + - ind> (toℕ i) (toℕ j)) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M)))))) + ≡⟨ + ∑∑Split + (λ i j → ind> (toℕ i) (toℕ j) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M))))) + (λ i j → (1r + - ind> (toℕ i) (toℕ j)) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M))))) + ⟩ + (∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M)))))) + + + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ i) (toℕ j)) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M))))))) + ≡⟨ +Compat refl (∑∑ShiftWeak λ i j → + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M))))) ⟩ + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M)))))) + + + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) · + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l) +ℕ toℕ j) · + minor k (weakenFin i) M (predFin l) j + · det (minor (predFin l) j (minor k (weakenFin i) M)))))) + ≡⟨ +Compat refl + (∑∑Compat + (λ i j → + (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) · + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l) +ℕ toℕ j) · + minor k (weakenFin i) M (predFin l) j + · det (minor (predFin l) j (minor k (weakenFin i) M))))) + (λ z z₁ → + (1r + - ind> (toℕ z) (toℕ z₁)) · + (M l (weakenFin z) · MF (toℕ k +ℕ toℕ (weakenFin z)) · + (MF (toℕ (predFin l) +ℕ toℕ z₁) · + minor k (weakenFin z) M (predFin l) z₁ + · det (minor (predFin l) z₁ (minor k (weakenFin z) M))))) + (λ i j → + cong + (λ a → + (1r + - ind> a (toℕ j)) · + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l) +ℕ toℕ j) · + minor k (weakenFin i) M (predFin l) j + · det (minor (predFin l) j (minor k (weakenFin i) M))))) + (toℕweakenFin i)) + ) + ⟩ + (∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j · + det (minor (predFin l) j (minor k i M)))))) + + + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ i) (toℕ j)) · + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l) +ℕ toℕ j) · + minor k (weakenFin i) M (predFin l) j + · det (minor (predFin l) j (minor k (weakenFin i) M))))))) + ≡⟨ +Compat (adjugatePropAux1a M k l le) (adjugatePropAux1b M k l le) ⟩ + (∑ + (λ i → + ∑ + (λ z → + ind> (toℕ i) (toℕ z) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ z) · M l (weakenFin z)) + · det (minor (predFin l) z (minor k i M))))) + + + ∑ + (λ i → + ∑ + (λ z → + (1r + - ind> (toℕ i) (toℕ z)) · + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc z))) · M l (suc z) · + det (minor (predFin l) i (minor k (suc z) M))))))) + ≡⟨ +Compat + refl + (∑Comm + (λ i z → + (1r + - ind> (toℕ i) (toℕ z)) · + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc z))) · M l (suc z) · + det (minor (predFin l) i (minor k (suc z) M)))))) ⟩ + (∑ + (λ i → + ∑ + (λ z → + ind> (toℕ i) (toℕ z) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ z) · M l (weakenFin z)) + · det (minor (predFin l) z (minor k i M))))) + + + ∑ + (λ j → + ∑ + (λ i → + (1r + - ind> (toℕ i) (toℕ j)) · + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc j))) · M l (suc j) · + det (minor (predFin l) i (minor k (suc j) M))))))) + ≡⟨ +Compat refl + (∑∑Compat + (λ j i → + (1r + - ind> (toℕ i) (toℕ j)) · + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc j))) · M l (suc j) · + det (minor (predFin l) i (minor k (suc j) M))))) + (λ z z₁ → + ind> (suc (toℕ z)) (toℕ z₁) · + (M l (weakenFin z₁) · MF (toℕ k +ℕ toℕ (weakenFin z₁)) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc z))) · M l (suc z) · + det (minor (predFin l) z₁ (minor k (suc z) M))))) + (λ j i → + cong + (λ a → a · + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc j))) · M l (suc j) · + det (minor (predFin l) i (minor k (suc j) M))))) + (sym (ind>Suc (toℕ j) (toℕ i))) + )) ⟩ + (∑ + (λ i → + ∑ + (λ z → + ind> (toℕ i) (toℕ z) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ z) · M l (weakenFin z)) + · det (minor (predFin l) z (minor k i M))))) + + + ∑ + (λ i → + ∑ + (λ z → + ind> (suc (toℕ i)) (toℕ z) · + (M l (weakenFin z) · MF (toℕ k +ℕ toℕ (weakenFin z)) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc i))) · M l (suc i) · + det (minor (predFin l) z (minor k (suc i) M))))))) + ≡⟨ +Compat refl + (sym (∑∑ShiftSuc + (λ i z → + (M l (weakenFin z) · MF (toℕ k +ℕ toℕ (weakenFin z)) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i · + det (minor (predFin l) z (minor k i M))))))) ⟩ + (∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (predFin l) +ℕ toℕ j) · M l (weakenFin j)) + · det (minor (predFin l) j (minor k i M))))) + + + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · MF (toℕ k +ℕ toℕ (weakenFin j)) · + (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i · + det (minor (predFin l) j (minor k i M))))))) + ≡⟨ +Compat + (adjugatePropAux2a M k l le) + (adjugatePropAux2b M k l le) ⟩ + (∑ + (λ i → + ∑ + (λ z → + 1r · + (ind> (toℕ i) (toℕ z) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ z) · M l (weakenFin z) · + det (minor (predFin l) z (minor k i M))))))) + + + ∑ + (λ i → + ∑ + (λ z → + - 1r · + (ind> (toℕ i) (toℕ z) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ z) · M l (weakenFin z) · + det (minor (predFin l) z (minor k i M)))))))) + ≡⟨ sym + (∑∑Split + (λ i z → + 1r · + (ind> (toℕ i) (toℕ z) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ z) · M l (weakenFin z) · + det (minor (predFin l) z (minor k i M)))))) + λ i z → + - 1r · + (ind> (toℕ i) (toℕ z) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ z) · M l (weakenFin z) · + det (minor (predFin l) z (minor k i M)))))) + ⟩ + ∑ + (λ i → + ∑ + (λ j → + 1r · + (ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) · + det (minor (predFin l) j (minor k i M))))) + + + - 1r · + (ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) · + det (minor (predFin l) j (minor k i M))))))) + ≡⟨ ∑∑Compat + (λ i j → + 1r · + (ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) · + det (minor (predFin l) j (minor k i M))))) + + + - 1r · + (ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) · + det (minor (predFin l) j (minor k i M)))))) + (λ i j → 0r) + (λ i j → + (1r · + (ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) · + det (minor (predFin l) j (minor k i M))))) + + + - 1r · + (ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) · + det (minor (predFin l) j (minor k i M)))))) + ≡⟨ sym (·DistL+ 1r (- 1r) (ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) · + det (minor (predFin l) j (minor k i M)))))) ⟩ + ((1r + - 1r) · + (ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) · + det (minor (predFin l) j (minor k i M)))))) + ≡⟨ cong + (λ a → a · (ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) · + det (minor (predFin l) j (minor k i M)))))) + (+InvR 1r) + ⟩ + (0r · + (ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) · + det (minor (predFin l) j (minor k i M)))))) + ≡⟨ RingTheory.0LeftAnnihilates (CommRing→Ring P') (ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) · + det (minor (predFin l) j (minor k i M))))) ⟩ + 0r + ∎) + ⟩ + ∑ (λ (i : Fin (suc (suc n))) → ∑ (λ (j : Fin (suc n)) → 0r)) + ≡⟨ ∑Compat + (λ (i : Fin (suc (suc n))) → ∑ (λ (j : Fin (suc n)) → 0r)) + (λ (i : Fin (suc (suc n))) → 0r) + (λ (i : Fin (suc (suc n))) → ∑Zero {suc n} (λ (i : Fin (suc n)) → 0r) (λ (i : Fin (suc n)) → refl)) ⟩ + ∑ (λ (i : Fin (suc (suc n))) → 0r) + ≡⟨ ∑Zero (λ (i : Fin (suc (suc n))) → 0r) (λ (i : Fin (suc (suc n))) → refl) ⟩ + 0r + ∎ + + adjugateInvRGcomponent : {n : ℕ} → (M : FinMatrix R n n) → (k l : Fin n) → toℕ l <' toℕ k → (M ⋆ adjugate M) k l ≡ (det M ∘ 𝟙) k l + adjugateInvRGcomponent {suc n} M k l le = + ∑ (λ i → M k i · (MF(toℕ l +ℕ toℕ i) · det(minor l i M)) ) + ≡⟨ adjugatePropRG M l k le ⟩ + 0r + ≡⟨ sym (RingTheory.0RightAnnihilates (CommRing→Ring P') (det M)) ⟩ + det M · 0r + ≡⟨ cong (λ a → det M · a) (sym (deltaPropSym k l le)) ⟩ + (det M ∘ 𝟙) k l + ∎ + + strongenFin : {n : ℕ} {j : Fin (suc n)} → (i : Fin (suc n)) → toℕ i <' toℕ j → Fin n + strongenFin {zero} {zero} i () + strongenFin {zero} {suc ()} i le + strongenFin {suc n} {suc j} zero le = zero + strongenFin {suc n} {suc j} (suc i) (s≤s le) = suc (strongenFin {n} {j} i le) + + strongenFinLeId : {n : ℕ} {j : Fin (suc n)} → (i : Fin (suc n)) → (le : toℕ i <' toℕ j) → + toℕ (strongenFin i le) <' toℕ j + strongenFinLeId {zero} {zero} zero () + strongenFinLeId {zero} {suc ()} i le + strongenFinLeId {suc n} {suc j} zero (s≤s z≤) = s≤s z≤ + strongenFinLeId {suc n} {suc j} (suc i) (s≤s le) = s≤s (strongenFinLeId {n} {j} i le) + + weakenStrongenFin : {n : ℕ} {j : Fin (suc n)} → (i : Fin (suc n)) → (le : toℕ i <' toℕ j) → + weakenFin (strongenFin i le) ≡ i + weakenStrongenFin {zero} {zero} i () + weakenStrongenFin {zero} {suc ()} zero le + weakenStrongenFin {suc n} {suc j} zero le = refl + weakenStrongenFin {suc n} {suc j} (suc i) (s≤s le) = + cong + (λ a → suc a) + (weakenStrongenFin {n} {j} i le) + + toℕstrongenFin : {n : ℕ} {j : Fin (suc n)} → (i : Fin (suc n)) → (le : toℕ i <' toℕ j) → + toℕ (strongenFin i le) ≡ toℕ i + toℕstrongenFin {zero} {zero} i () + toℕstrongenFin {zero} {suc ()} i (le) + toℕstrongenFin {suc n} {suc j} zero le = refl + toℕstrongenFin {suc n} {suc j} (suc i) (s≤s le) = + cong (λ a → suc a) (toℕstrongenFin {n} {j} i le) + + + adjugatePropAux3a : {n : ℕ} → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → (k l : Fin (suc (suc n))) → (le : toℕ l <' toℕ k) → + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M)))))) + ≡ + ∑ + (λ i → + ∑ + (λ z → + ind> (toℕ i) (toℕ z) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ l) · MF (toℕ z) · M l (weakenFin z) · + det (minor (strongenFin l le) z (minor k i M)))))) + adjugatePropAux3a M k l le = + ∑∑Compat + (λ i j → + ind> (toℕ i) (toℕ j) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M))))) + (λ z z₁ → + ind> (toℕ z) (toℕ z₁) · + (M l z · (MF (toℕ k) · MF (toℕ z)) · + (MF (toℕ l) · MF (toℕ z₁) · M l (weakenFin z₁) · + det (minor (strongenFin l le) z₁ (minor k z M))))) + (ind>prop + (λ i j → + M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M)))) + (λ z z₁ → + M l z · (MF (toℕ k) · MF (toℕ z)) · + (MF (toℕ l) · MF (toℕ z₁) · M l (weakenFin z₁) · + det (minor (strongenFin l le) z₁ (minor k z M)))) + (λ i j lf → + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M)))) + ≡⟨ + cong + (λ a → + M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · a + · det (minor (strongenFin l le) j (minor k i M)))) + (minorIdId + k + i + (strongenFin l le) + j + M + (strongenFinLeId l le) + lf) + ⟩ + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + M (weakenFin (strongenFin l le)) (weakenFin j) + · det (minor (strongenFin l le) j (minor k i M)))) + ≡⟨ + cong + (λ a → + M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + M a (weakenFin j) + · det (minor (strongenFin l le) j (minor k i M)))) + (weakenStrongenFin l le) + ⟩ + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · M l (weakenFin j) · + det (minor (strongenFin l le) j (minor k i M)))) + ≡⟨ + cong + (λ a → M l i · a · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · M l (weakenFin j) · + det (minor (strongenFin l le) j (minor k i M)))) + (sumMF (toℕ k) (toℕ i)) + ⟩ + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · M l (weakenFin j) · + det (minor (strongenFin l le) j (minor k i M)))) + ≡⟨ + cong + (λ a → + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (a · M l (weakenFin j) · + det (minor (strongenFin l le) j (minor k i M))))) + (sumMF (toℕ (strongenFin l le)) (toℕ j)) + ⟩ + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ (strongenFin l le)) · MF (toℕ j) · M l (weakenFin j) · + det (minor (strongenFin l le) j (minor k i M)))) + ≡⟨ + cong + (λ a → M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF a · MF (toℕ j) · M l (weakenFin j) · + det (minor (strongenFin l le) j (minor k i M)))) + (toℕstrongenFin l le) + ⟩ + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ l) · MF (toℕ j) · M l (weakenFin j) · + det (minor (strongenFin l le) j (minor k i M)))) + ∎) + ) + + adjugatePropAux3b : {n : ℕ} → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → (k l : Fin (suc (suc n))) → (le : toℕ l <' toℕ k) → + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) · + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k (weakenFin i) M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k (weakenFin i) M)))))) + ≡ + ∑ + (λ i → + ∑ + (λ z → + ind> (suc (toℕ z)) (toℕ i) · + (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) · + (MF (toℕ l) · (- 1r · MF (suc (toℕ z))) · M l (suc z) · + det (minor (strongenFin l le) i (minor k (suc z) M)))))) + adjugatePropAux3b M k l le = + ∑∑Compat + (λ i j → + (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) · + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k (weakenFin i) M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k (weakenFin i) M))))) + (λ z z₁ → + ind> (suc (toℕ z₁)) (toℕ z) · + (M l (weakenFin z) · (MF (toℕ k) · MF (toℕ (weakenFin z))) · + (MF (toℕ l) · (- 1r · MF (suc (toℕ z₁))) · M l (suc z₁) · + det (minor (strongenFin l le) z (minor k (suc z₁) M))))) + (λ i j → + (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) · + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k (weakenFin i) M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k (weakenFin i) M)))) + ≡⟨ cong + (λ a → (1r + - ind> a (toℕ j)) · + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k (weakenFin i) M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k (weakenFin i) M))))) + (toℕweakenFin i) ⟩ + (1r + - ind> (toℕ i) (toℕ j)) · + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k (weakenFin i) M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k (weakenFin i) M)))) + ≡⟨ + ind>anti + (λ i j → M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k (weakenFin i) M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k (weakenFin i) M)))) + (λ z z₁ → + M l (weakenFin z) · (MF (toℕ k) · MF (toℕ (weakenFin z))) · + (MF (toℕ l) · (- 1r · MF (suc (toℕ z₁))) · M l (suc z₁) · + det (minor (strongenFin l le) z (minor k (suc z₁) M)))) + (λ i j lf → + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k (weakenFin i) M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k (weakenFin i) M)))) + ≡⟨ + cong + (λ a → + M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · a + · det (minor (strongenFin l le) j (minor k (weakenFin i) M)))) + (minorIdSuc + k + (weakenFin i) + (strongenFin l le) + j + M + (strongenFinLeId l le) + (weakenweakenFinLe i j lf)) + ⟩ + M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + M (weakenFin (strongenFin l le)) (suc j) + · det (minor (strongenFin l le) j (minor k (weakenFin i) M))) + ≡⟨ + cong + (λ a → + M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + M (weakenFin (strongenFin l le)) (suc j) · a)) + (detComp + (minor (strongenFin l le) j (minor k (weakenFin i) M)) + (minor (strongenFin l le) i (minor k (suc j) M)) + (λ i₁ j₁ → sym + (minorSemiCommR k (strongenFin l le) j i i₁ j₁ M lf) ) + ) + ⟩ + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + M (weakenFin (strongenFin l le)) (suc j) + · det (minor (strongenFin l le) i (minor k (suc j) M)))) + ≡⟨ + cong + (λ a → + M l (weakenFin i) · a · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + M (weakenFin (strongenFin l le)) (suc j) + · det (minor (strongenFin l le) i (minor k (suc j) M)))) + (sumMF (toℕ k) (toℕ (weakenFin i))) + ⟩ + (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + M (weakenFin (strongenFin l le)) (suc j) + · det (minor (strongenFin l le) i (minor k (suc j) M)))) + ≡⟨ cong + (λ a → M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) · + (a · M (weakenFin (strongenFin l le)) (suc j) + · det (minor (strongenFin l le) i (minor k (suc j) M)))) + (sumMF (toℕ (strongenFin l le)) (toℕ j)) + ⟩ + (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) · + (MF (toℕ (strongenFin l le)) · MF (toℕ j) · + M (weakenFin (strongenFin l le)) (suc j) + · det (minor (strongenFin l le) i (minor k (suc j) M)))) + ≡⟨ + cong + (λ a → + M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) · + (MF a · MF (toℕ j) · + M (weakenFin (strongenFin l le)) (suc j) + · det (minor (strongenFin l le) i (minor k (suc j) M)))) + (toℕstrongenFin l le) + ⟩ + (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) · + (MF (toℕ l) · MF (toℕ j) · M (weakenFin (strongenFin l le)) (suc j) + · det (minor (strongenFin l le) i (minor k (suc j) M)))) + ≡⟨ + cong + (λ a → + M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) · + (MF (toℕ l) · a · M (weakenFin (strongenFin l le)) (suc j) + · det (minor (strongenFin l le) i (minor k (suc j) M)))) + (sucMFRev (toℕ j)) + ⟩ + (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) · + (MF (toℕ l) · (- 1r · MF (suc (toℕ j))) · + M (weakenFin (strongenFin l le)) (suc j) + · det (minor (strongenFin l le) i (minor k (suc j) M)))) + ≡⟨ cong + (λ a → + M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) · + (MF (toℕ l) · (- 1r · MF (suc (toℕ j))) · + M a (suc j) + · det (minor (strongenFin l le) i (minor k (suc j) M)))) + (weakenStrongenFin l le) + ⟩ + (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) · + (MF (toℕ l) · (- 1r · MF (suc (toℕ j))) · M l (suc j) · + det (minor (strongenFin l le) i (minor k (suc j) M)))) + ∎) + i + j + ⟩ + (1r + - ind> (toℕ i) (toℕ j)) · + (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) · + (MF (toℕ l) · (- 1r · MF (suc (toℕ j))) · M l (suc j) · + det (minor (strongenFin l le) i (minor k (suc j) M)))) + ≡⟨ + cong + (λ a → + a · + (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) · + (MF (toℕ l) · (- 1r · MF (suc (toℕ j))) · M l (suc j) · + det (minor (strongenFin l le) i (minor k (suc j) M))))) + (sym (ind>Suc (toℕ j) (toℕ i))) + ⟩ + (ind> (suc (toℕ j)) (toℕ i) · + (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) · + (MF (toℕ l) · (- 1r · MF (suc (toℕ j))) · M l (suc j) · + det (minor (strongenFin l le) i (minor k (suc j) M))))) + ∎) + + adjugatePropAux4a : {n : ℕ} → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + (k l : Fin (suc (suc n))) → (le : toℕ l <' toℕ k) → + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ l) · MF (toℕ j) · M l (weakenFin j) · + det (minor (strongenFin l le) j (minor k i M)))))) + ≡ + ∑ + (λ i → + ∑ + (λ z → + ind> (toℕ i) (toℕ z) · + (1r · + (M l i · (MF (toℕ k) · MF (toℕ z)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin z))) + · det (minor (strongenFin l le) z (minor k i M))))) + adjugatePropAux4a M k l le = + ∑∑Compat + (λ i j → + ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ l) · MF (toℕ j) · M l (weakenFin j) · + det (minor (strongenFin l le) j (minor k i M))))) + (λ z z₁ → + ind> (toℕ z) (toℕ z₁) · + (1r · + (M l z · (MF (toℕ k) · MF (toℕ z₁)) · + (MF (toℕ l) · MF (toℕ z) · M l (weakenFin z₁))) + · det (minor (strongenFin l le) z₁ (minor k z M)))) + (λ i j → + (ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ l) · MF (toℕ j) · M l (weakenFin j) · + det (minor (strongenFin l le) j (minor k i M))))) + ≡⟨ + cong + (λ a → + ind> (toℕ i) (toℕ j) · a) + (·Assoc _ _ _) + ⟩ + (ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ l) · MF (toℕ j) · M l (weakenFin j)) + · det (minor (strongenFin l le) j (minor k i M)))) + ≡⟨ + cong + (λ a → + ind> (toℕ i) (toℕ j) · + (a · det (minor (strongenFin l le) j (minor k i M)))) + (solve! P') + ⟩ + (ind> (toℕ i) (toℕ j) · + ( 1r · + ( M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))) · + det (minor (strongenFin l le) j (minor k i M)))) + ∎) + + adjugatePropAux4b : {n : ℕ} → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + (k l : Fin (suc (suc n))) → (le : toℕ l <' toℕ k) → + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · (MF (toℕ k) · MF (toℕ (weakenFin j))) · + (MF (toℕ l) · (- 1r · MF (toℕ i)) · M l i · + det (minor (strongenFin l le) j (minor k i M)))))) + ≡ + ∑ + (λ i → + ∑ + (λ z → + ind> (toℕ i) (toℕ z) · + (- 1r · + (M l i · (MF (toℕ k) · MF (toℕ z)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin z))) + · det (minor (strongenFin l le) z (minor k i M))))) + adjugatePropAux4b M k l le = + ∑∑Compat + (λ i j → + ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · (MF (toℕ k) · MF (toℕ (weakenFin j))) · + (MF (toℕ l) · (- 1r · MF (toℕ i)) · M l i · + det (minor (strongenFin l le) j (minor k i M))))) + (λ z z₁ → + ind> (toℕ z) (toℕ z₁) · + (- 1r · + (M l z · (MF (toℕ k) · MF (toℕ z₁)) · + (MF (toℕ l) · MF (toℕ z) · M l (weakenFin z₁))) + · det (minor (strongenFin l le) z₁ (minor k z M)))) + (λ i j → + (ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · (MF (toℕ k) · MF (toℕ (weakenFin j))) · + (MF (toℕ l) · (- 1r · MF (toℕ i)) · M l i · + det (minor (strongenFin l le) j (minor k i M))))) + ≡⟨ + cong + (λ a → + ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · (MF (toℕ k) · MF a) · + (MF (toℕ l) · (- 1r · MF (toℕ i)) · M l i · + det (minor (strongenFin l le) j (minor k i M))))) + (toℕweakenFin j) + ⟩ + ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · (- 1r · MF (toℕ i)) · M l i · + det (minor (strongenFin l le) j (minor k i M)))) + ≡⟨ cong + (λ a → ind> (toℕ i) (toℕ j) · a) + (·Assoc _ _ _) + ⟩ + ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · (- 1r · MF (toℕ i)) · M l i) + · det (minor (strongenFin l le) j (minor k i M))) + ≡⟨ + cong + (λ a → ind> (toℕ i) (toℕ j) · (a + · det (minor (strongenFin l le) j (minor k i M)))) + (solve! P') + ⟩ + ind> (toℕ i) (toℕ j) · + ((- 1r) ·( M l (weakenFin j) · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l i)) + · det (minor (strongenFin l le) j (minor k i M))) + ≡⟨ cong + (λ a → ind> (toℕ i) (toℕ j) · + ((- 1r) · a + · det (minor (strongenFin l le) j (minor k i M)))) + (solve! P') + ⟩ + ind> (toℕ i) (toℕ j) · + ((- 1r) · + ( M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))) · + det (minor (strongenFin l le) j (minor k i M))) + ∎) + + adjugatePropRL : {n : ℕ} → (M : FinMatrix R (suc n) (suc n)) → (k l : Fin (suc n)) → toℕ l <' toℕ k → + ∑ (λ i → (M l i · (MF (toℕ k +ℕ toℕ i) · det (minor k i M)))) ≡ 0r + adjugatePropRL {zero} M zero zero () + adjugatePropRL {zero} M (suc ()) zero (s≤s le) + adjugatePropRL {suc n} M k l le = + ∑ (λ i → M l i · (MF (toℕ k +ℕ toℕ i) · det (minor k i M))) + ≡⟨ ∑Compat + (λ i → M l i · (MF (toℕ k +ℕ toℕ i) · det (minor k i M))) + (λ i → M l i · MF (toℕ k +ℕ toℕ i) · det (minor k i M)) + (λ i → ·Assoc _ _ _) + ⟩ + ∑ (λ i → M l i · MF (toℕ k +ℕ toℕ i) · det (minor k i M)) + ≡⟨ ∑Compat + (λ i → M l i · MF (toℕ k +ℕ toℕ i) · det (minor k i M)) + (λ i → M l i · MF (toℕ k +ℕ toℕ i) · detR (strongenFin l le) (minor k i M)) + (λ i → + cong + (λ a → M l i · MF (toℕ k +ℕ toℕ i) · a) + (sym (DetRow (strongenFin l le) (minor k i M)))) ⟩ + ∑ + (λ i → + M l i · MF (toℕ k +ℕ toℕ i) · + detR (strongenFin l le) (minor k i M)) + ≡⟨ refl ⟩ + ∑ + (λ i → + M l i · MF (toℕ k +ℕ toℕ i) · + ∑ + (λ j → + MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M)))) + ≡⟨ ∑Compat + (λ i → + M l i · MF (toℕ k +ℕ toℕ i) · + ∑ + (λ j → + MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M)))) + (λ i → + ∑ + (λ j → M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M))))) + (λ i → + ∑DistR + (M l i · MF (toℕ k +ℕ toℕ i)) + ( (λ j → + MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M))))) + ⟩ + ∑ + (λ i → + ∑ + (λ j → + M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M))))) + ≡⟨ ∑∑Compat + (λ i j → + M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M)))) + (λ i j → + ind> (toℕ i) (toℕ j) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M)))) + + + (1r + - ind> (toℕ i) (toℕ j)) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M))))) + (λ i j → + DetRowAux2 + (ind> (toℕ i) (toℕ j)) + ( M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M)))) + ) + ⟩ + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M)))) + + + (1r + - ind> (toℕ i) (toℕ j)) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M)))))) + ≡⟨ ∑∑Split + (λ i j → + ind> (toℕ i) (toℕ j) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M))))) + (λ i j → + (1r + - ind> (toℕ i) (toℕ j)) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M))))) ⟩ + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M)))))) + + + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ i) (toℕ j)) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M)))))) + ≡⟨ +Compat refl (∑∑ShiftWeak (λ i j → + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M)))))) ⟩ + (∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (M l i · MF (toℕ k +ℕ toℕ i) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k i M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k i M)))))) + + + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) · + (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) · + (MF (toℕ (strongenFin l le) +ℕ toℕ j) · + minor k (weakenFin i) M (strongenFin l le) j + · det (minor (strongenFin l le) j (minor k (weakenFin i) M))))))) + ≡⟨ +Compat (adjugatePropAux3a M k l le) (adjugatePropAux3b M k l le) ⟩ + ∑ + (λ i → + ∑ + (λ z → + ind> (toℕ i) (toℕ z) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ l) · MF (toℕ z) · M l (weakenFin z) · + det (minor (strongenFin l le) z (minor k i M)))))) + + + ∑ + (λ i → + ∑ + (λ z → + ind> (suc (toℕ z)) (toℕ i) · + (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) · + (MF (toℕ l) · (- 1r · MF (suc (toℕ z))) · M l (suc z) · + det (minor (strongenFin l le) i (minor k (suc z) M)))))) + ≡⟨ +Compat + refl + (∑Comm (λ i z → + ind> (suc (toℕ z)) (toℕ i) · + (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) · + (MF (toℕ l) · (- 1r · MF (suc (toℕ z))) · M l (suc z) · + det (minor (strongenFin l le) i (minor k (suc z) M)))))) ⟩ + (∑ + (λ i → + ∑ + (λ z → + ind> (toℕ i) (toℕ z) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ l) · MF (toℕ z) · M l (weakenFin z) · + det (minor (strongenFin l le) z (minor k i M)))))) + + + ∑ + (λ j → + ∑ + (λ i → + ind> (suc (toℕ j)) (toℕ i) · + (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) · + (MF (toℕ l) · (- 1r · MF (suc (toℕ j))) · M l (suc j) · + det (minor (strongenFin l le) i (minor k (suc j) M))))))) + ≡⟨ + +Compat + refl + (sym + (∑∑ShiftSuc + λ j i → + (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) · + (MF (toℕ l) · (- 1r · MF (toℕ j)) · M l j · + det (minor (strongenFin l le) i (minor k j M)))))) + ⟩ + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (M l i · (MF (toℕ k) · MF (toℕ i)) · + (MF (toℕ l) · MF (toℕ j) · M l (weakenFin j) · + det (minor (strongenFin l le) j (minor k i M)))))) + + + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (M l (weakenFin j) · (MF (toℕ k) · MF (toℕ (weakenFin j))) · + (MF (toℕ l) · (- 1r · MF (toℕ i)) · M l i · + det (minor (strongenFin l le) j (minor k i M)))))) + ≡⟨ +Compat (adjugatePropAux4a M k l le) (adjugatePropAux4b M k l le) ⟩ + ∑ + (λ i → + ∑ + (λ z → + ind> (toℕ i) (toℕ z) · + (1r · + (M l i · (MF (toℕ k) · MF (toℕ z)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin z))) + · det (minor (strongenFin l le) z (minor k i M))))) + + + ∑ + (λ i → + ∑ + (λ z → + ind> (toℕ i) (toℕ z) · + (- 1r · + (M l i · (MF (toℕ k) · MF (toℕ z)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin z))) + · det (minor (strongenFin l le) z (minor k i M))))) + ≡⟨ + sym + (∑∑Split + (λ i z → + ind> (toℕ i) (toℕ z) · + (1r · + (M l i · (MF (toℕ k) · MF (toℕ z)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin z))) + · det (minor (strongenFin l le) z (minor k i M)))) + λ i z → + ind> (toℕ i) (toℕ z) · + (- 1r · + (M l i · (MF (toℕ k) · MF (toℕ z)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin z))) + · det (minor (strongenFin l le) z (minor k i M)))) + ⟩ + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (1r · + (M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))) + · det (minor (strongenFin l le) j (minor k i M))) + + + ind> (toℕ i) (toℕ j) · + (- 1r · + (M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))) + · det (minor (strongenFin l le) j (minor k i M))))) + ≡⟨ + ∑∑Compat + (λ i j → + ind> (toℕ i) (toℕ j) · + (1r · + (M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))) + · det (minor (strongenFin l le) j (minor k i M))) + + + ind> (toℕ i) (toℕ j) · + (- 1r · + (M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))) + · det (minor (strongenFin l le) j (minor k i M)))) + (λ _ _ → 0r) + (λ i j → + (ind> (toℕ i) (toℕ j) · + (1r · + (M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))) + · det (minor (strongenFin l le) j (minor k i M))) + + + ind> (toℕ i) (toℕ j) · + (- 1r · + (M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))) + · det (minor (strongenFin l le) j (minor k i M)))) + ≡⟨ sym + (·DistR+ + (ind> (toℕ i) (toℕ j)) + (1r · + (M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))) + · det (minor (strongenFin l le) j (minor k i M))) + (- 1r · (M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))) + · det (minor (strongenFin l le) j (minor k i M)))) ⟩ + (ind> (toℕ i) (toℕ j) · + (1r · + (M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))) + · det (minor (strongenFin l le) j (minor k i M)) + + + - 1r · + (M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))) + · det (minor (strongenFin l le) j (minor k i M))) + ) + ≡⟨ + cong + (λ a → ind> (toℕ i) (toℕ j) · a) + (sym + (·DistL+ + (1r · + (M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j)))) + ( - 1r · + (M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j)))) + (det (minor (strongenFin l le) j (minor k i M))))) + ⟩ + (ind> (toℕ i) (toℕ j) · + ((1r · + (M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))) + + + - 1r · + (M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j)))) + · det (minor (strongenFin l le) j (minor k i M)))) + ≡⟨ + cong + (λ a → + ind> (toℕ i) (toℕ j) · (a · + det (minor (strongenFin l le) j (minor k i M)))) + (sym + (·DistL+ + 1r + (- 1r) + (M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))))) + ⟩ + (ind> (toℕ i) (toℕ j) · + ((1r + - 1r) · + (M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))) + · det (minor (strongenFin l le) j (minor k i M)))) + ≡⟨ cong + (λ a → (ind> (toℕ i) (toℕ j) · + (a · (M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))) + · det (minor (strongenFin l le) j (minor k i M))))) + (+InvR 1r) + ⟩ + (ind> (toℕ i) (toℕ j) · + (0r · + (M l i · (MF (toℕ k) · MF (toℕ j)) · + (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))) + · det (minor (strongenFin l le) j (minor k i M)))) + ≡⟨ + cong + (λ a → (ind> (toℕ i) (toℕ j) · + (a · det (minor (strongenFin l le) j (minor k i M))))) + (solve! P') + ⟩ + (ind> (toℕ i) (toℕ j) · + (0r · det (minor (strongenFin l le) j (minor k i M)))) + ≡⟨ cong + (λ a → ind> (toℕ i) (toℕ j) · a) + (RingTheory.0LeftAnnihilates + (CommRing→Ring P') + (det (minor (strongenFin l le) j (minor k i M)))) ⟩ + (ind> (toℕ i) (toℕ j) · 0r) + ≡⟨ solve! P' ⟩ + 0r + ∎)⟩ + ∑ (λ (i : Fin (suc (suc n))) → ∑ (λ (j : Fin (suc n)) → 0r)) + ≡⟨ ∑Zero + (λ (i : Fin (suc (suc n))) → ∑ (λ (j : Fin (suc n)) → 0r)) + (λ i → ∑Zero (λ (j : Fin (suc n)) → 0r) (λ (j : Fin (suc n)) → refl)) ⟩ + 0r + ∎ + + + + adjugateInvRLcomponent : {n : ℕ} → (M : FinMatrix R n n) → (k l : Fin n) → toℕ k <' toℕ l → (M ⋆ adjugate M) k l ≡ (det M ∘ 𝟙) k l + adjugateInvRLcomponent {suc n} M k l le = + ∑ (λ i → M k i · (MF(toℕ l +ℕ toℕ i) · det(minor l i M)) ) + ≡⟨ adjugatePropRL M l k le ⟩ + 0r + ≡⟨ sym (RingTheory.0RightAnnihilates (CommRing→Ring P') (det M)) ⟩ + det M · 0r + ≡⟨ cong (λ a → det M · a) (sym (deltaProp k l le)) ⟩ + (det M ∘ 𝟙) k l + ∎ + + FinCompare : {n : ℕ} → (k l : Fin n) → (k ≡ l) ⊎ ((toℕ k <' toℕ l) ⊎ (toℕ l <' toℕ k)) + FinCompare {zero} () () + FinCompare {suc n} zero zero = inl refl + FinCompare {suc n} zero (suc l) = inr (inl (s≤s z≤)) + FinCompare {suc n} (suc k) zero = inr (inr (s≤s z≤)) + FinCompare {suc n} (suc k) (suc l) with FinCompare {n} k l + ... | inl x = inl (cong (λ a → (suc a)) x) + ... | inr (inl x) = inr (inl (s≤s x)) + ... | inr (inr x) = inr (inr (s≤s x)) + + + adjugateInvRComp : {n : ℕ} → (M : FinMatrix R n n) → (k l : Fin n) → (M ⋆ adjugate M) k l ≡ (det M ∘ 𝟙) k l + adjugateInvRComp {zero} M () () + adjugateInvRComp {suc n} M k l with FinCompare k l + ... | inl x = + (∑ (λ i → M k i · (MF(toℕ l +ℕ toℕ i) · det(minor l i M)) ) + ≡⟨ + ∑Compat + (λ i → M k i · (MF(toℕ l +ℕ toℕ i) · det(minor l i M))) + (λ i → M k i · MF(toℕ l +ℕ toℕ i) · det(minor l i M)) + (λ i → ·Assoc _ _ _) + ⟩ + ∑ (λ i → M k i · MF (toℕ l +ℕ toℕ i) · det (minor l i M)) + ≡⟨ + ∑Compat + (λ i → M k i · MF (toℕ l +ℕ toℕ i) · det (minor l i M)) + (λ i → M l i · MF (toℕ l +ℕ toℕ i) · det (minor l i M)) + (λ i → cong + (λ a → M a i · MF (toℕ l +ℕ toℕ i) · det (minor l i M)) + x ) + ⟩ + ∑ (λ i → M l i · MF (toℕ l +ℕ toℕ i) · det (minor l i M)) + ≡⟨ ∑Compat + (λ i → M l i · MF (toℕ l +ℕ toℕ i) · det (minor l i M)) + (λ i → MF (toℕ l +ℕ toℕ i) · M l i · det (minor l i M)) + (λ i → cong + (λ a → a · det (minor l i M)) + (CommRingStr.·Comm (snd P') (M l i) (MF (toℕ l +ℕ toℕ i))) ) ⟩ + detR l M + ≡⟨ DetRow l M ⟩ + det M + ≡⟨ sym (·IdR (det M)) ⟩ + (det M · 1r) + ≡⟨ cong (λ a → det M · a) (sym (deltaPropEq k l x))⟩ + (det M ∘ 𝟙) k l + ∎) + ... | inr (inl x) = adjugateInvRLcomponent M k l x + ... | inr (inr x) = adjugateInvRGcomponent M k l x + + adjugateInvLComp : {n : ℕ} → (M : FinMatrix R n n) → (k l : Fin n) → (adjugate M ⋆ M) k l ≡ (det M ∘ 𝟙) k l + adjugateInvLComp M k l = + (adjugate M ⋆ M) k l + ≡⟨ refl ⟩ + ∑ (λ i → adjugate M k i · (M ᵗ) l i) + ≡⟨ + ∑Compat + (λ i → adjugate M k i · (M ᵗ) l i) + (λ i → adjugate (M ᵗ) i k · (M ᵗ) l i) + (λ i → cong (λ a → a · (M ᵗ) l i) (sym (adjugateTransp M i k))) + ⟩ + ∑ (λ i → adjugate (M ᵗ) i k · (M ᵗ) l i) + ≡⟨ + ∑Compat + (λ i → adjugate (M ᵗ) i k · (M ᵗ) l i) + (λ z → (snd P' CommRingStr.· (M ᵗ) l z) (adjugate (M ᵗ) z k)) + (λ i → CommRingStr.·Comm (snd P') (adjugate (M ᵗ) i k) ((M ᵗ) l i)) + ⟩ + ∑ (λ i → (M ᵗ) l i · adjugate (M ᵗ) i k ) + ≡⟨ adjugateInvRComp (M ᵗ) l k ⟩ + (det (M ᵗ) ∘ 𝟙) l k + ≡⟨ cong (λ a → (a ∘ 𝟙) l k) (sym (detTransp M)) ⟩ + det M · δ l k + ≡⟨ cong (λ a → det M · a) (deltaComm l k) ⟩ + (det M · 𝟙 k l) + ∎ + + + adjugateInvR : {n : ℕ} → (M : FinMatrix R n n) → M ⋆ adjugate M ≡ det M ∘ 𝟙 + adjugateInvR M = funExt₂ (λ k l → adjugateInvRComp M k l) + + adjugateInvL : {n : ℕ} → (M : FinMatrix R n n) → adjugate M ⋆ M ≡ det M ∘ 𝟙 + adjugateInvL M = funExt₂ (λ k l → adjugateInvLComp M k l) diff --git a/Cubical/Algebra/Determinat/det.agda b/Cubical/Algebra/Determinat/det.agda new file mode 100644 index 000000000..0ead56c92 --- /dev/null +++ b/Cubical/Algebra/Determinat/det.agda @@ -0,0 +1,2493 @@ +{-# OPTIONS --cubical #-} + +module det where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Algebra.Matrix +open import Cubical.Algebra.Matrix.CommRingCoefficient +open import Cubical.Data.Bool +open import Cubical.Foundations.Structure using (⟨_⟩) +open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ + ; +-comm to +ℕ-comm + ; +-assoc to +ℕ-assoc + ; ·-assoc to ·ℕ-assoc) +open import Cubical.Data.FinData +open import Cubical.Data.FinData.Order using (_<'Fin_; _≤'Fin_) +open import Cubical.Algebra.Ring +open import Cubical.Algebra.Ring.Base +open import Cubical.Algebra.Ring.BigOps +open import Cubical.Algebra.Monoid.BigOp +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommRing.Base +open import Cubical.Algebra.Semiring +open import Cubical.Data.Int.Base using (pos; negsuc) +open import Cubical.Data.Vec.Base using (_∷_; []) +open import Cubical.Data.Nat.Order +open import Cubical.Tactics.CommRingSolver +open import Minor +open import RingSum + +module Determinat (ℓ : Level) (P' : CommRing ℓ) where + + open Minor.Minor ℓ + open RingSum.RingSum ℓ P' + open RingStr (snd (CommRing→Ring P')) renaming ( is-set to isSetR ) + + CommRingR' : CommRingStr (R' .fst) + CommRingR' = commringstr 0r 1r _+_ _·_ -_ (CommRingStr.isCommRing (snd P')) + + -- Definition of the minor factor + MF : (i : ℕ) → R + MF zero = 1r + MF (suc i) = (- 1r) · (MF i) + + --Multiplicity of the minor factor + sumMF : (i j : ℕ) → MF (i +ℕ j) ≡ (MF i) · (MF j) + sumMF zero j = + MF j + ≡⟨ sym (·IdL (MF j)) ⟩ + 1r · (MF j) + ≡⟨ refl ⟩ + (MF zero) · (MF j)∎ + sumMF (suc i) j = + MF (suc i +ℕ j) + ≡⟨ refl ⟩ + ((- 1r) · (MF (i +ℕ j))) + ≡⟨ cong (λ x → (- 1r) · x) (sumMF i j) ⟩ + ((- 1r) · ((MF i) · (MF j))) + ≡⟨ ·Assoc _ _ _ ⟩ + ((- 1r) · (MF i)) · (MF j) + ∎ + + sucMFRev : (i : ℕ) → MF i ≡ (- 1r) · MF (suc i) + sucMFRev i = solve! P' + + +Compat : {a b c d : R} → a ≡ b → c ≡ d → a + c ≡ b + d + +Compat {a} {b} {c} {d} eq1 eq2 = + a + c + ≡⟨ cong (λ x → x + c) eq1 ⟩ + b + c + ≡⟨ cong (λ x → b + x) eq2 ⟩ + b + d + ∎ + + -- Definition of the determinat by using Laplace expansion + det : ∀ {n} → FinMatrix R n n → R + det {zero} M = 1r + det {suc n} M = ∑ (λ j → (MF (toℕ j)) · (M zero j) · det {n} (minor zero j M)) + + detComp : {n : ℕ} → (M N : FinMatrix R n n) → ((i j : Fin n) → M i j ≡ N i j ) → det M ≡ det N + detComp {zero} M N f = refl + detComp {suc n} M N f = + ∑ (λ j → MF (toℕ j) · M zero j · det (minor zero j M)) + ≡⟨ ∑Compat (λ j → (MF (toℕ j)) · (M zero j) · det (minor zero j M)) + (λ j → (MF (toℕ j)) · (N zero j) · det (minor zero j M)) + (λ j → cong (λ a → (MF (toℕ j)) · a · det (minor zero j M)) (f zero j)) ⟩ + ∑ (λ j → MF (toℕ j) · N zero j · det (minor zero j M)) + ≡⟨ ∑Compat (λ j → (MF (toℕ j)) · (N zero j) · det (minor zero j M)) + (λ j → (MF (toℕ j)) · (N zero j) · det (minor zero j N)) + (λ j → cong (λ a → (MF (toℕ j)) · (N zero j) · a) (detComp (minor zero j M) (minor zero j N) (minorComp zero j M N f)) ) ⟩ + ∑ (λ j → MF (toℕ j) · N zero j · det (minor zero j N)) ∎ + + -- Independence of the row in the Laplace expansion. + detR : ∀ {n} → (k : Fin n) → FinMatrix R n n → R + detR {suc n} k M = ∑ (λ j → (MF ((toℕ k) +ℕ (toℕ j))) · (M k j) · det {n} (minor k j M)) + + DetRowAux1 : {n : ℕ} → + (k i : Fin (suc (suc n))) → + (j : Fin (suc n)) → + (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + MF ((toℕ k) +ℕ (toℕ i)) · M k i · + (MF (toℕ j) · minor k i M zero j · + det (minor zero j (minor k i M))) + ≡ + ( MF ((toℕ k) +ℕ (toℕ i) +ℕ (toℕ j)) · + M k i · minor k i M zero j · + det (minor zero j (minor k i M))) + DetRowAux1 k i j M = + (MF (toℕ k +ℕ toℕ i) · M k i · + (MF (toℕ j) · minor k i M zero j · + det (minor zero j (minor k i M)))) + ≡⟨ + ·Assoc + ( MF ((toℕ k) +ℕ (toℕ i)) · M k i) + (MF (toℕ j) · minor k i M zero j) + ( det (minor zero j (minor k i M))) + ⟩ + (MF (toℕ k +ℕ toℕ i) · M k i · (MF (toℕ j) · minor k i M zero j) · + det (minor zero j (minor k i M))) + ≡⟨ + cong + (λ x → (x · det (minor zero j (minor k i M)))) + (·Assoc + ( MF ((toℕ k) +ℕ (toℕ i)) · M k i) + (MF (toℕ j)) + ( minor k i M zero j)) + ⟩ + (MF (toℕ k +ℕ toℕ i) · M k i · MF (toℕ j) · minor k i M zero j · + det (minor zero j (minor k i M))) + ≡⟨ + cong + (λ x → x · minor k i M zero j · det (minor zero j (minor k i M))) + (sym (·Assoc (MF ((toℕ k) +ℕ (toℕ i))) ( M k i ) (MF (toℕ j)))) + ⟩ + (MF (toℕ k +ℕ toℕ i) · (M k i · MF (toℕ j)) · minor k i M zero j · + det (minor zero j (minor k i M))) + ≡⟨ + cong + ( λ x → + MF ((toℕ k) +ℕ (toℕ i)) · x · + minor k i M zero j · + det (minor zero j (minor k i M))) + (CommRingStr.·Comm CommRingR' (M k i) ( MF (toℕ j))) + ⟩ + MF (toℕ k +ℕ toℕ i) · (MF (toℕ j) · M k i) + · minor k i M zero j + · det (minor zero j (minor k i M)) + ≡⟨ + cong + (λ x → + x · minor k i M zero j · det (minor zero j (minor k i M))) + (·Assoc (MF ((toℕ k) +ℕ (toℕ i))) ( MF (toℕ j)) (M k i)) + ⟩ + (MF (toℕ k +ℕ toℕ i) · MF (toℕ j) · M k i · minor k i M zero j · + det (minor zero j (minor k i M))) + ≡⟨ + cong + (λ x → + x · M k i · minor k i M zero j + · det (minor zero j (minor k i M))) + (sym (sumMF (toℕ k +ℕ toℕ i) ( toℕ j))) + ⟩ + (MF (toℕ k +ℕ toℕ i +ℕ toℕ j) · M k i · minor k i M zero j · + det (minor zero j (minor k i M))) + ∎ + + DetRowAux2 : (a b : R) → b ≡ a · b + (1r + (- a)) · b + DetRowAux2 a b = solve! P' + + DetRowAux3a : + {n : ℕ} → (k : Fin (suc n)) → + (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + ∑ (λ (i : Fin (suc (suc n))) → + ∑ (λ (j : Fin (suc n)) → + ind> (toℕ i) (toℕ j) · + (MF (toℕ (suc k) +ℕ toℕ i +ℕ toℕ j) + · M (suc k) i · minor (suc k) i M zero j + · det (minor zero j (minor (suc k) i M))))) + ≡ + ∑ (λ (i : Fin (suc n)) → + ∑ (λ (j : Fin (suc n)) → + ind> (toℕ (suc i)) (toℕ j) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) + · M (suc k) (suc i) · minor (suc k) (suc i) M zero j + · det (minor zero j (minor (suc k) (suc i) M))))) + DetRowAux3a k M = + ∑∑ShiftSuc + (λ i j → + (MF (toℕ (suc k) +ℕ toℕ i +ℕ toℕ j) + · M (suc k) i · minor (suc k) i M zero j + · det (minor zero j (minor (suc k) i M)))) + + DetRowAux3b : {n : ℕ} → (k : Fin (suc n)) → + (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ (suc k) +ℕ toℕ i +ℕ toℕ j) · M (suc k) i · + minor (suc k) i M zero j + · det (minor zero j (minor (suc k) i M))))) + ≡ + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · M (suc k) (weakenFin i) · + minor (suc k) (weakenFin i) M zero j + · det (minor zero j (minor (suc k) (weakenFin i) M))))) + DetRowAux3b k M = + ∑∑ShiftWeak + (λ i j → + (MF (toℕ (suc k) +ℕ toℕ i +ℕ toℕ j) + · M (suc k) i · minor (suc k) i M zero j + · det (minor zero j (minor (suc k) i M)))) + + DetRowAux4a : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + ∑ (λ i → + ∑ (λ j → + ind> (toℕ (suc i)) (toℕ j) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + minor (suc k) (suc i) M zero j + · det (minor zero j (minor (suc k) (suc i) M))))) + ≡ + ∑ (λ i → + ∑ (λ j → + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero (weakenFin j) + · det (minor k i (minor zero (weakenFin j) M))))) + DetRowAux4a k M = + ∑∑Compat + (λ i j → + ind> (toℕ (suc i)) (toℕ j) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + minor (suc k) (suc i) M zero j + · det (minor zero j (minor (suc k) (suc i) M)))) + (λ i j → (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero (weakenFin j) + · det (minor k i (minor zero (weakenFin j) M)))) + λ i j → + ( + ind> (toℕ (suc i)) (toℕ j) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + minor (suc k) (suc i) M zero j + · det (minor zero j (minor (suc k) (suc i) M))) + ≡⟨ + cong + (λ a → + a ·(MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) + · M (suc k) (suc i) · minor (suc k) (suc i) M zero j + · det (minor zero j (minor (suc k) (suc i) M)))) + (ind>Suc (toℕ i) (toℕ j)) + ⟩ + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + minor (suc k) (suc i) M zero j + · det (minor zero j (minor (suc k) (suc i) M))) + ≡⟨ ind>anti + (λ j i → + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + minor (suc k) (suc i) M zero j + · det (minor zero j (minor (suc k) (suc i) M)))) + (λ j i → + MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero (weakenFin j) + · det (minor k i (minor zero (weakenFin j) M))) + (λ j i le → + ( + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + minor (suc k) (suc i) M zero j + · det (minor zero j (minor (suc k) (suc i) M))) + ≡⟨ + cong + (λ a → + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) + · M (suc k) (suc i) + · a + · det (minor zero j (minor (suc k) (suc i) M)))) + (minorIdId (suc k) (suc i) zero j M (s≤s z≤) (s≤s le)) + ⟩ + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero (weakenFin j) + · det (minor zero j (minor (suc k) (suc i) M))) + ≡⟨ cong + (λ a → + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero (weakenFin j) · a)) + (detComp + (minor zero j (minor (suc k) (suc i) M)) + (minor k i (minor (weakenFin zero) (weakenFin j) M)) + λ i₁ j₁ → + minorComm0 k zero i j i₁ j₁ M z≤ le ) + ⟩ + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero (weakenFin j) + · det (minor k i (minor zero (weakenFin j) M))) + ∎ + ) + ) + j + i ⟩ + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero (weakenFin j) + · det (minor k i (minor zero (weakenFin j) M))) + ∎) + + toℕweakenFin : {n : ℕ} → (i : Fin n) → toℕ (weakenFin i) ≡ toℕ i + toℕweakenFin zero = refl + toℕweakenFin (suc i) = cong suc (toℕweakenFin i) + + weakenweakenFinLe : {n : ℕ} → (i : Fin (suc n)) → (j : Fin (suc n)) → toℕ i ≤' toℕ j → weakenFin i ≤'Fin weakenFin j + weakenweakenFinLe {zero} zero zero le = le + weakenweakenFinLe {suc n} zero zero le = le + weakenweakenFinLe {suc n} zero (suc j) le = z≤ + weakenweakenFinLe {suc n} (suc i) (suc j) (s≤s le) = s≤s (weakenweakenFinLe {n} i j le) + + DetRowAux4b : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · minor (suc k) (weakenFin i) M zero j + · det (minor zero j (minor (suc k) (weakenFin i) M))))) + ≡ + ∑ + (λ i → + ∑ + (λ j → + (ind> (suc (toℕ j)) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor k i (minor zero (suc j) M)))))) + DetRowAux4b k M = + ∑∑Compat + (λ i j → + (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · minor (suc k) (weakenFin i) M zero j + · det (minor zero j (minor (suc k) (weakenFin i) M)))) + (λ z z₁ → + ind> (suc (toℕ z₁)) (toℕ z) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin z) +ℕ toℕ z₁) · + M (suc k) (weakenFin z) + · M (weakenFin zero) (suc z₁) + · det (minor k z (minor zero (suc z₁) M)))) + λ i j → + (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · minor (suc k) (weakenFin i) M zero j + · det (minor zero j (minor (suc k) (weakenFin i) M))) + ≡⟨ + cong + (λ a → + (1r + - ind> a (toℕ j)) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · minor (suc k) (weakenFin i) M zero j + · det (minor zero j (minor (suc k) (weakenFin i) M)))) + (toℕweakenFin i) + ⟩ + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · minor (suc k) (weakenFin i) M zero j + · det (minor zero j (minor (suc k) (weakenFin i) M))) + ≡⟨ ind>anti + (λ i j → (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · minor (suc k) (weakenFin i) M zero j + · det (minor zero j (minor (suc k) (weakenFin i) M)))) + (λ i j → MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor k i (minor zero (suc j) M))) + (λ i j le → + ((MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · minor (suc k) (weakenFin i) M zero j + · det (minor zero j (minor (suc k) (weakenFin i) M)))) + ≡⟨ cong + (λ a → + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) · a + · det (minor zero j (minor (suc k) (weakenFin i) M)))) + (minorIdSuc + (suc k) + (weakenFin i) + zero + j + M + (s≤s z≤) + (weakenweakenFinLe i j le)) ⟩ + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor zero j (minor (suc k) (weakenFin i) M))) + ≡⟨ cong + (λ a → + MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) · a) + (detComp + (minor zero j (minor (suc k) (weakenFin i) M)) + (minor k i (minor zero (suc j) M)) + (λ i₁ j₁ → + minorComm1 k zero i j i₁ j₁ M z≤ le)) + ⟩ + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor k i (minor zero (suc j) M))) + ∎) + i + j ⟩ + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor k i (minor zero (suc j) M))) + ≡⟨ cong + (λ a → + a · (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor k i (minor zero (suc j) M)))) + (sym (ind>Suc (toℕ j) (toℕ i))) + ⟩ + (ind> (suc (toℕ j)) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor k i (minor zero (suc j) M)))) + ∎ + + + DetRowAux5a : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero (weakenFin j) + · det (minor k i (minor zero (weakenFin j) M))))) + ≡ + ∑ + (λ j → + ∑ + (λ i → + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero (weakenFin j) + · det (minor k i (minor zero (weakenFin j) M))))) + DetRowAux5a k M = ∑Comm λ i j → (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero (weakenFin j) + · det (minor k i (minor zero (weakenFin j) M))) + + DetRowAux5b : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + ∑ + (λ i → + ∑ + (λ j → + ind> (suc (toℕ j)) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor k i (minor zero (suc j) M))))) + ≡ + ∑ + (λ j → + ∑ + (λ i → + ind> (suc (toℕ j)) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor k i (minor zero (suc j) M))))) + DetRowAux5b k M = + ∑Comm (λ i j → + ind> (suc (toℕ j)) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor k i (minor zero (suc j) M)))) + + DetRowAux6a : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + ∑ + (λ j → + ∑ + (λ i → + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero (weakenFin j) + · det (minor k i (minor zero (weakenFin j) M))))) + ≡ + ∑ + (λ j → + ∑ + (λ i → + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero j + · det (minor k i (minor zero j M))))) + DetRowAux6a k M = + ∑ + (λ j → + ∑ + (λ i → + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero (weakenFin j) + · det (minor k i (minor zero (weakenFin j) M))))) + ≡⟨ ∑∑Compat + (λ j i → + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero (weakenFin j) + · det (minor k i (minor zero (weakenFin j) M)))) + (λ j i → + (1r + - ind> (toℕ (weakenFin j)) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ (weakenFin j)) · M (suc k) (suc i) · + M zero (weakenFin j) + · det (minor k i (minor zero (weakenFin j) M)))) + (λ j i → + cong (λ a → + (1r + - ind> a (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ a) · M (suc k) (suc i) · + M zero (weakenFin j) + · det (minor k i (minor zero (weakenFin j) M)))) + (sym (toℕweakenFin j))) + ⟩ + ∑ + (λ j → + ∑ + (λ i → + (1r + - ind> (toℕ (weakenFin j)) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ (weakenFin j)) · + M (suc k) (suc i) + · M zero (weakenFin j) + · det (minor k i (minor zero (weakenFin j) M))))) + ≡⟨ sym (∑∑ShiftWeak + λ j i → + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · + M (suc k) (suc i) + · M zero j + · det (minor k i (minor zero j M)))) ⟩ + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ (suc k) +ℕ toℕ (suc j) +ℕ toℕ i) · M (suc k) (suc j) · + M zero i + · det (minor k j (minor zero i M))))) + ∎ + + DetRowAux6bAux : {n : ℕ} → (k : Fin (suc n)) → (i j : Fin (suc n)) → + MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) + ≡ + MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ (suc j)) + DetRowAux6bAux k i j = + MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) + ≡⟨ sumMF (toℕ (suc k) +ℕ toℕ (weakenFin i)) (toℕ j) ⟩ + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i)) · MF (toℕ j)) + ≡⟨ cong + (λ a → + a · MF (toℕ j)) + (sumMF (toℕ (suc k)) (toℕ (weakenFin i))) + ⟩ + (MF (toℕ (suc k)) · MF (toℕ (weakenFin i)) · MF (toℕ j)) + ≡⟨ cong + (λ a → + MF (toℕ (suc k)) · (MF a ) · MF (toℕ j)) + (toℕweakenFin i) + ⟩ + (MF (toℕ (suc k)) · MF (toℕ i) · MF (toℕ j)) + ≡⟨ sym + (·Assoc + (MF (toℕ (suc k))) + (MF (toℕ i)) + (MF (toℕ j))) + ⟩ + (MF (toℕ (suc k)) · (MF (toℕ i) · MF (toℕ j))) + ≡⟨ cong + (λ a → + MF (toℕ (suc k)) · a) + (solve! P') ⟩ + MF (toℕ (suc k)) · (MF (toℕ (suc i)) · MF (toℕ (suc j))) + ≡⟨ + ·Assoc + (MF (toℕ (suc k))) + (MF (toℕ (suc i))) + (MF (toℕ (suc j))) + ⟩ + (MF (toℕ (suc k)) · MF (toℕ (suc i)) · MF (toℕ (suc j))) + ≡⟨ cong + (λ a → a · MF (toℕ (suc j))) + (sym (sumMF (toℕ (suc k)) (toℕ (suc i)))) + ⟩ + (MF (toℕ (suc k) +ℕ toℕ (suc i)) · MF (toℕ (suc j))) + ≡⟨ sym (sumMF (toℕ (suc k) +ℕ toℕ (suc i)) (toℕ (suc j))) ⟩ + MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ (suc j)) + ∎ + + DetRowAux6b : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + ∑ + (λ j → + ∑ + (λ i → + ind> (suc (toℕ j)) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor k i (minor zero (suc j) M))))) + ≡ + ∑ + (λ j → + ∑ + (λ i → + ind> (toℕ j) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (weakenFin i) + · M zero j + · det (minor k i (minor zero j M))))) + + DetRowAux6b k M = + ∑ + (λ i → + ∑ + (λ i₁ → + ind> (suc (toℕ i)) (toℕ i₁) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i₁) +ℕ toℕ i) · + M (suc k) (weakenFin i₁) + · M (weakenFin zero) (suc i) + · det (minor k i₁ (minor zero (suc i) M))))) + ≡⟨ ∑∑Compat + (λ j i → + ind> (suc (toℕ j)) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor k i (minor zero (suc j) M)))) + (λ j i → + ind> (suc (toℕ j)) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ (suc j)) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor k i (minor zero (suc j) M)))) + (λ j i → + (ind> (suc (toℕ j)) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor k i (minor zero (suc j) M)))) + ≡⟨ cong + (λ a → + ind> (suc (toℕ j)) (toℕ i) · + (a · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor k i (minor zero (suc j) M)))) + (DetRowAux6bAux k i j) + ⟩ + (ind> (suc (toℕ j)) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ (suc j)) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor k i (minor zero (suc j) M)))) + ∎) + ⟩ + ∑ + (λ j → + ∑ + (λ i → + ind> (suc (toℕ j)) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ (suc j)) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor k i (minor zero (suc j) M))))) + ≡⟨ sym (∑∑ShiftSuc λ j i → (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · M (weakenFin zero) j + · det (minor k i (minor zero j M)))) ⟩ + ∑ + (λ j → + ∑ + (λ i → + ind> (toℕ j) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · M zero j + · det (minor k i (minor zero j M))))) + ∎ + + weakenFinLe : {n : ℕ} → (i : Fin (suc (suc n))) → (j : Fin (suc n)) → toℕ i ≤' toℕ j → i ≤'Fin weakenFin j + weakenFinLe {zero} zero zero le = le + weakenFinLe {zero} one zero () + weakenFinLe {zero} one (suc ()) le + weakenFinLe {suc n} zero j le = z≤ + weakenFinLe {suc n} (suc i) (suc j) (s≤s le) = s≤s (weakenFinLe {n} i j le) + + DetRowAux7a : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + ∑ + (λ j → + ∑ + (λ i → + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero j + · det (minor k i (minor zero j M))))) + ≡ + ∑ + (λ j → + ∑ + (λ i → + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i · + M zero j + · det (minor k i (minor zero j M))))) + + DetRowAux7a k M = + ∑∑Compat + (λ j i → + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero j + · det (minor k i (minor zero j M)))) + (λ j i → + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i · + M zero j + · det (minor k i (minor zero j M)))) + (λ j i → + ind>anti + (λ j i → (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero j + · det (minor k i (minor zero j M)))) + (λ j i → (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i · + M zero j + · det (minor k i (minor zero j M)))) + (λ j i le → + cong + ( λ a → MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · a · + M zero j + · det (minor k i (minor zero j M))) + (sym (minorSucSuc zero j k i M z≤ (weakenFinLe j i le)))) + j + i) + + DetRowAux7b : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + ∑ + (λ j → + ∑ + (λ i → + ind> (toℕ j) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (weakenFin i) + · M zero j + · det (minor k i (minor zero j M))))) + ≡ + ∑ + (λ j → + ∑ + (λ i → + ind> (toℕ j) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i · + M zero j + · det (minor k i (minor zero j M))))) + DetRowAux7b k M = + ∑∑Compat + (λ j i → + ind> (toℕ j) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (weakenFin i) + · M zero j + · det (minor k i (minor zero j M)))) + (λ j i → + (ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i · + M zero j + · det (minor k i (minor zero j M)))) + (λ j i → + ind>prop + (λ j i → + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (weakenFin i) · + M zero j · det (minor k i (minor zero j M)))) + (λ j i → + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i · + M zero j + · det (minor k i (minor zero j M)))) + (λ j i le → + cong + (λ a → + MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · a · + M zero j · det (minor k i (minor zero j M))) + (sym (minorSucId zero j k i M z≤ le)) ) + j + i + ) + + DetRowAux8 : {n : ℕ} → (i : Fin (suc (suc n))) → (j k : Fin (suc n)) + → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + MF (toℕ (suc k) +ℕ toℕ (suc j) +ℕ toℕ i) · minor zero i M k j · M zero i · det (minor k j (minor zero i M)) + ≡ + MF (toℕ i) · M zero i · (MF (toℕ k +ℕ toℕ j) · minor zero i M k j · det (minor k j (minor zero i M))) + DetRowAux8 i j k M = + (MF (toℕ (suc k) +ℕ toℕ (suc j) +ℕ toℕ i) · minor zero i M k j · + M zero i + · det (minor k j (minor zero i M))) + ≡⟨ cong + (λ a → + a · minor zero i M k j · M zero i · det (minor k j (minor zero i M))) + (sumMF (toℕ (suc k) +ℕ toℕ (suc j)) ( toℕ i)) + ⟩ + (MF (toℕ (suc k) +ℕ toℕ (suc j)) · MF (toℕ i) · minor zero i M k j · + M zero i + · det (minor k j (minor zero i M))) + ≡⟨ cong + (λ a → a · MF (toℕ i) · minor zero i M k j · + M zero i + · det (minor k j (minor zero i M))) + (sumMF (toℕ (suc k)) (toℕ (suc j))) + ⟩ + (MF (toℕ (suc k)) · MF (toℕ (suc j)) · MF (toℕ i) · + minor zero i M k j + · M zero i + · det (minor k j (minor zero i M))) + ≡⟨ cong + (λ a → + a · MF (toℕ i) · + minor zero i M k j + · M zero i + · det (minor k j (minor zero i M))) + (solve! P') + ⟩ + MF (toℕ k) · MF (toℕ j) · MF (toℕ i) · + minor zero i M k j + · M zero i + · det (minor k j (minor zero i M)) + ≡⟨ cong + (λ a → + a · MF (toℕ i) · minor zero i M k j + · M zero i · det (minor k j (minor zero i M))) + (sym (sumMF (toℕ k) (toℕ j))) ⟩ + (MF (toℕ k +ℕ toℕ j) · MF (toℕ i) · minor zero i M k j · M zero i · + det (minor k j (minor zero i M))) + ≡⟨ cong + (λ a → a · det (minor k j (minor zero i M))) + (solve! P') + ⟩ + ( MF (toℕ i) · M zero i · MF (toℕ k +ℕ toℕ j) · minor zero i M k j · + det (minor k j (minor zero i M))) + ≡⟨ sym + (·Assoc + (MF (toℕ i) · M zero i · MF (toℕ k +ℕ toℕ j)) + (minor zero i M k j) + (det (minor k j (minor zero i M)))) + ⟩ + (MF (toℕ i) · M zero i · MF (toℕ k +ℕ toℕ j) · + (minor zero i M k j · det (minor k j (minor zero i M)))) + ≡⟨ sym (·Assoc (MF (toℕ i) · M zero i) (MF (toℕ k +ℕ toℕ j)) (minor zero i M k j · det (minor k j (minor zero i M)))) ⟩ + MF (toℕ i) · M zero i · (MF (toℕ k +ℕ toℕ j) · + (minor zero i M k j · det (minor k j (minor zero i M)))) + ≡⟨ cong + (λ a → MF (toℕ i) · M zero i · a) + (·Assoc (MF (toℕ k +ℕ toℕ j)) (minor zero i M k j) (det (minor k j (minor zero i M)))) ⟩ + (MF (toℕ i) · M zero i · (MF (toℕ k +ℕ toℕ j) · + minor zero i M k j · det (minor k j (minor zero i M)))) + ∎ + + + DetRow : ∀ {n} → (k : Fin n) → (M : FinMatrix R n n) → (detR k M) ≡ (det M) + DetRow {one} zero M = refl + DetRow {suc (suc n)} zero M = refl + DetRow {suc (suc n)} (suc k) M = + detR (suc k) M + ≡⟨ refl ⟩ + ∑ + (λ (i : Fin (suc (suc n))) → + MF (toℕ (suc k) +ℕ toℕ i) · M (suc k) i · det (minor (suc k) i M)) + ≡⟨ refl ⟩ + ∑ + (λ i → + MF (toℕ (suc k) +ℕ toℕ i) · M (suc k) i · + ∑ + (λ j → + MF (toℕ j) · minor (suc k) i M zero j · + det (minor zero j (minor (suc k) i M)))) + ≡⟨ ∑Compat (λ i → + MF (toℕ (suc k) +ℕ toℕ i) · M (suc k) i · + ∑ + (λ j → + MF (toℕ j) · minor (suc k) i M zero j · + det (minor zero j (minor (suc k) i M)))) + ((λ i → + ∑ + (λ j → + MF (toℕ (suc k) +ℕ toℕ i) · M (suc k) i · + (MF (toℕ j) · minor (suc k) i M zero j · + det (minor zero j (minor (suc k) i M)))))) + (λ i → ∑DistR ( MF (toℕ (suc k) +ℕ toℕ i) · M (suc k) i) + (λ j → + MF (toℕ j) · minor (suc k) i M zero j · + det (minor zero j (minor (suc k) i M))))⟩ + ∑ + (λ i → + ∑ + (λ j → + MF (toℕ (suc k) +ℕ toℕ i) · M (suc k) i · + (MF (toℕ j) · minor (suc k) i M zero j · + det (minor zero j (minor (suc k) i M))))) + ≡⟨ + ∑∑Compat + (λ i j → + MF (toℕ (suc k) +ℕ toℕ i) · M (suc k) i · + (MF (toℕ j) · minor (suc k) i M zero j · + det (minor zero j (minor (suc k) i M)))) + (λ i j → + MF (toℕ (suc k) +ℕ toℕ i +ℕ toℕ j) · M (suc k) i · + minor (suc k) i M zero j · + det (minor zero j (minor (suc k) i M))) + (λ i j → DetRowAux1 (suc k) i j M) + ⟩ + ∑ + (λ i → + ∑ + (λ j → + MF (toℕ (suc k) +ℕ toℕ i +ℕ toℕ j) · M (suc k) i · + minor (suc k) i M zero j + · det (minor zero j (minor (suc k) i M)))) + ≡⟨ ∑∑Compat + (λ i j → + MF (toℕ (suc k) +ℕ toℕ i +ℕ toℕ j) · M (suc k) i · + minor (suc k) i M zero j · det (minor zero j (minor (suc k) i M))) + (λ i j → + ind> (toℕ i) (toℕ j) · + (MF (toℕ (suc k) +ℕ toℕ i +ℕ toℕ j) · M (suc k) i · + minor (suc k) i M zero j + · det (minor zero j (minor (suc k) i M))) + + + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ (suc k) +ℕ toℕ i +ℕ toℕ j) · M (suc k) i · + minor (suc k) i M zero j + · det (minor zero j (minor (suc k) i M)))) + (λ i j → + DetRowAux2 (ind> (toℕ i) (toℕ j)) + (MF (toℕ (suc k) +ℕ toℕ i +ℕ toℕ j) · M (suc k) i · + minor (suc k) i M zero j · det (minor zero j (minor (suc k) i M)))) + ⟩ + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (MF (toℕ (suc k) +ℕ toℕ i +ℕ toℕ j) · M (suc k) i · + minor (suc k) i M zero j + · det (minor zero j (minor (suc k) i M))) + + + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ (suc k) +ℕ toℕ i +ℕ toℕ j) · M (suc k) i · + minor (suc k) i M zero j + · det (minor zero j (minor (suc k) i M))))) + ≡⟨ ∑∑Split + (λ i j → + ind> (toℕ i) (toℕ j) · + (MF (toℕ (suc k) +ℕ toℕ i +ℕ toℕ j) · M (suc k) i · + minor (suc k) i M zero j + · det (minor zero j (minor (suc k) i M)))) + (λ i j → + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ (suc k) +ℕ toℕ i +ℕ toℕ j) · M (suc k) i · + minor (suc k) i M zero j + · det (minor zero j (minor (suc k) i M)))) + ⟩ + (∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (MF (toℕ (suc k) +ℕ toℕ i +ℕ toℕ j) · M (suc k) i · + minor (suc k) i M zero j + · det (minor zero j (minor (suc k) i M))))) + + + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ (suc k) +ℕ toℕ i +ℕ toℕ j) · M (suc k) i · + minor (suc k) i M zero j + · det (minor zero j (minor (suc k) i M)))))) + ≡⟨ +Compat (DetRowAux3a k M) (DetRowAux3b k M) ⟩ + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ (suc i)) (toℕ j) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + minor (suc k) (suc i) M zero j + · det (minor zero j (minor (suc k) (suc i) M))))) + + + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · minor (suc k) (weakenFin i) M zero j + · det (minor zero j (minor (suc k) (weakenFin i) M))))) + ≡⟨ +Compat (DetRowAux4a k M) (DetRowAux4b k M) ⟩ + (∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero (weakenFin j) + · det (minor k i (minor zero (weakenFin j) M))))) + + + ∑ + (λ i → + ∑ + (λ j → + ind> (suc (toℕ j)) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor k i (minor zero (suc j) M)))))) + ≡⟨ +Compat (DetRowAux5a k M) (DetRowAux5b k M) ⟩ + (∑ + (λ j → + ∑ + (λ i → + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero (weakenFin j) + · det (minor k i (minor zero (weakenFin j) M))))) + + ∑ + (λ j → + ∑ + (λ i → + ind> (suc (toℕ j)) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · + M (suc k) (weakenFin i) + · M (weakenFin zero) (suc j) + · det (minor k i (minor zero (suc j) M)))))) + ≡⟨ +Compat (DetRowAux6a k M) (DetRowAux6b k M) ⟩ + ∑ + (λ j → + ∑ + (λ i → + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) · + M zero j + · det (minor k i (minor zero j M))))) + + + ∑ + (λ j → + ∑ + (λ i → + ind> (toℕ j) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (weakenFin i) + · M zero j + · det (minor k i (minor zero j M))))) + ≡⟨ +Compat (DetRowAux7a k M) (DetRowAux7b k M) ⟩ + (∑ + (λ j → + ∑ + (λ i → + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i · + M zero j + · det (minor k i (minor zero j M))))) + + + ∑ + (λ j → + ∑ + (λ i → + ind> (toℕ j) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i · + M zero j + · det (minor k i (minor zero j M)))))) + ≡⟨ +Comm _ _ ⟩ + ∑ + (λ j → + ∑ + (λ i → + ind> (toℕ j) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i · + M zero j + · det (minor k i (minor zero j M))))) + + + ∑ + (λ j → + ∑ + (λ i → + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i · + M zero j + · det (minor k i (minor zero j M))))) + ≡⟨ sym + (∑∑Split + (λ j i → + ind> (toℕ j) (toℕ i) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i · + M zero j + · det (minor k i (minor zero j M)))) + λ j i → (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i · + M zero j + · det (minor k i (minor zero j M))) + ) ⟩ + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (MF (toℕ (suc k) +ℕ toℕ (suc j) +ℕ toℕ i) · minor zero i M k j · + M zero i + · det (minor k j (minor zero i M))) + + + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ (suc k) +ℕ toℕ (suc j) +ℕ toℕ i) · minor zero i M k j · + M zero i + · det (minor k j (minor zero i M))))) + ≡⟨ + ∑∑Compat + (λ i j → + ( + ind> (toℕ i) (toℕ j) · + (MF (toℕ (suc k) +ℕ toℕ (suc j) +ℕ toℕ i) · minor zero i M k j · + M zero i + · det (minor k j (minor zero i M))) + + + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ (suc k) +ℕ toℕ (suc j) +ℕ toℕ i) · minor zero i M k j · + M zero i + · det (minor k j (minor zero i M))))) + (λ z z₁ → + MF (toℕ (suc k) +ℕ toℕ (suc z₁) +ℕ toℕ z) · minor zero z M k z₁ · + M zero z + · det (minor k z₁ (minor zero z M))) + (λ i j → + sym + (DetRowAux2 + (ind> (toℕ i) (toℕ j)) + (MF (toℕ (suc k) +ℕ toℕ (suc j) +ℕ toℕ i) · minor zero i M k j · + M zero i · det (minor k j (minor zero i M))))) + ⟩ + ∑ + (λ i → + ∑ + (λ j → + MF (toℕ (suc k) +ℕ toℕ (suc j) +ℕ toℕ i) · minor zero i M k j · + M zero i + · det (minor k j (minor zero i M)))) + ≡⟨ + ∑∑Compat + (λ i j → MF (toℕ (suc k) +ℕ toℕ (suc j) +ℕ toℕ i) · minor zero i M k j · + M zero i + · det (minor k j (minor zero i M))) + (λ z z₁ → + MF (toℕ z) · M zero z · + (MF (toℕ k +ℕ toℕ z₁) · minor zero z M k z₁ · + det (minor k z₁ (minor zero z M)))) + (λ i j → DetRowAux8 i j k M) + ⟩ + ∑ + (λ i → + ∑ + (λ j → + MF (toℕ i) · M zero i · (MF (toℕ k +ℕ toℕ j) · minor zero i M k j + · det (minor k j (minor zero i M))))) + ≡⟨ + ∑Compat + (λ i → + ∑ + (λ j → + MF (toℕ i) · M zero i · (MF (toℕ k +ℕ toℕ j) · minor zero i M k j + · det (minor k j (minor zero i M))))) + (λ i → + MF (toℕ i) · M zero i · + ∑ + (λ j → + MF (toℕ k +ℕ toℕ j) · minor zero i M k j + · det (minor k j (minor zero i M)))) + (λ i → sym + (∑DistR + ( MF (toℕ i) · M zero i) + (λ j → MF (toℕ k +ℕ toℕ j) · minor zero i M k j + · det (minor k j (minor zero i M))))) + ⟩ + ∑ + (λ i → + MF (toℕ i) · M zero i · + ∑ + (λ j → + MF (toℕ k +ℕ toℕ j) · minor zero i M k j + · det (minor k j (minor zero i M)))) + ≡⟨ ∑Compat + (λ i → + MF (toℕ i) · M zero i · + detR k (minor zero i M)) + (λ i → + MF (toℕ i) · M zero i · + det (minor zero i M)) + (λ i → + cong + (λ a → MF (toℕ i) · M zero i · a) + (DetRow k (minor zero i M))) + ⟩ + ∑ (λ i → MF (toℕ i) · M zero i · det (minor zero i M)) + ∎ + + --Laplace expansion along columns + + detC : ∀ {n} → (k : Fin n) → FinMatrix R n n → R + detC {suc n} k M = ∑ (λ i → (MF ((toℕ i) +ℕ (toℕ k))) · (M i k) · det {n} (minor i k M)) + + DetRowColumnAux : {n : ℕ} → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + ∑ + (λ i → + ∑ + (λ j → + MF (toℕ (suc i) +ℕ zero) · M (suc i) zero · + (MF (toℕ j) · minor (suc i) zero M zero j · + det (minor zero j (minor (suc i) zero M))))) + ≡ + ∑ + (λ i → + ∑ + (λ j → + MF (toℕ (suc j))· M zero (suc j) · + (MF (toℕ i +ℕ zero)· minor zero (suc j) M i zero · + det (minor i zero (minor zero (suc j) M))))) + + DetRowColumnAux M = + ∑∑Compat + (λ i j → + MF (toℕ (suc i) +ℕ zero) · M (suc i) zero · + (MF (toℕ j) · minor (suc i) zero M zero j · + det (minor zero j (minor (suc i) zero M)))) + (λ i j → + MF (toℕ (suc j))· M zero (suc j) · + (MF (toℕ i +ℕ zero)· minor zero (suc j) M i zero · + det (minor i zero (minor zero (suc j) M)))) + (λ i j → + (MF (toℕ (suc i) +ℕ zero) · M (suc i) zero · + (MF (toℕ j) · minor (suc i) zero M zero j · + det (minor zero j (minor (suc i) zero M)))) + ≡⟨ cong + (λ a → + MF (toℕ (suc i) +ℕ zero) · M (suc i) zero · + (MF (toℕ j) · a · + det (minor zero j (minor (suc i) zero M)))) + (minorIdSuc (suc i) zero zero j M (s≤s z≤) z≤) + ⟩ + (MF (toℕ (suc i) +ℕ zero) · M (suc i) zero · + (MF (toℕ j) · M zero (suc j) · + det (minor zero j (minor (suc i) zero M)))) + ≡⟨ + cong + (λ a → + MF (toℕ (suc i) +ℕ zero) · M (suc i) zero · + (MF (toℕ j) · M zero (suc j) · a)) + (detComp + (minor zero j (minor (suc i) zero M)) + (minor i zero (minor zero (suc j) M)) + (λ i₁ j₁ → (minorComm1 i zero zero j i₁ j₁ M z≤ z≤))) + ⟩ + (MF (toℕ (suc i) +ℕ zero) · M (suc i) zero · + (MF (toℕ j) · M zero (suc j) · + det (minor i zero (minor zero (suc j) M)))) + ≡⟨ ·Assoc (MF (toℕ (suc i) +ℕ zero) · M (suc i) zero) (MF (toℕ j) · M zero (suc j)) (det (minor i zero (minor zero (suc j) M))) ⟩ + MF (toℕ (suc i) +ℕ zero) · M (suc i) zero · (MF (toℕ j) · M zero (suc j)) · + det (minor i zero (minor zero (suc j) M)) + ≡⟨ + cong + (λ a → a · M (suc i) zero · + (MF (toℕ j) · M zero (suc j)) · + det (minor i zero (minor zero (suc j) M))) + (MF (toℕ (suc i) +ℕ zero) + ≡⟨ sumMF (toℕ (suc i)) zero ⟩ + (MF (toℕ (suc i)) · MF zero) + ≡⟨ solve! P' ⟩ + MF (toℕ (suc i)) + ∎) + ⟩ + MF (toℕ (suc i)) · M (suc i) zero · (MF (toℕ j) · M zero (suc j)) · + det (minor i zero (minor zero (suc j) M)) + ≡⟨ cong + (λ a → + a · + det (minor i zero (minor zero (suc j) M))) + (solve! P') ⟩ + MF (toℕ (suc j)) · M zero (suc j) · + MF (toℕ i) · M (suc i) zero · + det (minor i zero (minor zero (suc j) M)) + ≡⟨ sym (·Assoc (MF (toℕ (suc j)) · M zero (suc j) · MF (toℕ i)) (M (suc i) zero) (det (minor i zero (minor zero (suc j) M)))) ⟩ + (MF (toℕ (suc j)) · M zero (suc j) · MF (toℕ i) · + (M (suc i) zero · det (minor i zero (minor zero (suc j) M)))) + ≡⟨ sym (·Assoc (MF (toℕ (suc j)) · M zero (suc j)) (MF (toℕ i)) (M (suc i) zero · det (minor i zero (minor zero (suc j) M)))) ⟩ + (MF (toℕ (suc j)) · M zero (suc j) · + (MF (toℕ i) · + (M (suc i) zero · det (minor i zero (minor zero (suc j) M))))) + ≡⟨ cong (λ a → MF (toℕ (suc j)) · M zero (suc j) · a) + (·Assoc (MF (toℕ i)) (M (suc i) zero) (det (minor i zero (minor zero (suc j) M)))) ⟩ + MF (toℕ (suc j)) · M zero (suc j) · + (MF (toℕ i) · M (suc i) zero · + det (minor i zero (minor zero (suc j) M))) + ≡⟨ refl ⟩ + (MF (toℕ (suc j)) · M zero (suc j) · + (MF (toℕ i) · minor zero (suc j) M i zero · + det (minor i zero (minor zero (suc j) M)))) + ≡⟨ + cong + (λ a → (MF (toℕ (suc j)) · M zero (suc j) · + (a · minor zero (suc j) M i zero · + det (minor i zero (minor zero (suc j) M))))) + (MF (toℕ i) + ≡⟨ solve! P' ⟩ + (MF (toℕ i) · MF zero) + ≡⟨ sym (sumMF (toℕ i) zero) ⟩ + MF (toℕ i +ℕ zero) ∎) + ⟩ + (MF (toℕ (suc j)) · M zero (suc j) · + (MF (toℕ i +ℕ zero) · minor zero (suc j) M i zero · + det (minor i zero (minor zero (suc j) M)))) + ∎) + + + DetRowColumn : ∀ {n} → (M : FinMatrix R (suc n) (suc n)) → + detC zero M ≡ det M + DetRowColumn {zero} M = refl + DetRowColumn {suc n} M = + detC zero M + ≡⟨ refl ⟩ + ∑ (λ i → (MF ((toℕ i) +ℕ zero)) · (M i zero) · det {suc n} (minor i zero M)) + ≡⟨ refl ⟩ + 1r · (M zero zero) · det (minor zero zero M) + + ∑ (λ i → (MF ((toℕ (suc i)) +ℕ zero)) · (M (suc i) zero) · det {suc n} (minor (suc i) zero M)) + ≡⟨ refl ⟩ + (1r · M zero zero · det (minor zero zero M) + + ∑ (λ i → + MF (toℕ (suc i) +ℕ zero) · M (suc i) zero · + ∑ (λ j → MF (toℕ j) · minor (suc i) zero M zero j · det (minor zero j (minor (suc i) zero M))))) + ≡⟨ +Compat + refl + (∑Compat + (λ i → MF (toℕ (suc i) +ℕ zero) · M (suc i) zero · + ∑ (λ j → MF (toℕ j) · minor (suc i) zero M zero j · + det (minor zero j (minor (suc i) zero M)))) + (λ i → ∑ (λ j → MF (toℕ (suc i) +ℕ zero) · M (suc i) zero · + (MF (toℕ j) · minor (suc i) zero M zero j · + det (minor zero j (minor (suc i) zero M))))) + (λ i → ∑DistR + (MF (toℕ (suc i) +ℕ zero) · M (suc i) zero) + (λ j → MF (toℕ j) · minor (suc i) zero M zero j · det (minor zero j (minor (suc i) zero M))))) + ⟩ + 1r · M zero zero · det (minor zero zero M) + + ∑ (λ i → + ∑ (λ j → + MF (toℕ (suc i) +ℕ zero) · M (suc i) zero · + (MF (toℕ j) · minor (suc i) zero M zero j · + det (minor zero j (minor (suc i) zero M))))) + ≡⟨ +Compat refl (DetRowColumnAux M) ⟩ + (1r · M zero zero · det (minor zero zero M) + + ∑ + (λ i → + ∑ + (λ j → + MF (toℕ (suc j)) · M zero (suc j) · + (MF (toℕ i +ℕ zero) · minor zero (suc j) M i zero · + det (minor i zero (minor zero (suc j) M)))))) + ≡⟨ +Compat refl (∑Comm + λ i j → + MF (toℕ (suc j)) · M zero (suc j) · + (MF (toℕ i +ℕ zero) · minor zero (suc j) M i zero · + det (minor i zero (minor zero (suc j) M)))) ⟩ + (1r · M zero zero · det (minor zero zero M) + + ∑ + (λ j → + ∑ + (λ i → + MF (toℕ (suc j)) · M zero (suc j) · + (MF (toℕ i +ℕ zero) · minor zero (suc j) M i zero · + det (minor i zero (minor zero (suc j) M)))))) + ≡⟨ +Compat + refl + (∑Compat (λ j → + ∑ + (λ i → + MF (toℕ (suc j)) · M zero (suc j) · + (MF (toℕ i +ℕ zero) · minor zero (suc j) M i zero · + det (minor i zero (minor zero (suc j) M))))) + (λ j → + MF (toℕ (suc j)) · M zero (suc j) · + ∑(λ i → + (MF (toℕ i +ℕ zero) · M (suc i) zero · + det (minor i zero (minor zero (suc j) M))))) + (λ j → sym (∑DistR (MF (toℕ (suc j)) · M zero (suc j)) + λ i → MF (toℕ i +ℕ zero) · M (suc i) zero · + det (minor i zero (minor zero (suc j) M))) )) ⟩ + (1r · M zero zero · det (minor zero zero M) + + ∑ + (λ j → + MF (toℕ (suc j)) · M zero (suc j) · + detC {suc n} zero (minor zero (suc j) M))) + ≡⟨ +Compat + refl + (∑Compat + (λ j → + MF (toℕ (suc j)) · M zero (suc j) · + detC {suc n} zero (minor zero (suc j) M)) + (λ j → + MF (toℕ (suc j)) · M zero (suc j) · + det (minor zero (suc j) M)) + (λ j → cong + (λ a → MF (toℕ (suc j)) · M zero (suc j) · a) + (DetRowColumn (minor zero (suc j) M)))) + ⟩ + (1r · M zero zero · det (minor zero zero M) + + ∑ + (λ j → + MF (toℕ (suc j)) · M zero (suc j) · + det (minor zero (suc j) M))) + ≡⟨ refl ⟩ + det M + ∎ + + DetColumnAux1a : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ (suc i)) (toℕ j) · + (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ j +ℕ zero) · minor (suc i) (suc k) M j zero · + det (minor j zero (minor (suc i) (suc k) M)))))) + ≡ + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ (weakenFin j)) (toℕ i)) · + (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ (weakenFin j) +ℕ zero) · M (weakenFin j) zero · + det (minor i k (minor (weakenFin j) zero M)))))) + DetColumnAux1a k M = + ∑∑Compat + (λ i j → ind> (toℕ (suc i)) (toℕ j) · + (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ j +ℕ zero) · minor (suc i) (suc k) M j zero · + det (minor j zero (minor (suc i) (suc k) M))))) + (λ z z₁ → + (1r + - ind> (toℕ (weakenFin z₁)) (toℕ z)) · + (MF (toℕ (suc z) +ℕ toℕ (suc k)) · M (suc z) (suc k) · + (MF (toℕ (weakenFin z₁) +ℕ zero) · M (weakenFin z₁) zero · + det (minor z k (minor (weakenFin z₁) zero M))))) + (λ i j → + (ind> (suc (toℕ i)) (toℕ j) · + (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ j +ℕ zero) · minor (suc i) (suc k) M j zero · + det (minor j zero (minor (suc i) (suc k) M))))) + ≡⟨ + cong + (λ a → a · (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ j +ℕ zero) · minor (suc i) (suc k) M j zero · + det (minor j zero (minor (suc i) (suc k) M))))) + (ind>Suc (toℕ i) (toℕ j)) + ⟩ + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ j +ℕ zero) · minor (suc i) (suc k) M j zero · + det (minor j zero (minor (suc i) (suc k) M)))) + ≡⟨ + ind>anti + (λ j i → (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ j +ℕ zero) · minor (suc i) (suc k) M j zero · + det (minor j zero (minor (suc i) (suc k) M))))) + (λ z z₁ → + MF (toℕ (suc z₁) +ℕ toℕ (suc k)) · M (suc z₁) (suc k) · + (MF (toℕ z +ℕ zero) · M (weakenFin z) zero · + det (minor z₁ k (minor (weakenFin z) zero M)))) + (λ j i le → + (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ j +ℕ zero) · minor (suc i) (suc k) M j zero · + det (minor j zero (minor (suc i) (suc k) M)))) + ≡⟨ cong + (λ a → (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ j +ℕ zero) · a · + det (minor j zero (minor (suc i) (suc k) M))))) + (minorIdId (suc i) (suc k) j zero M (s≤s le) (s≤s z≤)) + ⟩ + (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ j +ℕ zero) · M (weakenFin j) zero · + det (minor j zero (minor (suc i) (suc k) M)))) + ≡⟨ + cong + (λ a → (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ j +ℕ zero) · M (weakenFin j) zero · a))) + (detComp + (minor j zero (minor (suc i) (suc k) M)) + (minor i k (minor (weakenFin j) zero M)) + (λ i₁ j₁ → + minorComm0 i j k zero i₁ j₁ M le z≤)) + ⟩ + (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ j +ℕ zero) · M (weakenFin j) zero · + det (minor i k (minor (weakenFin j) zero M)))) + ∎) + j + i ⟩ + ((1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ j +ℕ zero) · M (weakenFin j) zero · + det (minor i k (minor (weakenFin j) zero M))))) + ≡⟨ + cong + (λ a → + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (a · M (weakenFin j) zero · + det (minor i k (minor (weakenFin j) zero M))))) + (MF (toℕ j +ℕ zero) + ≡⟨ sumMF (toℕ j) zero ⟩ + (MF (toℕ j) · MF zero) + ≡⟨ cong (λ a → MF a · MF zero) ((toℕ j) ≡⟨ sym (toℕweakenFin j) ⟩ toℕ (weakenFin j) ∎) ⟩ + (MF (toℕ (weakenFin j)) · MF zero) + ≡⟨ sym (sumMF (toℕ (weakenFin j)) zero) ⟩ + MF (toℕ (weakenFin j) +ℕ zero) + ∎) + ⟩ + (1r + - ind> (toℕ j) (toℕ i)) · + (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ (weakenFin j) +ℕ zero) · M (weakenFin j) zero · + det (minor i k (minor (weakenFin j) zero M)))) + ≡⟨ + cong + (λ a → (1r + - ind> a (toℕ i)) · + (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ (weakenFin j) +ℕ zero) · M (weakenFin j) zero · + det (minor i k (minor (weakenFin j) zero M))))) + (toℕ j ≡⟨ sym (toℕweakenFin j) ⟩ toℕ (weakenFin j) ∎) + ⟩ + ((1r + - ind> (toℕ (weakenFin j)) (toℕ i)) · + (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ (weakenFin j) +ℕ zero) · M (weakenFin j) zero · + det (minor i k (minor (weakenFin j) zero M))))) + ∎) + + + DetColumnAux1b : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) · + (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ j +ℕ zero) · minor (weakenFin i) (suc k) M j zero · + det (minor j zero (minor (weakenFin i) (suc k) M)))))) + ≡ + ∑ + (λ i → + ∑ + (λ z → + ind> (toℕ (suc z)) (toℕ i) · + (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ (suc z) +ℕ one) · M (suc z) zero · + det (minor i k (minor (suc z) zero M)))))) + DetColumnAux1b k M = + ∑∑Compat + (λ i j → + (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) · + (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ j +ℕ zero) · minor (weakenFin i) (suc k) M j zero · + det (minor j zero (minor (weakenFin i) (suc k) M))))) + (λ z z₁ → + ind> (toℕ (suc z₁)) (toℕ z) · + (MF (toℕ (weakenFin z) +ℕ toℕ (suc k)) · M (weakenFin z) (suc k) · + (MF (toℕ (suc z₁) +ℕ one) · M (suc z₁) zero · + det (minor z k (minor (suc z₁) zero M))))) + (λ i j → + ((1r + - ind> (toℕ (weakenFin i)) (toℕ j)) · + (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ j +ℕ zero) · minor (weakenFin i) (suc k) M j zero · + det (minor j zero (minor (weakenFin i) (suc k) M))))) + ≡⟨ cong + (λ a → (1r + - ind> a (toℕ j)) · + (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ j +ℕ zero) · minor (weakenFin i) (suc k) M j zero · + det (minor j zero (minor (weakenFin i) (suc k) M))))) + (toℕweakenFin i) ⟩ + ((1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ j +ℕ zero) · minor (weakenFin i) (suc k) M j zero · + det (minor j zero (minor (weakenFin i) (suc k) M))))) + ≡⟨ ind>anti + (λ i j → MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ j +ℕ zero) · minor (weakenFin i) (suc k) M j zero · + det (minor j zero (minor (weakenFin i) (suc k) M)))) + (λ i j → MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ j +ℕ zero) · M (suc j) zero · + det (minor i k (minor (suc j) zero M)))) + (λ i j le → + (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ j +ℕ zero) · minor (weakenFin i) (suc k) M j zero · + det (minor j zero (minor (weakenFin i) (suc k) M)))) + ≡⟨ cong + (λ a → + (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ j +ℕ zero) · a · + det (minor j zero (minor (weakenFin i) (suc k) M))))) + (minorSucId + (weakenFin i) + (suc k) + j + zero + M + (weakenweakenFinLe i j le) + (s≤s z≤)) + ⟩ + (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ j +ℕ zero) · M (suc j) zero · + det (minor j zero (minor (weakenFin i) (suc k) M)))) + ≡⟨ + cong + (λ a → + MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ j +ℕ zero) · M (suc j) zero · a)) + (detComp + (minor j zero (minor (weakenFin i) (suc k) M)) + (minor i k (minor (suc j) zero M)) + λ i₁ j₁ → + minorComm2 + i + j + k + zero + i₁ + j₁ + M + le + z≤) + ⟩ + (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ j +ℕ zero) · M (suc j) zero · + det (minor i k (minor (suc j) zero M)))) + ∎) + i + j + ⟩ + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ j +ℕ zero) · M (suc j) zero · + det (minor i k (minor (suc j) zero M)))) + ≡⟨ cong + (λ a → a · (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ j +ℕ zero) · M (suc j) zero · + det (minor i k (minor (suc j) zero M))))) + (sym (ind>Suc (toℕ j) (toℕ i))) ⟩ + (ind> (toℕ (suc j)) (toℕ i) · + (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ j +ℕ zero) · M (suc j) zero · + det (minor i k (minor (suc j) zero M))))) + ≡⟨ + cong + (λ a → (ind> (toℕ (suc j)) (toℕ i) · + (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (a · M (suc j) zero · + det (minor i k (minor (suc j) zero M)))))) + (MF (toℕ j +ℕ zero) + ≡⟨ sumMF (toℕ j) zero ⟩ + (MF (toℕ j) · MF zero) + ≡⟨ solve! P' ⟩ + (MF (toℕ (suc j)) · MF one) + ≡⟨ sym (sumMF (toℕ (suc j)) one) ⟩ + MF (toℕ (suc j) +ℕ one) + ∎) + ⟩ + (ind> (toℕ (suc j)) (toℕ i) · + (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ (suc j) +ℕ one) · M (suc j) zero · + det (minor i k (minor (suc j) zero M))))) + ∎) + + DetColumnAux2a : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · M (suc j) (suc k) · + (MF (toℕ i +ℕ zero) · M i zero · + det (minor j k (minor i zero M)))))) + ≡ + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M)))))) + + DetColumnAux2a k M = + ∑∑Compat + (λ i j → + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · M (suc j) (suc k) · + (MF (toℕ i +ℕ zero) · M i zero · + det (minor j k (minor i zero M))))) + (λ z z₁ → + (1r + - ind> (toℕ z) (toℕ z₁)) · + (MF (toℕ z +ℕ zero) · M z zero · + (MF (toℕ (suc z₁) +ℕ toℕ (suc k)) · minor z zero M z₁ k · + det (minor z₁ k (minor z zero M))))) + (ind>anti + (λ i j → + MF (toℕ (suc j) +ℕ toℕ (suc k)) · M (suc j) (suc k) · + (MF (toℕ i +ℕ zero) · M i zero · det (minor j k (minor i zero M)))) + (λ z z₁ → + MF (toℕ z +ℕ zero) · M z zero · + (MF (toℕ (suc z₁) +ℕ toℕ (suc k)) · minor z zero M z₁ k · + det (minor z₁ k (minor z zero M)))) + (λ i j le → + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · M (suc j) (suc k) · + (MF (toℕ i +ℕ zero) · M i zero · det (minor j k (minor i zero M)))) + ≡⟨ cong + (λ a → + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · a · + (MF (toℕ i +ℕ zero) · M i zero · det (minor j k (minor i zero M))))) + (sym + (minorSucSuc i zero j k M (weakenFinLe i j le) z≤)) + ⟩ + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + (MF (toℕ i +ℕ zero) · M i zero · det (minor j k (minor i zero M)))) + ≡⟨ + cong + (λ a → (a · minor i zero M j k · + (MF (toℕ i +ℕ zero) · M i zero · det (minor j k (minor i zero M))))) + (sumMF (toℕ (suc j)) (toℕ (suc k))) + ⟩ + (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k · + (MF (toℕ i +ℕ zero) · M i zero · det (minor j k (minor i zero M)))) + ≡⟨ + cong + (λ a → (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k · + (a · M i zero · det (minor j k (minor i zero M))))) + (sumMF (toℕ i) zero) + ⟩ + (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k · + (MF (toℕ i) · MF zero · M i zero · + det (minor j k (minor i zero M)))) + ≡⟨ ·Assoc + (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k) + (MF (toℕ i) · MF zero · M i zero) + (det (minor j k (minor i zero M))) ⟩ + (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k · + (MF (toℕ i) · MF zero · M i zero) + · det (minor j k (minor i zero M))) + ≡⟨ + cong + (λ a → a + · det (minor j k (minor i zero M))) + (solve! P') + ⟩ + (MF (toℕ i) · MF zero · M i zero) · + (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k) + · det (minor j k (minor i zero M)) + ≡⟨ + sym + (·Assoc + (MF (toℕ i) · MF zero · M i zero) + (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k) + (det (minor j k (minor i zero M)))) + ⟩ + MF (toℕ i) · MF zero · M i zero · + (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M))) + ≡⟨ + cong + (λ a → (a · M i zero · + (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M))))) + (sym (sumMF (toℕ i) zero)) + ⟩ + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M)))) + ≡⟨ + cong + (λ a → (MF (toℕ i +ℕ zero) · M i zero · + (a · minor i zero M j k · det (minor j k (minor i zero M))))) + (sym (sumMF (toℕ (suc j)) (toℕ (suc k)))) + ⟩ + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · det (minor j k (minor i zero M)))) + + ∎) + ) + + DetColumnAux2b : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (MF (toℕ (weakenFin j) +ℕ toℕ (suc k)) · M (weakenFin j) (suc k) · + (MF (toℕ i +ℕ one) · M i zero · + det (minor j k (minor i zero M)))))) + ≡ + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M)))))) + DetColumnAux2b k M = + ∑∑Compat + (λ i j → ind> (toℕ i) (toℕ j) · + (MF (toℕ (weakenFin j) +ℕ toℕ (suc k)) · M (weakenFin j) (suc k) · + (MF (toℕ i +ℕ one) · M i zero · + det (minor j k (minor i zero M))))) + (λ z z₁ → + ind> (toℕ z) (toℕ z₁) · + (MF (toℕ z +ℕ zero) · M z zero · + (MF (toℕ (suc z₁) +ℕ toℕ (suc k)) · minor z zero M z₁ k · + det (minor z₁ k (minor z zero M))))) + (λ i j → + ind>prop + (λ i j → (MF (toℕ (weakenFin j) +ℕ toℕ (suc k)) · M (weakenFin j) (suc k) · + (MF (toℕ i +ℕ one) · M i zero · + det (minor j k (minor i zero M))))) + (λ z z₁ → + MF (toℕ z +ℕ zero) · M z zero · + (MF (toℕ (suc z₁) +ℕ toℕ (suc k)) · minor z zero M z₁ k · + det (minor z₁ k (minor z zero M)))) + (λ i j le → + (MF (toℕ (weakenFin j) +ℕ toℕ (suc k)) · M (weakenFin j) (suc k) · + (MF (toℕ i +ℕ one) · M i zero · det (minor j k (minor i zero M)))) + ≡⟨ + cong + (λ a → + (MF (toℕ (weakenFin j) +ℕ toℕ (suc k)) · a · + (MF (toℕ i +ℕ one) · M i zero · det (minor j k (minor i zero M))))) + (sym (minorIdSuc i zero j k M le z≤)) + ⟩ + (MF (toℕ (weakenFin j) +ℕ toℕ (suc k)) · minor i zero M j k · + (MF (toℕ i +ℕ one) · M i zero · det (minor j k (minor i zero M)))) + ≡⟨ + cong + (λ a → a · minor i zero M j k · + (MF (toℕ i +ℕ one) · M i zero · det (minor j k (minor i zero M)))) + (sumMF (toℕ (weakenFin j)) (toℕ (suc k))) + ⟩ + (MF (toℕ (weakenFin j)) · MF (toℕ (suc k)) · minor i zero M j k · + (MF (toℕ i +ℕ one) · M i zero · det (minor j k (minor i zero M)))) + ≡⟨ + cong + (λ a → MF (toℕ (weakenFin j)) · MF (toℕ (suc k)) · minor i zero M j k · + (a · M i zero · det (minor j k (minor i zero M)))) + (sumMF (toℕ i) one) + ⟩ + (MF (toℕ (weakenFin j)) · MF (toℕ (suc k)) · minor i zero M j k · + (MF (toℕ i) · MF one · M i zero · det (minor j k (minor i zero M)))) + ≡⟨ cong + (λ a → (MF (a) · MF (toℕ (suc k)) · minor i zero M j k · + (MF (toℕ i) · MF one · M i zero · det (minor j k (minor i zero M))))) + (toℕweakenFin j) ⟩ + (MF (toℕ j) · MF (toℕ (suc k)) · minor i zero M j k · + (MF (toℕ i) · MF one · M i zero · det (minor j k (minor i zero M)))) + ≡⟨ ·Assoc + (MF (toℕ j) · MF (toℕ (suc k)) · minor i zero M j k) + (MF (toℕ i) · MF one · M i zero) + (det (minor j k (minor i zero M))) ⟩ + (MF (toℕ j) · MF (toℕ (suc k)) · minor i zero M j k · + (MF (toℕ i) · MF one · M i zero) + · det (minor j k (minor i zero M))) + ≡⟨ cong + (λ a → a · det (minor j k (minor i zero M))) + (solve! P') ⟩ + (MF one · MF (toℕ j) · MF (toℕ (suc k)) · minor i zero M j k · + (MF (toℕ i) · M i zero) + · det (minor j k (minor i zero M))) + ≡⟨ + cong + (λ a → a · MF (toℕ (suc k)) · minor i zero M j k · + (MF (toℕ i) · M i zero) + · det (minor j k (minor i zero M))) + (sym (sumMF one (toℕ j))) + ⟩ + (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k · + (MF (toℕ i) · M i zero) + · det (minor j k (minor i zero M))) + ≡⟨ + cong + (λ a → a · det (minor j k (minor i zero M))) + (solve! P') + ⟩ + (MF (toℕ i) · M i zero) + · MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M)) + ≡⟨ + cong + (λ a → ( a · M i zero) + · MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M))) + (solve! P') ⟩ + (MF (toℕ i) · MF zero · M i zero) + · MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M)) + ≡⟨ + cong + (λ a → a · det (minor j k (minor i zero M))) + (solve! P') + ⟩ + MF (toℕ i) · MF zero · M i zero · + (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k) + · det (minor j k (minor i zero M)) + ≡⟨ sym + (·Assoc + (MF (toℕ i) · MF zero · M i zero) + (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k) + (det (minor j k (minor i zero M)))) ⟩ + MF (toℕ i) · MF zero · M i zero · + (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M))) + ≡⟨ + cong + (λ a → (a · M i zero · + (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M))))) + (sym (sumMF (toℕ i) zero)) + ⟩ + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M)))) + ≡⟨ + cong + (λ a → (MF (toℕ i +ℕ zero) · M i zero · + (a · minor i zero M j k · det (minor j k (minor i zero M))))) + (sym (sumMF (toℕ (suc j)) (toℕ (suc k)))) + ⟩ + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · det (minor j k (minor i zero M)))) + ∎) + i + j) + + MFsucsuc : {n m : ℕ} → (j : Fin n) → (k : Fin m) → + MF (toℕ (suc j) +ℕ (toℕ (suc k))) ≡ MF (toℕ j +ℕ toℕ k) + MFsucsuc j k = + MF (toℕ (suc j) +ℕ toℕ (suc k)) + ≡⟨ sumMF (toℕ (suc j)) (toℕ (suc k)) ⟩ + (MF (toℕ (suc j)) · MF (toℕ (suc k))) + ≡⟨ refl ⟩ + ((- 1r) · MF (toℕ j) · ((- 1r) · MF (toℕ k)) ) + ≡⟨ solve! P' ⟩ + ( MF (toℕ j) · MF ( toℕ k)) + ≡⟨ sym (sumMF (toℕ j) (toℕ k))⟩ + MF (toℕ j +ℕ toℕ k) + ∎ + + DetColumnZero : ∀ {n} → (k : Fin (suc n)) → (M : FinMatrix R (suc n) (suc n)) → + detC k M ≡ detC zero M + DetColumnZero {zero} zero M = refl + DetColumnZero {suc n} zero M = refl + DetColumnZero {suc n} (suc k) M = + detC (suc k) M + ≡⟨ refl ⟩ + ∑ + (λ i → + MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · det (minor i (suc k) M)) + ≡⟨ ∑Compat + (λ i → + MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · det (minor i (suc k) M)) + (λ i → + MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · detC zero (minor i (suc k) M)) + (λ i → cong + (λ a → MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · a) + (sym (DetRowColumn (minor i (suc k) M)))) + ⟩ + ∑ + (λ i → + MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · detC zero (minor i (suc k) M)) + ≡⟨ refl ⟩ + ∑ + (λ i → + MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · + ∑ + (λ j → + MF (toℕ j +ℕ zero) · minor i (suc k) M j zero · + det (minor j zero (minor i (suc k) M)))) + ≡⟨ ∑Compat + ((λ i → + MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · + ∑ + (λ j → + MF (toℕ j +ℕ zero) · minor i (suc k) M j zero · + det (minor j zero (minor i (suc k) M))))) + (λ i → ∑ + (λ j → + MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · + (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero · + det (minor j zero (minor i (suc k) M))))) + (λ i → + ∑DistR ( MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k)) + (λ j → + (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero · + det (minor j zero (minor i (suc k) M))))) + ⟩ + ∑ + (λ i → + ∑ + (λ j → + MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · + (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero · + det (minor j zero (minor i (suc k) M))))) + ≡⟨ + ∑∑Compat + (λ i j → + MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · + (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero · + det (minor j zero (minor i (suc k) M)))) + (λ z z₁ → + ind> (toℕ z) (toℕ z₁) · + (MF (toℕ z +ℕ toℕ (suc k)) · M z (suc k) · + (MF (toℕ z₁ +ℕ zero) · minor z (suc k) M z₁ zero · + det (minor z₁ zero (minor z (suc k) M)))) + + + (1r + - ind> (toℕ z) (toℕ z₁)) · + (MF (toℕ z +ℕ toℕ (suc k)) · M z (suc k) · + (MF (toℕ z₁ +ℕ zero) · minor z (suc k) M z₁ zero · + det (minor z₁ zero (minor z (suc k) M))))) + (λ i j → + DetRowAux2 + (ind> (toℕ i) (toℕ j)) + (MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · + (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero · + det (minor j zero (minor i (suc k) M))))) + ⟩ + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · + (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero · + det (minor j zero (minor i (suc k) M)))) + + + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · + (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero · + det (minor j zero (minor i (suc k) M)))))) + ≡⟨ ∑∑Split + (λ i j → + ind> (toℕ i) (toℕ j) · + (MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · + (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero · + det (minor j zero (minor i (suc k) M))))) + (λ i j → + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · + (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero · + det (minor j zero (minor i (suc k) M))))) + ⟩ + (∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · + (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero · + det (minor j zero (minor i (suc k) M)))))) + + + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · + (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero · + det (minor j zero (minor i (suc k) M))))))) + ≡⟨ + +Compat + (∑∑ShiftSuc (λ i j → + MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · + (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero · + det (minor j zero (minor i (suc k) M))))) + (∑∑ShiftWeak (λ i j → MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · + (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero · + det (minor j zero (minor i (suc k) M))))) + ⟩ + (∑ + (λ i → + ∑ + (λ j → + ind> (toℕ (suc i)) (toℕ j) · + (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ j +ℕ zero) · minor (suc i) (suc k) M j zero · + det (minor j zero (minor (suc i) (suc k) M)))))) + + + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) · + (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ j +ℕ zero) · minor (weakenFin i) (suc k) M j zero · + det (minor j zero (minor (weakenFin i) (suc k) M))))))) + ≡⟨ +Compat (DetColumnAux1a k M) (DetColumnAux1b k M) ⟩ + ( + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ (weakenFin j)) (toℕ i)) · + (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ (weakenFin j) +ℕ zero) · M (weakenFin j) zero · + det (minor i k (minor (weakenFin j) zero M)))))) + + + ∑ + (λ i → + ∑ + (λ z → + ind> (toℕ (suc z)) (toℕ i) · + (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ (suc z) +ℕ one) · M (suc z) zero · + det (minor i k (minor (suc z) zero M))))))) + ≡⟨ +Compat + (∑Comm (λ i j → + (1r + - ind> (toℕ (weakenFin j)) (toℕ i)) · + (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ (weakenFin j) +ℕ zero) · M (weakenFin j) zero · + det (minor i k (minor (weakenFin j) zero M)))))) + (∑Comm (λ i j → + ind> (toℕ (suc j)) (toℕ i) · + (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ (suc j) +ℕ one) · M (suc j) zero · + det (minor i k (minor (suc j) zero M)))))) + ⟩ + ∑ + (λ j → + ∑ + (λ i → + (1r + - ind> (toℕ (weakenFin j)) (toℕ i)) · + (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ (weakenFin j) +ℕ zero) · M (weakenFin j) zero · + det (minor i k (minor (weakenFin j) zero M)))))) + + + ∑ + (λ j → + ∑ + (λ i → + ind> (toℕ (suc j)) (toℕ i) · + (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ (suc j) +ℕ one) · M (suc j) zero · + det (minor i k (minor (suc j) zero M)))))) + ≡⟨ +Compat + (sym (∑∑ShiftWeak (λ j i → (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) · + (MF (toℕ j +ℕ zero) · M j zero · + det (minor i k (minor j zero M))))))) + (sym (∑∑ShiftSuc (λ j i → (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) · + (MF (toℕ j +ℕ one) · M j zero · + det (minor i k (minor j zero M))))))) + ⟩ + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · M (suc j) (suc k) · + (MF (toℕ i +ℕ zero) · M i zero · + det (minor j k (minor i zero M)))))) + + + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (MF (toℕ (weakenFin j) +ℕ toℕ (suc k)) · M (weakenFin j) (suc k) · + (MF (toℕ i +ℕ one) · M i zero · + det (minor j k (minor i zero M)))))) + ≡⟨ +Compat (DetColumnAux2a k M) (DetColumnAux2b k M) ⟩ + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M)))))) + + + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M)))))) + ≡⟨ +Comm ( ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M))))))) (∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M))))))) ⟩ + (∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M)))))) + + + ∑ + (λ i → + ∑ + (λ j → + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M))))))) + ≡⟨ sym (∑∑Split + (λ i j → + ind> (toℕ i) (toℕ j) · + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M))))) + (λ i j → + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M)))))) + ⟩ + ∑ + (λ i → + ∑ + (λ j → + ind> (toℕ i) (toℕ j) · + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M)))) + + + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M)))))) + ≡⟨ ∑∑Compat + (λ i j → + ind> (toℕ i) (toℕ j) · + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M)))) + + + (1r + - ind> (toℕ i) (toℕ j)) · + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M))))) + (λ i j → + (MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M))))) + (λ i j → sym + (DetRowAux2 ( ind> (toℕ i) (toℕ j) ) + ((MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M))))))) ⟩ + ∑ + (λ i → + ∑ + (λ j → + MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M))))) + ≡⟨ ∑Compat + ((λ i → + ∑ + (λ j → + MF (toℕ i +ℕ zero) · M i zero · + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M)))))) + ((λ i → + MF (toℕ i +ℕ zero) · M i zero · + ∑ + (λ j → + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M)))))) + (λ i → + sym + (∑DistR + (MF (toℕ i +ℕ zero) · M i zero) + (λ j → + (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M)))))) + ⟩ + ∑ + (λ i → + MF (toℕ i +ℕ zero) · M i zero · + ∑ + (λ j → + MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M)))) + ≡⟨ ∑Compat + (λ i → + MF (toℕ i +ℕ zero) · M i zero · + ∑ + (λ j → + MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M)))) + (λ i → + MF (toℕ i +ℕ zero) · M i zero · + ∑ + (λ j → + MF (toℕ j +ℕ toℕ k) · minor i zero M j k · + det (minor j k (minor i zero M)))) + (λ i → + cong + (λ a → MF (toℕ i +ℕ zero) · M i zero · a) + (∑Compat + (λ j → + MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k · + det (minor j k (minor i zero M))) + (λ j → + MF (toℕ j +ℕ toℕ k) · minor i zero M j k · + det (minor j k (minor i zero M))) + (λ j → + cong + (λ a → a · minor i zero M j k · + det (minor j k (minor i zero M))) + (MFsucsuc j k) ) + ))⟩ + ∑ + (λ i → + MF (toℕ i +ℕ zero) · M i zero · + ∑ + (λ j → + MF (toℕ j +ℕ toℕ k) · minor i zero M j k · + det (minor j k (minor i zero M)))) + ≡⟨ refl ⟩ + ∑ + (λ i → + MF (toℕ i +ℕ zero) · M i zero · + detC k (minor i zero M)) + ≡⟨ ∑Compat + (λ i → MF (toℕ i +ℕ zero) · M i zero · + detC k (minor i zero M)) + (λ i → MF (toℕ i +ℕ zero) · M i zero · + detC zero (minor i zero M)) + (λ i → cong + (λ a → MF (toℕ i +ℕ zero) · M i zero · a) + (DetColumnZero k (minor i zero M))) ⟩ + ∑ + (λ i → MF (toℕ i +ℕ zero) · M i zero · detC zero (minor i zero M)) + ≡⟨ ∑Compat + (λ i → MF (toℕ i +ℕ zero) · M i zero · + detC zero (minor i zero M)) + (λ i → MF (toℕ i +ℕ zero) · M i zero · + det (minor i zero M)) + (λ i → cong + (λ a → MF (toℕ i +ℕ zero) · M i zero · a) + (DetRowColumn (minor i zero M))) ⟩ + ∑ (λ i → MF (toℕ i +ℕ zero) · M i zero · det (minor i zero M)) + ≡⟨ refl ⟩ + detC zero M + ∎ + + DetColumn : ∀ {n} → (k : Fin (suc n)) → (M : FinMatrix R (suc n) (suc n)) → + detC k M ≡ det M + DetColumn k M = + detC k M + ≡⟨ DetColumnZero k M ⟩ + detC zero M + ≡⟨ DetRowColumn M ⟩ + det M + ∎ + + open Coefficient (P') + + δ = KroneckerDelta.δ R' + + ∑Mul1r = Sum.∑Mul1r (CommRing→Ring P') + ∑Mulr1 = Sum.∑Mulr1 (CommRing→Ring P') + + detZero : {n : ℕ} → det {suc n} 𝟘 ≡ 0r + detZero {n} = + ∑Zero + (λ i → MF (toℕ i) · 0r · det {n} (minor zero i 𝟘)) + (λ i → + (MF (toℕ i) · 0r · det {n} (minor zero i 𝟘)) + ≡⟨ + cong + (λ a → a · det {n} (minor zero i 𝟘)) + (solve! P')⟩ + 0r · det (minor zero i 𝟘) + ≡⟨ RingTheory.0LeftAnnihilates (CommRing→Ring P') (det (minor zero i 𝟘)) ⟩ + 0r + ∎ + ) + + detOne : {n : ℕ} → det {n} 𝟙 ≡ 1r + detOne {zero} = refl + detOne {suc n} = + ∑ (λ i → MF (toℕ i) · 𝟙 (zero {n}) i · det {n} (minor zero i 𝟙)) + ≡⟨ refl ⟩ + ∑ (λ i → MF (toℕ i) · δ (zero {n}) i · det {n} (minor zero i 𝟙)) + ≡⟨ ∑Compat + (λ i → MF (toℕ i) · δ (zero {n}) i · det {n} (minor zero i 𝟙)) + (λ i → δ (zero {n}) i · MF (toℕ i) · det {n} (minor zero i 𝟙)) + (λ i → + cong + (λ a → a · det {n} (minor zero i 𝟙)) + (solve! P')) + ⟩ + ∑ (λ i → δ (zero {n}) i · MF (toℕ i) · det (minor zero i 𝟙)) + ≡⟨ ∑Compat + (λ i → δ (zero {n}) i · MF (toℕ i) · det (minor zero i 𝟙)) + (λ i → δ (zero {n}) i · (MF (toℕ i) · det (minor zero i 𝟙))) + (λ i → sym (·Assoc _ _ _)) ⟩ + ∑ (λ i → δ (zero {n}) i · (MF (toℕ i) · det (minor zero i 𝟙))) + ≡⟨ ∑Mul1r + (suc n) + (λ i → (MF (toℕ i) · det {n} (minor zero i 𝟙))) + zero ⟩ + MF zero · det {n} (minor zero zero 𝟙) + ≡⟨ refl ⟩ + (1r · det {n} 𝟙) + ≡⟨ ·IdL (det {n} 𝟙) ⟩ + det {n} 𝟙 + ≡⟨ detOne{n} ⟩ + 1r + ∎ + + MFplusZero : {n : ℕ} → (i : Fin n) → MF (toℕ i +ℕ zero) ≡ MF (toℕ i) + MFplusZero i = + MF (toℕ i +ℕ zero) + ≡⟨ sumMF (toℕ i) zero ⟩ + (MF (toℕ i) · MF zero) + ≡⟨ ·IdR (MF (toℕ i)) ⟩ + MF (toℕ i) + ∎ + + detTransp : {n : ℕ} → (M : FinMatrix R n n) → det M ≡ det (M ᵗ) + detTransp {zero} M = refl + detTransp {suc n} M = + det M + ≡⟨ refl ⟩ + ∑ (λ i → MF (toℕ i) · (M ᵗ) i zero · det ((minor i zero (M ᵗ))ᵗ)) + ≡⟨ + ∑Compat + (λ i → MF (toℕ i) · (M ᵗ) i zero · det ((minor i zero (M ᵗ))ᵗ)) + (λ i → MF (toℕ i) · (M ᵗ) i zero · det (minor i zero (M ᵗ))) + (λ i → + cong + (λ a → MF (toℕ i) · (M ᵗ) i zero · a) + (sym (detTransp (minor i zero (M ᵗ))))) + ⟩ + ∑ (λ i → MF (toℕ i) · (M ᵗ) i zero · det (minor i zero (M ᵗ))) + ≡⟨ ∑Compat + (λ i → MF (toℕ i) · (M ᵗ) i zero · det (minor i zero (M ᵗ))) + (λ i → MF (toℕ i +ℕ zero) · (M ᵗ) i zero · det (minor i zero (M ᵗ))) + (λ i → + cong + (λ a → + a · (M ᵗ) i zero · det (minor i zero (M ᵗ))) + (sym (MFplusZero i))) ⟩ + ∑ (λ i → MF (toℕ i +ℕ zero) · (M ᵗ) i zero · det (minor i zero (M ᵗ))) + ≡⟨ (DetRowColumn ((M ᵗ))) ⟩ + det (M ᵗ) + ∎ diff --git a/Cubical/Algebra/Determinat/minor.agda b/Cubical/Algebra/Determinat/minor.agda new file mode 100644 index 000000000..6ba1082d1 --- /dev/null +++ b/Cubical/Algebra/Determinat/minor.agda @@ -0,0 +1,186 @@ +{-# OPTIONS --cubical #-} + +module minor where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Algebra.Matrix +open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ + ; +-comm to +ℕ-comm + ; +-assoc to +ℕ-assoc + ; ·-assoc to ·ℕ-assoc) +open import Cubical.Data.Vec.Base using (_∷_; []) +open import Cubical.Foundations.Structure using (⟨_⟩) +open import Cubical.Data.FinData +open import Cubical.Data.FinData.Order using (_<'Fin_; _≤'Fin_) +open import Cubical.Algebra.Ring +open import Cubical.Algebra.Ring.Base +open import Cubical.Algebra.Ring.BigOps +open import Cubical.Algebra.Monoid.BigOp +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommRing.Base +open import Cubical.Data.Nat.Order +open import Cubical.Tactics.CommRingSolver + +module Minor (ℓ : Level) where + + -- definition and properties to remove one Index, i.e. (removeIndex i) is the monoton ebbeding from {0,...,n-1} to {0,...,n} ommiting i. + + removeIndex : {n : ℕ} → Fin (suc n) → Fin n → Fin (suc n) + removeIndex zero k = suc k + removeIndex (suc i) zero = zero + removeIndex (suc i) (suc k) = suc (removeIndex i k) + + -- On {0,...,i-1} the map (removeIndex i) is the identity. + removeIndexId : {n : ℕ} → (i : Fin (suc n)) → (k : Fin n) → (suc k) ≤'Fin i → (removeIndex i k) ≡ weakenFin k + removeIndexId (suc i) zero le = refl + removeIndexId (suc i) (suc k) (s≤s le) = cong (λ a → suc a) (removeIndexId i k le) + + -- On {i,...,n-1} the map (removeIndex i) is the successor function. + removeIndexSuc : {n : ℕ} → (i : Fin (suc n)) → (k : Fin n) → i ≤'Fin weakenFin k → (removeIndex i k) ≡ suc k + removeIndexSuc zero k le = refl + removeIndexSuc (suc i) (suc k) (s≤s le) = cong (λ a → suc a) (removeIndexSuc i k le) + + -- A formula for commuting removeIndex maps + removeIndexComm : {n : ℕ} → (i j : Fin (suc n)) → (k : Fin n) → i ≤'Fin j → + removeIndex (suc j) (removeIndex i k) ≡ removeIndex (weakenFin i) (removeIndex j k) + removeIndexComm zero j k le = refl + removeIndexComm (suc i) (suc j) zero le = refl + removeIndexComm (suc i) (suc j) (suc k) (s≤s le) = cong (λ a → suc a) (removeIndexComm i j k le) + + -- remove the j-th column of a matrix + + remove-column : {A : Type ℓ} {n m : ℕ} (j : Fin (suc m)) (M : FinMatrix A n (suc m)) → FinMatrix A n m + remove-column j M k l = M k (removeIndex j l) + + remove-column-comm : {A : Type ℓ} {n m : ℕ} (i : Fin (suc m)) (j : Fin (suc m)) (M : FinMatrix A n (suc (suc m))) (k : Fin n) (l : Fin m) → + j ≤'Fin i → + remove-column j (remove-column (suc i) M) k l ≡ remove-column i (remove-column (weakenFin j) M) k l + remove-column-comm i j M k l le = + remove-column j (remove-column (suc i) M) k l + ≡⟨ refl ⟩ + M k (removeIndex (suc i) (removeIndex j l)) + ≡⟨ cong (λ a → M k a) ( removeIndexComm j i l le) ⟩ + M k (removeIndex (weakenFin j) (removeIndex i l)) + ≡⟨ refl ⟩ + remove-column i (remove-column (weakenFin j) M) k l + ∎ + + -- remove the i-th row of a matrix + remove-row : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n)) (M : FinMatrix A (suc n) m) → FinMatrix A n m + remove-row i M k l = M (removeIndex i k) l + + remove-row-comm : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n)) (j : Fin (suc n)) (M : FinMatrix A (suc (suc n)) m) (k : Fin n) (l : Fin m) → + j ≤'Fin i → + remove-row j (remove-row (suc i) M) k l ≡ remove-row i (remove-row (weakenFin j) M) k l + remove-row-comm i j M k l le = + remove-row j (remove-row (suc i) M) k l + ≡⟨ refl ⟩ + M (removeIndex (suc i) (removeIndex j k)) l + ≡⟨ cong (λ a → M a l) ( removeIndexComm j i k le) ⟩ + M (removeIndex (weakenFin j) (removeIndex i k)) l + ≡⟨ refl ⟩ + remove-row i (remove-row (weakenFin j) M) k l + ∎ + + remove-column-row-comm : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n)) (j : Fin (suc m)) (M : FinMatrix A (suc n) (suc m)) (k : Fin n) (l : Fin m) → (remove-row i (remove-column j M)) k l ≡ (remove-column j (remove-row i M)) k l + remove-column-row-comm i j M k l = refl + + -- Calculating of the minor. + minor : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n)) (j : Fin (suc m)) (M : FinMatrix A (suc n) (suc m)) → FinMatrix A n m + minor i j M = remove-column j (remove-row i M) + + -- Compatability of the minor with the equality. + minorComp : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n)) (j : Fin (suc m)) (M N : FinMatrix A (suc n) (suc m)) → ((i : Fin (suc n)) → (j : Fin (suc m)) → M i j ≡ N i j ) → (k : Fin n) → (l : Fin m) → minor i j M k l ≡ minor i j N k l + minorComp {n = suc n} {suc m} i j M N f k l = f (removeIndex i k) (removeIndex j l) + + -- Formulas to commute minors + minorComm0 : {A : Type ℓ} {n m : ℕ} (i₁ i₂ : Fin (suc n)) (j₁ j₂ : Fin (suc m)) (k : Fin n) (l : Fin m) (M : FinMatrix A (suc (suc n)) (suc (suc m))) → + i₂ ≤'Fin i₁ → j₂ ≤'Fin j₁ → + minor i₂ j₂ (minor (suc i₁) (suc j₁) M) k l ≡ minor i₁ j₁ (minor (weakenFin i₂) (weakenFin j₂) M) k l + minorComm0 i₁ i₂ j₁ j₂ k l M lei lej = + M (removeIndex (suc i₁) (removeIndex i₂ k)) + (removeIndex (suc j₁) (removeIndex j₂ l)) + ≡⟨ cong (λ a → M a (removeIndex (suc j₁) (removeIndex j₂ l))) (removeIndexComm i₂ i₁ k lei) ⟩ + M (removeIndex (weakenFin i₂) (removeIndex i₁ k)) + (removeIndex (suc j₁) (removeIndex j₂ l)) + ≡⟨ cong (λ a → M (removeIndex (weakenFin i₂) (removeIndex i₁ k)) a ) ((removeIndexComm j₂ j₁ l lej)) ⟩ + M (removeIndex (weakenFin i₂) (removeIndex i₁ k)) + (removeIndex (weakenFin j₂) (removeIndex j₁ l)) + ∎ + + minorComm1 : {A : Type ℓ} {n m : ℕ} (i₁ i₂ : Fin (suc n)) (j₁ j₂ : Fin (suc m)) (k : Fin n) (l : Fin m) (M : FinMatrix A (suc (suc n)) (suc (suc m))) → + i₂ ≤'Fin i₁ → j₁ ≤'Fin j₂ → + minor i₂ j₂ (minor (suc i₁) (weakenFin j₁) M) k l ≡ minor i₁ j₁ (minor (weakenFin i₂) (suc j₂) M) k l + + minorComm1 i₁ i₂ j₁ j₂ k l M lei lej = + M (removeIndex (suc i₁) (removeIndex i₂ k)) + (removeIndex (weakenFin j₁) (removeIndex j₂ l)) + ≡⟨ cong (λ a → M a (removeIndex (weakenFin j₁) (removeIndex j₂ l))) ((removeIndexComm i₂ i₁ k lei)) ⟩ + M (removeIndex (weakenFin i₂) (removeIndex i₁ k)) + (removeIndex (weakenFin j₁) (removeIndex j₂ l)) + ≡⟨ cong (λ a → M (removeIndex (weakenFin i₂) (removeIndex i₁ k)) a) (sym ((removeIndexComm j₁ j₂ l lej))) ⟩ + M (removeIndex (weakenFin i₂) (removeIndex i₁ k)) + (removeIndex (suc j₂) (removeIndex j₁ l)) + ∎ + + minorComm2 : {A : Type ℓ} {n m : ℕ} (i₁ i₂ : Fin (suc n)) (j₁ j₂ : Fin (suc m)) (k : Fin n) (l : Fin m) (M : FinMatrix A (suc (suc n)) (suc (suc m))) → + i₁ ≤'Fin i₂ → j₂ ≤'Fin j₁ → + minor i₂ j₂ (minor (weakenFin i₁) (suc j₁) M) k l ≡ minor i₁ j₁ (minor (suc i₂) (weakenFin j₂) M) k l + + minorComm2 i₁ i₂ j₁ j₂ k l M lei lej = + M (removeIndex (weakenFin i₁) (removeIndex i₂ k)) + (removeIndex (suc j₁) (removeIndex j₂ l)) + ≡⟨ cong (λ a → M a (removeIndex (suc j₁) (removeIndex j₂ l))) (sym ((removeIndexComm i₁ i₂ k lei))) ⟩ + M (removeIndex (suc i₂) (removeIndex i₁ k)) + (removeIndex (suc j₁) (removeIndex j₂ l)) + ≡⟨ cong (λ a → M (removeIndex (suc i₂) (removeIndex i₁ k)) a) ((removeIndexComm j₂ j₁ l lej)) ⟩ + M (removeIndex (suc i₂) (removeIndex i₁ k)) + (removeIndex (weakenFin j₂) (removeIndex j₁ l)) + ∎ + + --Formulas to compute compute the entries of the minor. + minorIdId : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n))(j : Fin (suc m)) (k : Fin n)(l : Fin m) (M : FinMatrix A (suc n) (suc m)) → + suc k ≤'Fin i → suc l ≤'Fin j → + minor i j M k l ≡ M (weakenFin k) (weakenFin l) + minorIdId i j k l M lei lej = + M (removeIndex i k) (removeIndex j l) + ≡⟨ cong (λ a → M a (removeIndex j l)) (removeIndexId i k lei) ⟩ + M (weakenFin k) (removeIndex j l) + ≡⟨ cong (λ a → M (weakenFin k) a) (removeIndexId j l lej) ⟩ + M (weakenFin k) (weakenFin l) + ∎ + + minorSucSuc : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n))(j : Fin (suc m)) (k : Fin n)(l : Fin m) (M : FinMatrix A (suc n) (suc m)) → + i ≤'Fin weakenFin k → j ≤'Fin weakenFin l → + minor i j M k l ≡ M (suc k) (suc l) + minorSucSuc i j k l M lei lej = + M (removeIndex i k) (removeIndex j l) + ≡⟨ cong (λ a → M a (removeIndex j l)) (removeIndexSuc i k lei) ⟩ + M (suc k) (removeIndex j l) + ≡⟨ cong (λ a → M (suc k) a) (removeIndexSuc j l lej) ⟩ + M (suc k) (suc l) + ∎ + + minorIdSuc : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n))(j : Fin (suc m)) (k : Fin n)(l : Fin m) (M : FinMatrix A (suc n) (suc m)) → + suc k ≤'Fin i → j ≤'Fin weakenFin l → + minor i j M k l ≡ M (weakenFin k) (suc l) + minorIdSuc i j k l M lei lej = + M (removeIndex i k) (removeIndex j l) + ≡⟨ cong (λ a → M a (removeIndex j l)) (removeIndexId i k lei) ⟩ + M (weakenFin k) (removeIndex j l) + ≡⟨ cong (λ a → M (weakenFin k) a) (removeIndexSuc j l lej) ⟩ + M (weakenFin k) (suc l) + ∎ + + minorSucId : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n))(j : Fin (suc m)) (k : Fin n)(l : Fin m) (M : FinMatrix A (suc n) (suc m)) → + i ≤'Fin weakenFin k → suc l ≤'Fin j → + minor i j M k l ≡ M (suc k) (weakenFin l) + minorSucId i j k l M lei lej = + M (removeIndex i k) (removeIndex j l) + ≡⟨ cong (λ a → M a (removeIndex j l)) (removeIndexSuc i k lei) ⟩ + M (suc k) (removeIndex j l) + ≡⟨ cong (λ a → M (suc k) a) (removeIndexId j l lej) ⟩ + M (suc k) (weakenFin l) + ∎ +