Library mathcomp.algebra.vector
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
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 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
vectType R == interface structure for finite dimensional (more precisely, detachable) vector spaces over R, which should be at least a ringType. Vector.axiom n M <-> type M is linearly isomorphic to 'rV_n. := {v2r : M -> 'rV_n| linear v2r & bijective v2r}. VectMixin isoM == packages a proof isoV of Vector.axiom n M as the vectType mixin for an n-dimensional R-space structure on a type M that is an lmodType R. VectType K M mT == packs the vectType mixin mT to into a vectType K instance for T; T should have an lmodType K canonical instance. [vectType R of T for vS] == a copy of the vS : vectType R structure where the sort is replaced by T; vS : lmodType R should be convertible to a canonical lmodType for T. [vectType R of V] == a clone of an existing vectType R structure on V. {vspace vT} == the type of (detachable) subspaces of vT; vT should have a vectType structure over a fieldType. subvs_of U == the subtype of elements of V in the subspace U. This is canonically a vectType. vsval u == linear injection of u : subvs_of U into V. vsproj U v == linear projection of v : V in subvs U. 'Hom(aT, rT) == the type of linear functions (homomorphisms) from aT to rT, where aT and rT ARE vectType structures. Elements of 'Hom(aT, rT) coerce to Coq functions. > Caveat: aT and rT must denote actual vectType structures, not their projections on Type. linfun f == a vector linear function in 'Hom(aT, rT) that coincides with f : aT -> rT when f is linear. 'End(vT) == endomorphisms of vT (:= 'Hom(vT, vT)). > The types subvs_of U, 'Hom(aT, rT), 'End(vT), K^o, 'M[K](m, n), vT * wT, {ffun I -> vT}, vT ^ n all have canonical vectType instances.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
Module Vector.
Section ClassDef.
Variable R : ringType.
Definition axiom_def n (V : lmodType R) of phant V :=
{v2r : V → 'rV[R]_n | linear v2r & bijective v2r}.
Inductive mixin_of (V : lmodType R) := Mixin dim & axiom_def dim (Phant V).
Record class_of V := Class {
base : GRing.Lmodule.class_of R V;
mixin : mixin_of (GRing.Lmodule.Pack _ base)
}.
Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
Variables (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack phR T c.
Definition dim := let: Mixin n _ := mixin class in n.
Definition pack b0 (m0 : mixin_of (@GRing.Lmodule.Pack R _ T b0)) :=
fun bT b & phant_id (@GRing.Lmodule.class _ phR bT) b ⇒
fun m & phant_id m0 m ⇒ Pack phR (@Class T b m).
Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @GRing.Zmodule.Pack cT class.
Definition lmodType := @GRing.Lmodule.Pack R phR cT class.
End ClassDef.
Notation axiom n V := (axiom_def n (Phant V)).
Section OtherDefs.
Inductive space (K : fieldType) (vT : type (Phant K)) (phV : phant vT) :=
Space (mx : 'M[K]_vT) & <<mx>>%MS == mx.
Inductive hom (R : ringType) (vT wT : type (Phant R)) :=
Hom of 'M[R]_(vT, wT).
End OtherDefs.
Module Import Exports.
Coercion base : class_of >-> GRing.Lmodule.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType: type >-> Equality.type.
Bind Scope ring_scope with sort.
Canonical eqType.
Coercion choiceType: type >-> Choice.type.
Canonical choiceType.
Coercion zmodType: type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion lmodType: type>-> GRing.Lmodule.type.
Canonical lmodType.
Notation vectType R := (@type _ (Phant R)).
Notation VectType R V mV :=
(@pack _ (Phant R) V _ mV _ _ id _ id).
Notation VectMixin := Mixin.
Notation "[ 'vectType' R 'of' T 'for' cT ]" := (@clone _ (Phant R) T cT _ idfun)
(at level 0, format "[ 'vectType' R 'of' T 'for' cT ]") : form_scope.
Notation "[ 'vectType' R 'of' T ]" := (@clone _ (Phant R) T _ _ idfun)
(at level 0, format "[ 'vectType' R 'of' T ]") : form_scope.
Notation "{ 'vspace' vT }" := (space (Phant vT)) : type_scope.
Notation "''Hom' ( aT , rT )" := (hom aT rT) : type_scope.
Notation "''End' ( vT )" := (hom vT vT) : type_scope.
Delimit Scope vspace_scope with VS.
Bind Scope vspace_scope with space.
Delimit Scope lfun_scope with VF.
Bind Scope lfun_scope with hom.
End Exports.
Section ClassDef.
Variable R : ringType.
Definition axiom_def n (V : lmodType R) of phant V :=
{v2r : V → 'rV[R]_n | linear v2r & bijective v2r}.
Inductive mixin_of (V : lmodType R) := Mixin dim & axiom_def dim (Phant V).
Record class_of V := Class {
base : GRing.Lmodule.class_of R V;
mixin : mixin_of (GRing.Lmodule.Pack _ base)
}.
Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
Variables (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack phR T c.
Definition dim := let: Mixin n _ := mixin class in n.
Definition pack b0 (m0 : mixin_of (@GRing.Lmodule.Pack R _ T b0)) :=
fun bT b & phant_id (@GRing.Lmodule.class _ phR bT) b ⇒
fun m & phant_id m0 m ⇒ Pack phR (@Class T b m).
Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @GRing.Zmodule.Pack cT class.
Definition lmodType := @GRing.Lmodule.Pack R phR cT class.
End ClassDef.
Notation axiom n V := (axiom_def n (Phant V)).
Section OtherDefs.
Inductive space (K : fieldType) (vT : type (Phant K)) (phV : phant vT) :=
Space (mx : 'M[K]_vT) & <<mx>>%MS == mx.
Inductive hom (R : ringType) (vT wT : type (Phant R)) :=
Hom of 'M[R]_(vT, wT).
End OtherDefs.
Module Import Exports.
Coercion base : class_of >-> GRing.Lmodule.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType: type >-> Equality.type.
Bind Scope ring_scope with sort.
Canonical eqType.
Coercion choiceType: type >-> Choice.type.
Canonical choiceType.
Coercion zmodType: type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion lmodType: type>-> GRing.Lmodule.type.
Canonical lmodType.
Notation vectType R := (@type _ (Phant R)).
Notation VectType R V mV :=
(@pack _ (Phant R) V _ mV _ _ id _ id).
Notation VectMixin := Mixin.
Notation "[ 'vectType' R 'of' T 'for' cT ]" := (@clone _ (Phant R) T cT _ idfun)
(at level 0, format "[ 'vectType' R 'of' T 'for' cT ]") : form_scope.
Notation "[ 'vectType' R 'of' T ]" := (@clone _ (Phant R) T _ _ idfun)
(at level 0, format "[ 'vectType' R 'of' T ]") : form_scope.
Notation "{ 'vspace' vT }" := (space (Phant vT)) : type_scope.
Notation "''Hom' ( aT , rT )" := (hom aT rT) : type_scope.
Notation "''End' ( vT )" := (hom vT vT) : type_scope.
Delimit Scope vspace_scope with VS.
Bind Scope vspace_scope with space.
Delimit Scope lfun_scope with VF.
Bind Scope lfun_scope with hom.
End Exports.
The contents of this module exposes the matrix encodings, and should
therefore not be used outside of the vector library implementation.
Module InternalTheory.
Section Iso.
Variables (R : ringType) (vT rT : vectType R).
Fact v2r_subproof : axiom vT vT.
Definition v2r := s2val v2r_subproof.
Let v2r_bij : bijective v2r := s2valP' v2r_subproof.
Fact r2v_subproof : {r2v | cancel r2v v2r}.
Definition r2v := sval r2v_subproof.
Lemma r2vK : cancel r2v v2r.
Lemma r2v_inj : injective r2v.
Lemma v2rK : cancel v2r r2v.
Lemma v2r_inj : injective v2r.
Canonical v2r_linear := Linear (s2valP v2r_subproof : linear v2r).
Canonical r2v_linear := Linear (can2_linear v2rK r2vK).
End Iso.
Section Vspace.
Variables (K : fieldType) (vT : vectType K).
Definition b2mx n (X : n.-tuple vT) := \matrix_i v2r (tnth X i).
Lemma b2mxK n (X : n.-tuple vT) i : r2v (row i (b2mx X)) = X`_i.
Definition vs2mx {phV} (U : @space K vT phV) := let: Space mx _ := U in mx.
Lemma gen_vs2mx (U : {vspace vT}) : <<vs2mx U>>%MS = vs2mx U.
Fact mx2vs_subproof m (A : 'M[K]_(m, vT)) : <<(<<A>>)>>%MS == <<A>>%MS.
Definition mx2vs {m} A : {vspace vT} := Space _ (@mx2vs_subproof m A).
Canonical space_subType := [subType for @vs2mx (Phant vT)].
Lemma vs2mxK : cancel vs2mx mx2vs.
Lemma mx2vsK m (M : 'M_(m, vT)) : (vs2mx (mx2vs M) :=: M)%MS.
End Vspace.
Section Hom.
Variables (R : ringType) (aT rT : vectType R).
Definition f2mx (f : 'Hom(aT, rT)) := let: Hom A := f in A.
Canonical hom_subType := [newType for f2mx].
End Hom.
Arguments mx2vs {K vT m%N} A%MS.
End InternalTheory.
End Vector.
Export Vector.Exports.
Import Vector.InternalTheory.
Section VspaceDefs.
Variables (K : fieldType) (vT : vectType K).
Implicit Types (u : vT) (X : seq vT) (U V : {vspace vT}).
Definition space_eqMixin := Eval hnf in [eqMixin of {vspace vT} by <:].
Canonical space_eqType := EqType {vspace vT} space_eqMixin.
Definition space_choiceMixin := Eval hnf in [choiceMixin of {vspace vT} by <:].
Canonical space_choiceType := ChoiceType {vspace vT} space_choiceMixin.
Definition dimv U := \rank (vs2mx U).
Definition subsetv U V := (vs2mx U ≤ vs2mx V)%MS.
Definition vline u := mx2vs (v2r u).
Section Iso.
Variables (R : ringType) (vT rT : vectType R).
Fact v2r_subproof : axiom vT vT.
Definition v2r := s2val v2r_subproof.
Let v2r_bij : bijective v2r := s2valP' v2r_subproof.
Fact r2v_subproof : {r2v | cancel r2v v2r}.
Definition r2v := sval r2v_subproof.
Lemma r2vK : cancel r2v v2r.
Lemma r2v_inj : injective r2v.
Lemma v2rK : cancel v2r r2v.
Lemma v2r_inj : injective v2r.
Canonical v2r_linear := Linear (s2valP v2r_subproof : linear v2r).
Canonical r2v_linear := Linear (can2_linear v2rK r2vK).
End Iso.
Section Vspace.
Variables (K : fieldType) (vT : vectType K).
Definition b2mx n (X : n.-tuple vT) := \matrix_i v2r (tnth X i).
Lemma b2mxK n (X : n.-tuple vT) i : r2v (row i (b2mx X)) = X`_i.
Definition vs2mx {phV} (U : @space K vT phV) := let: Space mx _ := U in mx.
Lemma gen_vs2mx (U : {vspace vT}) : <<vs2mx U>>%MS = vs2mx U.
Fact mx2vs_subproof m (A : 'M[K]_(m, vT)) : <<(<<A>>)>>%MS == <<A>>%MS.
Definition mx2vs {m} A : {vspace vT} := Space _ (@mx2vs_subproof m A).
Canonical space_subType := [subType for @vs2mx (Phant vT)].
Lemma vs2mxK : cancel vs2mx mx2vs.
Lemma mx2vsK m (M : 'M_(m, vT)) : (vs2mx (mx2vs M) :=: M)%MS.
End Vspace.
Section Hom.
Variables (R : ringType) (aT rT : vectType R).
Definition f2mx (f : 'Hom(aT, rT)) := let: Hom A := f in A.
Canonical hom_subType := [newType for f2mx].
End Hom.
Arguments mx2vs {K vT m%N} A%MS.
End InternalTheory.
End Vector.
Export Vector.Exports.
Import Vector.InternalTheory.
Section VspaceDefs.
Variables (K : fieldType) (vT : vectType K).
Implicit Types (u : vT) (X : seq vT) (U V : {vspace vT}).
Definition space_eqMixin := Eval hnf in [eqMixin of {vspace vT} by <:].
Canonical space_eqType := EqType {vspace vT} space_eqMixin.
Definition space_choiceMixin := Eval hnf in [choiceMixin of {vspace vT} by <:].
Canonical space_choiceType := ChoiceType {vspace vT} space_choiceMixin.
Definition dimv U := \rank (vs2mx U).
Definition subsetv U V := (vs2mx U ≤ vs2mx V)%MS.
Definition vline u := mx2vs (v2r u).
Vspace membership is defined as line inclusion.
Definition pred_of_vspace phV (U : Vector.space phV) : {pred vT} :=
fun v ⇒ (vs2mx (vline v) ≤ vs2mx U)%MS.
Canonical vspace_predType :=
@PredType _ (unkeyed {vspace vT}) (@pred_of_vspace _).
Definition fullv : {vspace vT} := mx2vs 1%:M.
Definition addv U V := mx2vs (vs2mx U + vs2mx V).
Definition capv U V := mx2vs (vs2mx U :&: vs2mx V).
Definition complv U := mx2vs (vs2mx U)^C.
Definition diffv U V := mx2vs (vs2mx U :\: vs2mx V).
Definition vpick U := r2v (nz_row (vs2mx U)).
Fact span_key : unit.
Definition span_expanded_def X := mx2vs (b2mx (in_tuple X)).
Definition span := locked_with span_key span_expanded_def.
Canonical span_unlockable := [unlockable fun span].
Definition vbasis_def U :=
[tuple r2v (row i (row_base (vs2mx U))) | i < dimv U].
Definition vbasis := locked_with span_key vbasis_def.
Canonical vbasis_unlockable := [unlockable fun vbasis].
fun v ⇒ (vs2mx (vline v) ≤ vs2mx U)%MS.
Canonical vspace_predType :=
@PredType _ (unkeyed {vspace vT}) (@pred_of_vspace _).
Definition fullv : {vspace vT} := mx2vs 1%:M.
Definition addv U V := mx2vs (vs2mx U + vs2mx V).
Definition capv U V := mx2vs (vs2mx U :&: vs2mx V).
Definition complv U := mx2vs (vs2mx U)^C.
Definition diffv U V := mx2vs (vs2mx U :\: vs2mx V).
Definition vpick U := r2v (nz_row (vs2mx U)).
Fact span_key : unit.
Definition span_expanded_def X := mx2vs (b2mx (in_tuple X)).
Definition span := locked_with span_key span_expanded_def.
Canonical span_unlockable := [unlockable fun span].
Definition vbasis_def U :=
[tuple r2v (row i (row_base (vs2mx U))) | i < dimv U].
Definition vbasis := locked_with span_key vbasis_def.
Canonical vbasis_unlockable := [unlockable fun vbasis].
coord and directv are defined in the VectorTheory section.
Definition free X := dimv (span X) == size X.
Definition basis_of U X := (span X == U) && free X.
End VspaceDefs.
Coercion pred_of_vspace : Vector.space >-> pred_sort.
Notation "\dim U" := (dimv U) : nat_scope.
Notation "U <= V" := (subsetv U V) : vspace_scope.
Notation "U <= V <= W" := (subsetv U V && subsetv V W) : vspace_scope.
Notation "<[ v ] >" := (vline v) : vspace_scope.
Notation "<< X >>" := (span X) : vspace_scope.
Notation "0" := (vline 0) : vspace_scope.
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}).
Fact vspace_key U : pred_key U.
Canonical vspace_keyed U := KeyedPred (vspace_key U).
Lemma memvE v U : (v \in U) = (<[v]> ≤ U)%VS.
Lemma vlineP v1 v2 : reflect (∃ k, v1 = k *: v2) (v1 \in <[v2]>)%VS.
Fact memv_submod_closed U : submod_closed U.
Canonical memv_opprPred U := OpprPred (memv_submod_closed U).
Canonical memv_addrPred U := AddrPred (memv_submod_closed U).
Canonical memv_zmodPred U := ZmodPred (memv_submod_closed U).
Canonical memv_submodPred U := SubmodPred (memv_submod_closed U).
Lemma mem0v U : 0 \in U.
Lemma memvN U v : (- v \in U) = (v \in U).
Lemma memvD U : {in U &, ∀ u v, u + v \in U}.
Lemma memvB U : {in U &, ∀ u v, u - v \in U}.
Lemma memvZ U k : {in U, ∀ v, k *: v \in U}.
Lemma memv_suml I r (P : pred I) vs U :
(∀ i, P i → vs i \in U) → \sum_(i <- r | P i) vs i \in U.
Lemma memv_line u : u \in <[u]>%VS.
Lemma subvP U V : reflect {subset U ≤ V} (U ≤ V)%VS.
Lemma subvv U : (U ≤ U)%VS.
Hint Resolve subvv : core.
Lemma subv_trans : transitive subV.
Lemma subv_anti : antisymmetric subV.
Lemma eqEsubv U V : (U == V) = (U ≤ V ≤ U)%VS.
Lemma vspaceP U V : U =i V ↔ U = V.
Lemma subvPn {U V} : reflect (exists2 u, u \in U & u \notin V) (~~ (U ≤ V)%VS).
Empty space.
Lemma sub0v U : (0 ≤ U)%VS.
Lemma subv0 U : (U ≤ 0)%VS = (U == 0%VS).
Lemma memv0 v : v \in 0%VS = (v == 0).
Lemma subv0 U : (U ≤ 0)%VS = (U == 0%VS).
Lemma memv0 v : v \in 0%VS = (v == 0).
Full space
Picking a non-zero vector in a subspace.
Sum of subspaces.
Lemma subv_add U V W : (U + V ≤ W)%VS = (U ≤ W)%VS && (V ≤ W)%VS.
Lemma addvS U1 U2 V1 V2 : (U1 ≤ U2 → V1 ≤ V2 → U1 + V1 ≤ U2 + V2)%VS.
Lemma addvSl U V : (U ≤ U + V)%VS.
Lemma addvSr U V : (V ≤ U + V)%VS.
Lemma addvC : commutative addV.
Lemma addvA : associative addV.
Lemma addv_idPl {U V}: reflect (U + V = U)%VS (V ≤ U)%VS.
Lemma addv_idPr {U V} : reflect (U + V = V)%VS (U ≤ V)%VS.
Lemma addvv : idempotent addV.
Lemma add0v : left_id 0%VS addV.
Lemma addv0 : right_id 0%VS addV.
Lemma sumfv : left_zero fullv addV.
Lemma addvf : right_zero fullv addV.
Canonical addv_monoid := Monoid.Law addvA add0v addv0.
Canonical addv_comoid := Monoid.ComLaw addvC.
Lemma memv_add u v U V : u \in U → v \in V → u + v \in (U + V)%VS.
Lemma memv_addP {w U V} :
reflect (exists2 u, u \in U & exists2 v, v \in V & w = u + v)
(w \in U + V)%VS.
Section BigSum.
Variable I : finType.
Implicit Type P : pred I.
Lemma sumv_sup i0 P U Vs :
P i0 → (U ≤ Vs i0)%VS → (U ≤ \sum_(i | P i) Vs i)%VS.
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.
Canonical addv_monoid := Monoid.Law addvA add0v addv0.
Canonical addv_comoid := Monoid.ComLaw addvC.
Lemma memv_add u v U V : u \in U → v \in V → u + v \in (U + V)%VS.
Lemma memv_addP {w U V} :
reflect (exists2 u, u \in U & exists2 v, v \in V & w = u + v)
(w \in U + V)%VS.
Section BigSum.
Variable I : finType.
Implicit Type P : pred I.
Lemma sumv_sup i0 P U Vs :
P i0 → (U ≤ Vs i0)%VS → (U ≤ \sum_(i | P i) Vs i)%VS.
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.
Canonical capv_monoid := Monoid.Law capvA capfv capvf.
Canonical capv_comoid := Monoid.ComLaw capvC.
Lemma memv_cap w U V : (w \in U :&: V)%VS = (w \in U) && (w \in V).
Lemma memv_capP {w U V} : reflect (w \in U ∧ w \in V) (w \in U :&: V)%VS.
Lemma vspace_modl U V W : (U ≤ W → U + (V :&: W) = (U + V) :&: W)%VS.
Lemma vspace_modr U V W : (W ≤ U → (U :&: V) + W = U :&: (V + W))%VS.
Section BigCap.
Variable I : finType.
Implicit Type P : pred I.
Lemma bigcapv_inf i0 P Us V :
P i0 → (Us i0 ≤ V → \bigcap_(i | P i) Us i ≤ V)%VS.
Lemma subv_bigcapP {P U Vs} :
reflect (∀ i, P i → U ≤ Vs i)%VS (U ≤ \bigcap_(i | P i) Vs i)%VS.
End BigCap.
Complement
Difference
Lemma diffvSl U V : (U :\: V ≤ U)%VS.
Lemma capv_diff U V : ((U :\: V) :&: V = 0)%VS.
Lemma addv_diff_cap U V : (U :\: V + U :&: V)%VS = U.
Lemma addv_diff U V : (U :\: V + V = U + V)%VS.
Lemma capv_diff U V : ((U :\: V) :&: V = 0)%VS.
Lemma addv_diff_cap U V : (U :\: V + U :&: V)%VS = U.
Lemma addv_diff U V : (U :\: V + V = U + V)%VS.
Subspace dimension.
Lemma dimv0 : \dim (0%VS : {vspace vT}) = 0%N.
Lemma dimv_eq0 U : (\dim U == 0%N) = (U == 0%VS).
Lemma dimvf : \dim {:vT} = Vector.dim vT.
Lemma dim_vline v : \dim <[v]> = (v != 0).
Lemma dimvS U V : (U ≤ V)%VS → \dim U ≤ \dim V.
Lemma dimv_leqif_sup U V : (U ≤ V)%VS → \dim U ≤ \dim V ?= iff (V ≤ U)%VS.
Lemma dimv_leqif_eq U V : (U ≤ V)%VS → \dim U ≤ \dim V ?= iff (U == V).
Lemma eqEdim U V : (U == V) = (U ≤ V)%VS && (\dim V ≤ \dim U).
Lemma dimv_compl U : \dim U^C = (\dim {:vT} - \dim U)%N.
Lemma dimv_cap_compl U V : (\dim (U :&: V) + \dim (U :\: V))%N = \dim U.
Lemma dimv_sum_cap U V : (\dim (U + V) + \dim (U :&: V) = \dim U + \dim V)%N.
Lemma dimv_disjoint_sum U V :
(U :&: V = 0)%VS → \dim (U + V) = (\dim U + \dim V)%N.
Lemma dimv_add_leqif U V :
\dim (U + V) ≤ \dim U + \dim V ?= iff (U :&: V ≤ 0)%VS.
Lemma diffv_eq0 U V : (U :\: V == 0)%VS = (U ≤ V)%VS.
Lemma dimv_leq_sum I r (P : pred I) (Us : I → {vspace vT}) :
\dim (\sum_(i <- r | P i) Us i) ≤ \sum_(i <- r | P i) \dim (Us i).
Section SumExpr.
Lemma dimv_eq0 U : (\dim U == 0%N) = (U == 0%VS).
Lemma dimvf : \dim {:vT} = Vector.dim vT.
Lemma dim_vline v : \dim <[v]> = (v != 0).
Lemma dimvS U V : (U ≤ V)%VS → \dim U ≤ \dim V.
Lemma dimv_leqif_sup U V : (U ≤ V)%VS → \dim U ≤ \dim V ?= iff (V ≤ U)%VS.
Lemma dimv_leqif_eq U V : (U ≤ V)%VS → \dim U ≤ \dim V ?= iff (U == V).
Lemma eqEdim U V : (U == V) = (U ≤ V)%VS && (\dim V ≤ \dim U).
Lemma dimv_compl U : \dim U^C = (\dim {:vT} - \dim U)%N.
Lemma dimv_cap_compl U V : (\dim (U :&: V) + \dim (U :\: V))%N = \dim U.
Lemma dimv_sum_cap U V : (\dim (U + V) + \dim (U :&: V) = \dim U + \dim V)%N.
Lemma dimv_disjoint_sum U V :
(U :&: V = 0)%VS → \dim (U + V) = (\dim U + \dim V)%N.
Lemma dimv_add_leqif U V :
\dim (U + V) ≤ \dim U + \dim V ?= iff (U :&: V ≤ 0)%VS.
Lemma diffv_eq0 U V : (U :\: V == 0)%VS = (U ≤ V)%VS.
Lemma dimv_leq_sum I r (P : pred I) (Us : I → {vspace vT}) :
\dim (\sum_(i <- r | P i) Us i) ≤ \sum_(i <- r | P i) \dim (Us i).
Section SumExpr.
The vector direct sum theory clones the interface types of the matrix
direct sum theory (see mxalgebra for the technical details), but
nevetheless reuses much of the matrix theory.
Structure addv_expr := Sumv {
addv_val :> wrapped {vspace vT};
addv_dim : wrapped nat;
_ : mxsum_spec (vs2mx (unwrap addv_val)) (unwrap addv_dim)
}.
addv_val :> wrapped {vspace vT};
addv_dim : wrapped nat;
_ : mxsum_spec (vs2mx (unwrap addv_val)) (unwrap addv_dim)
}.
Piggyback on mxalgebra theory.
Definition vs2mx_sum_expr_subproof (S : addv_expr) :
mxsum_spec (vs2mx (unwrap S)) (unwrap (addv_dim S)).
Canonical vs2mx_sum_expr S := ProperMxsumExpr (vs2mx_sum_expr_subproof S).
Canonical trivial_addv U := @Sumv (Wrap U) (Wrap (\dim U)) (TrivialMxsum _).
Structure proper_addv_expr := ProperSumvExpr {
proper_addv_val :> {vspace vT};
proper_addv_dim :> nat;
_ : mxsum_spec (vs2mx proper_addv_val) proper_addv_dim
}.
Definition proper_addvP (S : proper_addv_expr) :=
let: ProperSumvExpr _ _ termS := S return mxsum_spec (vs2mx S) S in termS.
Canonical proper_addv (S : proper_addv_expr) :=
@Sumv (wrap (S : {vspace vT})) (wrap (S : nat)) (proper_addvP S).
Section Binary.
Variables S1 S2 : addv_expr.
Fact binary_addv_subproof :
mxsum_spec (vs2mx (unwrap S1 + unwrap S2))
(unwrap (addv_dim S1) + unwrap (addv_dim S2)).
Canonical binary_addv_expr := ProperSumvExpr binary_addv_subproof.
End Binary.
Section Nary.
Variables (I : Type) (r : seq I) (P : pred I) (S_ : I → addv_expr).
Fact nary_addv_subproof :
mxsum_spec (vs2mx (\sum_(i <- r | P i) unwrap (S_ i)))
(\sum_(i <- r | P i) unwrap (addv_dim (S_ i))).
Canonical nary_addv_expr := ProperSumvExpr nary_addv_subproof.
End Nary.
Definition directv_def S of phantom {vspace vT} (unwrap (addv_val S)) :=
\dim (unwrap S) == unwrap (addv_dim S).
End SumExpr.
Lemma directvE (S : addv_expr) :
directv (unwrap S) = (\dim (unwrap S) == unwrap (addv_dim S)).
Lemma directvP {S : proper_addv_expr} : reflect (\dim S = S :> nat) (directv S).
Lemma directv_trivial U : directv (unwrap (@trivial_addv U)).
Lemma dimv_sum_leqif (S : addv_expr) :
\dim (unwrap S) ≤ unwrap (addv_dim S) ?= iff directv (unwrap S).
Lemma directvEgeq (S : addv_expr) :
directv (unwrap S) = (\dim (unwrap S) ≥ unwrap (addv_dim S)).
Section BinaryDirect.
Lemma directv_addE (S1 S2 : addv_expr) :
directv (unwrap S1 + unwrap S2)
= [&& directv (unwrap S1), directv (unwrap S2)
& unwrap S1 :&: unwrap S2 == 0]%VS.
Lemma directv_addP {U V} : reflect (U :&: V = 0)%VS (directv (U + V)).
Lemma directv_add_unique {U V} :
reflect (∀ u1 u2 v1 v2, u1 \in U → u2 \in U → v1 \in V → v2 \in V →
(u1 + v1 == u2 + v2) = ((u1, v1) == (u2, v2)))
(directv (U + V)).
End BinaryDirect.
Section NaryDirect.
Context {I : finType} {P : pred I}.
Lemma directv_sumP {Us : I → {vspace vT}} :
reflect (∀ i, P i → Us i :&: (\sum_(j | P j && (j != i)) Us j) = 0)%VS
(directv (\sum_(i | P i) Us i)).
Lemma directv_sumE {Ss : I → addv_expr} (xunwrap := unwrap) :
reflect [/\ ∀ i, P i → directv (unwrap (Ss i))
& directv (\sum_(i | P i) xunwrap (Ss i))]
(directv (\sum_(i | P i) unwrap (Ss i))).
Lemma directv_sum_independent {Us : I → {vspace vT}} :
reflect (∀ us,
(∀ i, P i → us i \in Us i) → \sum_(i | P i) us i = 0 →
(∀ i, P i → us i = 0))
(directv (\sum_(i | P i) Us i)).
Lemma directv_sum_unique {Us : I → {vspace vT}} :
reflect (∀ us vs,
(∀ i, P i → us i \in Us i) →
(∀ i, P i → vs i \in Us i) →
(\sum_(i | P i) us i == \sum_(i | P i) vs i)
= [∀ (i | P i), us i == vs i])
(directv (\sum_(i | P i) Us i)).
End NaryDirect.
mxsum_spec (vs2mx (unwrap S)) (unwrap (addv_dim S)).
Canonical vs2mx_sum_expr S := ProperMxsumExpr (vs2mx_sum_expr_subproof S).
Canonical trivial_addv U := @Sumv (Wrap U) (Wrap (\dim U)) (TrivialMxsum _).
Structure proper_addv_expr := ProperSumvExpr {
proper_addv_val :> {vspace vT};
proper_addv_dim :> nat;
_ : mxsum_spec (vs2mx proper_addv_val) proper_addv_dim
}.
Definition proper_addvP (S : proper_addv_expr) :=
let: ProperSumvExpr _ _ termS := S return mxsum_spec (vs2mx S) S in termS.
Canonical proper_addv (S : proper_addv_expr) :=
@Sumv (wrap (S : {vspace vT})) (wrap (S : nat)) (proper_addvP S).
Section Binary.
Variables S1 S2 : addv_expr.
Fact binary_addv_subproof :
mxsum_spec (vs2mx (unwrap S1 + unwrap S2))
(unwrap (addv_dim S1) + unwrap (addv_dim S2)).
Canonical binary_addv_expr := ProperSumvExpr binary_addv_subproof.
End Binary.
Section Nary.
Variables (I : Type) (r : seq I) (P : pred I) (S_ : I → addv_expr).
Fact nary_addv_subproof :
mxsum_spec (vs2mx (\sum_(i <- r | P i) unwrap (S_ i)))
(\sum_(i <- r | P i) unwrap (addv_dim (S_ i))).
Canonical nary_addv_expr := ProperSumvExpr nary_addv_subproof.
End Nary.
Definition directv_def S of phantom {vspace vT} (unwrap (addv_val S)) :=
\dim (unwrap S) == unwrap (addv_dim S).
End SumExpr.
Lemma directvE (S : addv_expr) :
directv (unwrap S) = (\dim (unwrap S) == unwrap (addv_dim S)).
Lemma directvP {S : proper_addv_expr} : reflect (\dim S = S :> nat) (directv S).
Lemma directv_trivial U : directv (unwrap (@trivial_addv U)).
Lemma dimv_sum_leqif (S : addv_expr) :
\dim (unwrap S) ≤ unwrap (addv_dim S) ?= iff directv (unwrap S).
Lemma directvEgeq (S : addv_expr) :
directv (unwrap S) = (\dim (unwrap S) ≥ unwrap (addv_dim S)).
Section BinaryDirect.
Lemma directv_addE (S1 S2 : addv_expr) :
directv (unwrap S1 + unwrap S2)
= [&& directv (unwrap S1), directv (unwrap S2)
& unwrap S1 :&: unwrap S2 == 0]%VS.
Lemma directv_addP {U V} : reflect (U :&: V = 0)%VS (directv (U + V)).
Lemma directv_add_unique {U V} :
reflect (∀ u1 u2 v1 v2, u1 \in U → u2 \in U → v1 \in V → v2 \in V →
(u1 + v1 == u2 + v2) = ((u1, v1) == (u2, v2)))
(directv (U + V)).
End BinaryDirect.
Section NaryDirect.
Context {I : finType} {P : pred I}.
Lemma directv_sumP {Us : I → {vspace vT}} :
reflect (∀ i, P i → Us i :&: (\sum_(j | P j && (j != i)) Us j) = 0)%VS
(directv (\sum_(i | P i) Us i)).
Lemma directv_sumE {Ss : I → addv_expr} (xunwrap := unwrap) :
reflect [/\ ∀ i, P i → directv (unwrap (Ss i))
& directv (\sum_(i | P i) xunwrap (Ss i))]
(directv (\sum_(i | P i) unwrap (Ss i))).
Lemma directv_sum_independent {Us : I → {vspace vT}} :
reflect (∀ us,
(∀ i, P i → us i \in Us i) → \sum_(i | P i) us i = 0 →
(∀ i, P i → us i = 0))
(directv (\sum_(i | P i) Us i)).
Lemma directv_sum_unique {Us : I → {vspace vT}} :
reflect (∀ us vs,
(∀ i, P i → us i \in Us i) →
(∀ i, P i → vs i \in Us i) →
(\sum_(i | P i) us i == \sum_(i | P i) vs i)
= [∀ (i | P i), us i == vs i])
(directv (\sum_(i | P i) Us i)).
End NaryDirect.
Linear span generated by a list of vectors
Lemma memv_span X v : v \in X → v \in <<X>>%VS.
Lemma memv_span1 v : v \in <<[:: v]>>%VS.
Lemma dim_span X : \dim <<X>> ≤ size X.
Lemma span_subvP {X U} : reflect {subset X ≤ U} (<<X>> ≤ U)%VS.
Lemma sub_span X Y : {subset X ≤ Y} → (<<X>> ≤ <<Y>>)%VS.
Lemma eq_span X Y : X =i Y → (<<X>> = <<Y>>)%VS.
Lemma span_def X : span X = (\sum_(u <- X) <[u]>)%VS.
Lemma span_nil : (<<Nil vT>> = 0)%VS.
Lemma span_seq1 v : (<<[:: v]>> = <[v]>)%VS.
Lemma span_cons v X : (<<v :: X>> = <[v]> + <<X>>)%VS.
Lemma span_cat X Y : (<<X ++ Y>> = <<X>> + <<Y>>)%VS.
Lemma memv_span1 v : v \in <<[:: v]>>%VS.
Lemma dim_span X : \dim <<X>> ≤ size X.
Lemma span_subvP {X U} : reflect {subset X ≤ U} (<<X>> ≤ U)%VS.
Lemma sub_span X Y : {subset X ≤ Y} → (<<X>> ≤ <<Y>>)%VS.
Lemma eq_span X Y : X =i Y → (<<X>> = <<Y>>)%VS.
Lemma span_def X : span X = (\sum_(u <- X) <[u]>)%VS.
Lemma span_nil : (<<Nil vT>> = 0)%VS.
Lemma span_seq1 v : (<<[:: v]>> = <[v]>)%VS.
Lemma span_cons v X : (<<v :: X>> = <[v]> + <<X>>)%VS.
Lemma span_cat X Y : (<<X ++ Y>> = <<X>> + <<Y>>)%VS.
Coordinates function; should perhaps be generalized to nat indices.
Definition coord_expanded_def n (X : n.-tuple vT) i v :=
(v2r v ×m pinvmx (b2mx X)) 0 i.
Definition coord := locked_with span_key coord_expanded_def.
Canonical coord_unlockable := [unlockable fun coord].
Fact coord_is_scalar n (X : n.-tuple vT) i : scalar (coord X i).
Canonical coord_addidive n Xn i := Additive (@coord_is_scalar n Xn i).
Canonical coord_linear n Xn i := AddLinear (@coord_is_scalar n Xn i).
Lemma coord_span n (X : n.-tuple vT) v :
v \in span X → v = \sum_i coord X i v *: X`_i.
Lemma coord0 i v : coord [tuple 0] i v = 0.
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) :=
Vector.Hom (lin1_mx (v2r \o f \o r2v)).
Definition linfun := locked_with lfun_key linfun_def.
Canonical linfun_unlockable := [unlockable fun linfun].
Definition id_lfun vT := @linfun vT vT idfun.
Definition comp_lfun aT vT rT (f : 'Hom(vT, rT)) (g : 'Hom(aT, vT)) :=
linfun (fun_of_lfun f \o fun_of_lfun g).
End LfunDefs.
Coercion fun_of_lfun : Vector.hom >-> Funclass.
Notation "\1" := (@id_lfun _ _) : lfun_scope.
Notation "f \o g" := (comp_lfun f g) : lfun_scope.
Section LfunVspaceDefs.
Variable K : fieldType.
Implicit Types aT rT : vectType K.
Definition inv_lfun aT rT (f : 'Hom(aT, rT)) := Vector.Hom (pinvmx (f2mx f)).
Definition lker aT rT (f : 'Hom(aT, rT)) := mx2vs (kermx (f2mx f)).
Fact lfun_img_key : unit.
Definition lfun_img_def aT rT f (U : {vspace aT}) : {vspace rT} :=
mx2vs (vs2mx U ×m f2mx f).
Definition lfun_img := locked_with lfun_img_key lfun_img_def.
Canonical lfun_img_unlockable := [unlockable fun lfun_img].
Definition lfun_preim aT rT (f : 'Hom(aT, rT)) W :=
(lfun_img (inv_lfun f) (W :&: lfun_img f fullv) + lker f)%VS.
End LfunVspaceDefs.
Notation "f ^-1" := (inv_lfun f) : lfun_scope.
Notation "f @: U" := (lfun_img f%VF%R U) (at level 24) : vspace_scope.
Notation "f @^-1: W" := (lfun_preim f%VF%R W) (at level 24) : vspace_scope.
Notation limg f := (lfun_img f fullv).
Section LfunZmodType.
Variables (R : ringType) (aT rT : vectType R).
Implicit Types f g h : 'Hom(aT, rT).
Definition lfun_eqMixin := Eval hnf in [eqMixin of 'Hom(aT, rT) by <:].
Canonical lfun_eqType := EqType 'Hom(aT, rT) lfun_eqMixin.
Definition lfun_choiceMixin := [choiceMixin of 'Hom(aT, rT) by <:].
Canonical lfun_choiceType := ChoiceType 'Hom(aT, rT) lfun_choiceMixin.
Fact lfun_is_linear f : linear f.
Canonical lfun_additive f := Additive (lfun_is_linear f).
Canonical lfun_linear f := AddLinear (lfun_is_linear f).
Lemma lfunE (ff : {linear aT → rT}) : linfun ff =1 ff.
Lemma fun_of_lfunK : cancel (@fun_of_lfun R aT rT) linfun.
Lemma lfunP f g : f =1 g ↔ f = g.
Definition zero_lfun : 'Hom(aT, rT) := linfun \0.
Definition add_lfun f g := linfun (f \+ g).
Definition opp_lfun f := linfun (-%R \o f).
Fact lfun_addA : associative add_lfun.
Fact lfun_addC : commutative add_lfun.
Fact lfun_add0 : left_id zero_lfun add_lfun.
Lemma lfun_addN : left_inverse zero_lfun opp_lfun add_lfun.
Definition lfun_zmodMixin := ZmodMixin lfun_addA lfun_addC lfun_add0 lfun_addN.
Canonical lfun_zmodType := Eval hnf in ZmodType 'Hom(aT, rT) lfun_zmodMixin.
Lemma zero_lfunE x : (0 : 'Hom(aT, rT)) x = 0.
Lemma add_lfunE f g x : (f + g) x = f x + g x.
Lemma opp_lfunE f x : (- f) x = - f x.
Lemma sum_lfunE I (r : seq I) (P : pred I) (fs : I → 'Hom(aT, rT)) x :
(\sum_(i <- r | P i) fs i) x = \sum_(i <- r | P i) fs i x.
End LfunZmodType.
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.
Definition lfun_lmodMixin :=
LmodMixin lfun_scaleA lfun_scale1 lfun_scaleDr lfun_scaleDl.
Canonical lfun_lmodType := Eval hnf in LmodType R 'Hom(aT, rT) lfun_lmodMixin.
Lemma scale_lfunE k f x : (k *: f) x = k *: f x.
Fact lfun_vect_iso : Vector.axiom (Vector.dim aT × Vector.dim rT) 'Hom(aT, rT).
Definition lfun_vectMixin := VectMixin lfun_vect_iso.
Canonical lfun_vectType := VectType R 'Hom(aT, rT) lfun_vectMixin.
End LfunVectType.
Section CompLfun.
Variables (R : ringType) (wT aT vT rT : vectType R).
Implicit Types (f : 'Hom(vT, rT)) (g : 'Hom(aT, vT)) (h : 'Hom(wT, aT)).
Lemma id_lfunE u: \1%VF u = u :> aT.
Lemma comp_lfunE f g u : (f \o g)%VF u = f (g u).
Lemma comp_lfunA f g h : (f \o (g \o h) = (f \o g) \o h)%VF.
Lemma comp_lfun1l f : (\1 \o f)%VF = f.
Lemma comp_lfun1r f : (f \o \1)%VF = f.
Lemma comp_lfun0l g : (0 \o g)%VF = 0 :> 'Hom(aT, rT).
Lemma comp_lfun0r f : (f \o 0)%VF = 0 :> 'Hom(aT, rT).
Lemma comp_lfunDl f1 f2 g : ((f1 + f2) \o g = (f1 \o g) + (f2 \o g))%VF.
Lemma comp_lfunDr f g1 g2 : (f \o (g1 + g2) = (f \o g1) + (f \o g2))%VF.
Lemma comp_lfunNl f g : ((- f) \o g = - (f \o g))%VF.
Lemma comp_lfunNr f g : (f \o (- g) = - (f \o g))%VF.
End CompLfun.
Definition lfun_simp :=
(comp_lfunE, scale_lfunE, opp_lfunE, add_lfunE, sum_lfunE, lfunE).
Section ScaleCompLfun.
Variables (R : comRingType) (aT vT rT : vectType R).
Implicit Types (f : 'Hom(vT, rT)) (g : 'Hom(aT, vT)).
Lemma comp_lfunZl k f g : (k *: (f \o g) = (k *: f) \o g)%VF.
Lemma comp_lfunZr k f g : (k *: (f \o g) = f \o (k *: g))%VF.
End ScaleCompLfun.
Section LinearImage.
Variables (K : fieldType) (aT rT : vectType K).
Implicit Types (f g : 'Hom(aT, rT)) (U V : {vspace aT}) (W : {vspace rT}).
Lemma limgS f U V : (U ≤ V)%VS → (f @: U ≤ f @: V)%VS.
Lemma limg_line f v : (f @: <[v]> = <[f v]>)%VS.
Lemma limg0 f : (f @: 0 = 0)%VS.
Lemma memv_img f v U : v \in U → f v \in (f @: U)%VS.
Lemma memv_imgP f w U :
reflect (exists2 u, u \in U & w = f u) (w \in f @: U)%VS.
Lemma lim0g U : (0 @: U = 0 :> {vspace rT})%VS.
Lemma eq_in_limg V f g : {in V, f =1 g} → (f @: V = g @: V)%VS.
Lemma 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) :=
Vector.Hom (lin1_mx (v2r \o f \o r2v)).
Definition linfun := locked_with lfun_key linfun_def.
Canonical linfun_unlockable := [unlockable fun linfun].
Definition id_lfun vT := @linfun vT vT idfun.
Definition comp_lfun aT vT rT (f : 'Hom(vT, rT)) (g : 'Hom(aT, vT)) :=
linfun (fun_of_lfun f \o fun_of_lfun g).
End LfunDefs.
Coercion fun_of_lfun : Vector.hom >-> Funclass.
Notation "\1" := (@id_lfun _ _) : lfun_scope.
Notation "f \o g" := (comp_lfun f g) : lfun_scope.
Section LfunVspaceDefs.
Variable K : fieldType.
Implicit Types aT rT : vectType K.
Definition inv_lfun aT rT (f : 'Hom(aT, rT)) := Vector.Hom (pinvmx (f2mx f)).
Definition lker aT rT (f : 'Hom(aT, rT)) := mx2vs (kermx (f2mx f)).
Fact lfun_img_key : unit.
Definition lfun_img_def aT rT f (U : {vspace aT}) : {vspace rT} :=
mx2vs (vs2mx U ×m f2mx f).
Definition lfun_img := locked_with lfun_img_key lfun_img_def.
Canonical lfun_img_unlockable := [unlockable fun lfun_img].
Definition lfun_preim aT rT (f : 'Hom(aT, rT)) W :=
(lfun_img (inv_lfun f) (W :&: lfun_img f fullv) + lker f)%VS.
End LfunVspaceDefs.
Notation "f ^-1" := (inv_lfun f) : lfun_scope.
Notation "f @: U" := (lfun_img f%VF%R U) (at level 24) : vspace_scope.
Notation "f @^-1: W" := (lfun_preim f%VF%R W) (at level 24) : vspace_scope.
Notation limg f := (lfun_img f fullv).
Section LfunZmodType.
Variables (R : ringType) (aT rT : vectType R).
Implicit Types f g h : 'Hom(aT, rT).
Definition lfun_eqMixin := Eval hnf in [eqMixin of 'Hom(aT, rT) by <:].
Canonical lfun_eqType := EqType 'Hom(aT, rT) lfun_eqMixin.
Definition lfun_choiceMixin := [choiceMixin of 'Hom(aT, rT) by <:].
Canonical lfun_choiceType := ChoiceType 'Hom(aT, rT) lfun_choiceMixin.
Fact lfun_is_linear f : linear f.
Canonical lfun_additive f := Additive (lfun_is_linear f).
Canonical lfun_linear f := AddLinear (lfun_is_linear f).
Lemma lfunE (ff : {linear aT → rT}) : linfun ff =1 ff.
Lemma fun_of_lfunK : cancel (@fun_of_lfun R aT rT) linfun.
Lemma lfunP f g : f =1 g ↔ f = g.
Definition zero_lfun : 'Hom(aT, rT) := linfun \0.
Definition add_lfun f g := linfun (f \+ g).
Definition opp_lfun f := linfun (-%R \o f).
Fact lfun_addA : associative add_lfun.
Fact lfun_addC : commutative add_lfun.
Fact lfun_add0 : left_id zero_lfun add_lfun.
Lemma lfun_addN : left_inverse zero_lfun opp_lfun add_lfun.
Definition lfun_zmodMixin := ZmodMixin lfun_addA lfun_addC lfun_add0 lfun_addN.
Canonical lfun_zmodType := Eval hnf in ZmodType 'Hom(aT, rT) lfun_zmodMixin.
Lemma zero_lfunE x : (0 : 'Hom(aT, rT)) x = 0.
Lemma add_lfunE f g x : (f + g) x = f x + g x.
Lemma opp_lfunE f x : (- f) x = - f x.
Lemma sum_lfunE I (r : seq I) (P : pred I) (fs : I → 'Hom(aT, rT)) x :
(\sum_(i <- r | P i) fs i) x = \sum_(i <- r | P i) fs i x.
End LfunZmodType.
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.
Definition lfun_lmodMixin :=
LmodMixin lfun_scaleA lfun_scale1 lfun_scaleDr lfun_scaleDl.
Canonical lfun_lmodType := Eval hnf in LmodType R 'Hom(aT, rT) lfun_lmodMixin.
Lemma scale_lfunE k f x : (k *: f) x = k *: f x.
Fact lfun_vect_iso : Vector.axiom (Vector.dim aT × Vector.dim rT) 'Hom(aT, rT).
Definition lfun_vectMixin := VectMixin lfun_vect_iso.
Canonical lfun_vectType := VectType R 'Hom(aT, rT) lfun_vectMixin.
End LfunVectType.
Section CompLfun.
Variables (R : ringType) (wT aT vT rT : vectType R).
Implicit Types (f : 'Hom(vT, rT)) (g : 'Hom(aT, vT)) (h : 'Hom(wT, aT)).
Lemma id_lfunE u: \1%VF u = u :> aT.
Lemma comp_lfunE f g u : (f \o g)%VF u = f (g u).
Lemma comp_lfunA f g h : (f \o (g \o h) = (f \o g) \o h)%VF.
Lemma comp_lfun1l f : (\1 \o f)%VF = f.
Lemma comp_lfun1r f : (f \o \1)%VF = f.
Lemma comp_lfun0l g : (0 \o g)%VF = 0 :> 'Hom(aT, rT).
Lemma comp_lfun0r f : (f \o 0)%VF = 0 :> 'Hom(aT, rT).
Lemma comp_lfunDl f1 f2 g : ((f1 + f2) \o g = (f1 \o g) + (f2 \o g))%VF.
Lemma comp_lfunDr f g1 g2 : (f \o (g1 + g2) = (f \o g1) + (f \o g2))%VF.
Lemma comp_lfunNl f g : ((- f) \o g = - (f \o g))%VF.
Lemma comp_lfunNr f g : (f \o (- g) = - (f \o g))%VF.
End CompLfun.
Definition lfun_simp :=
(comp_lfunE, scale_lfunE, opp_lfunE, add_lfunE, sum_lfunE, lfunE).
Section ScaleCompLfun.
Variables (R : comRingType) (aT vT rT : vectType R).
Implicit Types (f : 'Hom(vT, rT)) (g : 'Hom(aT, vT)).
Lemma comp_lfunZl k f g : (k *: (f \o g) = (k *: f) \o g)%VF.
Lemma comp_lfunZr k f g : (k *: (f \o g) = f \o (k *: g))%VF.
End ScaleCompLfun.
Section LinearImage.
Variables (K : fieldType) (aT rT : vectType K).
Implicit Types (f g : 'Hom(aT, rT)) (U V : {vspace aT}) (W : {vspace rT}).
Lemma limgS f U V : (U ≤ V)%VS → (f @: U ≤ f @: V)%VS.
Lemma limg_line f v : (f @: <[v]> = <[f v]>)%VS.
Lemma limg0 f : (f @: 0 = 0)%VS.
Lemma memv_img f v U : v \in U → f v \in (f @: U)%VS.
Lemma memv_imgP f w U :
reflect (exists2 u, u \in U & w = f u) (w \in f @: U)%VS.
Lemma lim0g U : (0 @: U = 0 :> {vspace rT})%VS.
Lemma eq_in_limg V f g : {in V, f =1 g} → (f @: V = g @: V)%VS.
Lemma 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 : Vector.dim vT > 0.
Fact lfun1_neq0 : \1%VF != 0 :> 'End(vT).
Definition lfun_comp_ringMixin :=
RingMixin comp_lfunA comp_lfun1l comp_lfun1r comp_lfunDl comp_lfunDr
lfun1_neq0.
Definition lfun_comp_ringType := RingType 'End(vT) lfun_comp_ringMixin.
In the standard endomorphism ring product is categorical composition.
Definition lfun_ringMixin : GRing.Ring.mixin_of (lfun_zmodType vT vT) :=
GRing.converse_ringMixin lfun_comp_ringType.
Definition lfun_ringType := Eval hnf in RingType 'End(vT) lfun_ringMixin.
Definition lfun_lalgType := Eval hnf in [lalgType R of 'End(vT)
for LalgType R lfun_ringType (fun k x y ⇒ comp_lfunZr k y x)].
Definition lfun_algType := Eval hnf in [algType R of 'End(vT)
for AlgType R _ (fun k (x y : lfun_lalgType) ⇒ comp_lfunZl k y x)].
End LfunAlgebra.
Section Projection.
Variables (K : fieldType) (vT : vectType K).
Implicit Types U V : {vspace vT}.
Definition daddv_pi U V := Vector.Hom (proj_mx (vs2mx U) (vs2mx V)).
Definition projv U := daddv_pi U U^C.
Definition addv_pi1 U V := daddv_pi (U :\: V) V.
Definition addv_pi2 U V := daddv_pi V (U :\: V).
Lemma memv_pi U V w : (daddv_pi U V) w \in U.
Lemma memv_proj U w : projv U w \in U.
Lemma memv_pi1 U V w : (addv_pi1 U V) w \in U.
Lemma memv_pi2 U V w : (addv_pi2 U V) w \in V.
Lemma daddv_pi_id U V u : (U :&: V = 0)%VS → u \in U → daddv_pi U V u = u.
Lemma daddv_pi_proj U V w (pi := daddv_pi U V) :
(U :&: V = 0)%VS → pi (pi w) = pi w.
Lemma daddv_pi_add U V w :
(U :&: V = 0)%VS → (w \in U + V)%VS → daddv_pi U V w + daddv_pi V U w = w.
Lemma projv_id U u : u \in U → projv U u = u.
Lemma projv_proj U w : projv U (projv U w) = projv U w.
Lemma memv_projC U w : w - projv U w \in (U^C)%VS.
Lemma limg_proj U : limg (projv U) = U.
Lemma lker_proj U : lker (projv U) = (U^C)%VS.
Lemma addv_pi1_proj U V w (pi1 := addv_pi1 U V) : pi1 (pi1 w) = pi1 w.
Lemma addv_pi2_id U V v : v \in V → addv_pi2 U V v = v.
Lemma addv_pi2_proj U V w (pi2 := addv_pi2 U V) : pi2 (pi2 w) = pi2 w.
Lemma addv_pi1_pi2 U V w :
w \in (U + V)%VS → addv_pi1 U V w + addv_pi2 U V w = w.
Section Sumv_Pi.
Variables (I : eqType) (r0 : seq I) (P : pred I) (Vs : I → {vspace vT}).
Let sumv_pi_rec i :=
fix loop r := if r is j :: r1 then
let V1 := (\sum_(k <- r1) Vs k)%VS in
if j == i then addv_pi1 (Vs j) V1 else (loop r1 \o addv_pi2 (Vs j) V1)%VF
else 0.
Notation sumV := (\sum_(i <- r0 | P i) Vs i)%VS.
Definition sumv_pi_for V of V = sumV := fun i ⇒ sumv_pi_rec i (filter P r0).
Variables (V : {vspace vT}) (defV : V = sumV).
Lemma memv_sum_pi i v : sumv_pi_for defV i v \in Vs i.
Lemma sumv_pi_uniq_sum v :
uniq (filter P r0) → v \in V →
\sum_(i <- r0 | P i) sumv_pi_for defV i v = v.
End Sumv_Pi.
End Projection.
Notation sumv_pi V := (sumv_pi_for (erefl V)).
Section SumvPi.
Variable (K : fieldType) (vT : vectType K).
Lemma sumv_pi_sum (I : finType) (P : pred I) Vs v (V : {vspace vT})
(defV : V = (\sum_(i | P i) Vs i)%VS) :
v \in V → \sum_(i | P i) sumv_pi_for defV i v = v :> vT.
Lemma sumv_pi_nat_sum m n (P : pred nat) Vs v (V : {vspace vT})
(defV : V = (\sum_(m ≤ i < n | P i) Vs i)%VS) :
v \in V → \sum_(m ≤ i < n | P i) sumv_pi_for defV i v = v :> vT.
End SumvPi.
Section SubVector.
GRing.converse_ringMixin lfun_comp_ringType.
Definition lfun_ringType := Eval hnf in RingType 'End(vT) lfun_ringMixin.
Definition lfun_lalgType := Eval hnf in [lalgType R of 'End(vT)
for LalgType R lfun_ringType (fun k x y ⇒ comp_lfunZr k y x)].
Definition lfun_algType := Eval hnf in [algType R of 'End(vT)
for AlgType R _ (fun k (x y : lfun_lalgType) ⇒ comp_lfunZl k y x)].
End LfunAlgebra.
Section Projection.
Variables (K : fieldType) (vT : vectType K).
Implicit Types U V : {vspace vT}.
Definition daddv_pi U V := Vector.Hom (proj_mx (vs2mx U) (vs2mx V)).
Definition projv U := daddv_pi U U^C.
Definition addv_pi1 U V := daddv_pi (U :\: V) V.
Definition addv_pi2 U V := daddv_pi V (U :\: V).
Lemma memv_pi U V w : (daddv_pi U V) w \in U.
Lemma memv_proj U w : projv U w \in U.
Lemma memv_pi1 U V w : (addv_pi1 U V) w \in U.
Lemma memv_pi2 U V w : (addv_pi2 U V) w \in V.
Lemma daddv_pi_id U V u : (U :&: V = 0)%VS → u \in U → daddv_pi U V u = u.
Lemma daddv_pi_proj U V w (pi := daddv_pi U V) :
(U :&: V = 0)%VS → pi (pi w) = pi w.
Lemma daddv_pi_add U V w :
(U :&: V = 0)%VS → (w \in U + V)%VS → daddv_pi U V w + daddv_pi V U w = w.
Lemma projv_id U u : u \in U → projv U u = u.
Lemma projv_proj U w : projv U (projv U w) = projv U w.
Lemma memv_projC U w : w - projv U w \in (U^C)%VS.
Lemma limg_proj U : limg (projv U) = U.
Lemma lker_proj U : lker (projv U) = (U^C)%VS.
Lemma addv_pi1_proj U V w (pi1 := addv_pi1 U V) : pi1 (pi1 w) = pi1 w.
Lemma addv_pi2_id U V v : v \in V → addv_pi2 U V v = v.
Lemma addv_pi2_proj U V w (pi2 := addv_pi2 U V) : pi2 (pi2 w) = pi2 w.
Lemma addv_pi1_pi2 U V w :
w \in (U + V)%VS → addv_pi1 U V w + addv_pi2 U V w = w.
Section Sumv_Pi.
Variables (I : eqType) (r0 : seq I) (P : pred I) (Vs : I → {vspace vT}).
Let sumv_pi_rec i :=
fix loop r := if r is j :: r1 then
let V1 := (\sum_(k <- r1) Vs k)%VS in
if j == i then addv_pi1 (Vs j) V1 else (loop r1 \o addv_pi2 (Vs j) V1)%VF
else 0.
Notation sumV := (\sum_(i <- r0 | P i) Vs i)%VS.
Definition sumv_pi_for V of V = sumV := fun i ⇒ sumv_pi_rec i (filter P r0).
Variables (V : {vspace vT}) (defV : V = sumV).
Lemma memv_sum_pi i v : sumv_pi_for defV i v \in Vs i.
Lemma sumv_pi_uniq_sum v :
uniq (filter P r0) → v \in V →
\sum_(i <- r0 | P i) sumv_pi_for defV i v = v.
End Sumv_Pi.
End Projection.
Notation sumv_pi V := (sumv_pi_for (erefl V)).
Section SumvPi.
Variable (K : fieldType) (vT : vectType K).
Lemma sumv_pi_sum (I : finType) (P : pred I) Vs v (V : {vspace vT})
(defV : V = (\sum_(i | P i) Vs i)%VS) :
v \in V → \sum_(i | P i) sumv_pi_for defV i v = v :> vT.
Lemma sumv_pi_nat_sum m n (P : pred nat) Vs v (V : {vspace vT})
(defV : V = (\sum_(m ≤ i < n | P i) Vs i)%VS) :
v \in V → \sum_(m ≤ i < n | P i) sumv_pi_for defV i v = v :> vT.
End SumvPi.
Section SubVector.
Turn a {vspace V} into a vectType
Variable (K : fieldType) (vT : vectType K) (U : {vspace vT}).
Inductive subvs_of : predArgType := Subvs u & u \in U.
Definition vsval w := let: Subvs u _ := w in u.
Canonical subvs_subType := Eval hnf in [subType for vsval].
Definition subvs_eqMixin := Eval hnf in [eqMixin of subvs_of by <:].
Canonical subvs_eqType := Eval hnf in EqType subvs_of subvs_eqMixin.
Definition subvs_choiceMixin := [choiceMixin of subvs_of by <:].
Canonical subvs_choiceType := ChoiceType subvs_of subvs_choiceMixin.
Definition subvs_zmodMixin := [zmodMixin of subvs_of by <:].
Canonical subvs_zmodType := ZmodType subvs_of subvs_zmodMixin.
Definition subvs_lmodMixin := [lmodMixin of subvs_of by <:].
Canonical subvs_lmodType := LmodType K subvs_of subvs_lmodMixin.
Lemma subvsP w : vsval w \in U.
Lemma subvs_inj : injective vsval.
Lemma congr_subvs u v : u = v → vsval u = vsval v.
Lemma vsval_is_linear : linear vsval.
Canonical vsval_additive := Additive vsval_is_linear.
Canonical vsval_linear := AddLinear vsval_is_linear.
Fact vsproj_key : unit.
Definition vsproj_def u := Subvs (memv_proj U u).
Definition vsproj := locked_with vsproj_key vsproj_def.
Canonical vsproj_unlockable := [unlockable fun vsproj].
Lemma vsprojK : {in U, cancel vsproj vsval}.
Lemma vsvalK : cancel vsval vsproj.
Lemma vsproj_is_linear : linear vsproj.
Canonical vsproj_additive := Additive vsproj_is_linear.
Canonical vsproj_linear := AddLinear vsproj_is_linear.
Fact subvs_vect_iso : Vector.axiom (\dim U) subvs_of.
Definition subvs_vectMixin := VectMixin subvs_vect_iso.
Canonical subvs_vectType := VectType K subvs_of subvs_vectMixin.
End SubVector.
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 := let: Subvs u _ := w in u.
Canonical subvs_subType := Eval hnf in [subType for vsval].
Definition subvs_eqMixin := Eval hnf in [eqMixin of subvs_of by <:].
Canonical subvs_eqType := Eval hnf in EqType subvs_of subvs_eqMixin.
Definition subvs_choiceMixin := [choiceMixin of subvs_of by <:].
Canonical subvs_choiceType := ChoiceType subvs_of subvs_choiceMixin.
Definition subvs_zmodMixin := [zmodMixin of subvs_of by <:].
Canonical subvs_zmodType := ZmodType subvs_of subvs_zmodMixin.
Definition subvs_lmodMixin := [lmodMixin of subvs_of by <:].
Canonical subvs_lmodType := LmodType K subvs_of subvs_lmodMixin.
Lemma subvsP w : vsval w \in U.
Lemma subvs_inj : injective vsval.
Lemma congr_subvs u v : u = v → vsval u = vsval v.
Lemma vsval_is_linear : linear vsval.
Canonical vsval_additive := Additive vsval_is_linear.
Canonical vsval_linear := AddLinear vsval_is_linear.
Fact vsproj_key : unit.
Definition vsproj_def u := Subvs (memv_proj U u).
Definition vsproj := locked_with vsproj_key vsproj_def.
Canonical vsproj_unlockable := [unlockable fun vsproj].
Lemma vsprojK : {in U, cancel vsproj vsval}.
Lemma vsvalK : cancel vsval vsproj.
Lemma vsproj_is_linear : linear vsproj.
Canonical vsproj_additive := Additive vsproj_is_linear.
Canonical vsproj_linear := AddLinear vsproj_is_linear.
Fact subvs_vect_iso : Vector.axiom (\dim U) subvs_of.
Definition subvs_vectMixin := VectMixin subvs_vect_iso.
Canonical subvs_vectType := VectType K subvs_of subvs_vectMixin.
End SubVector.
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).
Definition matrix_vectMixin := VectMixin matrix_vect_iso.
Canonical matrix_vectType := VectType R 'M[R]_(m, n) matrix_vectMixin.
End MatrixVectType.
Definition matrix_vectMixin := VectMixin matrix_vect_iso.
Canonical matrix_vectType := VectType R 'M[R]_(m, n) matrix_vectMixin.
End MatrixVectType.
A ring is a one-dimension vector space
Section RegularVectType.
Variable R : ringType.
Fact regular_vect_iso : Vector.axiom 1 R^o.
Definition regular_vectMixin := VectMixin regular_vect_iso.
Canonical regular_vectType := VectType R R^o regular_vectMixin.
End RegularVectType.
Variable R : ringType.
Fact regular_vect_iso : Vector.axiom 1 R^o.
Definition regular_vectMixin := VectMixin regular_vect_iso.
Canonical regular_vectType := VectType R R^o regular_vectMixin.
End RegularVectType.
External direct product of two vectTypes.
Section ProdVector.
Variables (R : ringType) (vT1 vT2 : vectType R).
Fact pair_vect_iso : Vector.axiom (Vector.dim vT1 + Vector.dim vT2) (vT1 × vT2).
Definition pair_vectMixin := VectMixin pair_vect_iso.
Canonical pair_vectType := VectType R (vT1 × vT2) pair_vectMixin.
End ProdVector.
Variables (R : ringType) (vT1 vT2 : vectType R).
Fact pair_vect_iso : Vector.axiom (Vector.dim vT1 + Vector.dim vT2) (vT1 × vT2).
Definition pair_vectMixin := VectMixin pair_vect_iso.
Canonical pair_vectType := VectType R (vT1 × vT2) pair_vectMixin.
End ProdVector.
Function from a finType into a ring form a vectype.
Type unification with exist is again a problem in this proof.
Fact ffun_vect_iso : Vector.axiom (#|I| × Vector.dim vT) {ffun I → vT}.
Definition ffun_vectMixin := VectMixin ffun_vect_iso.
Canonical ffun_vectType := VectType R {ffun I → vT} ffun_vectMixin.
End FunVectType.
Canonical exp_vectType (K : fieldType) (vT : vectType K) n :=
[vectType K of vT ^ n].
Definition ffun_vectMixin := VectMixin ffun_vect_iso.
Canonical ffun_vectType := VectType R {ffun I → vT} ffun_vectMixin.
End FunVectType.
Canonical exp_vectType (K : fieldType) (vT : vectType K) n :=
[vectType K of vT ^ n].
Solving a tuple of linear equations.
Section Solver.
Variable (K : fieldType) (vT : vectType K).
Variables (n : nat) (lhs : n.-tuple 'End(vT)) (rhs : n.-tuple vT).
Let lhsf u := finfun ((tnth lhs)^~ u).
Definition vsolve_eq U := finfun (tnth rhs) \in (linfun lhsf @: U)%VS.
Lemma vsolve_eqP (U : {vspace vT}) :
reflect (exists2 u, u \in U & ∀ i, tnth lhs i u = tnth rhs i)
(vsolve_eq U).
End Solver.
Variable (K : fieldType) (vT : vectType K).
Variables (n : nat) (lhs : n.-tuple 'End(vT)) (rhs : n.-tuple vT).
Let lhsf u := finfun ((tnth lhs)^~ u).
Definition vsolve_eq U := finfun (tnth rhs) \in (linfun lhsf @: U)%VS.
Lemma vsolve_eqP (U : {vspace vT}) :
reflect (exists2 u, u \in U & ∀ i, tnth lhs i u = tnth rhs i)
(vsolve_eq U).
End Solver.