Let Lbeanonemptydoubleloopstructure.Notethatthereexistsan
FORMALIZED MATHEMATICS
Volume9,Number3,2001
University of Bia?ystok
The Algebra of Polynomials1
Ewa Gr?dzka
University of Bia?ystok
Summary.In this paper we de?ne the algebra of formal power series and the algebra of polynomials over an arbitrary?eld and prove some properties of
these structures.We also formulate and prove theorems showing some general
properties of sequences.These preliminaries will be used for de?ning and consi-
dering linear functionals on the algebra of polynomials.
MML Identi?er:POLYALG1.
The notation and terminology used here are introduced in the following papers: [9],[13],[1],[2],[3],[12],[8],[7],[11],[16],[5],[14],[10],[15],[6],and[4].
1.Preliminaries
Let F be a1-sorted structure.We introduce algebra structures over F which are extensions of double loop structure and vector space structure over F and are systems
a carrier,an addition,a multiplication,a reverse-map,a zero,a unity,a left multiplication ,
where the carrier is a set,the addition and the multiplication are binary ope-rations on the carrier,the reverse-map is a unary operation on the carrier,the zero and the unity are elements of the carrier,and the left multiplication is a function from[:the carrier of F,the carrier:]into the carrier.
Let L be a non empty double loop structure.Note that there exists an algebra structure over L which is strict and non empty.
Let L be a non empty double loop structure and let A be a non empty algebra structure over L.We say that A is mix-associative if and only if: 1This work has been partially supported by CALCULEMUS grant HPRN-CT-2000-00102.
637c 2001University of Bia?ystok
ISSN1426–2630
638ewa gr?dzka
(Def.1)For every element a of L and for all elements x,y of A holds a·(x·y)= (a·x)·y.
Let L be a non empty double loop structure.Note that there exists a non empty algebra structure over L which is well unital,distributive,vector space-like,and mix-associative.
Let L be a non empty double loop structure.An algebra of L is a well unital distributive vector space-like mix-associative non empty algebra structure over L.
Next we state two propositions:
(1)For all sets X,Y and for every function f from[:X,Y:]into X holds
dom f=[:X,Y:].
(2)For all sets X,Y and for every function f from[:X,Y:]into Y holds
dom f=[:X,Y:].
2.The Algebra of Formal Power Series
Let L be a non empty double loop structure.The functor Formal-Series L yields a strict non empty algebra structure over L and is de?ned by the condi-tions(Def.2).
(Def.2)For every set x holds x∈the carrier of Formal-Series L i?x is a sequence of L and for all elements x,y of the carrier of Formal-Series L and for all
sequences p,q of L such that x=p and y=q holds x+y=p+q and for
all elements x,y of the carrier of Formal-Series L and for all sequences p,
q of L such that x=p and y=q holds x·y=p?q and for every element
x of the carrier of Formal-Series L and for every sequence p of L such that
x=p holds?x=?p and for every element a of L and for every element
x of the carrier of Formal-Series L and for every sequence p of L such that
x=p holds a·x=a·p and0Formal-Series L=0.L and1Formal-Series L=1.L.
Let L be an Abelian non empty double loop structure.Note that Formal-Series L is Abelian.
Let L be an add-associative non empty double loop structure.Note that Formal-Series L is add-associative.
Let L be a right zeroed non empty double loop structure.Note that Formal-Series L is right zeroed.
Let L be an add-associative right zeroed right complementable non empty double loop structure.Note that Formal-Series L is right complementable.
Let L be an Abelian add-associative right zeroed commutative non empty double loop structure.Observe that Formal-Series L is commutative.
the algebra of polynomials639 Let L be an Abelian add-associative right zeroed right complementable unital associative distributive non empty double loop structure.Note that Formal-Series L is associative.
Let L be an add-associative right zeroed right complementable right unital right distributive non empty double loop structure.Note that Formal-Series L
is right unital.
One can verify that there exists a non empty double loop structure which
is add-associative,associative,right zeroed,left zeroed,right unital,left unital, right complementable,and distributive.
We now state three propositions:
(3)For every non empty set D and for every non empty?nite sequence f of
elements of D holds f?1=f?1.
(4)For every non empty set D and for every non empty?nite sequence f of
elements of D holds f= f(1) (f?1).
(5)Let L be an add-associative right zeroed left unital right complementable
left distributive non empty double loop structure and p be a sequence of
L.Then1.L?p=p.
Let L be an add-associative right zeroed right complementable left uni-
tal left distributive non empty double loop structure.One can verify that Formal-Series L is left unital.
Let L be an Abelian add-associative right zeroed right complementable di-stributive non empty double loop structure.One can check that Formal-Series L
is right distributive and Formal-Series L is left distributive.
We now state four propositions:
(6)Let L be an Abelian add-associative right zeroed right complementable
distributive non empty double loop structure,a be an element of L,and
p,q be sequences of L.Then a·(p+q)=a·p+a·q.
(7)Let L be an Abelian add-associative right zeroed right complementable
distributive non empty double loop structure,a,b be elements of L,and
p be a sequence of L.Then(a+b)·p=a·p+b·p.
(8)Let L be an associative non empty double loop structure,a,b be elements
of L,and p be a sequence of L.Then(a·b)·p=a·(b·p).
(9)Let L be an associative left unital non empty double loop structure and
p be a sequence of L.Then(the unity of L)·p=p.
Let L be an Abelian add-associative associative right zeroed right comple-mentable left unital distributive non empty double loop structure.One can check that Formal-Series L is vector space-like.
We now state the proposition
(10)Let L be an Abelian left zeroed add-associative associative right zeroed
right complementable distributive non empty double loop structure,a be
640ewa gr?dzka
an element of L,and p,q be sequences of L.Then a·(p?q)=(a·p)?q.
Let L be an Abelian left zeroed add-associative associative right zeroed right complementable distributive non empty double loop structure.One can verify that Formal-Series L is mix-associative.
Let L be a left zeroed right zeroed add-associative left unital right unital right complementable distributive non empty double loop structure.Observe that Formal-Series L is well unital.
Let L be a1-sorted structure and let A be an algebra structure over L.
An algebra structure over L is said to be a subalgebra of A if it satis?es the conditions(Def.3).
(Def.3)The carrier of it?the carrier of A and1it=1A and0it=0A and the addition of it=(the addition of A)?[:the carrier of it,the carrier of it:]
and the multiplication of it=(the multiplication of A)?[:the carrier of it,
the carrier of it:]and the reverse-map of it=(the reverse-map of A)?(the
carrier of it)and the left multiplication of it=(the left multiplication of
A)?[:the carrier of L,the carrier of it:].
We now state four propositions:
(11)For every1-sorted structure L holds every algebra structure A over L is
a subalgebra of A.
(12)Let L be a1-sorted structure and A,B,C be algebra structures over L.
Suppose A is a subalgebra of B and B is a subalgebra of C.Then A is a
subalgebra of C.
(13)Let L be a1-sorted structure and A,B be algebra structures over L.
Suppose A is a subalgebra of B and B is a subalgebra of A.Then the
algebra structure of A=the algebra structure of B.
(14)Let L be a1-sorted structure and A,B be algebra structures over L.
Suppose the algebra structure of A=the algebra structure of B.Then A
is a subalgebra of B and B is a subalgebra of A.
Let L be a non empty1-sorted structure.Observe that there exists an algebra structure over L which is non empty and strict.
Let L be a1-sorted structure and let B be an algebra structure over L.
Observe that there exists a subalgebra of B which is strict.
Let L be a non empty1-sorted structure and let B be a non empty algebra structure over L.Note that there exists a subalgebra of B which is strict and non empty.
Let L be a non empty groupoid,let B be a non empty algebra structure over L,and let A be a subset of B.We say that A is operations closed if and only if the conditions(Def.4)are satis?ed.
(Def.4)(i)A is linearly closed,
(ii)for all elements x,y of B such that x∈A and y∈A holds x·y∈A,
the algebra of polynomials641 (iii)for every element x of B such that x∈A holds?x∈A,
(iv)1B∈A,and
(v)0B∈A.
The following propositions are true:
(15)Let L be a non empty groupoid,B be a non empty algebra structure
over L,A be a non empty subalgebra of B,x,y be elements of the carrier
of B,and x′,y′be elements of the carrier of A.If x=x′and y=y′,then
x+y=x′+y′.
(16)Let L be a non empty groupoid,B be a non empty algebra structure
over L,A be a non empty subalgebra of B,x,y be elements of the carrier
of B,and x′,y′be elements of the carrier of A.If x=x′and y=y′,then
x·y=x′·y′.
(17)Let L be a non empty groupoid,B be a non empty algebra structure
over L,A be a non empty subalgebra of B,a be an element of the carrier
of L,x be an element of the carrier of B,and x′be an element of the
carrier of A.If x=x′,then a·x=a·x′.
(18)Let L be a non empty groupoid,B be a non empty algebra structure
over L,A be a non empty subalgebra of B,x be an element of the carrier
of B,and x′be an element of the carrier of A.If x=x′,then?x=?x′.
(19)Let L be a non empty groupoid,B be a non empty algebra structure
over L,and A be a non empty subalgebra of B.Then there exists a subset
C of B such that the carrier of A=C and C is operations closed.
(20)Let L be a non empty groupoid,B be a non empty algebra structure
over L,and A be a subset of B.Suppose A is operations closed.Then
there exists a strict subalgebra C of B such that the carrier of C=A.
(21)Let L be a non empty groupoid,B be a non empty algebra structure over
L,A be a non empty subset of B,and X be a family of subsets of the carrier
of B.Suppose that for every set Y holds Y∈X i?Y∈2the carrier of B
and there exists a subalgebra C of B such that Y=the carrier of C and
A?Y.Then X is operations closed.
Let L be a non empty groupoid,let B be a non empty algebra structure over L,and let A be a non empty subset of B.The functor GenAlg A yielding
a strict non empty subalgebra of B is de?ned by the conditions(Def.5). (Def.5)(i)A?the carrier of GenAlg A,and
(ii)for every subalgebra C of B such that A?the carrier of C holds the carrier of GenAlg A?the carrier of C.
We now state the proposition
(22)Let L be a non empty groupoid,B be a non empty algebra structure
over L,and A be a non empty subset of B.If A is operations closed,then
the carrier of GenAlg A=A.
642ewa gr?dzka
3.The Algebra of Polynomials
Let L be an add-associative right zeroed right complementable distributive non empty double loop structure.The functor Polynom-Algebra L yields a strict non empty algebra structure over L and is de?ned as follows:
(Def.6)There exists a non empty subset A of Formal-Series L such that A=the carrier of Polynom-Ring L and Polynom-Algebra L=GenAlg A.
Let L be an add-associative right zeroed right complementable distributive non empty double loop structure.One can verify that Polynom-Ring L is loop-like.
The following propositions are true:
(23)Let L be an add-associative right zeroed right complementable distri-
butive non empty double loop structure and A be a non empty subset of
Formal-Series L.If A=the carrier of Polynom-Ring L,then A is opera-
tions closed.
(24)Let L be an add-associative right zeroed right complementable distribu-
tive non empty double loop structure.Then the double loop structure of
Polynom-Algebra L=Polynom-Ring L.
Acknowledgments
I would like to thank Dr Andrzej Trybulec for his helpful advices on this
paper.
References
[1]Grzegorz Bancerek and Krzysztof Hryniewiecki.Segments of natural numbers and?nite
sequences.Formalized Mathematics,1(1):107–114,1990.
[2]Czes?aw Byliński.Functions and their basic properties.Formalized Mathematics,1(1):55–
65,1990.
[3]Czes?aw Byliński.Functions from a set to a set.Formalized Mathematics,1(1):153–164,
1990.
[4]Czes?aw Byliński.Some basic properties of sets.Formalized Mathematics,1(1):47–53,
1990.
[5]Jaros?aw Kotowicz.Functions and?nite sequences of real numbers.Formalized Mathe-
matics,3(2):275–278,1992.
[6]Eugeniusz Kusak,Wojciech Leończuk,and Micha?Muzalewski.Abelian groups,?elds
and vector spaces.Formalized Mathematics,1(2):335–342,1990.
[7]Robert Milewski.Fundamental theorem of algebra.Formalized Mathematics,9(3):461–
470,2001.
[8]Robert Milewski.The ring of polynomials.Formalized Mathematics,9(2):339–346,2001.
[9]Micha?Muzalewski and Wojciech Skaba.From loops to abelian multiplicative groups
with zero.Formalized Mathematics,1(5):833–840,1990.
[10]Beata Padlewska.Families of sets.Formalized Mathematics,1(1):147–152,1990.
[11]Beata Padlewska and Agata Darmochwa?.Topological spaces and continuous functions.
Formalized Mathematics,1(1):223–230,1990.
[12]Jan Popio?ek.Real normed space.Formalized Mathematics,2(1):111–115,1991.
[13]Wojciech Skaba and Micha?Muzalewski.From double loops to?elds.Formalized Mathe-
matics,2(1):185–191,1991.
the algebra of polynomials643
[14]Wojciech A.Trybulec.Vectors in real linear space.Formalized Mathematics,1(2):291–296,
1990.
[15]Zinaida Trybulec.Properties of subsets.Formalized Mathematics,1(1):67–71,1990.
[16]Edmund Woronowicz.Relations de?ned on sets.Formalized Mathematics,1(1):181–186,
1990.
Received February24,2001