Comments added

agda · Oct 30, 2024 · 67c51a8 · 67c51a8
1 parent fdc24bb
commit 67c51a8
Show file tree

Hide file tree

Showing 3 changed files with 62 additions and 235 deletions.
diff --git a/Cubical/Algebra/Determinat/adjugate.agda b/Cubical/Algebra/Determinat/adjugate.agda
@@ -39,17 +39,11 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
   open Determinat ℓ P'
   open Coefficient (P')
 
+  -- Scalar multiplication
   _∘_ : {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
-
+  -- Properties of ==
   ==Refl : {n : ℕ} → (k : Fin n) → k == k ≡ true
   ==Refl {n} zero = refl
   ==Refl {suc n} (suc k) = ==Refl {n} k
@@ -60,6 +54,15 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
   ==Sym {suc n} (suc k) zero = refl
   ==Sym {suc n} (suc k) (suc l) = ==Sym {n} k l
 
+  -- Properties of the Kronecker Delta
+  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
+
   deltaPropEq : {n : ℕ} → (k l : Fin n) → k ≡ l → δ k l ≡ 1r
   deltaPropEq k l e =
     δ k l
@@ -71,12 +74,12 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
 
   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)
 
+  -- Behavior of the cofactor matrix under transposition
   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 ᵗ))
@@ -92,10 +95,11 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
   adjugate : {n : ℕ} → FinMatrix R n n → FinMatrix R n n
   adjugate M i j = cof M j i
 
+  -- Behavior of the adjugate matrix under transposition
   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
 
-
+  -- Properties of WeakenFin
   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 ())
@@ -109,6 +113,7 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
   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 →
    ∑
@@ -612,7 +617,7 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
            (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
+        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 ·
@@ -1506,7 +1511,7 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
             minor k i M (strongenFin l le) j
             · det (minor (strongenFin l le) j (minor k i M)))))
       (λ i j →
-        DetRowAux2
+        distributeOne
         (ind> (toℕ i) (toℕ j))
         ( M l i · MF (toℕ k +ℕ toℕ i) ·
             (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
@@ -1828,8 +1833,6 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
     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)) )
@@ -1840,7 +1843,7 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
     ≡⟨ 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
@@ -1851,7 +1854,8 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
   ... | inr (inl x) = inr (inl (s≤s x))
   ... | inr (inr x) = inr (inr (s≤s x))
 
-
+  -- The adjugate matrix divided by the determinant is the right inverse.
+  -- Component-wise version
   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
@@ -1890,6 +1894,8 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
   ... | inr (inl x) = adjugateInvRLcomponent M k l x
   ... | inr (inr x) =  adjugateInvRGcomponent M k l x
 
+  -- The adjugate matrix divided by the determinant is the left inverse.
+  -- Component-wise version
   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
@@ -1917,9 +1923,10 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
     (det M · 𝟙 k l)
     ∎
 
-
+  -- The adjugate matrix divided by the determinant is the right inverse.
   adjugateInvR : {n : ℕ} → (M : FinMatrix R n n)  → M ⋆ adjugate M ≡  det M ∘ 𝟙
   adjugateInvR M = funExt₂ (λ k l →  adjugateInvRComp M k l)
 
+  -- The adjugate matrix divided by the determinant is the left inverse.
   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
@@ -42,7 +42,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
   MF zero = 1r
   MF (suc i) = (- 1r) · (MF i)
 
-  --Multiplicity of the minor factor
+  --Properties of the minor factor
   sumMF : (i j : ℕ) → MF (i +ℕ j) ≡ (MF i) · (MF j)
   sumMF zero j =
     MF j
@@ -63,6 +63,30 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
   sucMFRev : (i : ℕ) → MF i ≡ (- 1r) · MF (suc i)
   sucMFRev i = solve! P'
 
+  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)
+    ∎
+
+  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)
+    ∎
+
+  -- Other small lemmata
   +Compat : {a b c d : R} → a ≡ b → c ≡ d → a + c ≡ b + d
   +Compat {a} {b} {c} {d} eq1 eq2 =
    a + c
@@ -71,6 +95,9 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
    ≡⟨ cong (λ x → b + x) eq2 ⟩
    b + d
    ∎
+
+  distributeOne : (a b : R) → b ≡ a · b + (1r + (- a)) · b
+  distributeOne a b = solve! P'
 
   -- Definition of the determinat by using Laplace expansion
   det : ∀ {n} → FinMatrix R n n → R
@@ -164,9 +191,6 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
       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))) → 
@@ -952,7 +976,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
              minor (suc k) i M zero j
              · det (minor zero j (minor (suc k) i M))))
         (λ i j →
-          DetRowAux2 (ind> (toℕ i) (toℕ j))
+          distributeOne (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))))
     ⟩
@@ -1152,7 +1176,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
          · det (minor k z₁ (minor zero z M)))
      (λ i j →
        sym
-       (DetRowAux2
+       (distributeOne
        (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)))))
@@ -1338,7 +1362,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
           det (minor i zero (minor zero (suc j) M))))
        ∎)
 
-
+  -- The determinant can also be expanded along the first column.
   DetRowColumn : ∀ {n} →  (M : FinMatrix R (suc n) (suc n)) →
      detC zero M ≡ det M
   DetRowColumn {zero} M = refl
@@ -1960,20 +1984,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
         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)
-    ∎
-
+  -- The determinant expanded along a column is independent of the chosen column.
   DetColumnZero : ∀ {n} → (k : Fin (suc n)) → (M : FinMatrix R (suc n) (suc n)) →
     detC k M ≡ detC zero M
   DetColumnZero {zero} zero M = refl
@@ -2046,7 +2057,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
            (MF (toℕ z₁ +ℕ zero) · minor z (suc k) M z₁ zero ·
             det (minor z₁ zero (minor z (suc k) M)))))
       (λ i j →
-        DetRowAux2
+        distributeOne
           (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 ·
@@ -2285,7 +2296,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
              (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) )
+                (distributeOne ( 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))))))) ⟩
@@ -2388,6 +2399,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
     detC zero M
     ∎
 
+  -- The determinant expanded along a column is the regular determinant.
   DetColumn : ∀ {n} → (k : Fin (suc n)) → (M : FinMatrix R (suc n) (suc n)) →
     detC k M ≡ det M
   DetColumn k M =
@@ -2405,6 +2417,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
   ∑Mul1r = Sum.∑Mul1r (CommRing→Ring P')
   ∑Mulr1 = Sum.∑Mulr1 (CommRing→Ring P')
 
+  -- The determinant of the zero matrix is 0.
   detZero : {n : ℕ} → det {suc n} 𝟘 ≡ 0r
   detZero {n} =
     ∑Zero
@@ -2421,6 +2434,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
         ∎
         )
 
+  --The determinant of the identity matrix is 1.
   detOne : {n : ℕ} → det {n} 𝟙 ≡ 1r
   detOne {zero} = refl
   detOne {suc n} =
@@ -2454,15 +2468,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
     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)
-    ∎
-
+  --The determinant remains unchanged under transposition.
   detTransp : {n : ℕ} → (M : FinMatrix R n n) → det M ≡ det (M ᵗ)
   detTransp {zero} M = refl
   detTransp {suc n} M =