- -

Library mathcomp.field.falgebra

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- 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.
- -
-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)
-}.
-Definition base2 A c := @Vector.Class _ _ (@base1 A c) (mixin c).
- -
-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.
-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).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass.
-Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass.
-Definition ringType := @GRing.Ring.Pack cT xclass.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
-Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass.
-Definition algType := @GRing.Algebra.Pack R phR cT xclass.
-Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT xclass.
-Definition vectType := @Vector.Pack R phR cT xclass.
-Definition vect_ringType := @GRing.Ring.Pack vectType xclass.
-Definition vect_unitRingType := @GRing.UnitRing.Pack vectType xclass.
-Definition vect_lalgType := @GRing.Lalgebra.Pack R phR vectType xclass.
-Definition vect_algType := @GRing.Algebra.Pack R phR vectType xclass.
-Definition vect_unitAlgType := @GRing.UnitAlgebra.Pack R phR vectType xclass.
- -
-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.
-