- -

Library mathcomp.algebra.vector

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

Finite dimensional vector spaces

- - vectType R == interface structure for finite dimensional (more - precisely, detachable) vector spaces over R, which - should be at least a ringType. - Vector.axiom n M <-> type M is linearly isomorphic to 'rV_n. - := {v2r : M -> 'rV_n| linear v2r & bijective v2r}. - VectMixin isoM == packages a proof isoV of Vector.axiom n M as the - vectType mixin for an n-dimensional R-space - structure on a type M that is an lmodType R. - VectType K M mT == packs the vectType mixin mT to into a vectType K - instance for T; T should have an lmodType K - canonical instance. - [vectType R of T for vS] == a copy of the vS : vectType R structure where - the sort is replaced by T; vS : lmodType R should - be convertible to a canonical lmodType for T. - [vectType R of V] == a clone of an existing vectType R structure on V. - {vspace vT} == the type of (detachable) subspaces of vT; vT - should have a vectType structure over a fieldType. - subvs_of U == the subtype of elements of V in the subspace U. - This is canonically a vectType. - vsval u == linear injection of u : subvs_of U into V. - vsproj U v == linear projection of v : V in subvs U. - 'Hom(aT, rT) == the type of linear functions (homomorphisms) from - aT to rT, where aT and rT ARE vectType structures. - Elements of 'Hom(aT, rT) coerce to Coq functions. -> Caveat: aT and rT must denote actual vectType structures, not their - projections on Type. - linfun f == a vector linear function in 'Hom(aT, rT) that - coincides with f : aT -> rT when f is linear. - 'End(vT) == endomorphisms of vT (:= 'Hom(vT, vT)). -> The types subvs_of U, 'Hom(aT, rT), 'End(vT), K^o, 'M[K](m, n), - vT * wT, {ffun I -> vT}, vT ^ n all have canonical vectType instances. - -

- - Functions: - < [v]>%VS == the vector space generated by v (a line if v != 0). - 0%VS == the trivial vector subspace. - fullv, {:vT} == the complete vector subspace (displays as fullv). - (U + V)%VS == the join (sum) of two subspaces U and V. - (U :&: V)%VS == intersection of vector subspaces U and V. - (U^C)%VS == a complement of the vector subspace U. - (U :\: V)%VS == a local complement to U :& V in the subspace U. - \dim U == dimension of a vector space U. - span X, X%VS == the subspace spanned by the vector sequence X. - coord X i v == i'th coordinate of v on X, when v \in X%VS and - where X : n.-tuple vT and i : 'I_n. Note that - coord X i is a scalar function. - vpick U == a nonzero element of U if U= 0%VS, or 0 if U = 0. - vbasis U == a (\dim U).-tuple that is a basis of U. - \1%VF == the identity linear function. - (f \o g)%VF == the composite of two linear functions f and g. - (f^-1)%VF == a linear function that is a right inverse to the - linear function f on the codomain of f. - (f @: U)%VS == the image of vs by the linear function f. - (f @^-1: U)%VS == the pre-image of vs by the linear function f. - lker f == the kernel of the linear function f. - limg f == the image of the linear function f. - fixedSpace f == the fixed space of a linear endomorphism f - daddv_pi U V == projection onto U along V if U and V are disjoint; - daddv_pi U V + daddv_pi V U is then a projection - onto the direct sum (U + V)%VS. - projv U == projection onto U (along U^C, := daddv_pi U U^C). - addv_pi1 U V == projection onto the subspace U :\: V of U along V. - addv_pi2 U V == projection onto V along U :\: V; note that - addv_pi1 U V and addv_pi2 U V are (asymmetrical) - complementary projections on (U + V)%VS. - sumv_pi_for defV i == for defV : V = (V \sum(j <- r | P j) Vs j)%VS, - j ranging over an eqType, this is a projection on - a subspace of Vs i, along a complement in V, such - that \sum(j <- r | P j) sumv_pi_for defV j is a - projection onto V if filter P r is duplicate-free - (e.g., when V := \sum(j | P j) Vs j). - sumv_pi V i == notation the above when defV == erefl V, and V is - convertible to \sum(j <- r | P j) Vs j)%VS. - -

- - Predicates: - v \in U == v belongs to U (:= (< [v]> <= U)%VS). - (U <= V)%VS == U is a subspace of V. - free B == B is a sequence of nonzero linearly independent - vectors. - basis_of U b == b is a basis of the subspace U. - directv S == S is the expression for a direct sum of subspaces. -

- -
-Set Implicit Arguments.
-Local Open Scope ring_scope.
- -
-Reserved Notation "{ 'vspace' T }" (at level 0, format "{ 'vspace' T }").
-Reserved Notation "''Hom' ( T , rT )" (at level 8, format "''Hom' ( T , rT )").
-Reserved Notation "''End' ( T )" (at level 8, format "''End' ( T )").
-Reserved Notation "\dim A" (at level 10, A at level 8, format "\dim A").
- -
-Delimit Scope vspace_scope with VS.
- -
-Import GRing.Theory.
- -
-

- -

- Finite dimension vector space -

