Library mathcomp.field.falgebra
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
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.
Distributed under the terms of CeCILL-B. *)
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 vectType K interfaces
The HB class is called Falgebra.
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
'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
#[short(type="falgType")]
HB.structure Definition Falgebra (R : ringType) :=
{ A of Vector R A & GRing.UnitAlgebra R A }.
#[deprecated(since="mathcomp 2.0.0", note="Use falgType instead.")]
Notation FalgType := falgType.
HB.structure Definition Falgebra (R : ringType) :=
{ A of Vector R A & GRing.UnitAlgebra R A }.
#[deprecated(since="mathcomp 2.0.0", note="Use falgType instead.")]
Notation FalgType := falgType.
Supply a default unitRing mixin for the default unitAlgType base type.
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.
Lemma mulVr : {in uam, left_inverse 1 vam *%R}.
Lemma divrr : {in uam, right_inverse 1 vam *%R}.
Lemma unitrP : ∀ x y, y × x = 1 ∧ x × y = 1 → uam x.
Lemma invr_out : {in [predC uam], vam =1 id}.
Module FalgebraExports.
Bind Scope ring_scope with sort.
#[deprecated(since="mathcomp 2.0.0", note="Use Falgebra.clone instead.")]
Notation "[ 'FalgType' F 'of' L ]" := (Falgebra.clone F L%type _)
(at level 0, format "[ 'FalgType' F 'of' L ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use Falgebra.clone instead.")]
Notation "[ 'FalgType' F 'of' L 'for' L' ]" := (Falgebra.clone F L%type L')
(at level 0, format "[ 'FalgType' F 'of' L 'for' L' ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use Algebra_isFalgebra.Build instead.")]
Notation FalgUnitRingType T := (Algebra_isFalgebra.Build _ T).
End FalgebraExports.
Notation "1" := (vline 1) : vspace_scope.
FIXME: remove once https://github.com/math-comp/hierarchy-builder/issues/197
is fixed
Lemma regular_fullv (K : fieldType) : (fullv = 1 :> {vspace K^o})%VS.
Section Proper.
Variables (R : ringType) (aT : falgType R).
Import VectorInternalTheory.
Lemma FalgType_proper : dim aT > 0.
End Proper.
Module FalgLfun.
Section FalgLfun.
Variable (R : comRingType) (aT : falgType R).
Implicit Types f g : 'End(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.
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.
#[hnf]
HB.instance Definition _ := GRing.isLinear.Build K aT (hom aT aT) _ amull
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_linear : linear amulr.
Lemma amulr_is_multiplicative : multiplicative amulr.
#[hnf]
HB.instance Definition _ := GRing.isLinear.Build K aT (hom aT aT) _ amulr
amulr_is_linear.
#[hnf]
HB.instance Definition _ := GRing.isMultiplicative.Build aT (hom aT aT) amulr
amulr_is_multiplicative.
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.
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.
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.
Lemma prodvA : associative prodv.
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.
Lemma amullM u v : (amull (u × v) = amull v × amull u)%VF.
Lemma amulr_is_linear : linear amulr.
Lemma amulr_is_multiplicative : multiplicative amulr.
#[hnf]
HB.instance Definition _ := GRing.isLinear.Build K aT (hom aT aT) _ amulr
amulr_is_linear.
#[hnf]
HB.instance Definition _ := GRing.isMultiplicative.Build aT (hom aT aT) amulr
amulr_is_multiplicative.
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.
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.
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.
Lemma prodvA : associative prodv.
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.
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.integral_domain_axiom aT → GRing.field_axiom aT.
Section SkewField.
Hypothesis fieldT : GRing.field_axiom 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.
[/\ 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.
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.integral_domain_axiom aT → GRing.field_axiom aT.
Section SkewField.
Hypothesis fieldT : GRing.field_axiom 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}).
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.
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.
Lemma subvs_scaleAl k (x y : subvs_of A) : k *: (x × y) = (k *: x) × y.
Lemma subvs_scaleAr k (x y : subvs_of A) : k *: (x × y) = x × (k *: y).
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 : 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).
Lemma ahomP {f : 'Hom(aT, rT)} : reflect (multiplicative f) (ahom_in {:aT} f).
Structure ahom := AHom {ahval :> 'Hom(aT, rT); _ : ahom_in {:aT} ahval}.
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_multiplicative (f : ahom aT rT) : multiplicative f.
#[hnf]
HB.instance Definition _ (f : ahom aT rT) :=
GRing.isMultiplicative.Build aT rT f (ahom_is_multiplicative 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.
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.
Lemma subvs_scaleAl k (x y : subvs_of A) : k *: (x × y) = (k *: x) × y.
Lemma subvs_scaleAr k (x y : subvs_of A) : k *: (x × y) = x × (k *: y).
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 : 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).
Lemma ahomP {f : 'Hom(aT, rT)} : reflect (multiplicative f) (ahom_in {:aT} f).
Structure ahom := AHom {ahval :> 'Hom(aT, rT); _ : ahom_in {:aT} ahval}.
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_multiplicative (f : ahom aT rT) : multiplicative f.
#[hnf]
HB.instance Definition _ (f : ahom aT rT) :=
GRing.isMultiplicative.Build aT rT f (ahom_is_multiplicative 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.