It seems that an algebra is completely characterized by a ring plus a ring
homomorphism, both of which are developed in CoRN. Using ring
homomorphisms solves my problems, so I won't be creating CAlgebras.
On Tue, 23 Sep 2008, [EMAIL PROTECTED] wrote:
I'm planning on making a stub for an CAlgebras structure. I need some very
basic theory of algebras for my work with multi-variable polynomials over
rationals.
An algebra can be considered either a ring that is also an F-module, or an
F-module that is also a ring. Because the product over F can always be
translated into a ring product but not vice versa, I believe that the ring
product is what people will want to work with most of the time. This
suggests making an algbra a ring that happens to be an F-module.
My plan is to define a CAlgebra structure something like:
Record CAlbebra (F:CRing) : Type :=
{ca_crr :> CRing;
ca_eta : CSetoid_uni_fun F ca_crr;
ca_mu := fun (f:F) (x:ca_crr) => (ca_eta f)[*]x
ca_proof: is_RModule F ca_mu}.
(the above doesn't quite type check)
The idea is that an F-algebra is defined as a ring with a function
eta : F -> R, such that it forms an F-module with the scalar operation
fun f x => (eta f) x.
I've never actually studied algebras, so please let me know if you think this
is a poor approach.
Note that this is a commutative algebra because our rings are commutative.
--
Russell O'Connor <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''
_______________________________________________
C-CoRN mailing list
[email protected]
http://mailman.science.ru.nl/mailman/listinfo/c-corn
