(Joint Center)Library MathComp.falgebra

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype.
Require Import div tuple finfun bigop ssralg 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.
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
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 AGRing.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)
}.
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; _ : Type}.
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.
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].

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%VSf^-1%VF × f = 1.

Lemma lfun_mulrV f : lker f == 0%VSf × f^-1%VF = 1.

Fact lfun_mulRVr f : lker f == 0%VSlfun_invr f × f = 1.

Fact lfun_mulrRV f : lker f == 0%VSf × 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%VSlfun_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%VSf^-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.unitlker (amull u) == 0%VS.

Lemma lker0_amulr u : u \is a GRing.unitlker (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 U2V1 V2U1 × V1 U2 × V2)%VS.

Lemma prodvSl U1 U2 V : (U1 U2U1 × V U2 × V)%VS.

Lemma prodvSr U V1 V2 : (V1 V2U × 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 VU ^+ 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)%VSu ^+ 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 Uhas_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.

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 Au \is a GRing.unitalgid 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 AV AU × 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 Bis_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 aTGRing.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}).

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 Vagenv U × V V)%VS.

Lemma agenv_modr U V : (V × U VV × 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 VU × V Vagenv U V)%VS.

Lemma agenv_sub_modr U V : (1 VV × U Vagenv U V)%VS.

Lemma agenv_id U : agenv (agenv U) = agenv U.

Lemma agenvS U V : (U Vagenv 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 Uy \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.unitw \is a GRing.unit.

Lemma vsval_invr w : vsval w \is a GRing.unitval 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 xall (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 aTrT}) : 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} fahom_in V gahom_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.