Library mathcomp.field.falgebra

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)).

Finite dimensional algebra

Supply a default unitRing mixin for the default unitAlgType base type.

amull is a converse ring morphism

Centralisers and centers.

Building the predicate that checks is a vspace has a unit

Note that local centraliser might not be proper sub-algebras.

Subspaces of an F-algebra form a Kleene algebra

Kleene algebra properties

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.