Library mathcomp.algebra.vector
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
+
+ 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.
+
+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. + +
+
+
+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.
+ +
+
+
++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 V)
+}.
+ +
+Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
+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 T.
+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 T)) :=
+ fun bT b & phant_id (@GRing.Lmodule.class _ phR bT) b ⇒
+ fun m & phant_id m0 m ⇒ Pack phR (@Class T b m) T.
+ +
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
+ +
+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.
+ +
+
+
++ +
+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 V)
+}.
+ +
+Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
+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 T.
+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 T)) :=
+ fun bT b & phant_id (@GRing.Lmodule.class _ phR bT) b ⇒
+ fun m & phant_id m0 m ⇒ Pack phR (@Class T b m) T.
+ +
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
+ +
+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).
+ +
+
+
++ +
+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_class :=
+ fun v ⇒ (vs2mx (vline v) ≤ vs2mx U)%MS.
+Canonical vspace_predType :=
+ @mkPredType _ (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].
+ +
+
+
++ fun v ⇒ (vs2mx (vline v) ≤ vs2mx U)%MS.
+Canonical vspace_predType :=
+ @mkPredType _ (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_class.
+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.
+ +
+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).
+ +
+
+
++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_class.
+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.
+ +
+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).
+ +
+
+
++ +
+Lemma subv0 U : (U ≤ 0)%VS = (U == 0%VS).
+ +
+Lemma memv0 v : v \in 0%VS = (v == 0).
+ +
+
+ Full space
+
+
+
+
+ Picking a non-zero vector in a subspace.
+
+
+
+
+ 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.
+ +
+
+
++ +
+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.
+ +
+
+
++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
+
+
+
+
+ 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.
+ +
+
+
++ +
+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.
+ +
+
+
++ +
+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)
+}.
+ +
+
+
++ 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.
+ +
+
+
++ 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.
+ +
+
+
++ +
+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.
+ +
+
+
++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}.
+ +
+
+
++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.
+ +
+Notation directv S := (directv_def (Phantom _ S%VS)).
+ +
+
+
++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.
+ +
+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).
+ +
+Canonical 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.
+ +
+
+
++ +
+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).
+ +
+Canonical 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.
+
+
++ +
+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.
+ +
+
+
++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.
+ +
+
+
++ 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).
+ +
+
+
++ +
+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.
+ +
+
+
++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.
+ +
+
+
++ +
+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.
+ +
+
+
++ +
+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.
+
+
+
+
+ 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].
+ +
+
+
++ +
+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.
+ +
+
++ +
+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.
+ +
+