Library mathcomp.field.falgebra
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
Finite dimensional free algebras, usually known as F-algebras.
FalgType K == the interface type for F-algebras over K; it simply
joins the unitAlgType K and vectType K interfaces.
[FalgType K of aT] == an FalgType K structure for a type aT that has both
unitAlgType K and vectType K canonical structures.
[FalgType K of aT for vT] == an FalgType K structure for a type aT with a
unitAlgType K canonical structure, given a structure
vT : vectType K whose lmodType K projection matches
the canonical lmodType for aT.
FalgUnitRingType T == a default unitRingType structure for a type T with
both algType and vectType structures.
Any aT with an FalgType structure inherits all the Vector, Ring and
Algebra operations, and supports the following additional operations:
\dim_A M == (\dim M %/ dim A)%N -- free module dimension.
amull u == the linear function v |-> u * v, for u, v : aT.
amulr u == the linear function v |-> v * u, for u, v : aT.
1, f * g, f ^+ n == the identity function, the composite g \o f, the nth
iterate of f, for 1, f, g in 'End(aT). This is just
the usual F-algebra structure on 'End(aT). It is NOT
canonical by default, but can be activated by the
line Import FalgLfun. Beware also that (f^-1)%VF is
the linear function inverse, not the ring inverse of
f (though they do coincide when f is injective).
1%VS == the line generated by 1 : aT.
(U * V)%VS == the smallest subspace of aT that contains all
products u * v for u in U, v in V.
(U ^+ n)%VS == (U * U * ... * U), n-times. U ^+ 0 = 1%VS
'C[u]%VS == the centraliser subspace of the vector u.
'C_U[v]%VS := (U :&: 'C[v])%VS.
'C(V)%VS == the centraliser subspace of the subspace V.
'C_U(V)%VS := (U :&: 'C(V))%VS.
'Z(V)%VS == the center subspace of the subspace V.
agenv U == the smallest subalgebra containing U ^+ n for all n.
U; v%VS == agenv (U + < [v]>) (adjoin v to U).
U & vs%VS == agenv (U + vs) (adjoin vs to U).
{aspace aT} == a subType of {vspace aT} consisting of sub-algebras
of aT (see below); for A : {aspace aT}, subvs_of A
has a canonical FalgType K structure.
is_aspace U <=> the characteristic predicate of {aspace aT} stating
that U is closed under product and contains an
identity element, := has_algid U && (U * U <= U)%VS.
algid A == the identity element of A : {aspace aT}, which need
not be equal to 1 (indeed, in a Wedderburn
decomposition it is not even a unit in aT).
is_algid U e <-> e : aT is an identity element for the subspace U:
e in U, e != 0 & e * u = u * e = u for all u in U.
has_algid U <=> there is an e such that is_algid U e.
[aspace of U] == a clone of an existing {aspace aT} structure on
U : {vspace aT} (more instances of {aspace aT} will
be defined in extFieldType).
[aspace of U for A] == a clone of A : {aspace aT} for U : {vspace aT}.
1%AS == the canonical sub-algebra 1%VS.
{:aT}%AS == the canonical full algebra.
U%AS == the canonical algebra for agenv U; note that this is
unrelated to vs%VS, the subspace spanned by vs.
U; v%AS == the canonical algebra for U; v%VS.
U & vs%AS == the canonical algebra for U & vs%VS.
ahom_in U f <=> f : 'Hom(aT, rT) is a multiplicative homomorphism
inside U, and in addition f 1 = 1 (even if U doesn't
contain 1). Note that f @: U need not be a
subalgebra when U is, as f could annilate U.
'AHom(aT, rT) == the type of algebra homomorphisms from aT to rT,
where aT and rT ARE FalgType structures. Elements of
'AHom(aT, rT) coerce to 'End(aT, rT) and aT -> rT.
> Caveat: aT and rT must denote actual FalgType structures, not their
projections on Type.
'AEnd(aT) == algebra endomorphisms of aT (:= 'AHom(aT, aT)).
Set Implicit Arguments.
Open Local Scope ring_scope.
Reserved Notation "{ 'aspace' T }" (at level 0, format "{ 'aspace' T }").
Reserved Notation "<< U & vs >>" (at level 0, format "<< U & vs >>").
Reserved Notation "<< U ; x >>" (at level 0, format "<< U ; x >>").
Reserved Notation "''AHom' ( T , rT )"
(at level 8, format "''AHom' ( T , rT )").
Reserved Notation "''AEnd' ( T )" (at level 8, format "''AEnd' ( T )").
Notation "\dim_ E V" := (divn (\dim V) (\dim E))
(at level 10, E at level 2, V at level 8, format "\dim_ E V") : nat_scope.
Import GRing.Theory.
Finite dimensional algebra
Supply a default unitRing mixin for the default unitAlgType base type.
Section DefaultBase.
Variables (K : fieldType) (A : algType K).
Lemma BaseMixin : Vector.mixin_of A → GRing.UnitRing.mixin_of A.
Definition BaseType T :=
fun c vAm & phant_id c (GRing.UnitRing.Class (BaseMixin vAm)) ⇒
fun (vT : vectType K) & phant vT
& phant_id (Vector.mixin (Vector.class vT)) vAm ⇒
@GRing.UnitRing.Pack T c T.
End DefaultBase.
Section ClassDef.
Variable R : ringType.
Implicit Type phR : phant R.
Record class_of A := Class {
base1 : GRing.UnitAlgebra.class_of R A;
mixin : Vector.mixin_of (GRing.Lmodule.Pack _ base1 A)
}.
Definition base2 A c := @Vector.Class _ _ (@base1 A c) (mixin c).
Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
Variables (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition pack :=
fun bT b & phant_id (@GRing.UnitAlgebra.class R phR bT)
(b : GRing.UnitAlgebra.class_of R T) ⇒
fun mT m & phant_id (@Vector.class R phR mT) (@Vector.Class R T b m) ⇒
Pack (Phant R) (@Class T b m) T.
Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT.
Definition algType := @GRing.Algebra.Pack R phR cT xclass xT.
Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT xclass xT.
Definition vectType := @Vector.Pack R phR cT xclass cT.
Definition vect_ringType := @GRing.Ring.Pack vectType xclass xT.
Definition vect_unitRingType := @GRing.UnitRing.Pack vectType xclass xT.
Definition vect_lalgType := @GRing.Lalgebra.Pack R phR vectType xclass xT.
Definition vect_algType := @GRing.Algebra.Pack R phR vectType xclass xT.
Definition vect_unitAlgType := @GRing.UnitAlgebra.Pack R phR vectType xclass xT.
End ClassDef.
Module Exports.
Coercion base1 : class_of >-> GRing.UnitAlgebra.class_of.
Coercion base2 : class_of >-> Vector.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion lmodType : type>-> GRing.Lmodule.type.
Canonical lmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion lalgType : type >-> GRing.Lalgebra.type.
Canonical lalgType.
Coercion algType : type >-> GRing.Algebra.type.
Canonical algType.
Coercion unitAlgType : type >-> GRing.UnitAlgebra.type.
Canonical unitAlgType.
Coercion vectType : type >-> Vector.type.
Canonical vectType.
Canonical vect_ringType.
Canonical vect_unitRingType.
Canonical vect_lalgType.
Canonical vect_algType.
Canonical vect_unitAlgType.
Notation FalgType R := (type (Phant R)).
Notation "[ 'FalgType' R 'of' A ]" := (@pack _ (Phant R) A _ _ id _ _ id)
(at level 0, format "[ 'FalgType' R 'of' A ]") : form_scope.
Notation "[ 'FalgType' R 'of' A 'for' vT ]" :=
(@pack _ (Phant R) A _ _ id vT _ idfun)
(at level 0, format "[ 'FalgType' R 'of' A 'for' vT ]") : form_scope.
Notation FalgUnitRingType T := (@BaseType _ _ T _ _ id _ (Phant T) id).
End Exports.
End Falgebra.
Export Falgebra.Exports.
Notation "1" := (vline 1) : vspace_scope.
Canonical matrix_FalgType (K : fieldType) n := [FalgType K of 'M[K]_n.+1].
Canonical regular_FalgType (R : comUnitRingType) := [FalgType R of R^o].
Lemma regular_fullv (K : fieldType) : (fullv = 1 :> {vspace K^o})%VS.
Section Proper.
Variables (R : ringType) (aT : FalgType R).
Import Vector.InternalTheory.
Lemma FalgType_proper : Vector.dim aT > 0.
End Proper.
Module FalgLfun.
Section FalgLfun.
Variable (R : comRingType) (aT : FalgType R).
Implicit Types f g : 'End(aT).
Canonical Falg_fun_ringType := lfun_ringType (FalgType_proper aT).
Canonical Falg_fun_lalgType := lfun_lalgType (FalgType_proper aT).
Canonical Falg_fun_algType := lfun_algType (FalgType_proper aT).
Lemma lfun_mulE f g u : (f × g) u = g (f u).
Lemma lfun_compE f g : (g \o f)%VF = f × g.
End FalgLfun.
Section InvLfun.
Variable (K : fieldType) (aT : FalgType K).
Implicit Types f g : 'End(aT).
Definition lfun_invr f := if lker f == 0%VS then f^-1%VF else f.
Lemma lfun_mulVr f : lker f == 0%VS → f^-1%VF × f = 1.
Lemma lfun_mulrV f : lker f == 0%VS → f × f^-1%VF = 1.
Fact lfun_mulRVr f : lker f == 0%VS → lfun_invr f × f = 1.
Fact lfun_mulrRV f : lker f == 0%VS → f × lfun_invr f = 1.
Fact lfun_unitrP f g : g × f = 1 ∧ f × g = 1 → lker f == 0%VS.
Lemma lfun_invr_out f : lker f != 0%VS → lfun_invr f = f.
Definition lfun_unitRingMixin :=
UnitRingMixin lfun_mulRVr lfun_mulrRV lfun_unitrP lfun_invr_out.
Canonical lfun_unitRingType := UnitRingType 'End(aT) lfun_unitRingMixin.
Canonical lfun_unitAlgType := [unitAlgType K of 'End(aT)].
Canonical Falg_fun_FalgType := [FalgType K of 'End(aT)].
Lemma lfun_invE f : lker f == 0%VS → f^-1%VF = f^-1.
End InvLfun.
End FalgLfun.
Section FalgebraTheory.
Variables (K : fieldType) (aT : FalgType K).
Implicit Types (u v : aT) (U V W : {vspace aT}).
Import FalgLfun.
Definition amull u : 'End(aT) := linfun (u \*o @idfun aT).
Definition amulr u : 'End(aT) := linfun (u \o× @idfun aT).
Lemma amull_inj : injective amull.
Lemma amulr_inj : injective amulr.
Fact amull_is_linear : linear amull.
Canonical amull_additive := Eval hnf in Additive amull_is_linear.
Canonical amull_linear := Eval hnf in AddLinear amull_is_linear.
Variables (K : fieldType) (A : algType K).
Lemma BaseMixin : Vector.mixin_of A → GRing.UnitRing.mixin_of A.
Definition BaseType T :=
fun c vAm & phant_id c (GRing.UnitRing.Class (BaseMixin vAm)) ⇒
fun (vT : vectType K) & phant vT
& phant_id (Vector.mixin (Vector.class vT)) vAm ⇒
@GRing.UnitRing.Pack T c T.
End DefaultBase.
Section ClassDef.
Variable R : ringType.
Implicit Type phR : phant R.
Record class_of A := Class {
base1 : GRing.UnitAlgebra.class_of R A;
mixin : Vector.mixin_of (GRing.Lmodule.Pack _ base1 A)
}.
Definition base2 A c := @Vector.Class _ _ (@base1 A c) (mixin c).
Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
Variables (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition pack :=
fun bT b & phant_id (@GRing.UnitAlgebra.class R phR bT)
(b : GRing.UnitAlgebra.class_of R T) ⇒
fun mT m & phant_id (@Vector.class R phR mT) (@Vector.Class R T b m) ⇒
Pack (Phant R) (@Class T b m) T.
Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT.
Definition algType := @GRing.Algebra.Pack R phR cT xclass xT.
Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT xclass xT.
Definition vectType := @Vector.Pack R phR cT xclass cT.
Definition vect_ringType := @GRing.Ring.Pack vectType xclass xT.
Definition vect_unitRingType := @GRing.UnitRing.Pack vectType xclass xT.
Definition vect_lalgType := @GRing.Lalgebra.Pack R phR vectType xclass xT.
Definition vect_algType := @GRing.Algebra.Pack R phR vectType xclass xT.
Definition vect_unitAlgType := @GRing.UnitAlgebra.Pack R phR vectType xclass xT.
End ClassDef.
Module Exports.
Coercion base1 : class_of >-> GRing.UnitAlgebra.class_of.
Coercion base2 : class_of >-> Vector.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion lmodType : type>-> GRing.Lmodule.type.
Canonical lmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion lalgType : type >-> GRing.Lalgebra.type.
Canonical lalgType.
Coercion algType : type >-> GRing.Algebra.type.
Canonical algType.
Coercion unitAlgType : type >-> GRing.UnitAlgebra.type.
Canonical unitAlgType.
Coercion vectType : type >-> Vector.type.
Canonical vectType.
Canonical vect_ringType.
Canonical vect_unitRingType.
Canonical vect_lalgType.
Canonical vect_algType.
Canonical vect_unitAlgType.
Notation FalgType R := (type (Phant R)).
Notation "[ 'FalgType' R 'of' A ]" := (@pack _ (Phant R) A _ _ id _ _ id)
(at level 0, format "[ 'FalgType' R 'of' A ]") : form_scope.
Notation "[ 'FalgType' R 'of' A 'for' vT ]" :=
(@pack _ (Phant R) A _ _ id vT _ idfun)
(at level 0, format "[ 'FalgType' R 'of' A 'for' vT ]") : form_scope.
Notation FalgUnitRingType T := (@BaseType _ _ T _ _ id _ (Phant T) id).
End Exports.
End Falgebra.
Export Falgebra.Exports.
Notation "1" := (vline 1) : vspace_scope.
Canonical matrix_FalgType (K : fieldType) n := [FalgType K of 'M[K]_n.+1].
Canonical regular_FalgType (R : comUnitRingType) := [FalgType R of R^o].
Lemma regular_fullv (K : fieldType) : (fullv = 1 :> {vspace K^o})%VS.
Section Proper.
Variables (R : ringType) (aT : FalgType R).
Import Vector.InternalTheory.
Lemma FalgType_proper : Vector.dim aT > 0.
End Proper.
Module FalgLfun.
Section FalgLfun.
Variable (R : comRingType) (aT : FalgType R).
Implicit Types f g : 'End(aT).
Canonical Falg_fun_ringType := lfun_ringType (FalgType_proper aT).
Canonical Falg_fun_lalgType := lfun_lalgType (FalgType_proper aT).
Canonical Falg_fun_algType := lfun_algType (FalgType_proper aT).
Lemma lfun_mulE f g u : (f × g) u = g (f u).
Lemma lfun_compE f g : (g \o f)%VF = f × g.
End FalgLfun.
Section InvLfun.
Variable (K : fieldType) (aT : FalgType K).
Implicit Types f g : 'End(aT).
Definition lfun_invr f := if lker f == 0%VS then f^-1%VF else f.
Lemma lfun_mulVr f : lker f == 0%VS → f^-1%VF × f = 1.
Lemma lfun_mulrV f : lker f == 0%VS → f × f^-1%VF = 1.
Fact lfun_mulRVr f : lker f == 0%VS → lfun_invr f × f = 1.
Fact lfun_mulrRV f : lker f == 0%VS → f × lfun_invr f = 1.
Fact lfun_unitrP f g : g × f = 1 ∧ f × g = 1 → lker f == 0%VS.
Lemma lfun_invr_out f : lker f != 0%VS → lfun_invr f = f.
Definition lfun_unitRingMixin :=
UnitRingMixin lfun_mulRVr lfun_mulrRV lfun_unitrP lfun_invr_out.
Canonical lfun_unitRingType := UnitRingType 'End(aT) lfun_unitRingMixin.
Canonical lfun_unitAlgType := [unitAlgType K of 'End(aT)].
Canonical Falg_fun_FalgType := [FalgType K of 'End(aT)].
Lemma lfun_invE f : lker f == 0%VS → f^-1%VF = f^-1.
End InvLfun.
End FalgLfun.
Section FalgebraTheory.
Variables (K : fieldType) (aT : FalgType K).
Implicit Types (u v : aT) (U V W : {vspace aT}).
Import FalgLfun.
Definition amull u : 'End(aT) := linfun (u \*o @idfun aT).
Definition amulr u : 'End(aT) := linfun (u \o× @idfun aT).
Lemma amull_inj : injective amull.
Lemma amulr_inj : injective amulr.
Fact amull_is_linear : linear amull.
Canonical amull_additive := Eval hnf in Additive amull_is_linear.
Canonical amull_linear := Eval hnf in AddLinear amull_is_linear.
amull is a converse ring morphism
Lemma amull1 : amull 1 = \1%VF.
Lemma amullM u v : (amull (u × v) = amull v × amull u)%VF.
Lemma amulr_is_lrmorphism : lrmorphism amulr.
Canonical amulr_additive := Eval hnf in Additive amulr_is_lrmorphism.
Canonical amulr_linear := Eval hnf in AddLinear amulr_is_lrmorphism.
Canonical amulr_rmorphism := Eval hnf in AddRMorphism amulr_is_lrmorphism.
Canonical amulr_lrmorphism := Eval hnf in LRMorphism amulr_is_lrmorphism.
Lemma lker0_amull u : u \is a GRing.unit → lker (amull u) == 0%VS.
Lemma lker0_amulr u : u \is a GRing.unit → lker (amulr u) == 0%VS.
Lemma lfun1_poly (p : {poly aT}) : map_poly \1%VF p = p.
Fact prodv_key : unit.
Definition prodv :=
locked_with prodv_key (fun U V ⇒ <<allpairs *%R (vbasis U) (vbasis V)>>%VS).
Canonical prodv_unlockable := [unlockable fun prodv].
Lemma memv_mul U V : {in U & V, ∀ u v, u × v \in (U × V)%VS}.
Lemma prodvP {U V W} :
reflect {in U & V, ∀ u v, u × v \in W} (U × V ≤ W)%VS.
Lemma prodv_line u v : (<[u]> × <[v]> = <[u × v]>)%VS.
Lemma dimv1: \dim (1%VS : {vspace aT}) = 1%N.
Lemma dim_prodv U V : \dim (U × V) ≤ \dim U × \dim V.
Lemma vspace1_neq0 : (1 != 0 :> {vspace aT})%VS.
Lemma vbasis1 : exists2 k, k != 0 & vbasis 1 = [:: k%:A] :> seq aT.
Lemma prod0v : left_zero 0%VS prodv.
Lemma prodv0 : right_zero 0%VS prodv.
Canonical prodv_muloid := Monoid.MulLaw prod0v prodv0.
Lemma prod1v : left_id 1%VS prodv.
Lemma prodv1 : right_id 1%VS prodv.
Lemma prodvS U1 U2 V1 V2 : (U1 ≤ U2 → V1 ≤ V2 → U1 × V1 ≤ U2 × V2)%VS.
Lemma prodvSl U1 U2 V : (U1 ≤ U2 → U1 × V ≤ U2 × V)%VS.
Lemma prodvSr U V1 V2 : (V1 ≤ V2 → U × V1 ≤ U × V2)%VS.
Lemma prodvDl : left_distributive prodv addv.
Lemma prodvDr : right_distributive prodv addv.
Canonical addv_addoid := Monoid.AddLaw prodvDl prodvDr.
Lemma prodvA : associative prodv.
Canonical prodv_monoid := Monoid.Law prodvA prod1v prodv1.
Definition expv U n := iterop n.+1.-1 prodv U 1%VS.
Lemma expv0 U : (U ^+ 0 = 1)%VS.
Lemma expv1 U : (U ^+ 1 = U)%VS.
Lemma expv2 U : (U ^+ 2 = U × U)%VS.
Lemma expvSl U n : (U ^+ n.+1 = U × U ^+ n)%VS.
Lemma expv0n n : (0 ^+ n = if n is _.+1 then 0 else 1)%VS.
Lemma expv1n n : (1 ^+ n = 1)%VS.
Lemma expvD U m n : (U ^+ (m + n) = U ^+ m × U ^+ n)%VS.
Lemma expvSr U n : (U ^+ n.+1 = U ^+ n × U)%VS.
Lemma expvM U m n : (U ^+ (m × n) = U ^+ m ^+ n)%VS.
Lemma expvS U V n : (U ≤ V → U ^+ n ≤ V ^+ n)%VS.
Lemma expv_line u n : (<[u]> ^+ n = <[u ^+ n]>)%VS.
Lemma amullM u v : (amull (u × v) = amull v × amull u)%VF.
Lemma amulr_is_lrmorphism : lrmorphism amulr.
Canonical amulr_additive := Eval hnf in Additive amulr_is_lrmorphism.
Canonical amulr_linear := Eval hnf in AddLinear amulr_is_lrmorphism.
Canonical amulr_rmorphism := Eval hnf in AddRMorphism amulr_is_lrmorphism.
Canonical amulr_lrmorphism := Eval hnf in LRMorphism amulr_is_lrmorphism.
Lemma lker0_amull u : u \is a GRing.unit → lker (amull u) == 0%VS.
Lemma lker0_amulr u : u \is a GRing.unit → lker (amulr u) == 0%VS.
Lemma lfun1_poly (p : {poly aT}) : map_poly \1%VF p = p.
Fact prodv_key : unit.
Definition prodv :=
locked_with prodv_key (fun U V ⇒ <<allpairs *%R (vbasis U) (vbasis V)>>%VS).
Canonical prodv_unlockable := [unlockable fun prodv].
Lemma memv_mul U V : {in U & V, ∀ u v, u × v \in (U × V)%VS}.
Lemma prodvP {U V W} :
reflect {in U & V, ∀ u v, u × v \in W} (U × V ≤ W)%VS.
Lemma prodv_line u v : (<[u]> × <[v]> = <[u × v]>)%VS.
Lemma dimv1: \dim (1%VS : {vspace aT}) = 1%N.
Lemma dim_prodv U V : \dim (U × V) ≤ \dim U × \dim V.
Lemma vspace1_neq0 : (1 != 0 :> {vspace aT})%VS.
Lemma vbasis1 : exists2 k, k != 0 & vbasis 1 = [:: k%:A] :> seq aT.
Lemma prod0v : left_zero 0%VS prodv.
Lemma prodv0 : right_zero 0%VS prodv.
Canonical prodv_muloid := Monoid.MulLaw prod0v prodv0.
Lemma prod1v : left_id 1%VS prodv.
Lemma prodv1 : right_id 1%VS prodv.
Lemma prodvS U1 U2 V1 V2 : (U1 ≤ U2 → V1 ≤ V2 → U1 × V1 ≤ U2 × V2)%VS.
Lemma prodvSl U1 U2 V : (U1 ≤ U2 → U1 × V ≤ U2 × V)%VS.
Lemma prodvSr U V1 V2 : (V1 ≤ V2 → U × V1 ≤ U × V2)%VS.
Lemma prodvDl : left_distributive prodv addv.
Lemma prodvDr : right_distributive prodv addv.
Canonical addv_addoid := Monoid.AddLaw prodvDl prodvDr.
Lemma prodvA : associative prodv.
Canonical prodv_monoid := Monoid.Law prodvA prod1v prodv1.
Definition expv U n := iterop n.+1.-1 prodv U 1%VS.
Lemma expv0 U : (U ^+ 0 = 1)%VS.
Lemma expv1 U : (U ^+ 1 = U)%VS.
Lemma expv2 U : (U ^+ 2 = U × U)%VS.
Lemma expvSl U n : (U ^+ n.+1 = U × U ^+ n)%VS.
Lemma expv0n n : (0 ^+ n = if n is _.+1 then 0 else 1)%VS.
Lemma expv1n n : (1 ^+ n = 1)%VS.
Lemma expvD U m n : (U ^+ (m + n) = U ^+ m × U ^+ n)%VS.
Lemma expvSr U n : (U ^+ n.+1 = U ^+ n × U)%VS.
Lemma expvM U m n : (U ^+ (m × n) = U ^+ m ^+ n)%VS.
Lemma expvS U V n : (U ≤ V → U ^+ n ≤ V ^+ n)%VS.
Lemma expv_line u n : (<[u]> ^+ n = <[u ^+ n]>)%VS.
Centralisers and centers.
Definition centraliser1_vspace u := lker (amulr u - amull u).
Definition centraliser_vspace V := (\bigcap_i 'C[tnth (vbasis V) i])%VS.
Definition center_vspace V := (V :&: 'C(V))%VS.
Lemma cent1vP u v : reflect (u × v = v × u) (u \in 'C[v]%VS).
Lemma cent1v1 u : 1 \in 'C[u]%VS.
Lemma cent1v_id u : u \in 'C[u]%VS.
Lemma cent1vX u n : u ^+ n \in 'C[u]%VS.
Lemma cent1vC u v : (u \in 'C[v])%VS = (v \in 'C[u])%VS.
Lemma centvP u V : reflect {in V, ∀ v, u × v = v × u} (u \in 'C(V))%VS.
Lemma centvsP U V : reflect {in U & V, commutative *%R} (U ≤ 'C(V))%VS.
Lemma subv_cent1 U v : (U ≤ 'C[v])%VS = (v \in 'C(U)%VS).
Lemma centv1 V : 1 \in 'C(V)%VS.
Lemma centvX V u n : u \in 'C(V)%VS → u ^+ n \in 'C(V)%VS.
Lemma centvC U V : (U ≤ 'C(V))%VS = (V ≤ 'C(U))%VS.
Lemma centerv_sub V : ('Z(V) ≤ V)%VS.
Lemma cent_centerv V : (V ≤ 'C('Z(V)))%VS.
Building the predicate that checks is a vspace has a unit
Definition is_algid e U :=
[/\ e \in U, e != 0 & {in U, ∀ u, e × u = u ∧ u × e = u}].
Fact algid_decidable U : decidable (∃ e, is_algid e U).
Definition has_algid : pred {vspace aT} := algid_decidable.
Lemma has_algidP {U} : reflect (∃ e, is_algid e U) (has_algid U).
Lemma has_algid1 U : 1 \in U → has_algid U.
Definition is_aspace U := has_algid U && (U × U ≤ U)%VS.
Structure aspace := ASpace {asval :> {vspace aT}; _ : is_aspace asval}.
Definition aspace_of of phant aT := aspace.
Canonical aspace_subType := Eval hnf in [subType for asval].
Definition aspace_eqMixin := [eqMixin of aspace by <:].
Canonical aspace_eqType := Eval hnf in EqType aspace aspace_eqMixin.
Definition aspace_choiceMixin := [choiceMixin of aspace by <:].
Canonical aspace_choiceType := Eval hnf in ChoiceType aspace aspace_choiceMixin.
Canonical aspace_of_subType := Eval hnf in [subType of {aspace aT}].
Canonical aspace_of_eqType := Eval hnf in [eqType of {aspace aT}].
Canonical aspace_of_choiceType := Eval hnf in [choiceType of {aspace aT}].
Definition clone_aspace U (A : {aspace aT}) :=
fun algU & phant_id algU (valP A) ⇒ @ASpace U algU : {aspace aT}.
Fact aspace1_subproof : is_aspace 1.
Canonical aspace1 : {aspace aT} := ASpace aspace1_subproof.
Lemma aspacef_subproof : is_aspace fullv.
Canonical aspacef : {aspace aT} := ASpace aspacef_subproof.
Lemma polyOver1P p :
reflect (∃ q, p = map_poly (in_alg aT) q) (p \is a polyOver 1%VS).
End FalgebraTheory.
Delimit Scope aspace_scope with AS.
Notation "{ 'aspace' T }" := (aspace_of (Phant T)) : type_scope.
Notation "A * B" := (prodv A B) : vspace_scope.
Notation "A ^+ n" := (expv A n) : vspace_scope.
Notation "'C [ u ]" := (centraliser1_vspace u) : vspace_scope.
Notation "'C_ U [ v ]" := (capv U 'C[v]) : vspace_scope.
Notation "'C_ ( U ) [ v ]" := (capv U 'C[v]) (only parsing) : vspace_scope.
Notation "'C ( V )" := (centraliser_vspace V) : vspace_scope.
Notation "'C_ U ( V )" := (capv U 'C(V)) : vspace_scope.
Notation "'C_ ( U ) ( V )" := (capv U 'C(V)) (only parsing) : vspace_scope.
Notation "'Z ( V )" := (center_vspace V) : vspace_scope.
Notation "1" := (aspace1 _) : aspace_scope.
Notation "{ : aT }" := (aspacef aT) : aspace_scope.
Notation "[ 'aspace' 'of' U ]" := (@clone_aspace _ _ U _ _ id)
(at level 0, format "[ 'aspace' 'of' U ]") : form_scope.
Notation "[ 'aspace' 'of' U 'for' A ]" := (@clone_aspace _ _ U A _ idfun)
(at level 0, format "[ 'aspace' 'of' U 'for' A ]") : form_scope.
Implicit Arguments prodvP [K aT U V W].
Implicit Arguments cent1vP [K aT u v].
Implicit Arguments centvP [K aT u V].
Implicit Arguments centvsP [K aT U V].
Implicit Arguments has_algidP [K aT U].
Implicit Arguments polyOver1P [K aT p].
Section AspaceTheory.
Variables (K : fieldType) (aT : FalgType K).
Implicit Types (u v e : aT) (U V : {vspace aT}) (A B : {aspace aT}).
Import FalgLfun.
Lemma algid_subproof U :
{e | e \in U
& has_algid U ==> (U ≤ lker (amull e - 1) :&: lker (amulr e - 1))%VS}.
Definition algid U := s2val (algid_subproof U).
Lemma memv_algid U : algid U \in U.
Lemma algidl A : {in A, left_id (algid A) *%R}.
Lemma algidr A : {in A, right_id (algid A) *%R}.
Lemma unitr_algid1 A u : u \in A → u \is a GRing.unit → algid A = 1.
Lemma algid_eq1 A : (algid A == 1) = (1 \in A).
Lemma algid_neq0 A : algid A != 0.
Lemma dim_algid A : \dim <[algid A]> = 1%N.
Lemma adim_gt0 A : (0 < \dim A)%N.
Lemma not_asubv0 A : ~~ (A ≤ 0)%VS.
Lemma adim1P {A} : reflect (A = <[algid A]>%VS :> {vspace aT}) (\dim A == 1%N).
Lemma asubv A : (A × A ≤ A)%VS.
Lemma memvM A : {in A &, ∀ u v, u × v \in A}.
Lemma prodv_id A : (A × A)%VS = A.
Lemma prodv_sub U V A : (U ≤ A → V ≤ A → U × V ≤ A)%VS.
Lemma expv_id A n : (A ^+ n.+1)%VS = A.
Lemma limg_amulr U v : (amulr v @: U = U × <[v]>)%VS.
Lemma memv_cosetP {U v w} :
reflect (exists2 u, u\in U & w = u × v) (w \in U × <[v]>)%VS.
Lemma dim_cosetv_unit V u : u \is a GRing.unit → \dim (V × <[u]>) = \dim V.
Lemma memvV A u : (u^-1 \in A) = (u \in A).
Fact aspace_cap_subproof A B : algid A \in B → is_aspace (A :&: B).
Definition aspace_cap A B BeA := ASpace (@aspace_cap_subproof A B BeA).
Fact centraliser1_is_aspace u : is_aspace 'C[u].
Canonical centraliser1_aspace u := ASpace (centraliser1_is_aspace u).
Fact centraliser_is_aspace V : is_aspace 'C(V).
Canonical centraliser_aspace V := ASpace (centraliser_is_aspace V).
Lemma centv_algid A : algid A \in 'C(A)%VS.
Canonical center_aspace A := [aspace of 'Z(A) for aspace_cap (centv_algid A)].
Lemma algid_center A : algid 'Z(A) = algid A.
Lemma Falgebra_FieldMixin :
GRing.IntegralDomain.axiom aT → GRing.Field.mixin_of aT.
Section SkewField.
Hypothesis fieldT : GRing.Field.mixin_of aT.
Lemma skew_field_algid1 A : algid A = 1.
Lemma skew_field_module_semisimple A M :
let sumA X := (\sum_(x <- X) A × <[x]>)%VS in
(A × M ≤ M)%VS → {X | [/\ sumA X = M, directv (sumA X) & 0 \notin X]}.
Lemma skew_field_module_dimS A M : (A × M ≤ M)%VS → \dim A %| \dim M.
Lemma skew_field_dimS A B : (A ≤ B)%VS → \dim A %| \dim B.
End SkewField.
End AspaceTheory.
[/\ e \in U, e != 0 & {in U, ∀ u, e × u = u ∧ u × e = u}].
Fact algid_decidable U : decidable (∃ e, is_algid e U).
Definition has_algid : pred {vspace aT} := algid_decidable.
Lemma has_algidP {U} : reflect (∃ e, is_algid e U) (has_algid U).
Lemma has_algid1 U : 1 \in U → has_algid U.
Definition is_aspace U := has_algid U && (U × U ≤ U)%VS.
Structure aspace := ASpace {asval :> {vspace aT}; _ : is_aspace asval}.
Definition aspace_of of phant aT := aspace.
Canonical aspace_subType := Eval hnf in [subType for asval].
Definition aspace_eqMixin := [eqMixin of aspace by <:].
Canonical aspace_eqType := Eval hnf in EqType aspace aspace_eqMixin.
Definition aspace_choiceMixin := [choiceMixin of aspace by <:].
Canonical aspace_choiceType := Eval hnf in ChoiceType aspace aspace_choiceMixin.
Canonical aspace_of_subType := Eval hnf in [subType of {aspace aT}].
Canonical aspace_of_eqType := Eval hnf in [eqType of {aspace aT}].
Canonical aspace_of_choiceType := Eval hnf in [choiceType of {aspace aT}].
Definition clone_aspace U (A : {aspace aT}) :=
fun algU & phant_id algU (valP A) ⇒ @ASpace U algU : {aspace aT}.
Fact aspace1_subproof : is_aspace 1.
Canonical aspace1 : {aspace aT} := ASpace aspace1_subproof.
Lemma aspacef_subproof : is_aspace fullv.
Canonical aspacef : {aspace aT} := ASpace aspacef_subproof.
Lemma polyOver1P p :
reflect (∃ q, p = map_poly (in_alg aT) q) (p \is a polyOver 1%VS).
End FalgebraTheory.
Delimit Scope aspace_scope with AS.
Notation "{ 'aspace' T }" := (aspace_of (Phant T)) : type_scope.
Notation "A * B" := (prodv A B) : vspace_scope.
Notation "A ^+ n" := (expv A n) : vspace_scope.
Notation "'C [ u ]" := (centraliser1_vspace u) : vspace_scope.
Notation "'C_ U [ v ]" := (capv U 'C[v]) : vspace_scope.
Notation "'C_ ( U ) [ v ]" := (capv U 'C[v]) (only parsing) : vspace_scope.
Notation "'C ( V )" := (centraliser_vspace V) : vspace_scope.
Notation "'C_ U ( V )" := (capv U 'C(V)) : vspace_scope.
Notation "'C_ ( U ) ( V )" := (capv U 'C(V)) (only parsing) : vspace_scope.
Notation "'Z ( V )" := (center_vspace V) : vspace_scope.
Notation "1" := (aspace1 _) : aspace_scope.
Notation "{ : aT }" := (aspacef aT) : aspace_scope.
Notation "[ 'aspace' 'of' U ]" := (@clone_aspace _ _ U _ _ id)
(at level 0, format "[ 'aspace' 'of' U ]") : form_scope.
Notation "[ 'aspace' 'of' U 'for' A ]" := (@clone_aspace _ _ U A _ idfun)
(at level 0, format "[ 'aspace' 'of' U 'for' A ]") : form_scope.
Implicit Arguments prodvP [K aT U V W].
Implicit Arguments cent1vP [K aT u v].
Implicit Arguments centvP [K aT u V].
Implicit Arguments centvsP [K aT U V].
Implicit Arguments has_algidP [K aT U].
Implicit Arguments polyOver1P [K aT p].
Section AspaceTheory.
Variables (K : fieldType) (aT : FalgType K).
Implicit Types (u v e : aT) (U V : {vspace aT}) (A B : {aspace aT}).
Import FalgLfun.
Lemma algid_subproof U :
{e | e \in U
& has_algid U ==> (U ≤ lker (amull e - 1) :&: lker (amulr e - 1))%VS}.
Definition algid U := s2val (algid_subproof U).
Lemma memv_algid U : algid U \in U.
Lemma algidl A : {in A, left_id (algid A) *%R}.
Lemma algidr A : {in A, right_id (algid A) *%R}.
Lemma unitr_algid1 A u : u \in A → u \is a GRing.unit → algid A = 1.
Lemma algid_eq1 A : (algid A == 1) = (1 \in A).
Lemma algid_neq0 A : algid A != 0.
Lemma dim_algid A : \dim <[algid A]> = 1%N.
Lemma adim_gt0 A : (0 < \dim A)%N.
Lemma not_asubv0 A : ~~ (A ≤ 0)%VS.
Lemma adim1P {A} : reflect (A = <[algid A]>%VS :> {vspace aT}) (\dim A == 1%N).
Lemma asubv A : (A × A ≤ A)%VS.
Lemma memvM A : {in A &, ∀ u v, u × v \in A}.
Lemma prodv_id A : (A × A)%VS = A.
Lemma prodv_sub U V A : (U ≤ A → V ≤ A → U × V ≤ A)%VS.
Lemma expv_id A n : (A ^+ n.+1)%VS = A.
Lemma limg_amulr U v : (amulr v @: U = U × <[v]>)%VS.
Lemma memv_cosetP {U v w} :
reflect (exists2 u, u\in U & w = u × v) (w \in U × <[v]>)%VS.
Lemma dim_cosetv_unit V u : u \is a GRing.unit → \dim (V × <[u]>) = \dim V.
Lemma memvV A u : (u^-1 \in A) = (u \in A).
Fact aspace_cap_subproof A B : algid A \in B → is_aspace (A :&: B).
Definition aspace_cap A B BeA := ASpace (@aspace_cap_subproof A B BeA).
Fact centraliser1_is_aspace u : is_aspace 'C[u].
Canonical centraliser1_aspace u := ASpace (centraliser1_is_aspace u).
Fact centraliser_is_aspace V : is_aspace 'C(V).
Canonical centraliser_aspace V := ASpace (centraliser_is_aspace V).
Lemma centv_algid A : algid A \in 'C(A)%VS.
Canonical center_aspace A := [aspace of 'Z(A) for aspace_cap (centv_algid A)].
Lemma algid_center A : algid 'Z(A) = algid A.
Lemma Falgebra_FieldMixin :
GRing.IntegralDomain.axiom aT → GRing.Field.mixin_of aT.
Section SkewField.
Hypothesis fieldT : GRing.Field.mixin_of aT.
Lemma skew_field_algid1 A : algid A = 1.
Lemma skew_field_module_semisimple A M :
let sumA X := (\sum_(x <- X) A × <[x]>)%VS in
(A × M ≤ M)%VS → {X | [/\ sumA X = M, directv (sumA X) & 0 \notin X]}.
Lemma skew_field_module_dimS A M : (A × M ≤ M)%VS → \dim A %| \dim M.
Lemma skew_field_dimS A B : (A ≤ B)%VS → \dim A %| \dim B.
End SkewField.
End AspaceTheory.
Note that local centraliser might not be proper sub-algebras.
Notation "'C [ u ]" := (centraliser1_aspace u) : aspace_scope.
Notation "'C ( V )" := (centraliser_aspace V) : aspace_scope.
Notation "'Z ( A )" := (center_aspace A) : aspace_scope.
Implicit Arguments adim1P [K aT A].
Implicit Arguments memv_cosetP [K aT U v w].
Section Closure.
Variables (K : fieldType) (aT : FalgType K).
Implicit Types (u v : aT) (U V W : {vspace aT}).
Notation "'C ( V )" := (centraliser_aspace V) : aspace_scope.
Notation "'Z ( A )" := (center_aspace A) : aspace_scope.
Implicit Arguments adim1P [K aT A].
Implicit Arguments memv_cosetP [K aT U v w].
Section Closure.
Variables (K : fieldType) (aT : FalgType K).
Implicit Types (u v : aT) (U V W : {vspace aT}).
Subspaces of an F-algebra form a Kleene algebra
Definition agenv U := (\sum_(i < \dim {:aT}) U ^+ i)%VS.
Lemma agenvEl U : agenv U = (1 + U × agenv U)%VS.
Lemma agenvEr U : agenv U = (1 + agenv U × U)%VS.
Lemma agenv_modl U V : (U × V ≤ V → agenv U × V ≤ V)%VS.
Lemma agenv_modr U V : (V × U ≤ V → V × agenv U ≤ V)%VS.
Fact agenv_is_aspace U : is_aspace (agenv U).
Canonical agenv_aspace U : {aspace aT} := ASpace (agenv_is_aspace U).
Lemma agenvE U : agenv U = agenv_aspace U.
Lemma agenvEl U : agenv U = (1 + U × agenv U)%VS.
Lemma agenvEr U : agenv U = (1 + agenv U × U)%VS.
Lemma agenv_modl U V : (U × V ≤ V → agenv U × V ≤ V)%VS.
Lemma agenv_modr U V : (V × U ≤ V → V × agenv U ≤ V)%VS.
Fact agenv_is_aspace U : is_aspace (agenv U).
Canonical agenv_aspace U : {aspace aT} := ASpace (agenv_is_aspace U).
Lemma agenvE U : agenv U = agenv_aspace U.
Kleene algebra properties
Lemma agenvM U : (agenv U × agenv U)%VS = agenv U.
Lemma agenvX n U : (agenv U ^+ n.+1)%VS = agenv U.
Lemma sub1_agenv U : (1 ≤ agenv U)%VS.
Lemma sub_agenv U : (U ≤ agenv U)%VS.
Lemma subX_agenv U n : (U ^+ n ≤ agenv U)%VS.
Lemma agenv_sub_modl U V : (1 ≤ V → U × V ≤ V → agenv U ≤ V)%VS.
Lemma agenv_sub_modr U V : (1 ≤ V → V × U ≤ V → agenv U ≤ V)%VS.
Lemma agenv_id U : agenv (agenv U) = agenv U.
Lemma agenvS U V : (U ≤ V → agenv U ≤ agenv V)%VS.
Lemma agenv_add_id U V : agenv (agenv U + V) = agenv (U + V).
Lemma subv_adjoin U x : (U ≤ <<U; x>>)%VS.
Lemma subv_adjoin_seq U xs : (U ≤ <<U & xs>>)%VS.
Lemma memv_adjoin U x : x \in <<U; x>>%VS.
Lemma seqv_sub_adjoin U xs : {subset xs ≤ <<U & xs>>%VS}.
Lemma subvP_adjoin U x y : y \in U → y \in <<U; x>>%VS.
Lemma adjoin_nil V : <<V & [::]>>%VS = agenv V.
Lemma adjoin_cons V x rs : <<V & x :: rs>>%VS = << <<V; x>> & rs>>%VS.
Lemma adjoin_rcons V rs x : <<V & rcons rs x>>%VS = << <<V & rs>>%VS; x>>%VS.
Lemma adjoin_seq1 V x : <<V & [:: x]>>%VS = <<V; x>>%VS.
Lemma adjoinC V x y : << <<V; x>>; y>>%VS = << <<V; y>>; x>>%VS.
Lemma adjoinSl U V x : (U ≤ V → <<U; x>> ≤ <<V; x>>)%VS.
Lemma adjoin_seqSl U V rs : (U ≤ V → <<U & rs>> ≤ <<V & rs>>)%VS.
Lemma adjoin_seqSr U rs1 rs2 :
{subset rs1 ≤ rs2} → (<<U & rs1>> ≤ <<U & rs2>>)%VS.
End Closure.
Notation "<< U >>" := (agenv_aspace U) : aspace_scope.
Notation "<< U & vs >>" := (agenv (U + <<vs>>)) : vspace_scope.
Notation "<< U ; x >>" := (agenv (U + <[x]>)) : vspace_scope.
Notation "<< U & vs >>" := << U + <<vs>> >>%AS : aspace_scope.
Notation "<< U ; x >>" := << U + <[x]> >>%AS : aspace_scope.
Section SubFalgType.
The FalgType structure of subvs_of A for A : {aspace aT}.
We can't use the rpred-based mixin, because A need not contain 1.
Variable (K : fieldType) (aT : FalgType K) (A : {aspace aT}).
Definition subvs_one := Subvs (memv_algid A).
Definition subvs_mul (u v : subvs_of A) :=
Subvs (subv_trans (memv_mul (subvsP u) (subvsP v)) (asubv _)).
Fact subvs_mulA : associative subvs_mul.
Fact subvs_mu1l : left_id subvs_one subvs_mul.
Fact subvs_mul1 : right_id subvs_one subvs_mul.
Fact subvs_mulDl : left_distributive subvs_mul +%R.
Fact subvs_mulDr : right_distributive subvs_mul +%R.
Definition subvs_ringMixin :=
RingMixin subvs_mulA subvs_mu1l subvs_mul1 subvs_mulDl subvs_mulDr
(algid_neq0 _).
Canonical subvs_ringType := Eval hnf in RingType (subvs_of A) subvs_ringMixin.
Lemma subvs_scaleAl k (x y : subvs_of A) : k *: (x × y) = (k *: x) × y.
Canonical subvs_lalgType := Eval hnf in LalgType K (subvs_of A) subvs_scaleAl.
Lemma subvs_scaleAr k (x y : subvs_of A) : k *: (x × y) = x × (k *: y).
Canonical subvs_algType := Eval hnf in AlgType K (subvs_of A) subvs_scaleAr.
Canonical subvs_unitRingType := Eval hnf in FalgUnitRingType (subvs_of A).
Canonical subvs_unitAlgType := Eval hnf in [unitAlgType K of subvs_of A].
Canonical subvs_FalgType := Eval hnf in [FalgType K of subvs_of A].
Implicit Type w : subvs_of A.
Lemma vsval_unitr w : vsval w \is a GRing.unit → w \is a GRing.unit.
Lemma vsval_invr w : vsval w \is a GRing.unit → val w^-1 = (val w)^-1.
End SubFalgType.
Section AHom.
Variable K : fieldType.
Section Class_Def.
Variables aT rT : FalgType K.
Definition ahom_in (U : {vspace aT}) (f : 'Hom(aT, rT)) :=
let fM_at x y := f (x × y) == f x × f y in
all (fun x ⇒ all (fM_at x) (vbasis U)) (vbasis U) && (f 1 == 1).
Lemma ahom_inP {f : 'Hom(aT, rT)} {U : {vspace aT}} :
reflect ({in U &, {morph f : x y / x × y >-> x × y}} × (f 1 = 1))
(ahom_in U f).
Lemma ahomP {f : 'Hom(aT, rT)} : reflect (lrmorphism f) (ahom_in {:aT} f).
Structure ahom := AHom {ahval :> 'Hom(aT, rT); _ : ahom_in {:aT} ahval}.
Canonical ahom_subType := Eval hnf in [subType for ahval].
Definition ahom_eqMixin := [eqMixin of ahom by <:].
Canonical ahom_eqType := Eval hnf in EqType ahom ahom_eqMixin.
Definition ahom_choiceMixin := [choiceMixin of ahom by <:].
Canonical ahom_choiceType := Eval hnf in ChoiceType ahom ahom_choiceMixin.
Fact linfun_is_ahom (f : {lrmorphism aT → rT}) : ahom_in {:aT} (linfun f).
Canonical linfun_ahom f := AHom (linfun_is_ahom f).
End Class_Def.
Implicit Arguments ahom_in [aT rT].
Implicit Arguments ahom_inP [aT rT f U].
Implicit Arguments ahomP [aT rT f].
Section LRMorphism.
Variables aT rT sT : FalgType K.
Fact ahom_is_lrmorphism (f : ahom aT rT) : lrmorphism f.
Canonical ahom_rmorphism f := Eval hnf in AddRMorphism (ahom_is_lrmorphism f).
Canonical ahom_lrmorphism f := Eval hnf in AddLRMorphism (ahom_is_lrmorphism f).
Lemma ahomWin (f : ahom aT rT) U : ahom_in U f.
Lemma id_is_ahom (V : {vspace aT}) : ahom_in V \1.
Canonical id_ahom := AHom (id_is_ahom (aspacef aT)).
Lemma comp_is_ahom (V : {vspace aT}) (f : 'Hom(rT, sT)) (g : 'Hom(aT, rT)) :
ahom_in {:rT} f → ahom_in V g → ahom_in V (f \o g).
Canonical comp_ahom (f : ahom rT sT) (g : ahom aT rT) :=
AHom (comp_is_ahom (valP f) (valP g)).
Lemma aimgM (f : ahom aT rT) U V : (f @: (U × V) = f @: U × f @: V)%VS.
Lemma aimg1 (f : ahom aT rT) : (f @: 1 = 1)%VS.
Lemma aimgX (f : ahom aT rT) U n : (f @: (U ^+ n) = f @: U ^+ n)%VS.
Lemma aimg_agen (f : ahom aT rT) U : (f @: agenv U)%VS = agenv (f @: U).
Lemma aimg_adjoin (f : ahom aT rT) U x : (f @: <<U; x>> = <<f @: U; f x>>)%VS.
Lemma aimg_adjoin_seq (f : ahom aT rT) U xs :
(f @: <<U & xs>> = <<f @: U & map f xs>>)%VS.
Fact ker_sub_ahom_is_aspace (f g : ahom aT rT) :
is_aspace (lker (ahval f - ahval g)).
Canonical ker_sub_ahom_aspace f g := ASpace (ker_sub_ahom_is_aspace f g).
End LRMorphism.
Canonical fixedSpace_aspace aT (f : ahom aT aT) := [aspace of fixedSpace f].
End AHom.
Implicit Arguments ahom_in [K aT rT].
Notation "''AHom' ( aT , rT )" := (ahom aT rT) : type_scope.
Notation "''AEnd' ( aT )" := (ahom aT aT) : type_scope.
Delimit Scope lrfun_scope with AF.
Notation "\1" := (@id_ahom _ _) : lrfun_scope.
Notation "f \o g" := (comp_ahom f g) : lrfun_scope.
Definition subvs_one := Subvs (memv_algid A).
Definition subvs_mul (u v : subvs_of A) :=
Subvs (subv_trans (memv_mul (subvsP u) (subvsP v)) (asubv _)).
Fact subvs_mulA : associative subvs_mul.
Fact subvs_mu1l : left_id subvs_one subvs_mul.
Fact subvs_mul1 : right_id subvs_one subvs_mul.
Fact subvs_mulDl : left_distributive subvs_mul +%R.
Fact subvs_mulDr : right_distributive subvs_mul +%R.
Definition subvs_ringMixin :=
RingMixin subvs_mulA subvs_mu1l subvs_mul1 subvs_mulDl subvs_mulDr
(algid_neq0 _).
Canonical subvs_ringType := Eval hnf in RingType (subvs_of A) subvs_ringMixin.
Lemma subvs_scaleAl k (x y : subvs_of A) : k *: (x × y) = (k *: x) × y.
Canonical subvs_lalgType := Eval hnf in LalgType K (subvs_of A) subvs_scaleAl.
Lemma subvs_scaleAr k (x y : subvs_of A) : k *: (x × y) = x × (k *: y).
Canonical subvs_algType := Eval hnf in AlgType K (subvs_of A) subvs_scaleAr.
Canonical subvs_unitRingType := Eval hnf in FalgUnitRingType (subvs_of A).
Canonical subvs_unitAlgType := Eval hnf in [unitAlgType K of subvs_of A].
Canonical subvs_FalgType := Eval hnf in [FalgType K of subvs_of A].
Implicit Type w : subvs_of A.
Lemma vsval_unitr w : vsval w \is a GRing.unit → w \is a GRing.unit.
Lemma vsval_invr w : vsval w \is a GRing.unit → val w^-1 = (val w)^-1.
End SubFalgType.
Section AHom.
Variable K : fieldType.
Section Class_Def.
Variables aT rT : FalgType K.
Definition ahom_in (U : {vspace aT}) (f : 'Hom(aT, rT)) :=
let fM_at x y := f (x × y) == f x × f y in
all (fun x ⇒ all (fM_at x) (vbasis U)) (vbasis U) && (f 1 == 1).
Lemma ahom_inP {f : 'Hom(aT, rT)} {U : {vspace aT}} :
reflect ({in U &, {morph f : x y / x × y >-> x × y}} × (f 1 = 1))
(ahom_in U f).
Lemma ahomP {f : 'Hom(aT, rT)} : reflect (lrmorphism f) (ahom_in {:aT} f).
Structure ahom := AHom {ahval :> 'Hom(aT, rT); _ : ahom_in {:aT} ahval}.
Canonical ahom_subType := Eval hnf in [subType for ahval].
Definition ahom_eqMixin := [eqMixin of ahom by <:].
Canonical ahom_eqType := Eval hnf in EqType ahom ahom_eqMixin.
Definition ahom_choiceMixin := [choiceMixin of ahom by <:].
Canonical ahom_choiceType := Eval hnf in ChoiceType ahom ahom_choiceMixin.
Fact linfun_is_ahom (f : {lrmorphism aT → rT}) : ahom_in {:aT} (linfun f).
Canonical linfun_ahom f := AHom (linfun_is_ahom f).
End Class_Def.
Implicit Arguments ahom_in [aT rT].
Implicit Arguments ahom_inP [aT rT f U].
Implicit Arguments ahomP [aT rT f].
Section LRMorphism.
Variables aT rT sT : FalgType K.
Fact ahom_is_lrmorphism (f : ahom aT rT) : lrmorphism f.
Canonical ahom_rmorphism f := Eval hnf in AddRMorphism (ahom_is_lrmorphism f).
Canonical ahom_lrmorphism f := Eval hnf in AddLRMorphism (ahom_is_lrmorphism f).
Lemma ahomWin (f : ahom aT rT) U : ahom_in U f.
Lemma id_is_ahom (V : {vspace aT}) : ahom_in V \1.
Canonical id_ahom := AHom (id_is_ahom (aspacef aT)).
Lemma comp_is_ahom (V : {vspace aT}) (f : 'Hom(rT, sT)) (g : 'Hom(aT, rT)) :
ahom_in {:rT} f → ahom_in V g → ahom_in V (f \o g).
Canonical comp_ahom (f : ahom rT sT) (g : ahom aT rT) :=
AHom (comp_is_ahom (valP f) (valP g)).
Lemma aimgM (f : ahom aT rT) U V : (f @: (U × V) = f @: U × f @: V)%VS.
Lemma aimg1 (f : ahom aT rT) : (f @: 1 = 1)%VS.
Lemma aimgX (f : ahom aT rT) U n : (f @: (U ^+ n) = f @: U ^+ n)%VS.
Lemma aimg_agen (f : ahom aT rT) U : (f @: agenv U)%VS = agenv (f @: U).
Lemma aimg_adjoin (f : ahom aT rT) U x : (f @: <<U; x>> = <<f @: U; f x>>)%VS.
Lemma aimg_adjoin_seq (f : ahom aT rT) U xs :
(f @: <<U & xs>> = <<f @: U & map f xs>>)%VS.
Fact ker_sub_ahom_is_aspace (f g : ahom aT rT) :
is_aspace (lker (ahval f - ahval g)).
Canonical ker_sub_ahom_aspace f g := ASpace (ker_sub_ahom_is_aspace f g).
End LRMorphism.
Canonical fixedSpace_aspace aT (f : ahom aT aT) := [aspace of fixedSpace f].
End AHom.
Implicit Arguments ahom_in [K aT rT].
Notation "''AHom' ( aT , rT )" := (ahom aT rT) : type_scope.
Notation "''AEnd' ( aT )" := (ahom aT aT) : type_scope.
Delimit Scope lrfun_scope with AF.
Notation "\1" := (@id_ahom _ _) : lrfun_scope.
Notation "f \o g" := (comp_ahom f g) : lrfun_scope.