Module mathcomp.field.falgebra
From HB Require Import structures.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 nzVectType K interfaces
The HB class is called Falgebra.
Any aT with an falgType structure inherits all the Vector, NzRing 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
'AEnd(aT) == algebra endomorphisms of aT (:= 'AHom(aT, aT))
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Declare Scope aspace_scope.
Declare Scope lrfun_scope.
Local Open Scope ring_scope.
Reserved Notation "{ 'aspace' T }" (format "{ 'aspace' T }").
Reserved Notation "<< U & vs >>" (format "<< U & vs >>").
Reserved Notation "<< U ; x >>" (format "<< U ; x >>").
Reserved Notation "''AHom' ( T , rT )" (format "''AHom' ( T , rT )").
Reserved Notation "''AEnd' ( T )" (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.
#[short(type="falgType")]
HB.structure Definition Falgebra (R : nzRingType) :=
{ A of NzVector R A & GRing.UnitAlgebra R A }.
#[deprecated(since="mathcomp 2.0.0", use=falgType)]
Notation FalgType := falgType.
HB.factory Record UnitAlgebra_isFalgebra (R : nzRingType) A
& Vector R A & GRing.UnitAlgebra R A := {}.
HB.builders Context R A & UnitAlgebra_isFalgebra R A.
Import VectorInternalTheory.
Lemma dim_gt0 : dim A > 0.
Proof.
HB.instance Definition _ := SemiVector_isProper.Build R A dim_gt0.
HB.end.
HB.factory Record Algebra_isFalgebra (K : fieldType) A
& Vector K A & GRing.NzAlgebra K A := {}.
HB.builders Context K A & Algebra_isFalgebra K A.
Let vA : Vector.type K := A.
Let am u := linfun (u \o* idfun : vA -> vA).
Let uam := [pred u | lker (am u) == 0%VS].
Let vam := [fun u => if u \in uam then (am u)^-1%VF 1 else u].
Lemma amE u v : am u v = v * u
Proof.
Lemma mulVr : {in uam, left_inverse 1 vam *%R}.
Proof.
Lemma divrr : {in uam, right_inverse 1 vam *%R}.
Lemma unitrP : forall x y, y * x = 1 /\ x * y = 1 -> uam x.
Proof.
Lemma invr_out : {in [predC uam], vam =1 id}.
Proof.
HB.instance Definition _ := GRing.NzRing_hasMulInverse.Build A
mulVr divrr unitrP invr_out.
HB.instance Definition _ := UnitAlgebra_isFalgebra.Build K A.
HB.end.
Module FalgebraExports.
Bind Scope ring_scope with sort.
End FalgebraExports.
HB.export FalgebraExports.
Notation "1" := (vline 1) : vspace_scope.
HB.instance Definition _ (K : fieldType) n :=
Algebra_isFalgebra.Build K 'M[K]_n.+1.
HB.instance Definition _ (R : comUnitRingType) := GRing.UnitAlgebra.on R^o.
Lemma regular_fullv (K : fieldType) : (fullv = 1 :> {vspace K^o})%VS.
#[deprecated(since="mathcomp 2.6.0", use=dim_gt0)]
Lemma FalgType_proper (R : nzRingType) (aT : falgType R) : dim aT > 0.
Proof.
Module FalgLfun.
Section FalgLfun.
Variable (R : comNzRingType) (aT : falgType R).
Implicit Types f g : 'End(aT).
Lemma lfun_mulE f g u : (f * g) u = g (f u)
Proof.
Proof.
by []. Qed.
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.
Proof.
Lemma lfun_mulrV f : lker f == 0%VS -> f * f^-1%VF = 1.
Proof.
Fact lfun_mulRVr f : lker f == 0%VS -> lfun_invr f * f = 1.
Proof.
Fact lfun_mulrRV f : lker f == 0%VS -> f * lfun_invr f = 1.
Proof.
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.
HB.instance Definition _ := GRing.NzRing_hasMulInverse.Build 'End(aT)
lfun_mulRVr lfun_mulrRV lfun_unitrP lfun_invr_out.
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.
Proof.
HB.instance Definition _ := GRing.isSemilinear.Build K aT (hom aT aT) _ amull
(GRing.semilinear_linear amull_is_linear).
Lemma amull1 : amull 1 = \1%VF.
Lemma amullM u v : (amull (u * v) = amull v * amull u)%VF.
Proof.
Lemma amulr_is_linear : linear amulr.
Proof.
Lemma amulr_is_monoid_morphism : monoid_morphism amulr.
Proof.
Definition amulr_is_multiplicative :=
(fun p => (p.2, p.1)) amulr_is_monoid_morphism.
#[hnf]
HB.instance Definition _ := GRing.isSemilinear.Build K aT (hom aT aT) _ amulr
(GRing.semilinear_linear amulr_is_linear).
#[hnf]
HB.instance Definition _ := GRing.isMonoidMorphism.Build aT (hom aT aT) amulr
amulr_is_monoid_morphism.
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.
Proof.
Fact prodv_key : unit
Proof.
by []. Qed.
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, forall u v, u * v \in (U * V)%VS}.
Proof.
Lemma prodvP {U V W} :
reflect {in U & V, forall u v, u * v \in W} (U * V <= W)%VS.
Proof.
apply: (iffP idP) => [sUVW u v Uu Vv | sUVW].
by rewrite (subvP sUVW) ?memv_mul.
rewrite [prodv]unlock; apply/span_subvP=> _ /allpairsP[[u v] /= [Uu Vv ->]].
by rewrite sUVW ?vbasis_mem.
Qed.
by rewrite (subvP sUVW) ?memv_mul.
rewrite [prodv]unlock; apply/span_subvP=> _ /allpairsP[[u v] /= [Uu Vv ->]].
by rewrite sUVW ?vbasis_mem.
Qed.
Lemma prodv_line u v : (<[u]> * <[v]> = <[u * v]>)%VS.
Proof.
Lemma dimv1: \dim (1%VS : {vspace aT}) = 1.
Lemma dim_prodv U V : \dim (U * V) <= \dim U * \dim V.
Proof.
Lemma vspace1_neq0 : (1 != 0 :> {vspace aT})%VS.
Lemma vbasis1 : exists2 k, k != 0 & vbasis 1 = [:: k%:A] :> seq aT.
Proof.
Lemma prod0v : left_zero 0%VS prodv.
Proof.
Lemma prodv0 : right_zero 0%VS prodv.
Proof.
HB.instance Definition _ := Monoid.isMulLaw.Build {vspace aT} 0%VS prodv
prod0v prodv0.
Lemma prod1v : left_id 1%VS prodv.
Proof.
Lemma prodv1 : right_id 1%VS prodv.
Proof.
Lemma prodvS U1 U2 V1 V2 : (U1 <= U2 -> V1 <= V2 -> U1 * V1 <= U2 * V2)%VS.
Proof.
Lemma prodvSl U1 U2 V : (U1 <= U2 -> U1 * V <= U2 * V)%VS.
Proof.
Lemma prodvSr U V1 V2 : (V1 <= V2 -> U * V1 <= U * V2)%VS.
Proof.
Lemma prodvDl : left_distributive prodv addv.
Proof.
Lemma prodvDr : right_distributive prodv addv.
Proof.
HB.instance Definition _ := Monoid.isAddLaw.Build {vspace aT} prodv addv
prodvDl prodvDr.
Lemma prodvA : associative prodv.
Proof.
move=> U V W; rewrite -(span_basis (vbasisP U)) span_def !big_distrl /=.
apply: eq_bigr => u _; rewrite -(span_basis (vbasisP W)) span_def !big_distrr.
apply: eq_bigr => w _; rewrite -(span_basis (vbasisP V)) span_def /=.
rewrite !(big_distrl, big_distrr) /=; apply: eq_bigr => v _.
by rewrite !prodv_line mulrA.
Qed.
apply: eq_bigr => u _; rewrite -(span_basis (vbasisP W)) span_def !big_distrr.
apply: eq_bigr => w _; rewrite -(span_basis (vbasisP V)) span_def /=.
rewrite !(big_distrl, big_distrr) /=; apply: eq_bigr => v _.
by rewrite !prodv_line mulrA.
Qed.
HB.instance Definition _ := Monoid.isLaw.Build {vspace aT} 1%VS prodv
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
Proof.
by []. Qed.
Proof.
by []. Qed.
Proof.
by []. Qed.
Lemma expvSl U n : (U ^+ n.+1 = U * U ^+ n)%VS.
Proof.
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.
Proof.
Lemma expv_line u n : (<[u]> ^+ n = <[u ^+ n]>)%VS.
Proof.
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
Proof.
exact/cent1vP. Qed.
Lemma cent1vC u v : (u \in 'C[v])%VS = (v \in 'C[u])%VS.
Lemma centvP u V : reflect {in V, forall v, u * v = v * u} (u \in 'C(V))%VS.
Proof.
apply: (iffP subv_bigcapP) => [cVu y /coord_vbasis-> | cVu i _].
apply/esym/cent1vP/rpred_sum=> i _; apply: rpredZ.
by rewrite -tnth_nth cent1vC memvE cVu.
exact/cent1vP/cVu/vbasis_mem/mem_tnth.
Qed.
apply/esym/cent1vP/rpred_sum=> i _; apply: rpredZ.
by rewrite -tnth_nth cent1vC memvE cVu.
exact/cent1vP/cVu/vbasis_mem/mem_tnth.
Qed.
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
Proof.
Definition is_algid e U :=
[/\ e \in U, e != 0 & {in U, forall u, e * u = u /\ u * e = u}].
Fact algid_decidable U : decidable (exists e, is_algid e U).
Proof.
have [-> | nzU] := eqVneq U 0%VS.
by right=> [[e []]]; rewrite memv0 => ->.
pose X := vbasis U; pose feq f1 f2 := [tuple of map f1 X ++ map f2 X].
have feqL f i: tnth (feq _ f _) (lshift _ i) = f X`_i.
set v := f _; rewrite (tnth_nth v) /= nth_cat size_map size_tuple.
by rewrite ltn_ord (nth_map 0) ?size_tuple.
have feqR f i: tnth (feq _ _ f) (rshift _ i) = f X`_i.
set v := f _; rewrite (tnth_nth v) /= nth_cat size_map size_tuple.
by rewrite ltnNge leq_addr addKn /= (nth_map 0) ?size_tuple.
apply: decP (vsolve_eq (feq _ amulr amull) (feq _ id id) U) _.
apply: (iffP (vsolve_eqP _ _ _)) => [[e Ue id_e] | [e [Ue _ id_e]]].
suffices idUe: {in U, forall u, e * u = u /\ u * e = u}.
exists e; split=> //; apply: contraNneq nzU => e0; rewrite -subv0.
by apply/subvP=> u /idUe[<- _]; rewrite e0 mul0r mem0v.
move=> u /coord_vbasis->; rewrite mulr_sumr mulr_suml.
split; apply/eq_bigr=> i _; rewrite -(scalerAr, scalerAl); congr (_ *: _).
by have:= id_e (lshift _ i); rewrite !feqL lfunE.
by have:= id_e (rshift _ i); rewrite !feqR lfunE.
have{id_e} /all_and2[ideX idXe]:= id_e _ (vbasis_mem (mem_tnth _ X)).
exists e => // k; rewrite -[k]splitK.
by case: (split k) => i; rewrite !(feqL, feqR) lfunE /= -tnth_nth.
Qed.
by right=> [[e []]]; rewrite memv0 => ->.
pose X := vbasis U; pose feq f1 f2 := [tuple of map f1 X ++ map f2 X].
have feqL f i: tnth (feq _ f _) (lshift _ i) = f X`_i.
set v := f _; rewrite (tnth_nth v) /= nth_cat size_map size_tuple.
by rewrite ltn_ord (nth_map 0) ?size_tuple.
have feqR f i: tnth (feq _ _ f) (rshift _ i) = f X`_i.
set v := f _; rewrite (tnth_nth v) /= nth_cat size_map size_tuple.
by rewrite ltnNge leq_addr addKn /= (nth_map 0) ?size_tuple.
apply: decP (vsolve_eq (feq _ amulr amull) (feq _ id id) U) _.
apply: (iffP (vsolve_eqP _ _ _)) => [[e Ue id_e] | [e [Ue _ id_e]]].
suffices idUe: {in U, forall u, e * u = u /\ u * e = u}.
exists e; split=> //; apply: contraNneq nzU => e0; rewrite -subv0.
by apply/subvP=> u /idUe[<- _]; rewrite e0 mul0r mem0v.
move=> u /coord_vbasis->; rewrite mulr_sumr mulr_suml.
split; apply/eq_bigr=> i _; rewrite -(scalerAr, scalerAl); congr (_ *: _).
by have:= id_e (lshift _ i); rewrite !feqL lfunE.
by have:= id_e (rshift _ i); rewrite !feqR lfunE.
have{id_e} /all_and2[ideX idXe]:= id_e _ (vbasis_mem (mem_tnth _ X)).
exists e => // k; rewrite -[k]splitK.
by case: (split k) => i; rewrite !(feqL, feqR) lfunE /= -tnth_nth.
Qed.
Definition has_algid : pred {vspace aT} := algid_decidable.
Lemma has_algidP {U} : reflect (exists e, is_algid e U) (has_algid U).
Proof.
Lemma has_algid1 U : 1 \in U -> has_algid U.
Proof.
move=> U1; apply/has_algidP; exists 1; split; rewrite ?oner_eq0 // => u _.
by rewrite mulr1 mul1r.
Qed.
by rewrite mulr1 mul1r.
Qed.
Definition is_aspace U := has_algid U && (U * U <= U)%VS.
Structure aspace := ASpace {asval :> {vspace aT}; _ : is_aspace asval}.
HB.instance Definition _ := [isSub for asval].
HB.instance Definition _ := [Choice of aspace by <:].
Definition clone_aspace U (A : aspace) :=
fun algU & phant_id algU (valP A) => @ASpace U algU : aspace.
Fact aspace1_subproof : is_aspace 1.
Proof.
Lemma aspacef_subproof : is_aspace fullv.
Proof.
Lemma polyOver1P p :
reflect (exists q, p = map_poly (in_alg aT) q) (p \is a polyOver 1%VS).
Proof.
End FalgebraTheory.
Delimit Scope aspace_scope with AS.
Bind Scope aspace_scope with aspace.
Arguments asval {K aT} a%_AS.
Arguments aspace [K]%_type aT%_type.
Arguments clone_aspace [K aT U%_VS A%_AS algU] _.
Notation "{ 'aspace' T }" := (aspace 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)
(format "[ 'aspace' 'of' U ]") : form_scope.
Notation "[ 'aspace' 'of' U 'for' A ]" := (@clone_aspace _ _ U A _ idfun)
(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}.
Proof.
Definition algid U := s2val (algid_subproof U).
Lemma memv_algid U : algid U \in U.
Proof.
Lemma algidl A : {in A, left_id (algid A) *%R}.
Proof.
Lemma algidr A : {in A, right_id (algid A) *%R}.
Proof.
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).
Proof.
Lemma algid_neq0 A : algid A != 0.
Proof.
have /andP[/has_algidP[u [Au nz_u _]] _] := valP A.
by apply: contraNneq nz_u => e0; rewrite -(algidr Au) e0 mulr0.
Qed.
by apply: contraNneq nz_u => e0; rewrite -(algidr Au) e0 mulr0.
Qed.
Lemma dim_algid A : \dim <[algid A]> = 1%N.
Proof.
Lemma adim_gt0 A : (0 < \dim A)%N.
Proof.
Lemma not_asubv0 A : ~~ (A <= 0)%VS.
Lemma adim1P {A} : reflect (A = <[algid A]>%VS :> {vspace aT}) (\dim A == 1%N).
Proof.
Lemma asubv A : (A * A <= A)%VS.
Lemma memvM A : {in A &, forall u v, u * v \in A}.
Lemma prodv_id A : (A * A)%VS = A.
Proof.
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.
Proof.
rewrite -(span_basis (vbasisP U)) limg_span !span_def big_distrl /= big_map.
by apply: eq_bigr => u; rewrite prodv_line lfunE.
Qed.
by apply: eq_bigr => u; rewrite prodv_line lfunE.
Qed.
Lemma memv_cosetP {U v w} :
reflect (exists2 u, u\in U & w = u * v) (w \in U * <[v]>)%VS.
Proof.
Lemma dim_cosetv_unit V u : u \is a GRing.unit -> \dim (V * <[u]>) = \dim V.
Proof.
Lemma memvV A u : (u^-1 \in A) = (u \in A).
Proof.
suffices{u} invA: invr_closed A by apply/idP/idP=> /invA; rewrite ?invrK.
move=> u Au; have [Uu | /invr_out-> //] := boolP (u \is a GRing.unit).
rewrite memvE -(limg_ker0 _ _ (lker0_amulr Uu)) limg_line lfunE /= mulVr //.
suff ->: (amulr u @: A)%VS = A by rewrite -memvE -algid_eq1 (unitr_algid1 Au).
by apply/eqP; rewrite limg_amulr -dimv_leqif_eq ?prodv_sub ?dim_cosetv_unit.
Qed.
move=> u Au; have [Uu | /invr_out-> //] := boolP (u \is a GRing.unit).
rewrite memvE -(limg_ker0 _ _ (lker0_amulr Uu)) limg_line lfunE /= mulVr //.
suff ->: (amulr u @: A)%VS = A by rewrite -memvE -algid_eq1 (unitr_algid1 Au).
by apply/eqP; rewrite limg_amulr -dimv_leqif_eq ?prodv_sub ?dim_cosetv_unit.
Qed.
Fact aspace_cap_subproof A B : algid A \in B -> is_aspace (A :&: B).
Proof.
move=> BeA; apply/andP.
split; [apply/has_algidP | by rewrite subv_cap !prodv_sub ?capvSl ?capvSr].
exists (algid A); rewrite /is_algid algid_neq0 memv_cap memv_algid.
by split=> // u /memv_capP[Au _]; rewrite ?algidl ?algidr.
Qed.
split; [apply/has_algidP | by rewrite subv_cap !prodv_sub ?capvSl ?capvSr].
exists (algid A); rewrite /is_algid algid_neq0 memv_cap memv_algid.
by split=> // u /memv_capP[Au _]; rewrite ?algidl ?algidr.
Qed.
Fact centraliser1_is_aspace u : is_aspace 'C[u].
Proof.
Fact centraliser_is_aspace V : is_aspace 'C(V).
Proof.
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.
Proof.
rewrite -(algidl (subvP (centerv_sub A) _ (memv_algid _))) algidr //=.
by rewrite memv_cap memv_algid centv_algid.
Qed.
by rewrite memv_cap memv_algid centv_algid.
Qed.
Lemma Falgebra_FieldMixin :
GRing.integral_domain_axiom aT -> GRing.field_axiom aT.
Proof.
move=> domT u nz_u; apply/unitrP.
have kerMu: lker (amulr u) == 0%VS.
rewrite eqEsubv sub0v andbT; apply/subvP=> v; rewrite memv_ker lfunE /=.
by move/eqP/domT; rewrite (negPf nz_u) orbF memv0.
have /memv_imgP[v _ vu1]: 1 \in limg (amulr u); last rewrite lfunE /= in vu1.
suffices /eqP->: limg (amulr u) == fullv by rewrite memvf.
by rewrite -dimv_leqif_eq ?subvf ?limg_dim_eq // (eqP kerMu) capv0.
exists v; split=> //; apply: (lker0P kerMu).
by rewrite !lfunE /= -mulrA -vu1 mulr1 mul1r.
Qed.
have kerMu: lker (amulr u) == 0%VS.
rewrite eqEsubv sub0v andbT; apply/subvP=> v; rewrite memv_ker lfunE /=.
by move/eqP/domT; rewrite (negPf nz_u) orbF memv0.
have /memv_imgP[v _ vu1]: 1 \in limg (amulr u); last rewrite lfunE /= in vu1.
suffices /eqP->: limg (amulr u) == fullv by rewrite memvf.
by rewrite -dimv_leqif_eq ?subvf ?limg_dim_eq // (eqP kerMu) capv0.
exists v; split=> //; apply: (lker0P kerMu).
by rewrite !lfunE /= -mulrA -vu1 mulr1 mul1r.
Qed.
Section SkewField.
Hypothesis fieldT : GRing.field_axiom aT.
Lemma skew_field_algid1 A : algid A = 1.
Proof.
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]}.
Proof.
move=> sumA sAM_M; pose X := Nil aT; pose k := (\dim (A * M) - \dim (sumA X))%N.
have: (\dim (A * M) - \dim (sumA X) < k.+1)%N by [].
have: [/\ (sumA X <= A * M)%VS, directv (sumA X) & 0 \notin X].
by rewrite /sumA directvE /= !big_nil sub0v dimv0.
elim: {X k}k.+1 (X) => // k IHk X [sAX_AM dxAX nzX]; rewrite ltnS => leAXk.
have [sM_AX | /subvPn/sig2W[y My notAXy]] := boolP (M <= sumA X)%VS.
by exists X; split=> //; apply/eqP; rewrite eqEsubv (subv_trans sAX_AM).
have nz_y: y != 0 by rewrite (memPnC notAXy) ?mem0v.
pose AY := sumA (y :: X).
have sAY_AM: (AY <= A * M)%VS by rewrite [AY]big_cons subv_add ?prodvSr.
have dxAY: directv AY.
rewrite directvE /= !big_cons [_ == _]directv_addE dxAX directvE eqxx /=.
rewrite -/(sumA X) eqEsubv sub0v andbT -limg_amulr.
apply/subvP=> _ /memv_capP[/memv_imgP[a Aa ->]]/[!lfunE]/= AXay.
rewrite memv0 (mulIr_eq0 a (mulIr _)) ?fieldT //.
apply: contraR notAXy => /fieldT-Ua; rewrite -[y](mulKr Ua) /sumA.
by rewrite -big_distrr -(prodv_id A) /= -prodvA big_distrr memv_mul ?memvV.
apply: (IHk (y :: X)); first by rewrite !inE eq_sym negb_or nz_y.
rewrite -subSn ?dimvS // (directvP dxAY) /= big_cons -(directvP dxAX) /=.
rewrite subnDA (leq_trans _ leAXk) ?leq_sub2r // leq_subLR -add1n leq_add2r.
by rewrite dim_cosetv_unit ?fieldT ?adim_gt0.
Qed.
have: (\dim (A * M) - \dim (sumA X) < k.+1)%N by [].
have: [/\ (sumA X <= A * M)%VS, directv (sumA X) & 0 \notin X].
by rewrite /sumA directvE /= !big_nil sub0v dimv0.
elim: {X k}k.+1 (X) => // k IHk X [sAX_AM dxAX nzX]; rewrite ltnS => leAXk.
have [sM_AX | /subvPn/sig2W[y My notAXy]] := boolP (M <= sumA X)%VS.
by exists X; split=> //; apply/eqP; rewrite eqEsubv (subv_trans sAX_AM).
have nz_y: y != 0 by rewrite (memPnC notAXy) ?mem0v.
pose AY := sumA (y :: X).
have sAY_AM: (AY <= A * M)%VS by rewrite [AY]big_cons subv_add ?prodvSr.
have dxAY: directv AY.
rewrite directvE /= !big_cons [_ == _]directv_addE dxAX directvE eqxx /=.
rewrite -/(sumA X) eqEsubv sub0v andbT -limg_amulr.
apply/subvP=> _ /memv_capP[/memv_imgP[a Aa ->]]/[!lfunE]/= AXay.
rewrite memv0 (mulIr_eq0 a (mulIr _)) ?fieldT //.
apply: contraR notAXy => /fieldT-Ua; rewrite -[y](mulKr Ua) /sumA.
by rewrite -big_distrr -(prodv_id A) /= -prodvA big_distrr memv_mul ?memvV.
apply: (IHk (y :: X)); first by rewrite !inE eq_sym negb_or nz_y.
rewrite -subSn ?dimvS // (directvP dxAY) /= big_cons -(directvP dxAX) /=.
rewrite subnDA (leq_trans _ leAXk) ?leq_sub2r // leq_subLR -add1n leq_add2r.
by rewrite dim_cosetv_unit ?fieldT ?adim_gt0.
Qed.
Lemma skew_field_module_dimS A M : (A * M <= M)%VS -> \dim A %| \dim M.
Proof.
case/skew_field_module_semisimple=> X [<- /directvP-> nzX] /=.
rewrite big_seq prime.dvdn_sum // => x /(memPn nzX)nz_x.
by rewrite dim_cosetv_unit ?fieldT.
Qed.
rewrite big_seq prime.dvdn_sum // => x /(memPn nzX)nz_x.
by rewrite dim_cosetv_unit ?fieldT.
Qed.
Lemma skew_field_dimS A B : (A <= B)%VS -> \dim A %| \dim B.
Proof.
End SkewField.
End AspaceTheory.
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}).
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.
Proof.
pose f V := (1 + U * V)%VS; rewrite -/(f _); pose n := \dim {:aT}.
have ->: agenv U = iter n f 0%VS.
rewrite /agenv -/n; elim: n => [|n IHn]; first by rewrite big_ord0.
rewrite big_ord_recl /= -{}IHn; congr (1 + _)%VS; rewrite big_distrr /=.
by apply: eq_bigr => i; rewrite expvSl.
have fS i j: i <= j -> (iter i f 0 <= iter j f 0)%VS.
by elim: i j => [|i IHi] [|j] leij; rewrite ?sub0v //= addvS ?prodvSr ?IHi.
suffices /(@trajectP _ f _ n.+1)[i le_i_n Dfi]: looping f 0%VS n.+1.
by apply/eqP; rewrite eqEsubv -iterS fS // Dfi fS.
apply: contraLR (dimvS (subvf (iter n.+1 f 0%VS))); rewrite -/n -ltnNge.
rewrite -looping_uniq; elim: n.+1 => // i IHi; rewrite trajectSr rcons_uniq.
rewrite {1}trajectSr mem_rcons inE negb_or eq_sym eqEdim fS ?leqW // -ltnNge.
by rewrite -andbA => /and3P[lt_fi _ /IHi/leq_ltn_trans->].
Qed.
have ->: agenv U = iter n f 0%VS.
rewrite /agenv -/n; elim: n => [|n IHn]; first by rewrite big_ord0.
rewrite big_ord_recl /= -{}IHn; congr (1 + _)%VS; rewrite big_distrr /=.
by apply: eq_bigr => i; rewrite expvSl.
have fS i j: i <= j -> (iter i f 0 <= iter j f 0)%VS.
by elim: i j => [|i IHi] [|j] leij; rewrite ?sub0v //= addvS ?prodvSr ?IHi.
suffices /(@trajectP _ f _ n.+1)[i le_i_n Dfi]: looping f 0%VS n.+1.
by apply/eqP; rewrite eqEsubv -iterS fS // Dfi fS.
apply: contraLR (dimvS (subvf (iter n.+1 f 0%VS))); rewrite -/n -ltnNge.
rewrite -looping_uniq; elim: n.+1 => // i IHi; rewrite trajectSr rcons_uniq.
rewrite {1}trajectSr mem_rcons inE negb_or eq_sym eqEdim fS ?leqW // -ltnNge.
by rewrite -andbA => /and3P[lt_fi _ /IHi/leq_ltn_trans->].
Qed.
Lemma agenvEr U : agenv U = (1 + agenv U * U)%VS.
Proof.
rewrite [lhs in lhs = _]agenvEl big_distrr big_distrl /=; congr (_ + _)%VS.
by apply: eq_bigr => i _ /=; rewrite -expvSr -expvSl.
Qed.
by apply: eq_bigr => i _ /=; rewrite -expvSr -expvSl.
Qed.
Lemma agenv_modl U V : (U * V <= V -> agenv U * V <= V)%VS.
Proof.
rewrite big_distrl /= => idlU_V; apply/subv_sumP=> [[i _] /= _].
elim: i => [|i]; first by rewrite expv0 prod1v.
by apply: subv_trans; rewrite expvSr -prodvA prodvSr.
Qed.
elim: i => [|i]; first by rewrite expv0 prod1v.
by apply: subv_trans; rewrite expvSr -prodvA prodvSr.
Qed.
Lemma agenv_modr U V : (V * U <= V -> V * agenv U <= V)%VS.
Proof.
rewrite big_distrr /= => idrU_V; apply/subv_sumP=> [[i _] /= _].
elim: i => [|i]; first by rewrite expv0 prodv1.
by apply: subv_trans; rewrite expvSl prodvA prodvSl.
Qed.
elim: i => [|i]; first by rewrite expv0 prodv1.
by apply: subv_trans; rewrite expvSl prodvA prodvSl.
Qed.
Fact agenv_is_aspace U : is_aspace (agenv U).
Proof.
rewrite /is_aspace has_algid1; first by rewrite memvE agenvEl addvSl.
by rewrite agenv_modl // [V in (_ <= V)%VS]agenvEl addvSr.
Qed.
by rewrite agenv_modl // [V in (_ <= V)%VS]agenvEl addvSr.
Qed.
Lemma agenvE U : agenv U = agenv_aspace U
Proof.
by []. Qed.
Lemma agenvM U : (agenv U * agenv U)%VS = agenv U
Proof.
Proof.
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.
Proof.
Lemma agenv_sub_modl U V : (1 <= V -> U * V <= V -> agenv U <= V)%VS.
Proof.
Lemma agenv_sub_modr U V : (1 <= V -> V * U <= V -> agenv U <= V)%VS.
Proof.
Lemma agenv_id U : agenv (agenv U) = agenv U.
Proof.
Lemma agenvS U V : (U <= V -> agenv U <= agenv V)%VS.
Proof.
move=> sUV; rewrite agenv_sub_modl ?sub1_agenv //.
by rewrite -[Vs in (_ <= Vs)%VS]agenvM prodvSl ?(subv_trans sUV) ?sub_agenv.
Qed.
by rewrite -[Vs in (_ <= Vs)%VS]agenvM prodvSl ?(subv_trans sUV) ?sub_agenv.
Qed.
Lemma agenv_add_id U V : agenv (agenv U + V) = agenv (U + V).
Proof.
Lemma subv_adjoin U x : (U <= <<U; x>>)%VS.
Proof.
Lemma subv_adjoin_seq U xs : (U <= <<U & xs>>)%VS.
Proof.
Lemma memv_adjoin U x : x \in <<U; x>>%VS.
Proof.
Lemma seqv_sub_adjoin U xs : {subset xs <= <<U & xs>>%VS}.
Proof.
Lemma subvP_adjoin U x y : y \in U -> y \in <<U; x>>%VS.
Proof.
Lemma adjoin_nil V : <<V & [::]>>%VS = agenv V.
Lemma adjoin_cons V x rs : <<V & x :: rs>>%VS = << <<V; x>> & rs>>%VS.
Proof.
Lemma adjoin_rcons V rs x : <<V & rcons rs x>>%VS = << <<V & rs>>%VS; x>>%VS.
Proof.
Lemma adjoin_seq1 V x : <<V & [:: x]>>%VS = <<V; x>>%VS.
Proof.
Lemma adjoinC V x y : << <<V; x>>; y>>%VS = << <<V; y>>; x>>%VS.
Proof.
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.
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.
HB.instance Definition _ := GRing.Zmodule_isNzRing.Build (subvs_of A)
subvs_mulA subvs_mu1l subvs_mul1 subvs_mulDl subvs_mulDr (algid_neq0 _).
Lemma subvs_scaleAl k (x y : subvs_of A) : k *: (x * y) = (k *: x) * y.
HB.instance Definition _ :=
GRing.LSemiModule_isLSemiAlgebra.Build K (subvs_of A) subvs_scaleAl.
Lemma subvs_scaleAr k (x y : subvs_of A) : k *: (x * y) = x * (k *: y).
HB.instance Definition _ :=
GRing.LSemiAlgebra_isSemiAlgebra.Build K (subvs_of A) subvs_scaleAr.
HB.instance Definition _ := Algebra_isFalgebra.Build K (subvs_of A).
Implicit Type w : subvs_of A.
Lemma vsval_unitr w : vsval w \is a GRing.unit -> w \is a GRing.unit.
Proof.
Lemma vsval_invr w : vsval w \is a GRing.unit -> val w^-1 = (val w)^-1.
Proof.
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 : aT => f (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).
Proof.
apply: (iffP andP) => [[/allrelP fM /eqP f1] | [fM f1]]; last first.
rewrite f1; split=> //; apply/allrelP => x y Ax Ay.
by rewrite fM // vbasis_mem.
split=> // x y /coord_vbasis -> /coord_vbasis ->.
rewrite !mulr_suml ![f _]linear_sum mulr_suml; apply: eq_bigr => i _ /=.
rewrite !mulr_sumr linear_sum; apply: eq_bigr => j _ /=.
rewrite !linearZ -!scalerAr -!scalerAl 2!linearZ /=; congr (_ *: (_ *: _)).
by apply/eqP/fM; apply: memt_nth.
Qed.
rewrite f1; split=> //; apply/allrelP => x y Ax Ay.
by rewrite fM // vbasis_mem.
split=> // x y /coord_vbasis -> /coord_vbasis ->.
rewrite !mulr_suml ![f _]linear_sum mulr_suml; apply: eq_bigr => i _ /=.
rewrite !mulr_sumr linear_sum; apply: eq_bigr => j _ /=.
rewrite !linearZ -!scalerAr -!scalerAl 2!linearZ /=; congr (_ *: (_ *: _)).
by apply/eqP/fM; apply: memt_nth.
Qed.
Lemma ahomP_tmp {f : 'Hom(aT, rT)} : reflect (monoid_morphism f) (ahom_in {:aT} f).
Proof.
deprecated(since="mathcomp 2.5.0", use=ahomP_tmp)]
Lemma ahomP {f : 'Hom(aT, rT)} : reflect (multiplicative f) (ahom_in {:aT} f).
Structure ahom := AHom {ahval :> 'Hom(aT, rT); _ : ahom_in {:aT} ahval}.
HB.instance Definition _ := [isSub for ahval].
HB.instance Definition _ := [Equality of ahom by <:].
HB.instance Definition _ := [Choice of ahom by <:].
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}.
#[warning="-deprecated-since-mathcomp-2.5.0"]
Arguments ahomP {aT rT f}.
Arguments ahomP_tmp {aT rT f}.
Section LRMorphism.
Variables aT rT sT : falgType K.
Fact ahom_is_monoid_morphism (f : ahom aT rT) : monoid_morphism f.
Proof.
HB.instance Definition _ (f : ahom aT rT) :=
GRing.isMonoidMorphism.Build aT rT f (ahom_is_monoid_morphism f).
#[warning="-deprecated-reference-since-mathcomp-2.5.0",
deprecated(since="mathcomp 2.5.0", use=ahom_is_monoid_morphism)]
Definition ahom_is_multiplicative (f : ahom aT rT) : multiplicative f :=
(fun p => (p.2, p.1)) (ahom_is_monoid_morphism 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).
Proof.
move=> /ahom_inP fM /ahom_inP gM; apply/ahom_inP.
by split=> [x y Vx Vy|] /=; rewrite !comp_lfunE gM // fM ?memvf.
Qed.
by split=> [x y Vx Vy|] /=; rewrite !comp_lfunE gM // fM ?memvf.
Qed.
AHom (comp_is_ahom (valP f) (valP g)).
Lemma aimgM (f : ahom aT rT) U V : (f @: (U * V) = f @: U * f @: V)%VS.
Proof.
apply/eqP; rewrite eqEsubv; apply/andP; split; last first.
apply/prodvP=> _ _ /memv_imgP[u Hu ->] /memv_imgP[v Hv ->].
by rewrite -rmorphM memv_img // memv_mul.
apply/subvP=> _ /memv_imgP[w UVw ->]; rewrite memv_preim (subvP _ w UVw) //.
by apply/prodvP=> u v Uu Vv; rewrite -memv_preim rmorphM memv_mul // memv_img.
Qed.
apply/prodvP=> _ _ /memv_imgP[u Hu ->] /memv_imgP[v Hv ->].
by rewrite -rmorphM memv_img // memv_mul.
apply/subvP=> _ /memv_imgP[w UVw ->]; rewrite memv_preim (subvP _ w UVw) //.
by apply/prodvP=> u v Uu Vv; rewrite -memv_preim rmorphM memv_mul // memv_img.
Qed.
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).
Proof.
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)).
Proof.
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.