Library mathcomp.algebra.vector
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype bigop finfun tuple.
From mathcomp Require Import ssralg matrix mxalgebra zmodp.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype bigop finfun tuple.
From mathcomp Require Import ssralg matrix mxalgebra zmodp.
Finite dimensional vector spaces
NB: See CONTRIBUTING.md for an introduction to HB concepts and commands.
vectType R == interface structure for finite dimensional (more
precisely, detachable) vector spaces over R, which
should be at least a ringType
The HB class is called Vector.
Vector.axiom n M <-> type M is linearly isomorphic to 'rV_n
:= {v2r : M -> 'rV_n| linear v2r & bijective v2r}
{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.
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,
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
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
Set Implicit Arguments.
Declare Scope vspace_scope.
Declare Scope lfun_scope.
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
Definition vector_axiom_def (R : ringType) n (V : lmodType R) of phant V :=
{v2r : V → 'rV[R]_n | linear v2r & bijective v2r}.
#[mathcomp(axiom="vector_axiom_def"), infer(R), short(type="vectType")]
HB.structure Definition Vector (R : ringType) :=
{ V of Lmodule_hasFinDim R V & GRing.Lmodule R V }.
{v2r : V → 'rV[R]_n | linear v2r & bijective v2r}.
#[mathcomp(axiom="vector_axiom_def"), infer(R), short(type="vectType")]
HB.structure Definition Vector (R : ringType) :=
{ V of Lmodule_hasFinDim R V & GRing.Lmodule R V }.
FIXME: S/space and H/hom were defined behind the module Vector *
Perhaps we should change their names to avoid conflits.
Section OtherDefs.
Inductive space (K : fieldType) (vT : Vector.type K) (phV : phant vT) :=
Space (mx : 'M[K]_vT) & <<mx>>%MS == mx.
Inductive hom (R : ringType) (vT wT : Vector.type R) :=
Hom of 'M[R]_(vT, wT).
End OtherDefs.
Inductive space (K : fieldType) (vT : Vector.type K) (phV : phant vT) :=
Space (mx : 'M[K]_vT) & <<mx>>%MS == mx.
Inductive hom (R : ringType) (vT wT : Vector.type R) :=
Hom of 'M[R]_(vT, wT).
End OtherDefs.
/FIXME
Module Import VectorExports.
Bind Scope ring_scope with Vector.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use Vector.clone instead.")]
Notation "[ 'vectType' R 'of' T 'for' cT ]" := (Vector.clone R T%type cT)
(at level 0, format "[ 'vectType' R 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use Vector.clone instead.")]
Notation "[ 'vectType' R 'of' T ]" := (Vector.clone R T%type _)
(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.
Bind Scope vspace_scope with space.
Delimit Scope lfun_scope with VF.
Bind Scope lfun_scope with hom.
End VectorExports.
The contents of this module exposes the matrix encodings, and should
therefore not be used outside of the vector library implementation.
Module VectorInternalTheory.
Section Iso.
Variables (R : ringType) (vT rT : vectType R).
Fact v2r_subproof : vector_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.
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).
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.
End Hom.
Arguments mx2vs {K vT m%N} A%MS.
End VectorInternalTheory.
Export VectorExports.
Import VectorInternalTheory.
Section VspaceDefs.
Variables (K : fieldType) (vT : vectType K).
Implicit Types (u : vT) (X : seq vT) (U V : {vspace vT}).
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 : vector_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.
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).
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.
End Hom.
Arguments mx2vs {K vT m%N} A%MS.
End VectorInternalTheory.
Export VectorExports.
Import VectorInternalTheory.
Section VspaceDefs.
Variables (K : fieldType) (vT : vectType K).
Implicit Types (u : vT) (X : seq vT) (U V : {vspace vT}).
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 : 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].
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 : 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.
Arguments fullv {K vT}.
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}).
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.
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).
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.
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.
Arguments sumv_sup i0 [P U 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.
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.
Arguments sumv_sup i0 [P U 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.
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} = 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} = 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).
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.
#[global] Hint Resolve subvv : core.
Arguments subvP {K vT U V}.
Arguments addv_idPl {K vT U V}.
Arguments addv_idPr {K vT U V}.
Arguments memv_addP {K vT w U V }.
Arguments sumv_sup [K vT I] i0 [P U Vs].
Arguments memv_sumP {K vT I P Us v}.
Arguments subv_sumP {K vT I P Us V}.
Arguments capv_idPl {K vT U V}.
Arguments capv_idPr {K vT U V}.
Arguments memv_capP {K vT w U V}.
Arguments bigcapv_inf [K vT I] i0 [P Us V].
Arguments subv_bigcapP {K vT I P U Vs}.
Arguments directvP {K vT S}.
Arguments directv_addP {K vT U V}.
Arguments directv_add_unique {K vT U V}.
Arguments directv_sumP {K vT I P Us}.
Arguments directv_sumE {K vT I P Ss}.
Arguments directv_sum_independent {K vT I P Us}.
Arguments directv_sum_unique {K vT I P Us}.
Arguments span_subvP {K vT X U}.
Arguments freeP {K vT n X}.
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) :=
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 : 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)) := 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).
Fact lfun_is_linear f : 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.
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.
Arguments fun_of_lfunK {R aT rT}.
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.
Lemma scale_lfunE k f x : (k *: f) x = k *: f x.
Fact lfun_vect_iso : vector_axiom (dim aT × dim rT) 'Hom(aT, rT).
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 limgD 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.
Arguments memv_imgP {K aT rT f w U}.
Arguments lfunPn {K aT rT f g}.
Arguments lker0P {K aT rT f}.
Arguments eqlfunP {K aT rT f g v}.
Arguments eqlfun_inP {K aT rT V f g}.
Arguments limg_lfunVK {K aT rT f} [x] f_x.
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.
Arguments fixedSpaceP {K vT f a}.
Arguments fixedSpacesP {K vT f U}.
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.
Arguments lpreimK {K aT rT f} [W] fW.
Section LfunAlgebra.
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) :=
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 : 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)) := 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).
Fact lfun_is_linear f : 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.
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.
Arguments fun_of_lfunK {R aT rT}.
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.
Lemma scale_lfunE k f x : (k *: f) x = k *: f x.
Fact lfun_vect_iso : vector_axiom (dim aT × dim rT) 'Hom(aT, rT).
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 limgD 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.
Arguments memv_imgP {K aT rT f w U}.
Arguments lfunPn {K aT rT f g}.
Arguments lker0P {K aT rT f}.
Arguments eqlfunP {K aT rT f g v}.
Arguments eqlfun_inP {K aT rT V f g}.
Arguments limg_lfunVK {K aT rT f} [x] f_x.
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.
Arguments fixedSpaceP {K vT f a}.
Arguments fixedSpacesP {K vT f U}.
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.
Arguments lpreimK {K aT rT f} [W] fW.
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 : dim vT > 0.
Fact lfun1_neq0 : \1%VF != 0 :> 'End(vT).
FIXME: as explained above, the following structures should not be declared *
as canonical, so mixins and structures are built separately, and we *
don't use HB.instance Definition _ := ... *
This is ok, but maybe we could introduce an alias
Definition lfun_comp_ringMixin := GRing.Zmodule_isRing.Build 'End(vT)
comp_lfunA comp_lfun1l comp_lfun1r comp_lfunDl comp_lfunDr lfun1_neq0.
Definition lfun_comp_ringType : ringType :=
HB.pack 'End(vT) lfun_comp_ringMixin.
comp_lfunA comp_lfun1l comp_lfun1r comp_lfunDl comp_lfunDr lfun1_neq0.
Definition lfun_comp_ringType : ringType :=
HB.pack 'End(vT) lfun_comp_ringMixin.
In the standard endomorphism ring product is categorical composition.
Definition lfun_ringType : ringType := lfun_comp_ringType^c.
Definition lfun_lalgMixin := GRing.Lmodule_isLalgebra.Build R lfun_ringType
(fun k x y ⇒ comp_lfunZr k y x).
Definition lfun_lalgType : lalgType R :=
HB.pack 'End(vT) lfun_ringType lfun_lalgMixin.
Definition lfun_algMixin := GRing.Lalgebra_isAlgebra.Build R lfun_lalgType
(fun k x y ⇒ comp_lfunZl k y x).
Definition lfun_algType : algType R :=
HB.pack 'End(vT) lfun_lalgType lfun_algMixin.
End LfunAlgebra.
Section Projection.
Variables (K : fieldType) (vT : vectType K).
Implicit Types U V : {vspace vT}.
Definition daddv_pi U V := 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.
Definition lfun_lalgMixin := GRing.Lmodule_isLalgebra.Build R lfun_ringType
(fun k x y ⇒ comp_lfunZr k y x).
Definition lfun_lalgType : lalgType R :=
HB.pack 'End(vT) lfun_ringType lfun_lalgMixin.
Definition lfun_algMixin := GRing.Lalgebra_isAlgebra.Build R lfun_lalgType
(fun k x y ⇒ comp_lfunZl k y x).
Definition lfun_algType : algType R :=
HB.pack 'End(vT) lfun_lalgType lfun_algMixin.
End LfunAlgebra.
Section Projection.
Variables (K : fieldType) (vT : vectType K).
Implicit Types U V : {vspace vT}.
Definition daddv_pi U V := 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 : vT := let: Subvs u _ := w in u.
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.
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.
Fact subvs_vect_iso : vector_axiom (\dim U) subvs_of.
End SubVector.
Arguments subvs_inj {K vT U} [x1 x2].
Arguments vsprojK {K vT U} [x] Ux.
Section MatrixVectType.
Variables (R : ringType) (m n : nat).
Inductive subvs_of : predArgType := Subvs u & u \in U.
Definition vsval w : vT := let: Subvs u _ := w in u.
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.
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.
Fact subvs_vect_iso : vector_axiom (\dim U) subvs_of.
End SubVector.
Arguments subvs_inj {K vT U} [x1 x2].
Arguments vsprojK {K vT U} [x] Ux.
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.
A ring is a one-dimension vector space
Section RegularVectType.
Variable R : ringType.
Fact regular_vect_iso : vector_axiom 1 R^o.
End RegularVectType.
Variable R : ringType.
Fact regular_vect_iso : vector_axiom 1 R^o.
End RegularVectType.
External direct product of two vectTypes.
Section ProdVector.
Variables (R : ringType) (vT1 vT2 : vectType R).
Fact pair_vect_iso : vector_axiom (dim vT1 + dim vT2) (vT1 × vT2).
End ProdVector.
Variables (R : ringType) (vT1 vT2 : vectType R).
Fact pair_vect_iso : vector_axiom (dim vT1 + dim vT2) (vT1 × vT2).
End ProdVector.
Function from a finType into a ring form a vectype.
Type unification with exist is again a problem in this proof.
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.