+ +

Library mathcomp.field.falgebra

+ +

+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ 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.
+Local Open Scope ring_scope.
+ +
+Reserved Notation "{ 'aspace' T }" (at level 0, format "{ 'aspace' T }").
+Reserved Notation "<>" (at level 0, format "<>").
+Reserved Notation "<>" (at level 0, format "<>").
+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 +

+Module Falgebra.
+ +
+

+ +

+ 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.
+ +
+

+ +

+ 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.
+ +
+

+ +

+ 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.
+ +
+ +
+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.
+ +
+ +
+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.
+ +
+

+ +

+ 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 ≤ <>)%VS.
+ +
+Lemma subv_adjoin_seq U xs : (U ≤ <>)%VS.
+ +
+Lemma memv_adjoin U x : x \in <>%VS.
+ +
+Lemma seqv_sub_adjoin U xs : {subset xs ≤ <>%VS}.
+ +
+Lemma subvP_adjoin U x y : y \in U → y \in <>%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 → <> ≤ <<V ; x >>)%VS.
+ +
+Lemma adjoin_seqSl U V rs : (U ≤ V → <> ≤ <<V & rs >>)%VS.
+ +
+Lemma adjoin_seqSr U rs1 rs2 :
+ {subset rs1 ≤ rs2 } → (<> ≤ <>)%VS.
+ +
+End Closure.
+ +
+Notation "<>" := (agenv_aspace U) : aspace_scope.
+Notation "<>" := (agenv (U + <<vs>>)) : vspace_scope.
+Notation "<>" := (agenv (U + <[x]>)) : vspace_scope.
+Notation "<>" := <> >>%AS : aspace_scope.
+Notation "<>" := < >>%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.
+ +
+ +
+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 @: <> = <<f @: U ; f x >>)%VS.
+ +
+Lemma aimg_adjoin_seq (f : ahom aT rT) U xs :
+ (f @: <> = <<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.
+ +
+ +
+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.
+