Quotient Vector Spaces and Functionals

Jaroslaw Kotowicz

University of Bialystok

Summary.

The article presents well known facts about quotient vector spaces and functionals (see [8]). There are repeated theorems and constructions with either weaker assumptions or in more general situations (see [11], [7], [10]). The construction of coefficient functionals and non degenerated functional in quotient vector space generated by functional in the given vector space are the only new things which are done.

This work has been partially supported by TRIAL-SOLUTION grant IST-2001-35447 and SPUB-M grant of KBN.

MML Identifier: VECTSP10

Contents (PDF format)

1. Auxiliary Facts about Double Loops and Vector Spaces
2. Quotient Vector Space for Non Commutative Double Loop
3. Auxiliary Facts about Functionals
4. Kernel of Additive Functional. Linear Functionals in Quotient Vector Spaces

Bibliography

[1] Jozef Bialas. Group and field definitions. Journal of Formalized Mathematics, 1, 1989.

[2] Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.

[3] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[4] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[5] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.

[6] Jaroslaw Kotowicz. Monotone real sequences. Subsequences. Journal of Formalized Mathematics, 1, 1989.

[7] Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski. Abelian groups, fields and vector spaces. Journal of Formalized Mathematics, 1, 1989.

[8] Serge Lang. \em Algebra. Addison-Wesley Publishing Co., 1980.

[9] Anna Justyna Milewska. The Hahn Banach theorem in the vector space over the field of complex numbers. Journal of Formalized Mathematics, 12, 2000.

[10] Michal Muzalewski. Domains of submodules, join and meet of finite sequences of submodules and quotient modules. Journal of Formalized Mathematics, 5, 1993.

[11] Bogdan Nowak and Andrzej Trybulec. Hahn-Banach theorem. Journal of Formalized Mathematics, 5, 1993.

[12] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.

[13] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[14] Andrzej Trybulec. Function domains and Fr\aenkel operator. Journal of Formalized Mathematics, 2, 1990.

[15] Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.

[16] Wojciech A. Trybulec. Basis of vector space. Journal of Formalized Mathematics, 2, 1990.

[17] Wojciech A. Trybulec. Linear combinations in real linear space. Journal of Formalized Mathematics, 2, 1990.

[18] Wojciech A. Trybulec. Operations on subspaces in vector space. Journal of Formalized Mathematics, 2, 1990.

[19] Wojciech A. Trybulec. Subspaces and cosets of subspaces in vector space. Journal of Formalized Mathematics, 2, 1990.

[20] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[21] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.