-Module Vector.
- -
-Section ClassDef.
-Variable R : ringType.
- -
-Definition axiom_def n (V : lmodType R) of phant V :=
-  {v2r : V → 'rV [R ]_n | linear v2r & bijective v2r }.
- -
-Inductive mixin_of (V : lmodType R) := Mixin dim & axiom_def dim (Phant V).
- -
-Structure class_of V := Class {
-  base : GRing.Lmodule.class_of R V;
-  mixin : mixin_of (GRing.Lmodule.Pack _ base)
-}.
- -
-Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
-Variables (phR : phant R) (T : Type) (cT : type phR).
-Definition class := let: Pack _ c := cT return class_of cT in c.
-Definition clone c of phant_id class c := @Pack phR T c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
-Definition dim := let: Mixin n _ := mixin class in n.
- -
-Definition pack b0 (m0 : mixin_of (@GRing.Lmodule.Pack R _ T b0)) :=
-  fun bT b & phant_id (@GRing.Lmodule.class _ phR bT) b ⇒
-  fun m & phant_id m0 m ⇒ Pack phR (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass.
-Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass.
- -
-End ClassDef.
-Notation axiom n V := (axiom_def n (Phant V)).
- -
-Section OtherDefs.
-Inductive space (K : fieldType) (vT : type (Phant K)) (phV : phant vT) :=
-  Space (mx : 'M [K ]_vT) & <<mx >>%MS == mx.
-Inductive hom (R : ringType) (vT wT : type (Phant R)) :=
-  Hom of 'M [R ]_(vT , wT ).
-End OtherDefs.
- -
-Module Import Exports.
- -
-Coercion base : class_of >-> GRing.Lmodule.class_of.
-Coercion mixin : class_of >-> mixin_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> GRing.Zmodule.type.
-Canonical zmodType.
-Coercion lmodType : type >-> GRing.Lmodule.type.
-Canonical lmodType.
-Notation vectType R := (@type _ (Phant R)).
-Notation VectType R V mV :=
-   (@pack _ (Phant R) V _ mV _ _ id _ id).
-Notation VectMixin := Mixin.
-Notation "[ 'vectType' R 'of' T 'for' cT ]" := (@clone _ (Phant R) T cT _ idfun)
-  (at level 0, format "[ 'vectType' R 'of' T 'for' cT ]") : form_scope.
-Notation "[ 'vectType' R 'of' T ]" := (@clone _ (Phant R) T _ _ idfun)
-  (at level 0, format "[ 'vectType' R 'of' T ]") : form_scope.
- -
-Notation "{ 'vspace' vT }" := (space (Phant vT)) : type_scope.
-Notation "''Hom' ( aT , rT )" := (hom aT rT) : type_scope.
-Notation "''End' ( vT )" := (hom vT vT) : type_scope.
- -
- -
-Delimit Scope vspace_scope with VS.
-Delimit Scope lfun_scope with VF.
- -
-End Exports.
- -
-

- -

- The contents of this module exposes the matrix encodings, and should - therefore not be used outside of the vector library implementation. -

-Module InternalTheory.
- -
-Section Iso.
-Variables (R : ringType) (vT rT : vectType R).
- -
-Fact v2r_subproof : axiom vT vT.
-Definition v2r := s2val v2r_subproof.
- -
-Let v2r_bij : bijective v2r := s2valP' v2r_subproof.
-Fact r2v_subproof : {r2v | cancel r2v v2r }.
-Definition r2v := sval r2v_subproof.
- -
-Lemma r2vK : cancel r2v v2r.
-Lemma r2v_inj : injective r2v.
-Lemma v2rK : cancel v2r r2v.
-Lemma v2r_inj : injective v2r.
- -
-Canonical v2r_linear := Linear (s2valP v2r_subproof : linear v2r).
-Canonical r2v_linear := Linear (can2_linear v2rK r2vK).
-End Iso.
- -
-Section Vspace.
-Variables (K : fieldType) (vT : vectType K).
- -
-Definition b2mx n (X : n .-tuple vT) := \matrix_i v2r (tnth X i).
-Lemma b2mxK n (X : n .-tuple vT) i : r2v (row i (b2mx X)) = X `_i.
- -
-Definition vs2mx {phV} (U : @space K vT phV) := let: Space mx _ := U in mx.
-Lemma gen_vs2mx (U : {vspace vT }) : <<vs2mx U >>%MS = vs2mx U.
- -
-Fact mx2vs_subproof m (A : 'M [K ]_(m , vT )) : <<(<<A >>)>>%MS == <<A >>%MS.
- Definition mx2vs {m} A : {vspace vT } := Space _ (@mx2vs_subproof m A).
- -
-Canonical space_subType := [subType for @vs2mx (Phant vT)].
-Lemma vs2mxK : cancel vs2mx mx2vs.
- Lemma mx2vsK m (M : 'M_(m , vT )) : (vs2mx (mx2vs M) :=: M)%MS.
- End Vspace.
- -
-Section Hom.
-Variables (R : ringType) (aT rT : vectType R).
-Definition f2mx (f : 'Hom (aT , rT )) := let: Hom A := f in A.
-Canonical hom_subType := [newType for f2mx ].
-End Hom.
- -
- -
-End InternalTheory.
- -
-End Vector.
-Export Vector.Exports.
-Import Vector.InternalTheory.
- -
-Section VspaceDefs.
- -
-Variables (K : fieldType) (vT : vectType K).
-Implicit Types (u : vT) (X : seq vT) (U V : {vspace vT }).
- -
-Definition space_eqMixin := Eval hnf in [eqMixin of {vspace vT } by <:].
-Canonical space_eqType := EqType {vspace vT } space_eqMixin.
-Definition space_choiceMixin := Eval hnf in [choiceMixin of {vspace vT } by <:].
-Canonical space_choiceType := ChoiceType {vspace vT } space_choiceMixin.
- -
-Definition dimv U := \rank (vs2mx U ).
-Definition subsetv U V := (vs2mx U ≤ vs2mx V)%MS.
-Definition vline u := mx2vs (v2r u).
- -
-

- -

- Vspace membership is defined as line inclusion. -

-Definition pred_of_vspace phV (U : Vector.space phV) : {pred vT } :=
-  fun v ⇒ (vs2mx (vline v) ≤ vs2mx U)%MS.
-Canonical vspace_predType :=
-  @PredType _ (unkeyed {vspace vT }) (@pred_of_vspace _).
- -
-Definition fullv : {vspace vT } := mx2vs 1%:M.
-Definition addv U V := mx2vs (vs2mx U + vs2mx V).
-Definition capv U V := mx2vs (vs2mx U :&: vs2mx V).
-Definition complv U := mx2vs (vs2mx U )^C.
-Definition diffv U V := mx2vs (vs2mx U :\: vs2mx V).
-Definition vpick U := r2v (nz_row (vs2mx U)).
-Fact span_key : unit.
-Definition span_expanded_def X := mx2vs (b2mx (in_tuple X)).
-Definition span := locked_with span_key span_expanded_def.
-Canonical span_unlockable := [unlockable fun span ].
-Definition vbasis_def U :=
-  [tuple r2v (row i (row_base (vs2mx U))) | i < dimv U ].
-Definition vbasis := locked_with span_key vbasis_def.
-Canonical vbasis_unlockable := [unlockable fun vbasis ].
- -
-

- -

- coord and directv are defined in the VectorTheory section. -

- -
-Definition free X := dimv (span X) == size X.
-Definition basis_of U X := (span X == U ) && free X.
- -
-End VspaceDefs.
- -
-Coercion pred_of_vspace : Vector.space >-> pred_sort.
-Notation "\dim U" := (dimv U) : nat_scope.
-Notation "U <= V" := (subsetv U V) : vspace_scope.
-Notation "U <= V <= W" := (subsetv U V && subsetv V W) : vspace_scope.
-Notation "<[ v ] >" := (vline v) : vspace_scope.
-Notation "<< X >>" := (span X) : vspace_scope.
-Notation "0" := (vline 0) : vspace_scope.
- -
-Notation "U + V" := (addv U V) : vspace_scope.
-Notation "U :&: V" := (capv U V) : vspace_scope.
-Notation "U ^C" := (complv U) (at level 8, format "U ^C") : vspace_scope.
-Notation "U :\: V" := (diffv U V) : vspace_scope.
-Notation "{ : vT }" := (@fullv _ vT) (only parsing) : vspace_scope.
- -
-Notation "\sum_ ( i <- r | P ) U" :=
-  (\big [addv /0%VS]_(i <- r | P%B) U%VS) : vspace_scope.
-Notation "\sum_ ( i <- r ) U" :=
-  (\big [addv /0%VS]_(i <- r) U%VS) : vspace_scope.
-Notation "\sum_ ( m <= i < n | P ) U" :=
-  (\big [addv /0%VS]_(m ≤ i < n | P%B) U%VS) : vspace_scope.
-Notation "\sum_ ( m <= i < n ) U" :=
-  (\big [addv /0%VS]_(m ≤ i < n) U%VS) : vspace_scope.
-Notation "\sum_ ( i | P ) U" :=
-  (\big [addv /0%VS]_(i | P%B) U%VS) : vspace_scope.
-Notation "\sum_ i U" :=
-  (\big [addv /0%VS]_i U%VS) : vspace_scope.
-Notation "\sum_ ( i : t | P ) U" :=
-  (\big [addv /0%VS]_(i : t | P%B) U%VS) (only parsing) : vspace_scope.
-Notation "\sum_ ( i : t ) U" :=
-  (\big [addv /0%VS]_(i : t) U%VS) (only parsing) : vspace_scope.
-Notation "\sum_ ( i < n | P ) U" :=
-  (\big [addv /0%VS]_(i < n | P%B) U%VS) : vspace_scope.
-Notation "\sum_ ( i < n ) U" :=
-  (\big [addv /0%VS]_(i < n) U%VS) : vspace_scope.
-Notation "\sum_ ( i 'in' A | P ) U" :=
-  (\big [addv /0%VS]_(i in A | P%B) U%VS) : vspace_scope.
-Notation "\sum_ ( i 'in' A ) U" :=
-  (\big [addv /0%VS]_(i in A) U%VS) : vspace_scope.
- -
-Notation "\bigcap_ ( i <- r | P ) U" :=
-  (\big [capv /fullv ]_(i <- r | P%B) U%VS) : vspace_scope.
-Notation "\bigcap_ ( i <- r ) U" :=
-  (\big [capv /fullv ]_(i <- r) U%VS) : vspace_scope.
-Notation "\bigcap_ ( m <= i < n | P ) U" :=
-  (\big [capv /fullv ]_(m ≤ i < n | P%B) U%VS) : vspace_scope.
-Notation "\bigcap_ ( m <= i < n ) U" :=
-  (\big [capv /fullv ]_(m ≤ i < n) U%VS) : vspace_scope.
-Notation "\bigcap_ ( i | P ) U" :=
-  (\big [capv /fullv ]_(i | P%B) U%VS) : vspace_scope.
-Notation "\bigcap_ i U" :=
-  (\big [capv /fullv ]_i U%VS) : vspace_scope.
-Notation "\bigcap_ ( i : t | P ) U" :=
-  (\big [capv /fullv ]_(i : t | P%B) U%VS) (only parsing) : vspace_scope.
-Notation "\bigcap_ ( i : t ) U" :=
-  (\big [capv /fullv ]_(i : t) U%VS) (only parsing) : vspace_scope.
-Notation "\bigcap_ ( i < n | P ) U" :=
-  (\big [capv /fullv ]_(i < n | P%B) U%VS) : vspace_scope.
-Notation "\bigcap_ ( i < n ) U" :=
-  (\big [capv /fullv ]_(i < n) U%VS) : vspace_scope.
-Notation "\bigcap_ ( i 'in' A | P ) U" :=
-  (\big [capv /fullv ]_(i in A | P%B) U%VS) : vspace_scope.
-Notation "\bigcap_ ( i 'in' A ) U" :=
-  (\big [capv /fullv ]_(i in A) U%VS) : vspace_scope.
- -
-Section VectorTheory.
- -
-Variables (K : fieldType) (vT : vectType K).
-Implicit Types (a : K) (u v w : vT) (X Y : seq vT) (U V W : {vspace vT }).
- -
- -
- -
-Fact vspace_key U : pred_key U.
-Canonical vspace_keyed U := KeyedPred (vspace_key U).
- -
-Lemma memvE v U : (v \in U ) = (<[v ]> ≤ U)%VS.
- -
-Lemma vlineP v1 v2 : reflect (∃ k, v1 = k *: v2) (v1 \in <[v2 ]>)%VS.
- -
-Fact memv_submod_closed U : submod_closed U.
-Canonical memv_opprPred U := OpprPred (memv_submod_closed U).
-Canonical memv_addrPred U := AddrPred (memv_submod_closed U).
-Canonical memv_zmodPred U := ZmodPred (memv_submod_closed U).
-Canonical memv_submodPred U := SubmodPred (memv_submod_closed U).
- -
-Lemma mem0v U : 0 \in U.
-Lemma memvN U v : (- v \in U ) = (v \in U ).
-Lemma memvD U : {in U &, ∀ u v, u + v \in U }.
-Lemma memvB U : {in U &, ∀ u v, u - v \in U }.
-Lemma memvZ U k : {in U , ∀ v, k *: v \in U }.
- -
-Lemma memv_suml I r (P : pred I) vs U :
-  (∀ i, P i → vs i \in U ) → \sum_(i <- r | P i ) vs i \in U.
- -
-Lemma memv_line u : u \in <[u ]>%VS.
- -
-Lemma subvP U V : reflect {subset U ≤ V } (U ≤ V)%VS.
- -
-Lemma subvv U : (U ≤ U)%VS.
-Hint Resolve subvv : core.
- -
-Lemma subv_trans : transitive subV.
- -
-Lemma subv_anti : antisymmetric subV.
- -
-Lemma eqEsubv U V : (U == V ) = (U ≤ V ≤ U)%VS.
- -
-Lemma vspaceP U V : U =i V ↔ U = V.
- -
-Lemma subvPn {U V} : reflect (exists2 u, u \in U & u \notin V) (~~ (U ≤ V)%VS).
- -
-

- -

- Empty space. -

-Lemma sub0v U : (0 ≤ U)%VS.
- -
-Lemma subv0 U : (U ≤ 0)%VS = (U == 0%VS).
- -
-Lemma memv0 v : v \in 0%VS = (v == 0).
- -
-

- -

- Full space -

- -
-Lemma subvf U : (U ≤ fullv)%VS.
-Lemma memvf v : v \in fullv.
- -
-

- -

- Picking a non-zero vector in a subspace. -

-Lemma memv_pick U : vpick U \in U.
- -
-Lemma vpick0 U : (vpick U == 0) = (U == 0%VS).
- -
-

- -

- Sum of subspaces. -

-Lemma subv_add U V W : (U + V ≤ W)%VS = (U ≤ W)%VS && (V ≤ W)%VS.
- -
-Lemma addvS U1 U2 V1 V2 : (U1 ≤ U2 → V1 ≤ V2 → U1 + V1 ≤ U2 + V2)%VS.
- -
-Lemma addvSl U V : (U ≤ U + V)%VS.
- -
-Lemma addvSr U V : (V ≤ U + V)%VS.
- -
-Lemma addvC : commutative addV.
- -
-Lemma addvA : associative addV.
- -
-Lemma addv_idPl {U V}: reflect (U + V = U)%VS (V ≤ U)%VS.
- -
-Lemma addv_idPr {U V} : reflect (U + V = V)%VS (U ≤ V)%VS.
- -
-Lemma addvv : idempotent addV.
- -
-Lemma add0v : left_id 0%VS addV.
- -
-Lemma addv0 : right_id 0%VS addV.
- -
-Lemma sumfv : left_zero fullv addV.
- -
-Lemma addvf : right_zero fullv addV.
- -
-Canonical addv_monoid := Monoid.Law addvA add0v addv0.
-Canonical addv_comoid := Monoid.ComLaw addvC.
- -
-Lemma memv_add u v U V : u \in U → v \in V → u + v \in (U + V)%VS.
- -
-Lemma memv_addP {w U V} :
-  reflect (exists2 u, u \in U & exists2 v, v \in V & w = u + v)
-          (w \in U + V)%VS.
- -
-Section BigSum.
-Variable I : finType.
-Implicit Type P : pred I.
- -
-Lemma sumv_sup i0 P U Vs :
-  P i0 → (U ≤ Vs i0)%VS → (U ≤ \sum_(i | P i ) Vs i)%VS.
- -
-Lemma subv_sumP {P Us V} :
-  reflect (∀ i, P i → Us i ≤ V)%VS (\sum_(i | P i ) Us i ≤ V)%VS.
- -
-Lemma memv_sumr P vs (Us : I → {vspace vT }) :
-    (∀ i, P i → vs i \in Us i ) →
-  \sum_(i | P i ) vs i \in (\sum_(i | P i ) Us i)%VS.
- -
-Lemma memv_sumP {P} {Us : I → {vspace vT }} {v} :
-  reflect (exists2 vs, ∀ i, P i → vs i \in Us i
-                     & v = \sum_(i | P i ) vs i)
-          (v \in \sum_(i | P i ) Us i)%VS.
- -
-End BigSum.
- -
-

- -

- Intersection -

- -
-Lemma subv_cap U V W : (U ≤ V :&: W)%VS = (U ≤ V)%VS && (U ≤ W)%VS.
- -
-Lemma capvS U1 U2 V1 V2 : (U1 ≤ U2 → V1 ≤ V2 → U1 :&: V1 ≤ U2 :&: V2)%VS.
- -
-Lemma capvSl U V : (U :&: V ≤ U)%VS.
- -
-Lemma capvSr U V : (U :&: V ≤ V)%VS.
- -
-Lemma capvC : commutative capV.
- -
-Lemma capvA : associative capV.
- -
-Lemma capv_idPl {U V} : reflect (U :&: V = U)%VS (U ≤ V)%VS.
- -
-Lemma capv_idPr {U V} : reflect (U :&: V = V)%VS (V ≤ U)%VS.
- -
-Lemma capvv : idempotent capV.
- -
-Lemma cap0v : left_zero 0%VS capV.
- -
-Lemma capv0 : right_zero 0%VS capV.
- -
-Lemma capfv : left_id fullv capV.
- -
-Lemma capvf : right_id fullv capV.
- -
-Canonical capv_monoid := Monoid.Law capvA capfv capvf.
-Canonical capv_comoid := Monoid.ComLaw capvC.
- -
-Lemma memv_cap w U V : (w \in U :&: V)%VS = (w \in U ) && (w \in V ).
- -
-Lemma memv_capP {w U V} : reflect (w \in U ∧ w \in V) (w \in U :&: V)%VS.
- -
-Lemma vspace_modl U V W : (U ≤ W → U + (V :&: W ) = (U + V ) :&: W)%VS.
- -
-Lemma vspace_modr U V W : (W ≤ U → (U :&: V ) + W = U :&: (V + W ))%VS.
- -
-Section BigCap.
-Variable I : finType.
-Implicit Type P : pred I.
- -
-Lemma bigcapv_inf i0 P Us V :
- P i0 → (Us i0 ≤ V → \bigcap_(i | P i ) Us i ≤ V)%VS.
- -
-Lemma subv_bigcapP {P U Vs} :
- reflect (∀ i, P i → U ≤ Vs i)%VS (U ≤ \bigcap_(i | P i ) Vs i)%VS.
- -
-End BigCap.
- -
-

- -

- Complement -

-Lemma addv_complf U : (U + U ^C)%VS = fullv.
- -
-Lemma capv_compl U : (U :&: U ^C = 0)%VS.
- -
-

- -

- Difference -

-Lemma diffvSl U V : (U :\: V ≤ U)%VS.
- -
-Lemma capv_diff U V : ((U :\: V ) :&: V = 0)%VS.
- -
-Lemma addv_diff_cap U V : (U :\: V + U :&: V)%VS = U.
- -
-Lemma addv_diff U V : (U :\: V + V = U + V)%VS.
- -
-

- -

- Subspace dimension. -

-Lemma dimv0 : \dim (0%VS : {vspace vT }) = 0%N.
- -
-Lemma dimv_eq0 U : (\dim U == 0%N) = (U == 0%VS).
- -
-Lemma dimvf : \dim {:vT } = Vector.dim vT.
- -
-Lemma dim_vline v : \dim <[v ]> = (v != 0).
- -
-Lemma dimvS U V : (U ≤ V)%VS → \dim U ≤ \dim V.
- -
-Lemma dimv_leqif_sup U V : (U ≤ V)%VS → \dim U ≤ \dim V ?= iff (V ≤ U)%VS.
- -
-Lemma dimv_leqif_eq U V : (U ≤ V)%VS → \dim U ≤ \dim V ?= iff (U == V ).
- -
-Lemma eqEdim U V : (U == V ) = (U ≤ V)%VS && (\dim V ≤ \dim U ).
- -
-Lemma dimv_compl U : \dim U ^C = (\dim {:vT } - \dim U)%N.
- -
-Lemma dimv_cap_compl U V : (\dim (U :&: V ) + \dim (U :\: V ))%N = \dim U.
- -
-Lemma dimv_sum_cap U V : (\dim (U + V ) + \dim (U :&: V ) = \dim U + \dim V)%N.
- -
-Lemma dimv_disjoint_sum U V :
-  (U :&: V = 0)%VS → \dim (U + V ) = (\dim U + \dim V)%N.
- -
-Lemma dimv_add_leqif U V :
-  \dim (U + V ) ≤ \dim U + \dim V ?= iff (U :&: V ≤ 0)%VS.
- -
-Lemma diffv_eq0 U V : (U :\: V == 0)%VS = (U ≤ V)%VS.
- -
-Lemma dimv_leq_sum I r (P : pred I) (Us : I → {vspace vT }) :
-  \dim (\sum_(i <- r | P i ) Us i ) ≤ \sum_(i <- r | P i ) \dim (Us i ).
- -
-Section SumExpr.
- -
-

- -

- The vector direct sum theory clones the interface types of the matrix - direct sum theory (see mxalgebra for the technical details), but - nevetheless reuses much of the matrix theory. -

-Structure addv_expr := Sumv {
-  addv_val :> wrapped {vspace vT };
-  addv_dim : wrapped nat;
-  _ : mxsum_spec (vs2mx (unwrap addv_val)) (unwrap addv_dim)
-}.
- -
-

- -

- Piggyback on mxalgebra theory. -

-Definition vs2mx_sum_expr_subproof (S : addv_expr) :
-  mxsum_spec (vs2mx (unwrap S)) (unwrap (addv_dim S)).
- Canonical vs2mx_sum_expr S := ProperMxsumExpr (vs2mx_sum_expr_subproof S).
- -
-Canonical trivial_addv U := @Sumv (Wrap U) (Wrap (\dim U)) (TrivialMxsum _).
- -
-Structure proper_addv_expr := ProperSumvExpr {
-  proper_addv_val :> {vspace vT };
-  proper_addv_dim :> nat;
-  _ : mxsum_spec (vs2mx proper_addv_val) proper_addv_dim
-}.
- -
-Definition proper_addvP (S : proper_addv_expr) :=
-  let: ProperSumvExpr _ _ termS := S return mxsum_spec (vs2mx S) S in termS.
- -
-Canonical proper_addv (S : proper_addv_expr) :=
-  @Sumv (wrap (S : {vspace vT })) (wrap (S : nat)) (proper_addvP S).
- -
-Section Binary.
-Variables S1 S2 : addv_expr.
-Fact binary_addv_subproof :
-  mxsum_spec (vs2mx (unwrap S1 + unwrap S2))
-             (unwrap (addv_dim S1) + unwrap (addv_dim S2)).
- Canonical binary_addv_expr := ProperSumvExpr binary_addv_subproof.
-End Binary.
- -
-Section Nary.
-Variables (I : Type) (r : seq I) (P : pred I) (S_ : I → addv_expr).
-Fact nary_addv_subproof :
-  mxsum_spec (vs2mx (\sum_(i <- r | P i ) unwrap (S_ i)))
-             (\sum_(i <- r | P i ) unwrap (addv_dim (S_ i))).
- Canonical nary_addv_expr := ProperSumvExpr nary_addv_subproof.
-End Nary.
- -
-Definition directv_def S of phantom {vspace vT } (unwrap (addv_val S)) :=
-  \dim (unwrap S ) == unwrap (addv_dim S).
- -
-End SumExpr.
- -
- -
-Lemma directvE (S : addv_expr) :
-  directv (unwrap S) = (\dim (unwrap S ) == unwrap (addv_dim S)).
- -
-Lemma directvP {S : proper_addv_expr} : reflect (\dim S = S :> nat) (directv S).
- -
-Lemma directv_trivial U : directv (unwrap (@trivial_addv U)).
- -
-Lemma dimv_sum_leqif (S : addv_expr) :
-  \dim (unwrap S ) ≤ unwrap (addv_dim S) ?= iff directv (unwrap S).
- -
-Lemma directvEgeq (S : addv_expr) :
-  directv (unwrap S) = (\dim (unwrap S ) ≥ unwrap (addv_dim S)).
- -
-Section BinaryDirect.
- -
-Lemma directv_addE (S1 S2 : addv_expr) :
-  directv (unwrap S1 + unwrap S2)
-    = [&& directv (unwrap S1), directv (unwrap S2)
-        & unwrap S1 :&: unwrap S2 == 0]%VS.
- -
-Lemma directv_addP {U V} : reflect (U :&: V = 0)%VS (directv (U + V)).
- -
-Lemma directv_add_unique {U V} :
-   reflect (∀ u1 u2 v1 v2, u1 \in U → u2 \in U → v1 \in V → v2 \in V →
-             (u1 + v1 == u2 + v2 ) = ((u1 , v1 ) == (u2 , v2 )))
-           (directv (U + V)).
- -
-End BinaryDirect.
- -
-Section NaryDirect.
- -
-Context {I : finType} {P : pred I}.
- -
-Lemma directv_sumP {Us : I → {vspace vT }} :
-  reflect (∀ i, P i → Us i :&: (\sum_(j | P j && (j != i )) Us j ) = 0)%VS
-          (directv (\sum_(i | P i ) Us i)).
- -
-Lemma directv_sumE {Ss : I → addv_expr} (xunwrap := unwrap) :
-  reflect [/\ ∀ i, P i → directv (unwrap (Ss i))
-            & directv (\sum_(i | P i ) xunwrap (Ss i))]
-          (directv (\sum_(i | P i ) unwrap (Ss i))).
- -
-Lemma directv_sum_independent {Us : I → {vspace vT }} :
-   reflect (∀ us,
-               (∀ i, P i → us i \in Us i ) → \sum_(i | P i ) us i = 0 →
-             (∀ i, P i → us i = 0))
-           (directv (\sum_(i | P i ) Us i)).
- -
-Lemma directv_sum_unique {Us : I → {vspace vT }} :
-  reflect (∀ us vs,
-              (∀ i, P i → us i \in Us i ) →
-              (∀ i, P i → vs i \in Us i ) →
-            (\sum_(i | P i ) us i == \sum_(i | P i ) vs i )
-              = [∀ (i | P i ), us i == vs i ])
-          (directv (\sum_(i | P i ) Us i)).
- -
-End NaryDirect.
- -
-

- -

- Linear span generated by a list of vectors -

-Lemma memv_span X v : v \in X → v \in <<X >>%VS.
- -
-Lemma memv_span1 v : v \in <<[:: v ]>>%VS.
- -
-Lemma dim_span X : \dim <<X >> ≤ size X.
- -
-Lemma span_subvP {X U} : reflect {subset X ≤ U } (<<X >> ≤ U)%VS.
- -
-Lemma sub_span X Y : {subset X ≤ Y } → (<<X >> ≤ <<Y >>)%VS.
- -
-Lemma eq_span X Y : X =i Y → (<<X >> = <<Y >>)%VS.
- -
-Lemma span_def X : span X = (\sum_(u <- X ) <[u ]>)%VS.
- -
-Lemma span_nil : (<<Nil vT >> = 0)%VS.
- -
-Lemma span_seq1 v : (<<[:: v ]>> = <[v ]>)%VS.
- -
-Lemma span_cons v X : (<<v :: X >> = <[v ]> + <<X >>)%VS.
- -
-Lemma span_cat X Y : (<<X ++ Y >> = <<X >> + <<Y >>)%VS.
- -
-

- -

- Coordinates function; should perhaps be generalized to nat indices. -

- -
-Definition coord_expanded_def n (X : n .-tuple vT) i v :=
- (v2r v ×m pinvmx (b2mx X)) 0 i.
-Definition coord := locked_with span_key coord_expanded_def.
-Canonical coord_unlockable := [unlockable fun coord ].
- -
-Fact coord_is_scalar n (X : n .-tuple vT) i : scalar (coord X i).
- Canonical coord_addidive n Xn i := Additive (@coord_is_scalar n Xn i).
-Canonical coord_linear n Xn i := AddLinear (@coord_is_scalar n Xn i).
- -
-Lemma coord_span n (X : n .-tuple vT) v :
- v \in span X → v = \sum_i coord X i v *: X `_i.
- -
-Lemma coord0 i v : coord [tuple 0] i v = 0.
- -
-

- -

- Free generator sequences. -

- -
-Lemma nil_free : free (Nil vT).
- -
-Lemma seq1_free v : free [:: v ] = (v != 0).
- -
-Lemma perm_free X Y : perm_eq X Y → free X = free Y.
- -
-Lemma free_directv X : free X = (0 \notin X ) && directv (\sum_(v <- X ) <[v ]>).
- -
-Lemma free_not0 v X : free X → v \in X → v != 0.
- -
-Lemma freeP n (X : n .-tuple vT) :
-  reflect (∀ k, \sum_(i < n ) k i *: X `_i = 0 → (∀ i, k i = 0))
-          (free X).
- -
-Lemma coord_free n (X : n .-tuple vT) (i j : 'I_n) :
-  free X → coord X j (X `_i) = (i == j )%:R.
- -
-Lemma coord_sum_free n (X : n .-tuple vT) k j :
-  free X → coord X j (\sum_(i < n ) k i *: X `_i) = k j.
- -
-Lemma cat_free X Y :
-  free (X ++ Y) = [&& free X , free Y & directv (<<X >> + <<Y >>)].
- -
-Lemma catl_free Y X : free (X ++ Y) → free X.
- -
-Lemma catr_free X Y : free (X ++ Y) → free Y.
- -
-Lemma filter_free p X : free X → free (filter p X).
- -
-Lemma free_cons v X : free (v :: X) = (v \notin <<X >>)%VS && free X.
- -
-Lemma freeE n (X : n .-tuple vT) :
-  free X = [∀ i : 'I_n , X `_i \notin <<drop i .+1 X >>%VS].
- -
-Lemma freeNE n (X : n .-tuple vT) :
-  ~~ free X = [∃ i : 'I_n , X `_i \in <<drop i .+1 X >>%VS].
- -
-Lemma free_uniq X : free X → uniq X.
- -
-Lemma free_span X v (sumX := fun k ⇒ \sum_(x <- X ) k x *: x) :
-    free X → v \in <<X >>%VS →
-  {k | v = sumX k & ∀ k1, v = sumX k1 → {in X , k1 =1 k }}.
- -
-Lemma linear_of_free (rT : lmodType K) X (fX : seq rT) :
-  {f : {linear vT → rT } | free X → size fX = size X → map f X = fX }.
- -
-

- -

- Subspace bases -

- -
-Lemma span_basis U X : basis_of U X → <<X >>%VS = U.
- -
-Lemma basis_free U X : basis_of U X → free X.
- -
-Lemma coord_basis U n (X : n .-tuple vT) v :
-  basis_of U X → v \in U → v = \sum_i coord X i v *: X `_i.
- -
-Lemma nil_basis : basis_of 0 (Nil vT).
- -
-Lemma seq1_basis v : v != 0 → basis_of <[v ]> [:: v ].
- -
-Lemma basis_not0 x U X : basis_of U X → x \in X → x != 0.
- -
-Lemma basis_mem x U X : basis_of U X → x \in X → x \in U.
- -
-Lemma cat_basis U V X Y :
-  directv (U + V) → basis_of U X → basis_of V Y → basis_of (U + V) (X ++ Y).
- -
-Lemma size_basis U n (X : n .-tuple vT) : basis_of U X → \dim U = n.
- -
-Lemma basisEdim X U : basis_of U X = (U ≤ <<X >>)%VS && (size X ≤ \dim U ).
- -
-Lemma basisEfree X U :
-  basis_of U X = [&& free X , (<<X >> ≤ U)%VS & \dim U ≤ size X ].
- -
-Lemma perm_basis X Y U : perm_eq X Y → basis_of U X = basis_of U Y.
- -
-Lemma vbasisP U : basis_of U (vbasis U).
- -
-Lemma vbasis_mem v U : v \in (vbasis U ) → v \in U.
- -
-Lemma coord_vbasis v U :
-  v \in U → v = \sum_(i < \dim U ) coord (vbasis U) i v *: (vbasis U )`_i.
- -
-Section BigSumBasis.
- -
-Variables (I : finType) (P : pred I) (Xs : I → seq vT).
- -
-Lemma span_bigcat :
-  (<<\big [cat /[::]]_(i | P i ) Xs i >> = \sum_(i | P i ) <<Xs i >>)%VS.
- -
-Lemma bigcat_free :
-    directv (\sum_(i | P i ) <<Xs i >>) →
-  (∀ i, P i → free (Xs i)) → free (\big [cat /[::]]_(i | P i ) Xs i).
- -
-Lemma bigcat_basis Us (U := (\sum_(i | P i ) Us i)%VS) :
-    directv U → (∀ i, P i → basis_of (Us i) (Xs i)) →
-  basis_of U (\big [cat /[::]]_(i | P i ) Xs i).
- -
-End BigSumBasis.
- -
-End VectorTheory.
- -
-Hint Resolve subvv : core.
- -
-Notation directv S := (directv_def (Phantom _ S%VS)).
- -
-

- -

- Linear functions over a vectType -

-Section LfunDefs.
- -
-Variable R : ringType.
-Implicit Types aT vT rT : vectType R.
- -
-Fact lfun_key : unit.
-Definition fun_of_lfun_def aT rT (f : 'Hom (aT , rT )) :=
-  r2v \o mulmxr (f2mx f) \o v2r.
-Definition fun_of_lfun := locked_with lfun_key fun_of_lfun_def.
-Canonical fun_of_lfun_unlockable := [unlockable fun fun_of_lfun ].
-Definition linfun_def aT rT (f : aT → rT) :=
-  Vector.Hom (lin1_mx (v2r \o f \o r2v)).
-Definition linfun := locked_with lfun_key linfun_def.
-Canonical linfun_unlockable := [unlockable fun linfun ].
- -
-Definition id_lfun vT := @linfun vT vT idfun.
-Definition comp_lfun aT vT rT (f : 'Hom (vT , rT )) (g : 'Hom (aT , vT )) :=
-  linfun (fun_of_lfun f \o fun_of_lfun g).
- -
-End LfunDefs.
- -
-Coercion fun_of_lfun : Vector.hom >-> Funclass.
-Notation "\1" := (@id_lfun _ _) : lfun_scope.
-Notation "f \o g" := (comp_lfun f g) : lfun_scope.
- -
-Section LfunVspaceDefs.
- -
-Variable K : fieldType.
-Implicit Types aT rT : vectType K.
- -
-Definition inv_lfun aT rT (f : 'Hom (aT , rT )) := Vector.Hom (pinvmx (f2mx f)).
-Definition lker aT rT (f : 'Hom (aT , rT )) := mx2vs (kermx (f2mx f)).
-Fact lfun_img_key : unit.
-Definition lfun_img_def aT rT f (U : {vspace aT }) : {vspace rT } :=
-  mx2vs (vs2mx U ×m f2mx f).
-Definition lfun_img := locked_with lfun_img_key lfun_img_def.
-Canonical lfun_img_unlockable := [unlockable fun lfun_img ].
-Definition lfun_preim aT rT (f : 'Hom (aT , rT )) W :=
-  (lfun_img (inv_lfun f) (W :&: lfun_img f fullv) + lker f)%VS.
- -
-End LfunVspaceDefs.
- -
-Notation "f ^-1" := (inv_lfun f) : lfun_scope.
-Notation "f @: U" := (lfun_img f%VF%R U) (at level 24) : vspace_scope.
-Notation "f @^-1: W" := (lfun_preim f%VF%R W) (at level 24) : vspace_scope.
-Notation limg f := (lfun_img f fullv).
- -
-Section LfunZmodType.
- -
-Variables (R : ringType) (aT rT : vectType R).
-Implicit Types f g h : 'Hom (aT , rT ).
- -
-Definition lfun_eqMixin := Eval hnf in [eqMixin of 'Hom (aT , rT ) by <:].
-Canonical lfun_eqType := EqType 'Hom (aT , rT ) lfun_eqMixin.
-Definition lfun_choiceMixin := [choiceMixin of 'Hom (aT , rT ) by <:].
-Canonical lfun_choiceType := ChoiceType 'Hom (aT , rT ) lfun_choiceMixin.
- -
-Fact lfun_is_linear f : linear f.
- Canonical lfun_additive f := Additive (lfun_is_linear f).
-Canonical lfun_linear f := AddLinear (lfun_is_linear f).
- -
-Lemma lfunE (ff : {linear aT → rT }) : linfun ff =1 ff.
- -
-Lemma fun_of_lfunK : cancel (@fun_of_lfun R aT rT) linfun.
- -
-Lemma lfunP f g : f =1 g ↔ f = g.
- -
-Definition zero_lfun : 'Hom (aT , rT ) := linfun \0.
-Definition add_lfun f g := linfun (f \+ g).
-Definition opp_lfun f := linfun (-%R \o f).
- -
-Fact lfun_addA : associative add_lfun.
- -
-Fact lfun_addC : commutative add_lfun.
- -
-Fact lfun_add0 : left_id zero_lfun add_lfun.
- -
-Lemma lfun_addN : left_inverse zero_lfun opp_lfun add_lfun.
- -
-Definition lfun_zmodMixin := ZmodMixin lfun_addA lfun_addC lfun_add0 lfun_addN.
-Canonical lfun_zmodType := Eval hnf in ZmodType 'Hom (aT , rT ) lfun_zmodMixin.
- -
-Lemma zero_lfunE x : (0 : 'Hom (aT , rT )) x = 0.
-Lemma add_lfunE f g x : (f + g) x = f x + g x.
-Lemma opp_lfunE f x : (- f) x = - f x.
-Lemma sum_lfunE I (r : seq I) (P : pred I) (fs : I → 'Hom (aT , rT )) x :
-  (\sum_(i <- r | P i ) fs i) x = \sum_(i <- r | P i ) fs i x.
- -
-End LfunZmodType.
- -
- -
-Section LfunVectType.
- -
-Variables (R : comRingType) (aT rT : vectType R).
-Implicit Types f : 'Hom (aT , rT ).
- -
-Definition scale_lfun k f := linfun (k \*: f).
- -
-Fact lfun_scaleA k1 k2 f : k1 *:l (k2 *:l f ) = (k1 × k2 ) *:l f.
- -
-Fact lfun_scale1 f : 1 *:l f = f.
- -
-Fact lfun_scaleDr k f1 f2 : k *:l (f1 + f2 ) = k *:l f1 + k *:l f2.
- -
-Fact lfun_scaleDl f k1 k2 : (k1 + k2 ) *:l f = k1 *:l f + k2 *:l f.
- -
-Definition lfun_lmodMixin :=
-  LmodMixin lfun_scaleA lfun_scale1 lfun_scaleDr lfun_scaleDl.
-Canonical lfun_lmodType := Eval hnf in LmodType R 'Hom (aT , rT ) lfun_lmodMixin.
- -
-Lemma scale_lfunE k f x : (k *: f) x = k *: f x.
- -
-

- -

- GG: exists (Vector.Hom \o vec_mx) fails in the proof below in 8.3, - probably because of incomplete type unification. Will it work in 8.4? -

-Fact lfun_vect_iso : Vector.axiom (Vector.dim aT × Vector.dim rT) 'Hom (aT , rT ).
- -
-Definition lfun_vectMixin := VectMixin lfun_vect_iso.
-Canonical lfun_vectType := VectType R 'Hom (aT , rT ) lfun_vectMixin.
- -
-End LfunVectType.
- -
-Section CompLfun.
- -
-Variables (R : ringType) (wT aT vT rT : vectType R).
-Implicit Types (f : 'Hom (vT , rT )) (g : 'Hom (aT , vT )) (h : 'Hom (wT , aT )).
- -
-Lemma id_lfunE u: \1%VF u = u :> aT.
-Lemma comp_lfunE f g u : (f \o g)%VF u = f (g u).
- -
-Lemma comp_lfunA f g h : (f \o (g \o h ) = (f \o g ) \o h)%VF.
- -
-Lemma comp_lfun1l f : (\1 \o f)%VF = f.
- -
-Lemma comp_lfun1r f : (f \o \1)%VF = f.
- -
-Lemma comp_lfun0l g : (0 \o g)%VF = 0 :> 'Hom (aT , rT ).
- -
-Lemma comp_lfun0r f : (f \o 0)%VF = 0 :> 'Hom (aT , rT ).
- -
-Lemma comp_lfunDl f1 f2 g : ((f1 + f2 ) \o g = (f1 \o g ) + (f2 \o g ))%VF.
- -
-Lemma comp_lfunDr f g1 g2 : (f \o (g1 + g2 ) = (f \o g1 ) + (f \o g2 ))%VF.
- -
-Lemma comp_lfunNl f g : ((- f ) \o g = - (f \o g ))%VF.
- -
-Lemma comp_lfunNr f g : (f \o (- g ) = - (f \o g ))%VF.
- -
-End CompLfun.
- -
-Definition lfun_simp :=
-  (comp_lfunE , scale_lfunE , opp_lfunE , add_lfunE , sum_lfunE , lfunE ).
- -
-Section ScaleCompLfun.
- -
-Variables (R : comRingType) (aT vT rT : vectType R).
-Implicit Types (f : 'Hom (vT , rT )) (g : 'Hom (aT , vT )).
- -
-Lemma comp_lfunZl k f g : (k *: (f \o g ) = (k *: f ) \o g)%VF.
- -
-Lemma comp_lfunZr k f g : (k *: (f \o g ) = f \o (k *: g ))%VF.
- -
-End ScaleCompLfun.
- -
-Section LinearImage.
- -
-Variables (K : fieldType) (aT rT : vectType K).
-Implicit Types (f g : 'Hom (aT , rT )) (U V : {vspace aT }) (W : {vspace rT }).
- -
-Lemma limgS f U V : (U ≤ V)%VS → (f @: U ≤ f @: V)%VS.
- -
-Lemma limg_line f v : (f @: <[v ]> = <[f v ]>)%VS.
- -
-Lemma limg0 f : (f @: 0 = 0)%VS.
- -
-Lemma memv_img f v U : v \in U → f v \in (f @: U)%VS.
- -
-Lemma memv_imgP f w U :
-  reflect (exists2 u, u \in U & w = f u) (w \in f @: U)%VS.
- -
-Lemma lim0g U : (0 @: U = 0 :> {vspace rT })%VS.
- -
-Lemma eq_in_limg V f g : {in V , f =1 g } → (f @: V = g @: V)%VS.
- -
-Lemma limg_add f : {morph lfun_img f : U V / U + V }%VS.
- -
-Lemma limg_sum f I r (P : pred I) Us :
-  (f @: (\sum_(i <- r | P i ) Us i ) = \sum_(i <- r | P i ) f @: Us i)%VS.
- -
-Lemma limg_cap f U V : (f @: (U :&: V ) ≤ f @: U :&: f @: V)%VS.
- -
-Lemma limg_bigcap f I r (P : pred I) Us :
-  (f @: (\bigcap_(i <- r | P i ) Us i ) ≤ \bigcap_(i <- r | P i ) f @: Us i)%VS.
- -
-Lemma limg_span f X : (f @: <<X >> = <<map f X >>)%VS.
- -
-Lemma lfunPn f g : reflect (∃ u, f u != g u) (f != g).
- -
-Lemma inv_lfun_def f : (f \o f ^-1 \o f)%VF = f.
- -
-Lemma limg_lfunVK f : {in limg f , cancel f ^-1%VF f }.
- -
-Lemma lkerE f U : (U ≤ lker f)%VS = (f @: U == 0)%VS.
- -
-Lemma memv_ker f v : (v \in lker f ) = (f v == 0).
- -
-Lemma eqlfunP f g v : reflect (f v = g v) (v \in lker (f - g)).
- -
-Lemma eqlfun_inP V f g : reflect {in V , f =1 g } (V ≤ lker (f - g))%VS.
- -
-Lemma limg_ker_compl f U : (f @: (U :\: lker f ) = f @: U)%VS.
- -
-Lemma limg_ker_dim f U : (\dim (U :&: lker f ) + \dim (f @: U ) = \dim U)%N.
- -
-Lemma limg_dim_eq f U : (U :&: lker f = 0)%VS → \dim (f @: U ) = \dim U.
- -
-Lemma limg_basis_of f U X :
-  (U :&: lker f = 0)%VS → basis_of U X → basis_of (f @: U) (map f X).
- -
-Lemma lker0P f : reflect (injective f) (lker f == 0%VS).
- -
-Lemma limg_ker0 f U V : lker f == 0%VS → (f @: U ≤ f @: V)%VS = (U ≤ V)%VS.
- -
-Lemma eq_limg_ker0 f U V : lker f == 0%VS → (f @: U == f @: V)%VS = (U == V ).
- -
-Lemma lker0_lfunK f : lker f == 0%VS → cancel f f ^-1%VF.
- -
-Lemma lker0_compVf f : lker f == 0%VS → (f ^-1 \o f = \1)%VF.
- -
-End LinearImage.
- -
- -
-Section FixedSpace.
- -
-Variables (K : fieldType) (vT : vectType K).
-Implicit Types (f : 'End (vT )) (U : {vspace vT }).
- -
-Definition fixedSpace f : {vspace vT } := lker (f - \1%VF).
- -
-Lemma fixedSpaceP f a : reflect (f a = a) (a \in fixedSpace f).
- -
-Lemma fixedSpacesP f U : reflect {in U , f =1 id } (U ≤ fixedSpace f)%VS.
- -
-Lemma fixedSpace_limg f U : (U ≤ fixedSpace f → f @: U = U)%VS.
- -
-Lemma fixedSpace_id : fixedSpace \1 = {:vT }%VS.
- -
-End FixedSpace.
- -
- -
-Section LinAut.
- -
-Variables (K : fieldType) (vT : vectType K) (f : 'End (vT )).
-Hypothesis kerf0 : lker f == 0%VS.
- -
-Lemma lker0_limgf : limg f = fullv.
- -
-Lemma lker0_lfunVK : cancel f ^-1%VF f.
- -
-Lemma lker0_compfV : (f \o f ^-1 = \1)%VF.
- -
-Lemma lker0_compVKf aT g : (f \o (f ^-1 \o g ))%VF = g :> 'Hom (aT , vT ).
- -
-Lemma lker0_compKf aT g : (f ^-1 \o (f \o g ))%VF = g :> 'Hom (aT , vT ).
- -
-Lemma lker0_compfK rT h : ((h \o f ) \o f ^-1)%VF = h :> 'Hom (vT , rT ).
- -
-Lemma lker0_compfVK rT h : ((h \o f ^-1 ) \o f)%VF = h :> 'Hom (vT , rT ).
- -
-End LinAut.
- -
-Section LinearImageComp.
- -
-Variables (K : fieldType) (aT vT rT : vectType K).
-Implicit Types (f : 'Hom (aT , vT )) (g : 'Hom (vT , rT )) (U : {vspace aT }).
- -
-Lemma lim1g U : (\1 @: U)%VS = U.
- -
-Lemma limg_comp f g U : ((g \o f ) @: U = g @: (f @: U ))%VS.
- -
-End LinearImageComp.
- -
-Section LinearPreimage.
- -
-Variables (K : fieldType) (aT rT : vectType K).
-Implicit Types (f : 'Hom (aT , rT )) (U : {vspace aT }) (V W : {vspace rT }).
- -
-Lemma lpreim_cap_limg f W : (f @^-1: (W :&: limg f ))%VS = (f @^-1: W)%VS.
- -
-Lemma lpreim0 f : (f @^-1: 0)%VS = lker f.
- -
-Lemma lpreimS f V W : (V ≤ W)%VS→ (f @^-1: V ≤ f @^-1: W)%VS.
- -
-Lemma lpreimK f W : (W ≤ limg f)%VS → (f @: (f @^-1: W ))%VS = W.
- -
-Lemma memv_preim f u W : (f u \in W ) = (u \in f @^-1: W)%VS.
- -
-End LinearPreimage.
- -
- -
-Section LfunAlgebra.
-

- -

- This section is a bit of a place holder: the instances we build here can't - be canonical because we are missing an interface for proper vectTypes, - would sit between Vector and Falgebra. For now, we just supply structure - definitions here and supply actual instances for F-algebras in a submodule - of the algebra library (there is currently no actual use of the End(vT) - algebra structure). Also note that the unit ring structure is missing. -

- -
-Variables (R : comRingType) (vT : vectType R).
-Hypothesis vT_proper : Vector.dim vT > 0.
- -
-Fact lfun1_neq0 : \1%VF != 0 :> 'End (vT ).
- -
- -
-Definition lfun_comp_ringMixin :=
- RingMixin comp_lfunA comp_lfun1l comp_lfun1r comp_lfunDl comp_lfunDr
- lfun1_neq0.
-Definition lfun_comp_ringType := RingType 'End (vT ) lfun_comp_ringMixin.
- -
-

- -

- In the standard endomorphism ring product is categorical composition. -

-Definition lfun_ringMixin : GRing.Ring.mixin_of (lfun_zmodType vT vT) :=
-  GRing.converse_ringMixin lfun_comp_ringType.
-Definition lfun_ringType := Eval hnf in RingType 'End (vT ) lfun_ringMixin.
-Definition lfun_lalgType := Eval hnf in [lalgType R of 'End (vT )
-  for LalgType R lfun_ringType (fun k x y ⇒ comp_lfunZr k y x)].
-Definition lfun_algType := Eval hnf in [algType R of 'End (vT )
-  for AlgType R _ (fun k (x y : lfun_lalgType) ⇒ comp_lfunZl k y x)].
- -
-End LfunAlgebra.
- -
-Section Projection.
- -
-Variables (K : fieldType) (vT : vectType K).
-Implicit Types U V : {vspace vT }.
- -
-Definition daddv_pi U V := Vector.Hom (proj_mx (vs2mx U) (vs2mx V)).
-Definition projv U := daddv_pi U U ^C.
-Definition addv_pi1 U V := daddv_pi (U :\: V) V.
-Definition addv_pi2 U V := daddv_pi V (U :\: V).
- -
-Lemma memv_pi U V w : (daddv_pi U V) w \in U.
- -
-Lemma memv_proj U w : projv U w \in U.
- -
-Lemma memv_pi1 U V w : (addv_pi1 U V) w \in U.
- -
-Lemma memv_pi2 U V w : (addv_pi2 U V) w \in V.
- -
-Lemma daddv_pi_id U V u : (U :&: V = 0)%VS → u \in U → daddv_pi U V u = u.
- -
-Lemma daddv_pi_proj U V w (pi := daddv_pi U V) :
-  (U :&: V = 0)%VS → pi (pi w) = pi w.
- -
-Lemma daddv_pi_add U V w :
-  (U :&: V = 0)%VS → (w \in U + V)%VS → daddv_pi U V w + daddv_pi V U w = w.
- -
-Lemma projv_id U u : u \in U → projv U u = u.
- -
-Lemma projv_proj U w : projv U (projv U w) = projv U w.
- -
-Lemma memv_projC U w : w - projv U w \in (U ^C)%VS.
- -
-Lemma limg_proj U : limg (projv U) = U.
- -
-Lemma lker_proj U : lker (projv U) = (U ^C)%VS.
- -
-Lemma addv_pi1_proj U V w (pi1 := addv_pi1 U V) : pi1 (pi1 w) = pi1 w.
- -
-Lemma addv_pi2_id U V v : v \in V → addv_pi2 U V v = v.
- -
-Lemma addv_pi2_proj U V w (pi2 := addv_pi2 U V) : pi2 (pi2 w) = pi2 w.
- -
-Lemma addv_pi1_pi2 U V w :
-  w \in (U + V)%VS → addv_pi1 U V w + addv_pi2 U V w = w.
- -
-Section Sumv_Pi.
- -
-Variables (I : eqType) (r0 : seq I) (P : pred I) (Vs : I → {vspace vT }).
- -
-Let sumv_pi_rec i :=
-  fix loop r := if r is j :: r1 then
-    let V1 := (\sum_(k <- r1) Vs k)%VS in
-    if j == i then addv_pi1 (Vs j) V1 else (loop r1 \o addv_pi2 (Vs j) V1)%VF
-  else 0.
- -
-Notation sumV := (\sum_(i <- r0 | P i ) Vs i)%VS.
-Definition sumv_pi_for V of V = sumV := fun i ⇒ sumv_pi_rec i (filter P r0).
- -
-Variables (V : {vspace vT }) (defV : V = sumV).
- -
-Lemma memv_sum_pi i v : sumv_pi_for defV i v \in Vs i.
- -
-Lemma sumv_pi_uniq_sum v :
-    uniq (filter P r0) → v \in V →
-  \sum_(i <- r0 | P i ) sumv_pi_for defV i v = v.
- -
-End Sumv_Pi.
- -
-End Projection.
- -
-Notation sumv_pi V := (sumv_pi_for (erefl V)).
- -
-Section SumvPi.
- -
-Variable (K : fieldType) (vT : vectType K).
- -
-Lemma sumv_pi_sum (I : finType) (P : pred I) Vs v (V : {vspace vT })
-                  (defV : V = (\sum_(i | P i ) Vs i)%VS) :
-  v \in V → \sum_(i | P i ) sumv_pi_for defV i v = v :> vT.
- -
-Lemma sumv_pi_nat_sum m n (P : pred nat) Vs v (V : {vspace vT })
-                      (defV : V = (\sum_(m ≤ i < n | P i ) Vs i)%VS) :
-  v \in V → \sum_(m ≤ i < n | P i ) sumv_pi_for defV i v = v :> vT.
- -
-End SumvPi.
- -
-Section SubVector.
- -
-

- -

- Turn a {vspace V} into a vectType -

-Variable (K : fieldType) (vT : vectType K) (U : {vspace vT }).
- -
-Inductive subvs_of : predArgType := Subvs u & u \in U.
- -
-Definition vsval w := let: Subvs u _ := w in u.
-Canonical subvs_subType := Eval hnf in [subType for vsval ].
-Definition subvs_eqMixin := Eval hnf in [eqMixin of subvs_of by <:].
-Canonical subvs_eqType := Eval hnf in EqType subvs_of subvs_eqMixin.
-Definition subvs_choiceMixin := [choiceMixin of subvs_of by <:].
-Canonical subvs_choiceType := ChoiceType subvs_of subvs_choiceMixin.
-Definition subvs_zmodMixin := [zmodMixin of subvs_of by <:].
-Canonical subvs_zmodType := ZmodType subvs_of subvs_zmodMixin.
-Definition subvs_lmodMixin := [lmodMixin of subvs_of by <:].
-Canonical subvs_lmodType := LmodType K subvs_of subvs_lmodMixin.
- -
-Lemma subvsP w : vsval w \in U.
-Lemma subvs_inj : injective vsval.
-Lemma congr_subvs u v : u = v → vsval u = vsval v.
- -
-Lemma vsval_is_linear : linear vsval.
-Canonical vsval_additive := Additive vsval_is_linear.
-Canonical vsval_linear := AddLinear vsval_is_linear.
- -
-Fact vsproj_key : unit.
-Definition vsproj_def u := Subvs (memv_proj U u).
-Definition vsproj := locked_with vsproj_key vsproj_def.
-Canonical vsproj_unlockable := [unlockable fun vsproj ].
- -
-Lemma vsprojK : {in U , cancel vsproj vsval }.
- Lemma vsvalK : cancel vsval vsproj.
- -
-Lemma vsproj_is_linear : linear vsproj.
- Canonical vsproj_additive := Additive vsproj_is_linear.
-Canonical vsproj_linear := AddLinear vsproj_is_linear.
- -
-Fact subvs_vect_iso : Vector.axiom (\dim U) subvs_of.
- -
-Definition subvs_vectMixin := VectMixin subvs_vect_iso.
-Canonical subvs_vectType := VectType K subvs_of subvs_vectMixin.
- -
-End SubVector.
- -
-Section MatrixVectType.
- -
-Variables (R : ringType) (m n : nat).
- -
-

- -

- The apparently useless => /= in line 1 of the proof performs some evar - expansions that the Ltac interpretation of exists is incapable of doing. -

-Fact matrix_vect_iso : Vector.axiom (m × n) 'M [R ]_(m , n ).
-Definition matrix_vectMixin := VectMixin matrix_vect_iso.
-Canonical matrix_vectType := VectType R 'M [R ]_(m , n ) matrix_vectMixin.
- -
-End MatrixVectType.
- -
-

- -

- A ring is a one-dimension vector space -

-Section RegularVectType.
- -
-Variable R : ringType.
- -
-Fact regular_vect_iso : Vector.axiom 1 R ^o.
-Definition regular_vectMixin := VectMixin regular_vect_iso.
-Canonical regular_vectType := VectType R R ^o regular_vectMixin.
- -
-End RegularVectType.
- -
-

- -

- External direct product of two vectTypes. -

-Section ProdVector.
- -
-Variables (R : ringType) (vT1 vT2 : vectType R).
- -
-Fact pair_vect_iso : Vector.axiom (Vector.dim vT1 + Vector.dim vT2) (vT1 × vT2).
-Definition pair_vectMixin := VectMixin pair_vect_iso.
-Canonical pair_vectType := VectType R (vT1 × vT2) pair_vectMixin.
- -
-End ProdVector.
- -
-

- -

- Function from a finType into a ring form a vectype. -

-Section FunVectType.
- -
-Variable (I : finType) (R : ringType) (vT : vectType R).
- -
-

- -

- Type unification with exist is again a problem in this proof. -

-Fact ffun_vect_iso : Vector.axiom (#|I | × Vector.dim vT) {ffun I → vT }.
- -
-Definition ffun_vectMixin := VectMixin ffun_vect_iso.
-Canonical ffun_vectType := VectType R {ffun I → vT } ffun_vectMixin.
- -
-End FunVectType.
- -
-Canonical exp_vectType (K : fieldType) (vT : vectType K) n :=
- [vectType K of vT ^ n ].
- -
-

- -

- Solving a tuple of linear equations. -

-Section Solver.
- -
-Variable (K : fieldType) (vT : vectType K).
-Variables (n : nat) (lhs : n .-tuple 'End (vT )) (rhs : n .-tuple vT).
- -
-Let lhsf u := finfun ((tnth lhs )^~ u).
-Definition vsolve_eq U := finfun (tnth rhs) \in (linfun lhsf @: U)%VS.
- -
-Lemma vsolve_eqP (U : {vspace vT }) :
- reflect (exists2 u, u \in U & ∀ i, tnth lhs i u = tnth rhs i)
- (vsolve_eq U).
- -
-End Solver.
- -
-