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
rVof e v == row vector in 'rV_(\dim vT) of coordinates of
v : vT in the basis e
vecof e v == vector in vT whose coordinates in the basis e are
given by v : 'rV_(\dim vT)
Note that this is the inverse of rVof.
mxof e e' f == \dim uT * \dim vT matrix of the linear function
f : 'Hom(uT, vT) in the bases e of uT and e' of vT,
acting on row vectors
hommx e f M == linear function in 'Hom(uT, vT) whose matrix
in the bases e and f is M : 'M_(\dim uT, \dim vT)
Note that this is the inverse of mxof.
vsof e M == the subspace of vT generated by the rows of M,
seen as coordinates in the basis e
msof e U == matrix whose rows, seen as coordinates in the
basis e, generate the subspace U of vT
Note that this is the inverse of vsof.
'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, <<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 U by the linear function f
(f @^-1: U)%VS == the pre-image of U 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
leigenspace f a == linear eigenspace of the linear function f for
the (potential) eigenvalue a
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
leigenvalue f a == a is a linear eigenvalue of the linear function f
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) :=
{v2r : V → 'rV[R]_n | linear v2r & bijective v2r}.
Arguments vector_axiom_def [R] n%N V%type.
#[mathcomp(axiom="vector_axiom_def"), short(type="vectType")]
HB.structure Definition Vector (R : ringType) :=
{ V of Lmodule_hasFinDim R V & GRing.Lmodule R V }.
#[deprecated(since="mathcomp 2.2.0", note="Use Vector.axiom instead.")]
Notation vector_axiom := Vector.axiom.
Arguments dim {R} s.
{v2r : V → 'rV[R]_n | linear v2r & bijective v2r}.
Arguments vector_axiom_def [R] n%N V%type.
#[mathcomp(axiom="vector_axiom_def"), short(type="vectType")]
HB.structure Definition Vector (R : ringType) :=
{ V of Lmodule_hasFinDim R V & GRing.Lmodule R V }.
#[deprecated(since="mathcomp 2.2.0", note="Use Vector.axiom instead.")]
Notation vector_axiom := Vector.axiom.
Arguments dim {R} s.
FIXME: S/space and H/hom were defined behind the module Vector *
Perhaps we should change their names to avoid conflicts.
Section OtherDefs.
Local Coercion dim : Vector.type >-> nat.
Inductive space (K : fieldType) (vT : Vector.type K) :=
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.
Local Coercion dim : Vector.type >-> nat.
Inductive space (K : fieldType) (vT : Vector.type K) :=
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.
Arguments space [K] vT%type.
Notation "{ 'vspace' vT }" := (space 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).
Local Coercion dim : Vector.type >-> nat.
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).
Local Coercion dim : Vector.type >-> nat.
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 (U : @space K vT) := 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).
Local Coercion dim : Vector.type >-> nat.
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).
Local Coercion dim : Vector.type >-> nat.
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 (U : @space K vT) := 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 (U : space vT) : {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}).
Local Notation subV := (@subsetv K vT) (only parsing).
Local Notation addV := (@addv K vT) (only parsing).
Local Notation capV := (@capv K vT) (only parsing).
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_op 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_op 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_op 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.
Lemma dimv_eq0 U : (\dim U == 0) = (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) = (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.
Local Notation directv A := (directv_def (Phantom {vspace _} A%VS)).
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.
Local Notation directv A := (directv_def (Phantom {vspace _} A%VS)).
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).
Local Infix "*:l" := scale_lfun (at level 40).
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 subset_limgP f U (r : seq rT) :
{subset r ≤ (f @: U)%VS} ↔ (exists2 a, all (mem U) a & r = map f a).
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.
Lemma lker0_img_cap f U V : lker f == 0%VS →
(f @: (U :&: V) = f @: U :&: f @: V)%VS.
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).
Local Infix "*:l" := scale_lfun (at level 40).
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 subset_limgP f U (r : seq rT) :
{subset r ≤ (f @: U)%VS} ↔ (exists2 a, all (mem U) a & r = map f a).
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.
Lemma lker0_img_cap f U V : lker f == 0%VS →
(f @: (U :&: V) = f @: U :&: f @: V)%VS.
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.
Lemma SubvsE x (xU : x \in U) : Subvs xU = vsproj x.
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.
Lemma SubvsE x (xU : x \in U) : Subvs xU = vsproj x.
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.
Fact matrix_vect_iso : Vector.axiom (m × n) 'M[R]_(m, n).
Lemma dim_matrix : dim 'M[R]_(m, n) = m × n.
End MatrixVectType.
Lemma dim_matrix : dim 'M[R]_(m, n) = m × n.
End MatrixVectType.
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.
Section lfunP.
Variable (F : fieldType).
Context {uT vT : vectType F}.
Local Notation m := (\dim {:uT}).
Local Notation n := (\dim {:vT}).
Lemma span_lfunP (U : seq uT) (phi psi : 'Hom(uT,vT)) :
{in <<U>>%VS, phi =1 psi} ↔ {in U, phi =1 psi}.
Lemma fullv_lfunP (U : seq uT) (phi psi : 'Hom(uT,vT)) : <<U>>%VS = fullv →
phi = psi ↔ {in U, phi =1 psi}.
End lfunP.
Module passmx.
Section passmx.
Variable (F : fieldType).
Section vecmx.
Context {vT : vectType F}.
Local Notation n := (\dim {:vT}).
Variables (e : n.-tuple vT).
Definition rVof (v : vT) := \row_i coord e i v.
Lemma rVof_linear : linear rVof.
Lemma coord_rVof i v : coord e i v = rVof v 0 i.
Definition vecof (v : 'rV_n) := \sum_i v 0 i *: e`_i.
Lemma vecof_delta i : vecof (delta_mx 0 i) = e`_i.
Lemma vecof_linear : linear vecof.
Variable e_basis : basis_of {:vT} e.
Lemma rVofK : cancel rVof vecof.
Lemma vecofK : cancel vecof rVof.
Lemma rVofE (i : 'I_n) : rVof e`_i = delta_mx 0 i.
Lemma coord_vecof i v : coord e i (vecof v) = v 0 i.
Lemma rVof_eq0 v : (rVof v == 0) = (v == 0).
Lemma vecof_eq0 v : (vecof v == 0) = (v == 0).
End vecmx.
Section hommx.
Context {uT vT : vectType F}.
Local Notation m := (\dim {:uT}).
Local Notation n := (\dim {:vT}).
Variables (e : m.-tuple uT) (e' : n.-tuple vT).
Definition mxof (h : 'Hom(uT, vT)) := lin1_mx (rVof e' \o h \o vecof e).
Lemma mxof_linear : linear mxof.
Definition funmx (M : 'M[F]_(m, n)) u := vecof e' (rVof e u ×m M).
Lemma funmx_linear M : linear (funmx M).
Definition hommx M : 'Hom(uT, vT) := linfun (funmx M).
Lemma hommx_linear : linear hommx.
Hypothesis e_basis: basis_of {:uT} e.
Hypothesis f_basis: basis_of {:vT} e'.
Lemma mxofK : cancel mxof hommx.
Lemma hommxK : cancel hommx mxof.
Lemma mul_mxof phi u : u ×m mxof phi = rVof e' (phi (vecof e u)).
Lemma hommxE M u : hommx M u = vecof e' (rVof e u ×m M).
Lemma rVof_mul M u : rVof e u ×m M = rVof e' (hommx M u).
Lemma hom_vecof (phi : 'Hom(uT, vT)) u :
phi (vecof e u) = vecof e' (u ×m mxof phi).
Lemma rVof_app (phi : 'Hom(uT, vT)) u :
rVof e' (phi u) = rVof e u ×m mxof phi.
Lemma vecof_mul M u : vecof e' (u ×m M) = hommx M (vecof e u).
Lemma mxof_eq0 phi : (mxof phi == 0) = (phi == 0).
Lemma hommx_eq0 M : (hommx M == 0) = (M == 0).
End hommx.
Section hommx_comp.
Context {uT vT wT : vectType F}.
Local Notation m := (\dim {:uT}).
Local Notation n := (\dim {:vT}).
Local Notation p := (\dim {:wT}).
Variables (e : m.-tuple uT) (f : n.-tuple vT) (g : p.-tuple wT).
Hypothesis e_basis: basis_of {:uT} e.
Hypothesis f_basis: basis_of {:vT} f.
Hypothesis g_basis: basis_of {:wT} g.
Lemma mxof_comp (phi : 'Hom(uT, vT)) (psi : 'Hom(vT, wT)) :
mxof e g (psi \o phi)%VF = mxof e f phi ×m mxof f g psi.
Lemma hommx_mul (A : 'M_(m,n)) (B : 'M_(n, p)) :
hommx e g (A ×m B) = (hommx f g B \o hommx e f A)%VF.
End hommx_comp.
Section vsms.
Context {vT : vectType F}.
Local Notation n := (\dim {:vT}).
Variables (e : n.-tuple vT).
Definition msof (V : {vspace vT}) : 'M_n := mxof e e (projv V).
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.
Section lfunP.
Variable (F : fieldType).
Context {uT vT : vectType F}.
Local Notation m := (\dim {:uT}).
Local Notation n := (\dim {:vT}).
Lemma span_lfunP (U : seq uT) (phi psi : 'Hom(uT,vT)) :
{in <<U>>%VS, phi =1 psi} ↔ {in U, phi =1 psi}.
Lemma fullv_lfunP (U : seq uT) (phi psi : 'Hom(uT,vT)) : <<U>>%VS = fullv →
phi = psi ↔ {in U, phi =1 psi}.
End lfunP.
Module passmx.
Section passmx.
Variable (F : fieldType).
Section vecmx.
Context {vT : vectType F}.
Local Notation n := (\dim {:vT}).
Variables (e : n.-tuple vT).
Definition rVof (v : vT) := \row_i coord e i v.
Lemma rVof_linear : linear rVof.
Lemma coord_rVof i v : coord e i v = rVof v 0 i.
Definition vecof (v : 'rV_n) := \sum_i v 0 i *: e`_i.
Lemma vecof_delta i : vecof (delta_mx 0 i) = e`_i.
Lemma vecof_linear : linear vecof.
Variable e_basis : basis_of {:vT} e.
Lemma rVofK : cancel rVof vecof.
Lemma vecofK : cancel vecof rVof.
Lemma rVofE (i : 'I_n) : rVof e`_i = delta_mx 0 i.
Lemma coord_vecof i v : coord e i (vecof v) = v 0 i.
Lemma rVof_eq0 v : (rVof v == 0) = (v == 0).
Lemma vecof_eq0 v : (vecof v == 0) = (v == 0).
End vecmx.
Section hommx.
Context {uT vT : vectType F}.
Local Notation m := (\dim {:uT}).
Local Notation n := (\dim {:vT}).
Variables (e : m.-tuple uT) (e' : n.-tuple vT).
Definition mxof (h : 'Hom(uT, vT)) := lin1_mx (rVof e' \o h \o vecof e).
Lemma mxof_linear : linear mxof.
Definition funmx (M : 'M[F]_(m, n)) u := vecof e' (rVof e u ×m M).
Lemma funmx_linear M : linear (funmx M).
Definition hommx M : 'Hom(uT, vT) := linfun (funmx M).
Lemma hommx_linear : linear hommx.
Hypothesis e_basis: basis_of {:uT} e.
Hypothesis f_basis: basis_of {:vT} e'.
Lemma mxofK : cancel mxof hommx.
Lemma hommxK : cancel hommx mxof.
Lemma mul_mxof phi u : u ×m mxof phi = rVof e' (phi (vecof e u)).
Lemma hommxE M u : hommx M u = vecof e' (rVof e u ×m M).
Lemma rVof_mul M u : rVof e u ×m M = rVof e' (hommx M u).
Lemma hom_vecof (phi : 'Hom(uT, vT)) u :
phi (vecof e u) = vecof e' (u ×m mxof phi).
Lemma rVof_app (phi : 'Hom(uT, vT)) u :
rVof e' (phi u) = rVof e u ×m mxof phi.
Lemma vecof_mul M u : vecof e' (u ×m M) = hommx M (vecof e u).
Lemma mxof_eq0 phi : (mxof phi == 0) = (phi == 0).
Lemma hommx_eq0 M : (hommx M == 0) = (M == 0).
End hommx.
Section hommx_comp.
Context {uT vT wT : vectType F}.
Local Notation m := (\dim {:uT}).
Local Notation n := (\dim {:vT}).
Local Notation p := (\dim {:wT}).
Variables (e : m.-tuple uT) (f : n.-tuple vT) (g : p.-tuple wT).
Hypothesis e_basis: basis_of {:uT} e.
Hypothesis f_basis: basis_of {:vT} f.
Hypothesis g_basis: basis_of {:wT} g.
Lemma mxof_comp (phi : 'Hom(uT, vT)) (psi : 'Hom(vT, wT)) :
mxof e g (psi \o phi)%VF = mxof e f phi ×m mxof f g psi.
Lemma hommx_mul (A : 'M_(m,n)) (B : 'M_(n, p)) :
hommx e g (A ×m B) = (hommx f g B \o hommx e f A)%VF.
End hommx_comp.
Section vsms.
Context {vT : vectType F}.
Local Notation n := (\dim {:vT}).
Variables (e : n.-tuple vT).
Definition msof (V : {vspace vT}) : 'M_n := mxof e e (projv V).
alternative
(\sum_(v <- vbasis V) <<rVof e v>>)%MS.
alternative
<< [seq vecof e (row i M) | i : 'I_n]#>>%VS.
Lemma mxof1 : free e → mxof e e \1 = 1%:M.
Hypothesis e_basis : basis_of {:vT} e.
Lemma hommx1 : hommx e e 1%:M = \1%VF.
Lemma msofK : cancel msof vsof.
Lemma mem_vecof u (V : {vspace vT}) : (vecof e u \in V) = (u ≤ msof V)%MS.
Lemma rVof_sub u M : (rVof e u ≤ M)%MS = (u \in vsof M).
Lemma vsof_sub M V : (vsof M ≤ V)%VS = (M ≤ msof V)%MS.
Lemma msof_sub V M : (msof V ≤ M)%MS = (V ≤ vsof M)%VS.
Lemma vsofK M : (msof (vsof M) == M)%MS.
Lemma sub_msof : {mono msof : V V' / (V ≤ V')%VS >-> (V ≤ V')%MS}.
Lemma sub_vsof : {mono vsof : M M' / (M ≤ M')%MS >-> (M ≤ M')%VS}.
Lemma msof0 : msof 0 = 0.
Lemma vsof0 : vsof 0 = 0%VS.
Lemma msof_eq0 V : (msof V == 0) = (V == 0%VS).
Lemma vsof_eq0 M : (vsof M == 0%VS) = (M == 0).
End vsms.
Section eigen.
Context {uT : vectType F}.
Definition leigenspace (phi : 'End(uT)) a := lker (phi - a *: \1%VF).
Definition leigenvalue phi a := leigenspace phi a != 0%VS.
Local Notation m := (\dim {:uT}).
Variables (e : m.-tuple uT).
Hypothesis e_basis: basis_of {:uT} e.
Let e_free := basis_free e_basis.
Lemma lker_ker phi : lker phi = vsof e (kermx (mxof e e phi)).
Lemma limgE phi : limg phi = vsof e (mxof e e phi).
Lemma leigenspaceE f a : leigenspace f a = vsof e (eigenspace (mxof e e f) a).
End eigen.
End passmx.
End passmx.