Determinant and Adjugate Matrix#1165
Open
FranziskusWiesnet wants to merge 8 commits into
Open
Conversation
added 3 commits
October 30, 2024 14:43
felixwellen
reviewed
Oct 31, 2024
Collaborator
There was a problem hiding this comment.
This looks like accidentally committed files
Author
There was a problem hiding this comment.
Yes. I have removed it.
Collaborator
|
Thanks for opening a PR on this! Determinants would certainly be very useful to have. |
felixwellen
reviewed
Oct 31, 2024
| @@ -0,0 +1,194 @@ | |||
| {-# OPTIONS --cubical #-} | |||
|
|
|||
| module Minor where | |||
Collaborator
There was a problem hiding this comment.
Module names should always be fully qualified, i.e. Cubical.Algebra.Determinant.Minor in this case.
Author
There was a problem hiding this comment.
Thank you! I have fixed it.
added 2 commits
October 31, 2024 13:14
anshwad10
reviewed
Jan 15, 2025
| CommRingR' : CommRingStr (R' .fst) | ||
| CommRingR' = commringstr 0r 1r _+_ _·_ -_ (CommRingStr.isCommRing (snd P')) | ||
|
|
||
| -- Definition of the minor factor |
Contributor
There was a problem hiding this comment.
I noticed that there is some redundancy in the Determinat (is that a typo?) .Base file. MF i is just (- 1r) ^ i (_^_ is defined in Cubical.Algebra.CommRing.Properties, and many of the properties of minor factor you prove are already proved there). And +Compat can by proved more simply by cong₂ _+_.
Author
There was a problem hiding this comment.
Thank you! That could very well be the case. There is certainly a lot to improve here. When I wrote that, I had just started with Agda.
Collaborator
There was a problem hiding this comment.
Sounds right. Can you fix?
…c000fafb882e5b6046408f6993e0" This reverts commit e7aee8949ba8708c0ffbdb8f8d21fbdb13af6153.
Some fixes for your PR on determinants
Collaborator
|
What is the state of this PR? Has all comments been addressed so that it's ready for another round of reviews/merging? |
Collaborator
|
I honestly don't remember - I think I had a discussion with @FranziskusWiesnet which might not have taken place here. At a quick glance I only see |
Author
|
Thanks for checking in! Since this PR has been open for quite some time, I do not remember all details either. Could someone start another round of review? I would be happy to address any remaining issues. |
mortberg
requested changes
May 18, 2026
mortberg
left a comment
mortberg
left a comment
Collaborator
There was a problem hiding this comment.
Many thanks! Lots of good stuff! I had some suggestions for improvements and then it can be merged
| @@ -0,0 +1,1943 @@ | |||
| {-# OPTIONS --safe #-} | |||
Comment on lines
+1
to
+111
| {-# OPTIONS --safe #-} | ||
|
|
||
| module Cubical.Algebra.Determinat.Adjugate where | ||
|
|
||
| open import Cubical.Foundations.Prelude | ||
| open import Cubical.Foundations.Equiv | ||
| open import Cubical.Foundations.Structure using (⟨_⟩) | ||
| open import Cubical.Functions.FunExtEquiv | ||
|
|
||
| open import Cubical.Data.Bool | ||
| open import Cubical.Data.Sum | ||
| 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.Data.Int.Base using (pos; negsuc) | ||
| open import Cubical.Data.Vec.Base using (_∷_; []) | ||
| open import Cubical.Data.Nat.Order | ||
|
|
||
| open import Cubical.Algebra.Matrix | ||
| open import Cubical.Algebra.Matrix.CommRingCoefficient | ||
| 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.Tactics.CommRingSolver | ||
|
|
||
| open import Cubical.Algebra.Determinat.Minor | ||
| open import Cubical.Algebra.Determinat.RingSum | ||
| open import Cubical.Algebra.Determinat.Base | ||
|
|
||
| module Adjugate (ℓ : Level) (P' : CommRing ℓ) where | ||
| open Cubical.Algebra.Determinat.Minor.Minor ℓ | ||
| open Cubical.Algebra.Determinat.RingSum.RingSum ℓ P' | ||
| open RingStr (snd (CommRing→Ring P')) | ||
| open Cubical.Algebra.Determinat.Base.Determinat ℓ P' | ||
| open Coefficient (P') | ||
|
|
||
| private variable | ||
| n m : ℕ | ||
|
|
||
| -- Scalar multiplication | ||
| _∘_ : R → FinMatrix R n m → FinMatrix R n m | ||
| (a ∘ M) i j = a · (M i j) | ||
|
|
||
| opaque | ||
| -- Properties of == | ||
| ==Refl : (k : Fin n) → k == k ≡ true | ||
| ==Refl {n} zero = refl | ||
| ==Refl {suc n} (suc k) = ==Refl {n} k | ||
|
|
||
| ==Sym : (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 | ||
|
|
||
| -- Properties of the Kronecker Delta | ||
| deltaProp : (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 : (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 | ||
|
|
||
| deltaPropEq : (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 : (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 : 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) | ||
|
|
||
| opaque | ||
| -- Behavior of the cofactor matrix under transposition | ||
| cofTransp : (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 : FinMatrix R n n → FinMatrix R n n | ||
| adjugate M i j = cof M j i | ||
|
|
||
| opaque | ||
| -- Behavior of the adjugate matrix under transposition | ||
| adjugateTransp : (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 | ||
|
|
||
| -- Properties of WeakenFin |
Comment on lines
+1
to
+120
| {-# OPTIONS --safe #-} | ||
|
|
||
| module Cubical.Algebra.Determinat.Adjugate where | ||
|
|
||
| open import Cubical.Foundations.Prelude | ||
| open import Cubical.Foundations.Equiv | ||
| open import Cubical.Foundations.Structure using (⟨_⟩) | ||
| open import Cubical.Functions.FunExtEquiv | ||
|
|
||
| open import Cubical.Data.Bool | ||
| open import Cubical.Data.Sum | ||
| 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.Data.Int.Base using (pos; negsuc) | ||
| open import Cubical.Data.Vec.Base using (_∷_; []) | ||
| open import Cubical.Data.Nat.Order | ||
|
|
||
| open import Cubical.Algebra.Matrix | ||
| open import Cubical.Algebra.Matrix.CommRingCoefficient | ||
| 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.Tactics.CommRingSolver | ||
|
|
||
| open import Cubical.Algebra.Determinat.Minor | ||
| open import Cubical.Algebra.Determinat.RingSum | ||
| open import Cubical.Algebra.Determinat.Base | ||
|
|
||
| module Adjugate (ℓ : Level) (P' : CommRing ℓ) where | ||
| open Cubical.Algebra.Determinat.Minor.Minor ℓ | ||
| open Cubical.Algebra.Determinat.RingSum.RingSum ℓ P' | ||
| open RingStr (snd (CommRing→Ring P')) | ||
| open Cubical.Algebra.Determinat.Base.Determinat ℓ P' | ||
| open Coefficient (P') | ||
|
|
||
| private variable | ||
| n m : ℕ | ||
|
|
||
| -- Scalar multiplication | ||
| _∘_ : R → FinMatrix R n m → FinMatrix R n m | ||
| (a ∘ M) i j = a · (M i j) | ||
|
|
||
| opaque | ||
| -- Properties of == | ||
| ==Refl : (k : Fin n) → k == k ≡ true | ||
| ==Refl {n} zero = refl | ||
| ==Refl {suc n} (suc k) = ==Refl {n} k | ||
|
|
||
| ==Sym : (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 | ||
|
|
||
| -- Properties of the Kronecker Delta | ||
| deltaProp : (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 : (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 | ||
|
|
||
| deltaPropEq : (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 : (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 : 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) | ||
|
|
||
| opaque | ||
| -- Behavior of the cofactor matrix under transposition | ||
| cofTransp : (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 : FinMatrix R n n → FinMatrix R n n | ||
| adjugate M i j = cof M j i | ||
|
|
||
| opaque | ||
| -- Behavior of the adjugate matrix under transposition | ||
| adjugateTransp : (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 | ||
|
|
||
| -- Properties of WeakenFin | ||
| weakenPredFinLt : (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 : (k l : Fin (suc (suc n))) → toℕ k <' toℕ l → suc (predFin l) ≡ l |
Comment on lines
+1
to
+972
| {-# OPTIONS --safe #-} | ||
|
|
||
| module Cubical.Algebra.Determinat.Adjugate where | ||
|
|
||
| open import Cubical.Foundations.Prelude | ||
| open import Cubical.Foundations.Equiv | ||
| open import Cubical.Foundations.Structure using (⟨_⟩) | ||
| open import Cubical.Functions.FunExtEquiv | ||
|
|
||
| open import Cubical.Data.Bool | ||
| open import Cubical.Data.Sum | ||
| 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.Data.Int.Base using (pos; negsuc) | ||
| open import Cubical.Data.Vec.Base using (_∷_; []) | ||
| open import Cubical.Data.Nat.Order | ||
|
|
||
| open import Cubical.Algebra.Matrix | ||
| open import Cubical.Algebra.Matrix.CommRingCoefficient | ||
| 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.Tactics.CommRingSolver | ||
|
|
||
| open import Cubical.Algebra.Determinat.Minor | ||
| open import Cubical.Algebra.Determinat.RingSum | ||
| open import Cubical.Algebra.Determinat.Base | ||
|
|
||
| module Adjugate (ℓ : Level) (P' : CommRing ℓ) where | ||
| open Cubical.Algebra.Determinat.Minor.Minor ℓ | ||
| open Cubical.Algebra.Determinat.RingSum.RingSum ℓ P' | ||
| open RingStr (snd (CommRing→Ring P')) | ||
| open Cubical.Algebra.Determinat.Base.Determinat ℓ P' | ||
| open Coefficient (P') | ||
|
|
||
| private variable | ||
| n m : ℕ | ||
|
|
||
| -- Scalar multiplication | ||
| _∘_ : R → FinMatrix R n m → FinMatrix R n m | ||
| (a ∘ M) i j = a · (M i j) | ||
|
|
||
| opaque | ||
| -- Properties of == | ||
| ==Refl : (k : Fin n) → k == k ≡ true | ||
| ==Refl {n} zero = refl | ||
| ==Refl {suc n} (suc k) = ==Refl {n} k | ||
|
|
||
| ==Sym : (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 | ||
|
|
||
| -- Properties of the Kronecker Delta | ||
| deltaProp : (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 : (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 | ||
|
|
||
| deltaPropEq : (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 : (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 : 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) | ||
|
|
||
| opaque | ||
| -- Behavior of the cofactor matrix under transposition | ||
| cofTransp : (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 : FinMatrix R n n → FinMatrix R n n | ||
| adjugate M i j = cof M j i | ||
|
|
||
| opaque | ||
| -- Behavior of the adjugate matrix under transposition | ||
| adjugateTransp : (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 | ||
|
|
||
| -- Properties of WeakenFin | ||
| weakenPredFinLt : (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 : (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 : (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 : (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 : (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 : (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)))))) | ||
| (weakenRespToℕ 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 : (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 → | ||
| distributeOne | ||
| (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))))) | ||
| (weakenRespToℕ 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 : (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 : {j : Fin (suc n)} → (i : Fin (suc n)) → toℕ i <' toℕ j → Fin n |
Collaborator
There was a problem hiding this comment.
Also, "strongen" should probably be "strengthen"?
| (det M ∘ 𝟙) k l | ||
| ∎ | ||
|
|
||
| FinCompare : {n : ℕ} → (k l : Fin n) → (k ≡ l) ⊎ ((toℕ k <' toℕ l) ⊎ (toℕ l <' toℕ k)) |
Comment on lines
+1
to
+52
| {-# OPTIONS --safe #-} | ||
|
|
||
| module Cubical.Algebra.Determinat.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 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 |
Comment on lines
+69
to
+85
| 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 |
Collaborator
There was a problem hiding this comment.
Long line. There are other examples in this file as well
| @@ -0,0 +1,349 @@ | |||
| {-# OPTIONS --cubical #-} | |||
Comment on lines
+1
to
+2
| {-# OPTIONS --cubical #-} | ||
| {-# OPTIONS --safe #-} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
In the four new files, the determinant of a matrix over a commutative ring is introduced through Laplace expansion, and it is proven that the adjugate matrix multiplied by the matrix itself equals the determinant times the identity matrix.
Additionally, it is shown that the determinant is independent of the row or column chosen for expansion, along with a few other minor properties of the determinant.
I am happy to consider any improvements.