Skip to content

Commit

Permalink
Refactor classes
Browse files Browse the repository at this point in the history
  • Loading branch information
@valis
valis committed Feb 21, 2024
1 parent 9f2ebd4 commit cbb33d5
Show file tree
Hide file tree
Showing 55 changed files with 456 additions and 458 deletions.
6 changes: 3 additions & 3 deletions meta/src/main/java/org/arend/lib/meta/SIPMeta.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,9 +37,9 @@ public class SIPMeta extends BaseMetaDefinition {
@Dependency(module = "Category", name = "Map.cod") public CoreClassField mapCod;
@Dependency(module = "Category", name = "Map.f") public CoreClassField mapFunc;
@Dependency(module = "Category") public CoreClassDefinition Iso;
@Dependency(module = "Category", name = "Iso.inv") public CoreClassField isoInv;
@Dependency(module = "Category", name = "Iso.f_inv") public CoreClassField isoFuncInv;
@Dependency(module = "Category", name = "Iso.inv_f") public CoreClassField isoInvFunc;
@Dependency(module = "Category", name = "Iso.hinv") public CoreClassField isoInv;
@Dependency(module = "Category", name = "Iso.f_hinv") public CoreClassField isoFuncInv;
@Dependency(module = "Category", name = "Iso.hinv_f") public CoreClassField isoInvFunc;
@Dependency(module = "Category", name = "Precat.Ob") public CoreClassField catOb;
@Dependency(module = "Category", name = "Precat.Hom") public CoreClassField catHom;
@Dependency(module = "Category", name = "Precat.id") public CoreClassField catId;
Expand Down
30 changes: 15 additions & 15 deletions src/AG/Scheme.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -189,12 +189,12 @@
| trans => homMap p
| natural h => inv M.R.F.Func-o *> pmap M.R.F.Func prop-pi *> M.R.F.Func-o

\func natTrans-inv {L M : RingedLocale} {e : Iso {RingedLocalePrecat} {L} {M}} (f : NatTrans L.R (Comp M.R (Functor.op {FrameHom.functor {e.inv}})))
\func natTrans-inv {L M : RingedLocale} {e : Iso {RingedLocalePrecat} {L} {M}} (f : NatTrans L.R (Comp M.R (Functor.op {FrameHom.functor {e.hinv}})))
: NatTrans (Comp L.R (Functor.op {FrameHom.functor {e.f}})) M.R \cowith
| trans x => homMap e.f_inv x Cat.∘ f (e.f x)
| trans x => homMap e.f_hinv x Cat.∘ f (e.f x)
| natural {a} {b} h =>
\let t : homMap e.f_inv b Cat.∘ M.R.F.Func (Func {Functor.op {FrameHom.functor {e.inv}}} (func-<= {e.f} h)) = M.R.F.Func h Cat.∘ homMap e.f_inv a
=> pmap (_ Cat.∘ M.R.F.Func __) prop-pi *> natural {homMap-natural e.f_inv} h *> pmap (Cat.`∘ _) (pmap M.R.F.Func prop-pi)
\let t : homMap e.f_hinv b Cat.∘ M.R.F.Func (Func {Functor.op {FrameHom.functor {e.hinv}}} (func-<= {e.f} h)) = M.R.F.Func h Cat.∘ homMap e.f_hinv a
=> pmap (_ Cat.∘ M.R.F.Func __) prop-pi *> natural {homMap-natural e.f_hinv} h *> pmap (Cat.`∘ _) (pmap M.R.F.Func prop-pi)
\in unfold Func $ rewrite (prop-isProp (Func {Functor.op {FrameHom.functor {e.f}}} h) (func-<= {e.f} h)) $ o-assoc *> rewrite (f.natural (func-<= {e.f} h)) (inv o-assoc *> path (\lam i => t i Cat.∘ f (e.f a)) *> o-assoc)

\lemma homMap_o {L L' : RingedLocale} (f : RingedLocaleHom L L') (g : RingedLocaleHom L' L) (p : f RingedLocalePrecat.∘ g = id L') (q : g RingedLocalePrecat.∘ f = id L) (a : L')
Expand All @@ -211,10 +211,10 @@
=> o-assoc *> rewrite (homMap_o f g p q a) (homMap-lem2 p a)

\func fromIso {L L' : RingedLocale} (e : Iso {RingedLocalePrecat} {L} {L'}) : Iso {VSheafCat CRingCat L'.L} {VSheaf.direct_image_locale e.f L.R} {L'.R} \cowith
| f => natTrans-inv (RingedLocaleHom.f# {e.inv})
| inv => RingedLocaleHom.f# {e.f}
| inv_f => exts (homMap_o-right e.f e.inv e.f_inv e.inv_f)
| f_inv => exts (homMap_o-left e.f e.inv e.f_inv e.inv_f)
| f => natTrans-inv (RingedLocaleHom.f# {e.hinv})
| hinv => RingedLocaleHom.f# {e.f}
| hinv_f => exts (homMap_o-right e.f e.hinv e.f_hinv e.hinv_f)
| f_hinv => exts (homMap_o-left e.f e.hinv e.f_hinv e.hinv_f)

\func isotoid (e : Iso {RingedLocalePrecat}) : e.dom = e.cod
=> ext (Cat.isotoid (RingedLocalePrecat.forget.Func-iso e), VSheaf.transport_direct_image-iso _ (RingedLocale.R {e.dom}) *> Cat.isotoid (RingedLocalePrecat.fromIso e))
Expand Down Expand Up @@ -450,14 +450,14 @@
\where {
\func locale_iso {L : Locale} : Iso {LocaleCat} {L.restrict L.top} {L} \cowith
| f => Locale.restrict.map
| inv => \new FrameHom {
| hinv => \new FrameHom {
| func x => x.1
| func-top => idp
| func-meet => idp
| func-Join => idp
}
| inv_f => exts $ \lam p => ext L.top-right
| f_inv => exts $ \lam x => L.top-right
| hinv_f => exts $ \lam p => ext L.top-right
| f_hinv => exts $ \lam x => L.top-right

\func restrict_map {L : Locale} (a : L) (S : VSheaf CRingCat L) : RingedLocaleHom (\new RingedLocale (L.restrict a) (VSheaf.restrict a S)) (\new RingedLocale L S) \cowith
| f => Locale.restrict.map
Expand All @@ -468,13 +468,13 @@

\func restrict_iso {L : Locale} (S : VSheaf CRingCat L) : Iso {RingedLocalePrecat} {VSheaf.restrict L.top S} {S} \cowith
| f => restrict_map L.top S
| inv : RingedLocaleHom => \new RingedLocaleHom S (VSheaf.restrict L.top S) {
| f => locale_iso.inv
| hinv : RingedLocaleHom => \new RingedLocaleHom S (VSheaf.restrict L.top S) {
| f => locale_iso.hinv
| f# => \new NatTrans {
| trans p => id _
| natural h => id-left *> pmap S.F.Func prop-pi *> Paths.inv id-right
}
}
| inv_f => RingedLocaleHom.ext (inv RingedLocalePrecat.∘ restrict_map L.top S) _ locale_iso.inv_f $ \lam p x => pmap (S.F.Func __ x) prop-pi
| f_inv => RingedLocaleHom.ext (restrict_map L.top S RingedLocalePrecat.∘ inv) _ locale_iso.f_inv $ \lam a x => pmap (S.F.Func __ x) prop-pi
| hinv_f => RingedLocaleHom.ext (hinv RingedLocalePrecat.∘ restrict_map L.top S) _ locale_iso.hinv_f $ \lam p x => pmap (S.F.Func __ x) prop-pi
| f_hinv => RingedLocaleHom.ext (restrict_map L.top S RingedLocalePrecat.∘ hinv) _ locale_iso.f_hinv $ \lam a x => pmap (S.F.Func __ x) prop-pi
}
2 changes: 1 addition & 1 deletion src/Algebra/Algebra.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
\import Algebra.Ring.RingHom
\import Paths

\class AAlgebra \extends Ring, LModule {
\class AAlgebra \extends LModule, Ring {
\override R : CRing
| *c-comm-left {r : R} {a b : E} : r *c (a * b) = (r *c a) * b
| *c-comm-right {r : R} {a b : E} : r *c (a * b) = a * (r *c b)
Expand Down
2 changes: 1 addition & 1 deletion src/Algebra/Group/Symmetric.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@
| *-assoc => Sym.equals $ \lam j => idp
| inverse e => symQEquiv e
| inverse-left => Sym.equals Equiv.f_ret
| inverse-right => Sym.equals Equiv.ret_f
| inverse-right => Sym.equals ret_f
\where {
\func inv-isEquiv {n : Nat} : QEquiv {Sym n} {Sym n} \cowith
| f e => symQEquiv e
Expand Down
22 changes: 11 additions & 11 deletions src/Algebra/Linear/Matrix.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -117,15 +117,15 @@
| negative M => mkMatrix $ \lam i j => negative (M i j)
| negative-left => matrixExt $ \lam i j => negative-left

\instance MatrixModule (R : Ring) (n m : Nat) : LModule' R \cowith
\instance MatrixModule (R : Ring) (n m : Nat) : LModule R \cowith
| AbGroup => MatrixAbGroup R n m
| *c a M => mkMatrix $ \lam i j => a * M i j
| *c-assoc => matrixExt $ \lam i j => *-assoc
| *c-ldistr => matrixExt $ \lam i j => ldistr
| *c-rdistr => matrixExt $ \lam i j => rdistr
| ide_*c => matrixExt $ \lam i j => ide-left
\where {
\func *c-gen {R : Ring} {M : LModule' R} (a : R) {n m : Nat} (A : Matrix M n m) : Matrix M n m
\func *c-gen {R : Ring} {M : LModule R} (a : R) {n m : Nat} (A : Matrix M n m) : Matrix M n m
=> mkMatrix $ \lam i j => a *c A i j
}

Expand Down Expand Up @@ -153,13 +153,13 @@
\where {
\open AddMonoid

\func product-gen {R : Ring} {L : LModule' R} {n m k : Nat} (M : Matrix R n m) (N : Matrix L m k) : Matrix L n k
\func product-gen {R : Ring} {L : LModule R} {n m k : Nat} (M : Matrix R n m) (N : Matrix L m k) : Matrix L n k
=> mkMatrix $ \lam i k => BigSum $ \lam j => M i j *c N j k

\func \infixl 7 product {R : Ring} {n m k : Nat} (M : Matrix R n m) (N : Matrix R m k) : Matrix R n k
=> mkMatrix $ \lam i k => BigSum $ \lam j => M i j * N j k

\lemma product-gen_ide-left {R : Ring} {M : LModule' R} {n m : Nat} (A : Matrix M n m) : product-gen ide A = A
\lemma product-gen_ide-left {R : Ring} {M : LModule R} {n m : Nat} (A : Matrix M n m) : product-gen ide A = A
=> matrixExt $ \lam i j => BigSum-unique i (\lam k i/=k => later $ rewrite (decideEq/=_reduce i/=k) M.*c_zro-left) *> rewrite (decideEq=_reduce idp) M.ide_*c

\lemma product_ide-left {R : Ring} {n m : Nat} {A : Matrix R n m} : ide product A = A
Expand All @@ -174,39 +174,39 @@
\lemma product_zro-right {R : Ring} {n m k : Nat} (A : Matrix R n m) : A product zro = {Matrix R n k} zro
=> matrixExt \lam i j => BigSum_zro \lam k => zro_*-right

\lemma product-gen-assoc {R : Ring} {M : LModule' R} {n m k l : Nat} {A : Matrix R n m} {B : Matrix R m k} {C : Matrix M k l} : product-gen (A product B) C = product-gen A (product-gen B C)
\lemma product-gen-assoc {R : Ring} {M : LModule R} {n m k l : Nat} {A : Matrix R n m} {B : Matrix R m k} {C : Matrix M k l} : product-gen (A product B) C = product-gen A (product-gen B C)
=> matrixExt $ \lam j1 j2 => path (\lam i => BigSum (\lam j3 => M.*c_BigSum-rdistr {\lam j4 => A j1 j4 * B j4 j3} {C j3 j2} i)) *>
M.BigSum-transpose _ *> pmap BigSum (arrayExt $ \lam j3 => pmap BigSum $ arrayExt $ \lam j4 => *c-assoc) *>
inv (path (\lam i => BigSum (\lam j3 => M.*c_BigSum-ldistr {A j1 j3} {\lam j4 => B j3 j4 *c C j4 j2} i)))

\lemma product-assoc {R : Ring} {n m k l : Nat} (A : Matrix R n m) (B : Matrix R m k) (C : Matrix R k l) : A product B product C = A product (B product C)
=> product-gen-assoc {_} {RingLModule R}

\lemma product-gen-ldistr {R : Ring} {M : LModule' R} {n m k : Nat} {A : Matrix R n m} {B C : Matrix M m k} : product-gen A (B + C) = product-gen A B + product-gen A C
\lemma product-gen-ldistr {R : Ring} {M : LModule R} {n m k : Nat} {A : Matrix R n m} {B C : Matrix M m k} : product-gen A (B + C) = product-gen A B + product-gen A C
=> matrixExt $ \lam i j => pmap BigSum (arrayExt $ \lam k => *c-ldistr) *> M.BigSum_+

\lemma product-ldistr {R : Ring} {n m k : Nat} {A : Matrix R n m} {B C : Matrix R m k} : A product (B + C) = A product B + A product C
=> product-gen-ldistr {_} {RingLModule R}

\lemma product-gen-rdistr {R : Ring} {M : LModule' R} {n m k : Nat} (A B : Matrix R n m) {C : Matrix M m k} : product-gen (A + B) C = product-gen A C + product-gen B C
\lemma product-gen-rdistr {R : Ring} {M : LModule R} {n m k : Nat} (A B : Matrix R n m) {C : Matrix M m k} : product-gen (A + B) C = product-gen A C + product-gen B C
=> matrixExt $ \lam i j => pmap BigSum (arrayExt $ \lam k => *c-rdistr) *> M.BigSum_+

\lemma product-rdistr {R : Ring} {n m k : Nat} (A B : Matrix R n m) {C : Matrix R m k} : (A + B) product C = A product C + B product C
=> product-gen-rdistr {_} {RingLModule R} A B

\lemma product-gen_negative-left {R : Ring} {L : LModule' R} {n m k : Nat} (M : Matrix R n m) (N : Matrix L m k) : product-gen (negative M) N = negative (product-gen M N)
\lemma product-gen_negative-left {R : Ring} {L : LModule R} {n m k : Nat} (M : Matrix R n m) (N : Matrix L m k) : product-gen (negative M) N = negative (product-gen M N)
=> matrixExt $ \lam i j => pmap BigSum (arrayExt $ \lam k => L.*c_negative-left) *> inv L.BigSum_negative

\lemma product_negative-left {R : Ring} {n m k : Nat} {M : Matrix R n m} {N : Matrix R m k} : negative M product N = negative (M product N)
=> product-gen_negative-left {_} {RingLModule R} _ _

\lemma product-gen_negative-right {R : Ring} {L : LModule' R} {n m k : Nat} (M : Matrix R n m) (N : Matrix L m k) : product-gen M (negative N) = negative (product-gen M N)
\lemma product-gen_negative-right {R : Ring} {L : LModule R} {n m k : Nat} (M : Matrix R n m) (N : Matrix L m k) : product-gen M (negative N) = negative (product-gen M N)
=> matrixExt $ \lam i j => pmap BigSum (arrayExt $ \lam k => L.*c_negative-right) *> inv L.BigSum_negative

\lemma product_negative-right {R : Ring} {n m k : Nat} {M : Matrix R n m} {N : Matrix R m k} : M product negative N = negative (M product N)
=> product-gen_negative-right {_} {RingLModule R} _ _

\lemma product-gen_negative-rdistr {R : Ring} {M : LModule' R} {n m k : Nat} (A B : Matrix R n m) {C : Matrix M m k} : product-gen (A - B) C = product-gen A C - product-gen B C
\lemma product-gen_negative-rdistr {R : Ring} {M : LModule R} {n m k : Nat} (A B : Matrix R n m) {C : Matrix M m k} : product-gen (A - B) C = product-gen A C - product-gen B C
=> product-gen-rdistr A (negative B) *> pmap (product-gen A C +) (product-gen_negative-left B C)

\lemma ide_generates {R : Ring} {n : Nat} : LModule.IsGenerated {ArrayLModule n (RingLModule R)} ide
Expand Down Expand Up @@ -575,7 +575,7 @@
- Indeed, if we take `R := S[X]`, `M := S^n` with `p *c U := p(B) * U`, and `A := X *c ide - B`, then `A * U = 0` for all `U`.
- Let `p := charPoly B` (which is equal to `determinant A`). Then `p(B) * U = p *c U = 0` for all `U`, which implies `p(B) = 0`.
-}
\lemma equations-determinant {R : CRing} {M : LModule' R} {n k : Nat} (A : Matrix R n n) {U : Matrix M n k}
\lemma equations-determinant {R : CRing} {M : LModule R} {n k : Nat} (A : Matrix R n n) {U : Matrix M n k}
(p : product-gen A U = 0) : MatrixModule.*c-gen (determinant A) U = 0
=> \have | r : product-gen (adjugate A) 0 = 0 => matrixExt $ \lam i j => M.BigSum_zro $ \lam k => M.*c_zro-right
| t : product-gen (determinant A *c ide) U = 0
Expand Down
2 changes: 1 addition & 1 deletion src/Algebra/Linear/Matrix/CayleyHamilton.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@
rewrite (decideEq=_reduce idp) (exts \lam k => simplify (R.BigSum-unique i (\lam j i/=j => later $ rewrite (decideEq/=_reduce i/=j) (pmap (_ *) (simplify $ R.BigSum_zro \lam _ => R.zro_*-right) *> R.zro_*-right)) *> later (rewrite (decideEq=_reduce idp, decideEq=_reduce idp) (pmap (_ *) (simplify $ pmap (`+ _) (R.BigSum_zro \lam _ => R.zro_*-right) *> zro-left) *> ide-right *> inv zro-left *> inv (pmap2 (+) (R.BigSum_zro \lam _ => R.zro_*-right) ide-right))) *> inv (R.BigSum-unique k (\lam j k/=j => later $ rewrite (decideEq/=_reduce (/=-sym k/=j)) $ simplify $ R.BigSum_zro \lam _ => R.zro_*-right))) *> inv ArrayLModule.BigSum-index))
\in matrixExt (poly_func_matrix (charPoly A) A) *> pmap toMatrix t
\where {
\func toLinearMap {R : CRing} {n m : Nat} (A : Matrix R n m) : LinearMap' (ArrayFinModule n) (ArrayFinModule m) \cowith
\func toLinearMap {R : CRing} {n m : Nat} (A : Matrix R n m) : LinearMap (ArrayFinModule n) (ArrayFinModule m) \cowith
| func u => \lam j => R.BigSum \lam i => A i j * u i
| func-+ => exts \lam j => pmap R.BigSum (exts \lam i => R.ldistr) *> R.BigSum_+
| func-*c => exts \lam j => pmap R.BigSum (exts \lam i => equation) *> inv R.BigSum-ldistr
Expand Down
24 changes: 10 additions & 14 deletions src/Algebra/Linear/VectorSpace.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
\import Category
\import Data.Array
\import Data.Or
\import Equiv (Equiv)
\import Equiv
\import Function (Image)
\import Function.Meta
\import Logic
Expand All @@ -35,18 +35,14 @@
\import Relation.Equivalence
\import Set
\import Set.Fin
\open LModule
\open LModule \hiding (count)

\class VectorSpace \extends LModule {
\override R : DiscreteField
}

\class FinVectorSpace \extends VectorSpace, FinModule

\meta VectorSpace' K => VectorSpace { | R => K }

\meta FinVectorSpace' K => FinVectorSpace { | R => K }

\func rank {R : SmithDomain} {n m : Nat} (A : Matrix R n m) : Nat
=> firstNonZero (rank-array A).1
\where {
Expand Down Expand Up @@ -123,14 +119,14 @@
\lemma rank<=columns {R : SmithDomain} {n m : Nat} {A : Matrix R n m} : rank A <= m
=> rank.firstNonZero<=len <=∘ meet-right

\lemma smith-bases {R : SmithDomain} {U V : LModule' R} {lu : Array U} (bu : U.IsBasis lu) {lv : Array V} (bv : V.IsBasis lv) (f : LinearMap' U V)
\lemma smith-bases {R : SmithDomain} {U V : LModule R} {lu : Array U} (bu : U.IsBasis lu) {lv : Array V} (bv : V.IsBasis lv) (f : LinearMap U V)
: ∃ (lu' : Array U lu.len) (U.IsBasis lu') (lv' : Array V lv.len) (bv' : V.IsBasis lv') (d : Array R lu.len)
(\Pi (j : Fin lu.len) -> f (lu' j) = d j *c fit V.zro lv' j)
(\Pi (j : Fin lu.len) -> (d j = 0) <-> rank (toMatrix lu' bv' f) <= j)
=> \have | (inP (B, Bs, A~B)) => R.toSmith (toMatrix lu bv f)
| (inP Bs2) => IsSmith.smith-diag-func Bs
| (inP (lu',lv',bu',bv',p)) => M~_toLinearMap bu bv A~B
| q : f = toLinearMap bu' lv' B => inv (Equiv.ret_f {matrix-equiv bu bv} f) *> p
| q : f = toLinearMap bu' lv' B => inv (ret_f {matrix-equiv bu bv} f) *> p
\in inP (lu', bu', lv', bv', \lam j =>
\case LinearOrder.dec<_<= j lv.len \with {
| inl p => B j (toFin j p)
Expand All @@ -147,20 +143,20 @@
\open LinearMap
\open Monoid

\lemma M~_toLinearMap {R : Ring} {U V : LModule' R} {lu : Array U} {lv : Array V} (bu : U.IsBasis lu) (bv : V.IsBasis lv) {A B : Matrix R lu.len lv.len} (A~B : A M~ B)
\lemma M~_toLinearMap {R : Ring} {U V : LModule R} {lu : Array U} {lv : Array V} (bu : U.IsBasis lu) (bv : V.IsBasis lv) {A B : Matrix R lu.len lv.len} (A~B : A M~ B)
: ∃ (lu' : Array U lu.len) (lv' : Array V lv.len) (bu' : U.IsBasis lu') (bv' : V.IsBasis lv') (toLinearMap bu lv A = toLinearMap bu' lv' B)
=> \let | (inP (C : Inv, D : Inv, A=CBD)) => ~-symmetric A~B
| t => pmap (toLinearMap bu lv) A=CBD *> toLinearMap_* (C.val MatrixRing.product B) D.val bu bv bv *> pmap (_ ∘ {LModuleCat R}) (toLinearMap_* C.val B bu bu bv) *> pmap (_ ∘ {LModuleCat R}) (change-basis-right (toLinearMapIso bu bu C) bu bv B) *> change-basis-left (toLinearMap bv lv D.val) (iso-basis (Iso.reverse {toLinearMapIso bu bu C}) bu) bv B
\in inP (_, _, _, iso-basis (toLinearMapIso bv bv D) bv, t)
}

\instance image-fin {R : SmithDomain} {U V : FinModule' R} (f : LinearMap' U V) : FinModule
\instance image-fin {R : SmithDomain} {U V : FinModule R} (f : LinearMap U V) : FinModule
| LModule => ImageLModule f
| isFinModule => \case U.isFinModule, V.isFinModule \with {
| inP (lu,bu), inP (lv,bv) => TruncP.map (basis f bu bv) \lam s => (s.1,s.2)
}
\where {
\protected \lemma basis {U V : LModule' R} (f : LinearMap' U V) {lu' : Array U} (bu' : U.IsBasis lu') {lv' : Array V} (bv' : V.IsBasis lv')
\protected \lemma basis {U V : LModule R} (f : LinearMap U V) {lu' : Array U} (bu' : U.IsBasis lu') {lv' : Array V} (bv' : V.IsBasis lv')
: ∃ (l : Array (Image f)) (IsBasis {ImageLModule f} l) (l.len = rank (LinearMap.toMatrix lu' bv' f))
=> \let | (inP (lu, bu, lv, bv, d, g, d0)) => smith-bases bu' bv' f
| r => rank (LinearMap.toMatrix lu bv f)
Expand All @@ -179,13 +175,13 @@
\lam j r<=j => func-*c *> pmap (_ *c) (g j *> pmap (`*c _) ((d0 j).2 r<=j) *> *c_zro-left) *> *c_zro-right) *> inv (AddMonoidHom.func-BigSum {ImageLModuleRightHom f}))),
rank.rank_M~ $ LinearMap.change-basis_M~ f bu bu' bv bv')

\lemma dimension_rank {f : LinearMap' U V} {lu : Array U} (bu : U.IsBasis lu) {lv : Array V} (bv : V.IsBasis lv) : FinModule.dimension (image-fin f) = rank (LinearMap.toMatrix lu bv f)
\lemma dimension_rank {f : LinearMap U V} {lu : Array U} (bu : U.IsBasis lu) {lv : Array V} (bv : V.IsBasis lv) : FinModule.dimension (image-fin f) = rank (LinearMap.toMatrix lu bv f)
=> \case basis f bu bv \with {
| inP (li,bi,p) => FinModule.dimension-unique bi *> p
}
}

\instance kernel-fin {R : SmithDomain} {U V : FinModule' R} (f : LinearMap' U V) : FinModule
\instance kernel-fin {R : SmithDomain} {U V : FinModule R} (f : LinearMap U V) : FinModule
| LModule => KerLModule f
| isFinModule => \case U.isFinModule, V.isFinModule \with {
| inP (_,bu'), inP (_,bv') => \case smith-bases bu' bv' f \with {
Expand Down Expand Up @@ -223,7 +219,7 @@
}
}

\func dependency-dec {R : SmithDomain} {U : FinModule' R} (l : Array U) : Or (U.IsDependent l) (U.IsIndependent l)
\func dependency-dec {R : SmithDomain} {U : FinModule R} (l : Array U) : Or (U.IsDependent l) (U.IsIndependent l)
=> \let K => kernel-fin {R} {ArrayFinModule l.len} (arrayLinearMap l)
\in cases (FinModule.dimension {R} K arg addPath) \with {
| 0, p => inr $ arrayLinearMap.inj-char.1 $ (kernel=0<->inj {arrayLinearMap l}).2 (FinModule.dimension=0.1 p)
Expand Down
Loading

0 comments on commit cbb33d5

Please sign in to comment.