Library mathcomp.field.falgebra

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

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
From mathcomp Require Import choice fintype div tuple finfun bigop ssralg.
From mathcomp Require Import finalg zmodp matrix vector poly.

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.

Declare Scope aspace_scope.
Declare Scope lrfun_scope.

Local Open 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
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)
}.
Local Coercion base1 : class_of >-> GRing.UnitAlgebra.class_of.
Definition base2 A c := @Vector.Class _ _ (@base1 A c) (mixin c).
Local Coercion base2 : class_of >-> Vector.class_of.

Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
Local Coercion sort : type >-> Sortclass.

Variables (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c := cT return class_of cT in c.

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 class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @GRing.Zmodule.Pack cT class.
Definition lmodType := @GRing.Lmodule.Pack R phR cT class.
Definition ringType := @GRing.Ring.Pack cT class.
Definition unitRingType := @GRing.UnitRing.Pack cT class.
Definition lalgType := @GRing.Lalgebra.Pack R phR cT class.
Definition algType := @GRing.Algebra.Pack R phR cT class.
Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT class.
Definition vectType := @Vector.Pack R phR cT class.
Definition vect_ringType := @GRing.Ring.Pack vectType class.
Definition vect_unitRingType := @GRing.UnitRing.Pack vectType class.
Definition vect_lalgType := @GRing.Lalgebra.Pack R phR vectType class.
Definition vect_algType := @GRing.Algebra.Pack R phR vectType class.
Definition vect_unitAlgType := @GRing.UnitAlgebra.Pack R phR vectType class.

End ClassDef.

Module Exports.

Coercion base1 : class_of >-> GRing.UnitAlgebra.class_of.
Coercion base2 : class_of >-> Vector.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
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].
Local Notation "A * B" := (prodv A B) : vspace_scope.

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.
Local Notation "A ^+ n" := (expv A n) : vspace_scope.

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).
Local Notation "'C [ u ]" := (centraliser1_vspace u) : vspace_scope.
Definition centraliser_vspace V := (\bigcap_i 'C[tnth (vbasis V) i])%VS.
Local Notation "'C ( V )" := (centraliser_vspace V) : vspace_scope.
Definition center_vspace V := (V :&: 'C(V))%VS.
Local Notation "'Z ( V )" := (center_vspace V) : vspace_scope.

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.
Local Notation "{ 'aspace' T }" := (aspace_of (Phant T)) : type_scope.

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.
Bind Scope aspace_scope with aspace.
Bind Scope aspace_scope with aspace_of.
Arguments asval {K aT} a%AS.
Arguments clone_aspace [K aT U%VS A%AS algU] _.

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.

Arguments prodvP {K aT U V W}.
Arguments cent1vP {K aT u v}.
Arguments centvP {K aT u V}.
Arguments centvsP {K aT U V}.
Arguments has_algidP {K aT U}.
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.

Arguments adim1P {K aT A}.
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.
Local Notation "<< U & vs >>" := (agenv (U + <<vs>>)) : vspace_scope.
Local Notation "<< U ; x >>" := (agenv (U + <[x]>)) : vspace_scope.

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)) :=
  all2rel (fun x y : aTf (x × y) == f x × f y) (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.

Arguments ahom_in [aT rT].
Arguments ahom_inP {aT rT f U}.
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.

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.
Bind Scope lrfun_scope with ahom.

Notation "\1" := (@id_ahom _ _) : lrfun_scope.
Notation "f \o g" := (comp_ahom f g) : lrfun_scope.