diff --git a/IsarMathLib/Field_ZF.thy b/IsarMathLib/Field_ZF.thy index 3c5e57f..826e950 100644 --- a/IsarMathLib/Field_ZF.thy +++ b/IsarMathLib/Field_ZF.thy @@ -65,7 +65,7 @@ locale field0 = ring0 K A M for K A M + assumes not_triv: "\ \ \" - assumes inv_exists: "\a\K. a\\ \ (\b\K. a\b = \)" + assumes inv_exists: "\x\K. x\\ \ (\y\K. x\y = \)" fixes non_zero ("K\<^sub>0") defines non_zero_def[simp]: "K\<^sub>0 \ K-{\}" diff --git a/IsarMathLib/Fol1.thy b/IsarMathLib/Fol1.thy index 6e032eb..dae1cfe 100644 --- a/IsarMathLib/Fol1.thy +++ b/IsarMathLib/Fol1.thy @@ -178,6 +178,12 @@ text\The "exclusive or" is the same as negation of equivalence.\ lemma Fol1_L9: shows "p Xor q \ \(p\q)" using Xor_def by auto +text\Constructions from the same sets are the same. + It is suprising but we do have to use this as a rule in rarte cases.\ + +lemma same_constr: assumes "x=y" shows "P(x) = P(y)" + using assms by simp + text\Equivalence relations are symmetric.\ lemma equiv_is_sym: assumes A1: "equiv(X,r)" and A2: "\x,y\ \ r" diff --git a/IsarMathLib/Group_ZF_2.thy b/IsarMathLib/Group_ZF_2.thy index 929db6a..8f2c434 100644 --- a/IsarMathLib/Group_ZF_2.thy +++ b/IsarMathLib/Group_ZF_2.thy @@ -229,6 +229,13 @@ proof - by simp qed +text\The propositions proven in the \group0\ context are valid in the same context + when applied to the function space with the lifted group operation.\ + +lemma (in group0) group0_valid_fun_space: + shows "group0(X\G,P {lifted to function space over} X)" + using Group_ZF_2_1_T2 unfolding group0_def by simp + text\What is the group inverse for the lifted group?\ lemma (in group0) Group_ZF_2_1_L6: @@ -276,6 +283,21 @@ proof - ultimately show ?thesis by simp qed +text\The neutral element of a subgroup of the lifted group is the constant + function with value equal to the neutral element of the group. \ + +lemma (in group0) lift_group_subgr_neut: + assumes "F = P {lifted to function space over} X" and "IsAsubgroup(H,F)" + shows "TheNeutralElement(H,restrict(F,H\H)) = ConstantFunction(X,\)" +proof - + from assms have + "TheNeutralElement(H,restrict(F,H\H)) = TheNeutralElement(X\G,F)" + using group0_valid_fun_space group0.group0_3_L4 by blast + also from groupAssum assms(1) have "... = ConstantFunction(X,\)" + using Group_ZF_2_1_L2 unfolding IsAgroup_def by simp + finally show ?thesis by simp +qed + text\If a group is abelian, then its lift to a function space is also abelian.\ diff --git a/IsarMathLib/Group_ZF_5.thy b/IsarMathLib/Group_ZF_5.thy index 9aa9c5f..216bb63 100644 --- a/IsarMathLib/Group_ZF_5.thy +++ b/IsarMathLib/Group_ZF_5.thy @@ -112,7 +112,7 @@ text\Endomoprhisms of a group form a monoid with composition as the binary theorem (in group0) end_comp_monoid: shows "IsAmonoid(End(G,P),InEnd(Composition(G),G,P))" - and "TheNeutralElement(End(G,P),InEnd(Composition(G),G,P))=id(G)" + and "TheNeutralElement(End(G,P),InEnd(Composition(G),G,P)) = id(G)" proof - let ?C\<^sub>0 = "InEnd(Composition(G),G,P)" have fun: "id(G):G\G" unfolding id_def by auto @@ -153,6 +153,14 @@ proof- } with fun2 show ?thesis using eq_endomor by simp qed +text\The value of a product of endomorphisms on a group element is the product of values.\ + +lemma (in abelian_group) end_pointwise_add_val: + assumes "f\End(G,P)" "g\End(G,P)" "x\G" "F = P {lifted to function space over} G" + shows "(InEnd(F,G,P)`\f,g\)`(x) = (f`(x))\(g`(x))" + using assms group_oper_fun monoid.group0_1_L3B func_ZF_1_L4 + unfolding End_def by simp + text\The inverse of an abelian group is an endomorphism.\ lemma (in abelian_group) end_inverse_group: @@ -162,7 +170,7 @@ lemma (in abelian_group) end_inverse_group: unfolding End_def IsMorphism_def by simp text\The set of homomorphisms of an abelian group is an abelian subgroup of - the group of functions from a set to a group, under pointwise multiplication.\ + the group of functions from a set to a group, under pointwise addition.\ theorem (in abelian_group) end_addition_group: assumes "F = P {lifted to function space over} G" @@ -172,7 +180,7 @@ proof- have "End(G,P)\0" using end_comp_monoid(1) monoid0.group0_1_L3A unfolding monoid0_def by auto moreover have "End(G,P) \ G\G" unfolding End_def by auto - moreover from isAbelian assms(1) have "End(G,P){is closed under}F" + moreover from isAbelian assms(1) have "End(G,P){is closed under} F" unfolding IsOpClosed_def using end_pointwise_addition by auto moreover from groupAssum assms(1) have "\f\End(G,P). GroupInv(G\G,F)`(f) \ End(G,P)" @@ -187,6 +195,20 @@ proof- using Group_ZF_2_1_L7 unfolding End_def IsCommutative_def by auto qed +text\Endomorphisms form a subgroup of the space of functions that map the group to itself.\ + +lemma (in abelian_group) end_addition_subgroup: + shows "IsAsubgroup(End(G,P),P {lifted to function space over} G)" + using end_addition_group unfolding IsAsubgroup_def by simp + +text\The neutral element of the group of endomorphisms of a group is the constant function + with value equal to the neutral element of the group.\ + +lemma (in abelian_group) end_add_neut_elem: + assumes "F = P {lifted to function space over} G" + shows "TheNeutralElement(End(G,P),InEnd(F,G,P)) = ConstantFunction(G,\)" + using assms end_addition_subgroup lift_group_subgr_neut by simp + text\For the endomorphisms of a group $G$ the group operation lifted to the function space over $G$ is distributive with respect to the composition operation. \ diff --git a/IsarMathLib/Module_ZF.thy b/IsarMathLib/Module_ZF.thy new file mode 100755 index 0000000..5fb50c8 --- /dev/null +++ b/IsarMathLib/Module_ZF.thy @@ -0,0 +1,270 @@ +(* + This file is a part of IsarMathLib - + a library of formalized mathematics written for Isabelle/Isar. + + Copyright (C) 2024 Slawomir Kolodynski + + This program is free software; Redistribution and use in source and binary forms, + with or without modification, are permitted provided that the following conditions are met: + + 1. Redistributions of source code must retain the above copyright notice, + this list of conditions and the following disclaimer. + 2. Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation and/or + other materials provided with the distribution. + 3. The name of the author may not be used to endorse or promote products + derived from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, +INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A +PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, +INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE, DATA, OR PROFITS OR +BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, +STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE +USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +*) + +section \ Modules\ + +theory Module_ZF imports Ring_ZF_3 Field_ZF + +begin + +text\A module is a generalization of the concept of a vector space in which scalars + do not form a field but a ring. \ + +subsection\Definition and basic properties of modules\ + +text\Let $R$ be a ring and $M$ be an abelian group. The most common definition + of a left $R$-module states posits the existence of a scalar multiplication operation + $R\times M\rightarrow M$ satisfying certain four properties. + Here we take a bit more concise and abstract approach defining a module as a ring action + on an abelian group. \ + +text\We know that endomorphisms of an abelian group $\cal{M}$ form a ring with pointwise addition + as the additive operation and composition as the ring multiplication. + This asssertion is a bit imprecise though as the domain of pointwise addition + is a binary operation on the space of functions $\cal{M}\rightarrow \cal{M}$ + (i.e. its domain is $(\cal{M}\rightarrow \cal{M})\times \cal{M}\rightarrow \cal{M}$) + while we need the space of endomorphisms to be the + domain of the ring addition and multiplication. Therefore, to get the actual additive operation + we need to restrict the pointwise addition of functions $\cal{M}\rightarrow \cal{M}$ + to the set of endomorphisms of $\cal{M}$. + Recall from the \Group_ZF_5\ that the \InEnd\ operator restricts an operation to + the set of endomorphisms and see the \func_ZF\ theory for definitions + of lifting an operation on a set to a function space over that set. \ + +definition "EndAdd(\,A) \ InEnd(A {lifted to function space over} \,\,A)" + +text\Similarly we define the multiplication in the ring of endomorphisms + as the restriction of compositions to the endomorphisms of $\cal{M}$. + See the \func_ZF\ theory for the definition of the \Composition\ operator. \ + +definition "EndMult(\,A) \ InEnd(Composition(\),\,A)" + +text\We can now reformulate the theorem \end_is_ring\ from the \Group_ZF_5\ theory + in terms of the addition and multiplication of endomorphisms defined above. \ + +lemma (in abelian_group) end_is_ring1: + shows "IsAring(End(G,P),EndAdd(G,P),EndMult(G,P))" + using end_is_ring unfolding EndAdd_def EndMult_def by simp + +text\We define an \action\ as a homomorphism into a space of endomorphisms (typically of some + abelian group). In the definition below $S$ is the set of scalars, $A$ is the addition operation + on this set, $M$ is multiplication on the set, $V$ is the set of vectors, $A_V$ is the + operation of vector addition, and $H$ is the homomorphism that defines the vector space. + On the right hand side of the definition \End(V,A\<^sub>V)\ is the set of endomorphisms, + This definition is only ever used as part of the definition of a module and vector space, + it's just convenient to split it off to shorten the main definitions. \ + +definition + "IsAction(S,A,M,\,A\<^sub>M,H) \ ringHomomor(H,S,A,M,End(\,A\<^sub>M),EndAdd(\,A\<^sub>M),EndMult(\,A\<^sub>M))" + +text\A module is a ring action on an abelian group.\ + +definition "IsLeftModule(S,A,M,\,A\<^sub>M,H) \ + IsAring(S,A,M) \ IsAgroup(\,A\<^sub>M) \ (A\<^sub>M {is commutative on} \) \ IsAction(S,A,M,\,A\<^sub>M,H)" + + +text\The next locale defines context (i.e. common assumptions and notation) when considering + modules. We reuse notation from the \ring0\ locale and add notation specific to + modules. The addition and multiplication in the ring of scalars is denoted $+$ and $\cdot$, + resp. The addition of module elements will be denoted $+_V$. + The multiplication (scaling) of scalars by module elemenst will be denoted $\cdot_S$. + $\Theta$ is the zero module element, i.e. the neutral element of the abelian group + of the module elements. \ + +locale module0 = ring0 + + + fixes \ A\<^sub>M H + + assumes mAbGr: "IsAgroup(\,A\<^sub>M) \ (A\<^sub>M {is commutative on} \)" + + assumes mAction: "IsAction(R,A,M,\,A\<^sub>M,H)" + + fixes zero_vec ("\") + defines zero_vec_def [simp]: "\ \ TheNeutralElement(\,A\<^sub>M)" + + fixes vAdd (infixl "+\<^sub>V" 80) + defines vAdd_def [simp]: "v\<^sub>1 +\<^sub>V v\<^sub>2 \ A\<^sub>M`\v\<^sub>1,v\<^sub>2\" + + fixes scal (infix "\\<^sub>S" 90) + defines scal_def [simp]: "s \\<^sub>S v \ (H`(s))`(v)" + + fixes negV ("\_") + defines negV_def [simp]: "\v \ GroupInv(\,A\<^sub>M)`(v)" + + fixes vSub (infix "-\<^sub>V" 80) + defines vSub_def [simp]: "v\<^sub>1 -\<^sub>V v\<^sub>2 \ v\<^sub>1 +\<^sub>V (\v\<^sub>2)" + +text\We indeed talk about modules in the \module0\ context.\ + +lemma (in module0) module_in_module0: shows "IsLeftModule(R,A,M,\,A\<^sub>M,H)" + using ringAssum mAbGr mAction unfolding IsLeftModule_def by simp + +text\Theorems proven in the \abelian_group\ context are valid as applied to the \module0\ + context as applied to the abelian group of "vectors". \ + +lemma (in module0) abelian_group_valid_module0: + shows "abelian_group(\,A\<^sub>M)" + using mAbGr group0_def abelian_group_def abelian_group_axioms_def + by simp + +text\Another way to state that theorems proven in the \abelian_group\ context + can be used in the \module0\ context: \ + +sublocale module0 < mod_ab_gr: abelian_group \ A\<^sub>M "\" vAdd negV + using abelian_group_valid_module0 by auto + +text\Theorems proven in the \ring_homo\ context are valid in the \module0\ context, as + applied to ring $R$ and the ring of endomorphisms of the vector group. \ + +lemma (in module0) ring_homo_valid_module0: + shows "ring_homo(R,A,M,End(\,A\<^sub>M),EndAdd(\,A\<^sub>M),EndMult(\,A\<^sub>M),H)" + using ringAssum mAction abelian_group_valid_module0 abelian_group.end_is_ring1 + unfolding IsAction_def ring_homo_def by simp + +text\Another way to make theorems proven in the \ring_homo\ context available in the + \module0\ context: \ + +sublocale module0 < vec_act_homo: ring_homo R A M + "End(\,A\<^sub>M)" "EndAdd(\,A\<^sub>M)" "EndMult(\,A\<^sub>M)" H + ringa + ringminus + ringsub + ringm + ringzero + ringone + ringtwo + ringsq + "\x y. EndAdd(\,A\<^sub>M) ` \x, y\" + "\x. GroupInv(End(\,A\<^sub>M), EndAdd(\, A\<^sub>M))`(x)" + "\x y. EndAdd(\,A\<^sub>M)`\x,GroupInv(End(\, A\<^sub>M), EndAdd(\, A\<^sub>M))`(y)\" + "\x y. EndMult(\,A\<^sub>M)`\x, y\" + "TheNeutralElement(End(\, A\<^sub>M), EndAdd(\, A\<^sub>M))" + "TheNeutralElement(End(\, A\<^sub>M), EndMult(\, A\<^sub>M))" + "EndAdd(\,A\<^sub>M)`\TheNeutralElement(End(\, A\<^sub>M),EndMult(\, A\<^sub>M)),TheNeutralElement(End(\, A\<^sub>M), EndMult(\,A\<^sub>M))\" + "\x. EndMult(\,A\<^sub>M)`\x, x\" + using ring_homo_valid_module0 by auto + +text\In the ring of endomorphisms of the module the neutral element of the additive operation + is the zero valued constant function. The neutral element of the multiplicative operation is + the identity function.\ + +lemma (in module0) add_mult_neut_elems: shows + "TheNeutralElement(End(\, A\<^sub>M), EndMult(\,A\<^sub>M)) = id(\)" and + "TheNeutralElement(End(\,A\<^sub>M),EndAdd(\,A\<^sub>M)) = ConstantFunction(\,\)" +proof - + show "TheNeutralElement(End(\, A\<^sub>M), EndMult(\, A\<^sub>M)) = id(\)" + using mod_ab_gr.end_comp_monoid(2) unfolding EndMult_def + by blast + show "TheNeutralElement(End(\, A\<^sub>M), EndAdd(\, A\<^sub>M)) = ConstantFunction(\,\)" + using mod_ab_gr.end_add_neut_elem unfolding EndAdd_def by blast +qed + +text\The value of the homomorphism defining the module is an endomorphism + of the vector space group and hence a function that maps the vector space into itself.\ + +lemma (in module0) H_val_type: assumes "r\R" shows + "H`(r) \ End(\,A\<^sub>M)" and "H`(r):\\\" + using mAction assms apply_funtype unfolding IsAction_def ringHomomor_def End_def + by auto + +text\ In the \module0\ context the neutral element of addition of module elements + is denoted $\Theta$. Of course $\Theta$ is an element of the module. \ + +lemma (in module0) zero_in_mod: shows "\ \ \" + using mod_ab_gr.group0_2_L2 by simp + +text\ $\Theta$ is indeed the neutral element of addition of module elements.\ + +lemma (in module0) zero_neutral: assumes "x\\" + shows "x +\<^sub>V \ = x" and "\ +\<^sub>V x = x" + using assms mod_ab_gr.group0_2_L2 by simp_all + +subsection\Module axioms\ + +text\A more common definition of a module assumes that $R$ is a ring, $V$ + is an abelian group and lists a couple of properties that the multiplications of scalars + (elements of $R$) by the elements of the module $V$ should have. + In this section we show that the definition of a module as a ring action + on an abelian group $V$ implies these properties. \ + +text\The scalar multiplication is distributive with respect to the module addition.\ + +lemma (in module0) module_ax1: assumes "r\R" "x\\" "y\\" + shows "r\\<^sub>S(x+\<^sub>Vy) = r\\<^sub>Sx +\<^sub>V r\\<^sub>Sy" + using assms H_val_type(1) mod_ab_gr.endomor_eq by simp + +text\The scalar addition is distributive with respect to scalar multiplication.\ + +lemma (in module0) module_ax2: assumes "r\R" "s\R" "x\\" + shows "(r\s)\\<^sub>Sx = r\\<^sub>Sx +\<^sub>V s\\<^sub>Sx" + using assms vec_act_homo.homomor_dest_add H_val_type(1) mod_ab_gr.end_pointwise_add_val + unfolding EndAdd_def by simp + +text\Multiplication by scalars is associative with multiplication of scalars.\ + +lemma (in module0) module_ax3: assumes "r\R" "s\R" "x\\" + shows "(r\s)\\<^sub>Sx = r\\<^sub>S(s\\<^sub>Sx)" +proof - + let ?e = "EndMult(\,A\<^sub>M)`\H`(r),H`(s)\" + have "(r\s)\\<^sub>Sx = (H`(r\s))`(x)" by simp + also have "(H`(r\s))`(x) = ?e`(x)" + proof - + from mAction assms(1,2) have "H`(r\s) = ?e" + using vec_act_homo.homomor_dest_mult unfolding IsAction_def + by blast + then show ?thesis by (rule same_constr) + qed + also have "?e`(x) = r\\<^sub>S(s\\<^sub>Sx)" + proof - + from assms(1,2) have "?e`(x) = (Composition(\)`\H`(r),H`(s)\)`(x)" + using H_val_type(1) unfolding EndMult_def by simp + also from assms have "... = r\\<^sub>S(s\\<^sub>Sx)" using H_val_type(2) func_ZF_5_L3 + by simp + finally show "?e`(x) = r\\<^sub>S(s\\<^sub>Sx)" by blast + qed + finally show ?thesis by simp +qed + +text\Scaling a module element by one gives the same module element.\ + +lemma (in module0) module_ax4: assumes "x\\" shows "\\\<^sub>Sx = x" +proof - + let ?n = "TheNeutralElement(End(\,A\<^sub>M),EndMult(\,A\<^sub>M))" + from mAction have "H`(TheNeutralElement(R,M)) = ?n" + unfolding IsAction_def ringHomomor_def by blast + moreover have "TheNeutralElement(R,M) = \" by simp + ultimately have "H`(\) = ?n" by blast + also have "?n = id(\)" by (rule add_mult_neut_elems) + finally have "H`(\) = id(\)" by simp + with assms show "\\\<^sub>Sx = x" by simp +qed + +end + + + diff --git a/IsarMathLib/ROOT b/IsarMathLib/ROOT index 865712b..1d9521d 100644 --- a/IsarMathLib/ROOT +++ b/IsarMathLib/ROOT @@ -49,6 +49,8 @@ session "IsarMathLib" = "ZF" + Ring_ZF_2 Ring_ZF_3 Field_ZF + Module_ZF + VectorSpace_ZF OrderedField_ZF Int_ZF_IML Int_ZF_1 diff --git a/IsarMathLib/Ring_ZF.thy b/IsarMathLib/Ring_ZF.thy index cee4333..24def0e 100644 --- a/IsarMathLib/Ring_ZF.thy +++ b/IsarMathLib/Ring_ZF.thy @@ -75,16 +75,16 @@ locale ring0 = assumes ringAssum: "IsAring(R,A,M)" fixes ringa (infixl "\" 90) - defines ringa_def [simp]: "a\b \ A`\ a,b\" + defines ringa_def [simp]: "x\y \ A`\x,y\" fixes ringminus ("\ _" 89) - defines ringminus_def [simp]: "(\a) \ GroupInv(R,A)`(a)" + defines ringminus_def [simp]: "(\x) \ GroupInv(R,A)`(x)" fixes ringsub (infixl "\" 90) - defines ringsub_def [simp]: "a\b \ a\(\b)" + defines ringsub_def [simp]: "x\y \ x\(\y)" fixes ringm (infixl "\" 95) - defines ringm_def [simp]: "a\b \ M`\ a,b\" + defines ringm_def [simp]: "x\y \ M`\x,y\" fixes ringzero ("\") defines ringzero_def [simp]: "\ \ TheNeutralElement(R,A)" @@ -96,7 +96,7 @@ locale ring0 = defines ringtwo_def [simp]: "\ \ \\\" fixes ringsq ("_\<^sup>2" [96] 97) - defines ringsq_def [simp]: "a\<^sup>2 \ a\a" + defines ringsq_def [simp]: "x\<^sup>2 \ x\x" text\In the \ring0\ context we can use theorems proven in some other contexts.\ diff --git a/IsarMathLib/Ring_ZF_3.thy b/IsarMathLib/Ring_ZF_3.thy index 6659fc8..e457d66 100644 --- a/IsarMathLib/Ring_ZF_3.thy +++ b/IsarMathLib/Ring_ZF_3.thy @@ -64,16 +64,16 @@ locale ring_homo = and homomorphism: "ringHomomor(f,R,A,M,S,U,V)" fixes ringa (infixl "\\<^sub>R" 90) - defines ringa_def [simp]: "x\\<^sub>Rb \ A`\x,b\" + defines ringa_def [simp]: "x\\<^sub>Ry \ A`\x,y\" fixes ringminus ("\\<^sub>R _" 89) defines ringminus_def [simp]: "(\\<^sub>Rx) \ GroupInv(R,A)`(x)" fixes ringsub (infixl "\\<^sub>R" 90) - defines ringsub_def [simp]: "x\\<^sub>Rb \ x\\<^sub>R(\\<^sub>Rb)" + defines ringsub_def [simp]: "x\\<^sub>Ry \ x\\<^sub>R(\\<^sub>Ry)" fixes ringm (infixl "\\<^sub>R" 95) - defines ringm_def [simp]: "x\\<^sub>Rb \ M`\x,b\" + defines ringm_def [simp]: "x\\<^sub>Ry \ M`\x,y\" fixes ringzero ("\\<^sub>R") defines ringzero_def [simp]: "\\<^sub>R \ TheNeutralElement(R,A)" diff --git a/IsarMathLib/VectorSpace_ZF.thy b/IsarMathLib/VectorSpace_ZF.thy old mode 100644 new mode 100755 index b2b5276..ddd807b --- a/IsarMathLib/VectorSpace_ZF.thy +++ b/IsarMathLib/VectorSpace_ZF.thy @@ -26,9 +26,9 @@ USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) -section \ Modules and vector spaces \ +section \Vector spaces\ -theory VectorSpace_ZF imports Ring_ZF_3 Field_ZF +theory VectorSpace_ZF imports Module_ZF begin @@ -40,7 +40,7 @@ text\ Vector spaces have a long history of applications in mathematics and This theory has nothing to do with LLM's however - it just defines vector space as a mathematical structure as it has been understood from at least the beginning of the XXth century. \ -subsection\Definition and basic properties of modules and vector spaces\ +subsection\Definition and basic properties of vector spaces\ text\ The canonical example of a vector space is $\mathbb{R}^2$ - the set of $n$-tuples of real numbers. We can add them adding respective coordinates and scale them by @@ -50,88 +50,120 @@ text\ The canonical example of a vector space is $\mathbb{R}^2$ - the set properties $x(v_1 + v_2) = s v_1 + s v_2$ and $(s_1+s_2)v =s_1 v + s_2 v$ are satisfied for any scalars $s,s_1,s_2$ and vectors $v,v_1,v_2$. \ -text\we know that endomorphisms of an abelian group $G$ form a ring with pointwise addition - as the additive operation and composition as the ring multiplication. This asssertion is a bit - imprecise though as the domain of pointwise addition is a binary operation on - the space of functions $G\rightarrow G$ (i.e. its domain is - $(G\rightarrow G)\times G\rightarrow G$) while we need the space of endomorphisms to be the - domain of the ring addition and multiplication. Therefore, to get the actual additive operation - we need to restrict the pointwise addition of functions $G\rightarrow G$ - to the set of endomorphisms of G$G$. - Recall from the \Group_ZF_5\ that the \InEnd\ operator restricts an operation to - the set of endomorphisms and see the \func_ZF\ theory for definitions - of lifting an operation on a set to a function space over that set. \ -definition "EndAdd(G,P) \ InEnd(P {lifted to function space over} G,G,P)" +text\A vector space is a field action on an abelian group. \ -text\Similarly we define the multiplication in the ring of endomorphisms - as the restriction of compositions to the endomorphisms of $G$. - See the \func_ZF\ theory for the definition of the \Composition\ operator. \ +definition "IsVectorSpace(S,A,M,V,A\<^sub>V,H) \ + IsAfield(S,A,M) \ IsAgroup(V,A\<^sub>V) \ (A\<^sub>V {is commutative on} V) \ IsAction(S,A,M,V,A\<^sub>V,H)" -definition "EndMult(G,P) \ InEnd(Composition(G),G,P)" +text\The next locale defines context (i.e. common assumptions and notation) when considering + vector spaces. We reuse notation from the \field0\ locale adding more similarly to the + \module0\ locale. \ -text\We can now reformulate the theorem \end_is_ring\ from the \Group_ZF_5\ theory - in terms of the addition and multiplication of endomorphisms defined above. \ +locale vector_space0 = field0 + + fixes V A\<^sub>V H -lemma (in abelian_group) end_is_ring1: - shows "IsAring(End(G,P),EndAdd(G,P),EndMult(G,P))" - using end_is_ring unfolding EndAdd_def EndMult_def by simp + assumes mAbGr: "IsAgroup(V,A\<^sub>V) \ (A\<^sub>V {is commutative on} V)" -text\We define an \action\ as a homomorphism into a space of endomorphisms (typically of some - abelian group). In the definition below $S$ is the set of scalars, $A$ is the addition operation - on this set, $M$ is multiplication on the set, $V$ is the set of vectors, $A_V$ is the - operation of vector addition, and $H$ is the homomorphism that defines the vector space. - On the right hand side of the definition \End(V,A\<^sub>V)\ is the set of endomorphisms, - This definition is only ever used as part of the definition of a module and vector space, - it's just convenient to split it off to shorten the main definitions. \ + assumes mAction: "IsAction(K,A,M,V,A\<^sub>V,H)" -definition - "IsAction(S,A,M,V,A\<^sub>V,H) \ ringHomomor(H,S,A,M,End(V,A\<^sub>V),EndAdd(V,A\<^sub>V),EndMult(V,A\<^sub>V))" + fixes zero_vec ("\") + defines zero_vec_def [simp]: "\ \ TheNeutralElement(V,A\<^sub>V)" -text\A module is a ring action on an abelian group.\ + fixes vAdd (infixl "+\<^sub>V" 80) + defines vAdd_def [simp]: "v\<^sub>1 +\<^sub>V v\<^sub>2 \ A\<^sub>V`\v\<^sub>1,v\<^sub>2\" -definition "IsModule(S,A,M,V,A\<^sub>V,H) \ - IsAring(S,A,M) \ IsAgroup(V,A\<^sub>V) \ (A\<^sub>V {is commutative on} V) \ IsAction(S,A,M,V,A\<^sub>V,H)" + fixes scal (infix "\\<^sub>S" 90) + defines scal_def [simp]: "s \\<^sub>S v \ (H`(s))`(v)" -text\A vector space is a field action on an abelian group. \ + fixes negV ("\_") + defines negV_def [simp]: "\v \ GroupInv(V,A\<^sub>V)`(v)" -definition "IsVectorSpace(S,A,M,V,A\<^sub>V,H) \ - IsAfield(S,A,M) \ IsAgroup(V,A\<^sub>V) \ (A\<^sub>V {is commutative on} V) \ IsAction(S,A,M,V,A\<^sub>V,H)" + fixes vSub (infix "-\<^sub>V" 80) + defines vSub_def [simp]: "v\<^sub>1 -\<^sub>V v\<^sub>2 \ v\<^sub>1 +\<^sub>V (\v\<^sub>2)" +text\The assumptions of \vector_spce0\ context hold in the \module0\ context.\ -text\The next locale defines context (i.e. common assumptions and notation) when considering - modules. We reuse notation from the \ring0\ locale and add notation specific to the - vector spaces. We split the definition of a module into components to make the assumptions - easier to use. The addition and multiplication in the ring of scalars is denoted $+$ and $\cdot$, - resp. The addition of vectors will be denoted $+_V$. The multiplication (scaling) of scalars and - by vectors will be denoted $\cdot_S$. \ +lemma (in vector_space0) vec_spce_mod: shows "module0(K, A, M, V, A\<^sub>V, H)" +proof + from mAbGr show "IsAgroup(V,A\<^sub>V) \ (A\<^sub>V {is commutative on} V)" by simp + from mAction show "IsAction(K,A,M,V,A\<^sub>V,H)" by simp +qed -locale module0 = ring0 + - - fixes V A\<^sub>V H +text\Propositions proven in the \module0\ context are valid in the \vector_spce0\ context.\ + +sublocale vector_space0 < vspce_mod: module0 K A M + ringa ringminus ringsub ringm ringzero ringone ringtwo ringsq V A\<^sub>V + using vec_spce_mod by auto + +subsection\Vector space axioms\ + +text\In this section we show that the definition of a vector space as a field action + on an abelian group implies the vector space axioms as listed on Wikipedia (March 2024). + The first four axioms just state that vectors with addition form an abelian group. + That is fine of course, but in such case the axioms for scalars being a field should be listed + too, and they are not. The entry on modules is more consistent, + it states that module elements form an abelian group, scalars form a ring and lists only + four properties of multiplication of scalars by vectors as module axioms. + The remaining four axioms are just restatemenst of module axioms and since + vector spaces are modules we can prove them by refering to the module axioms + proven in the \module0\ context \ + +text\Vector addition is associative.\ + +lemma (in vector_space0) vec_spce_ax1: assumes "u\V" "v\V" "w\V" + shows "u +\<^sub>V (v +\<^sub>V w) = (u +\<^sub>V v) +\<^sub>V w" + using assms vspce_mod.mod_ab_gr.group_oper_assoc by simp + +text\Vector addition is commutative.\ + +lemma (in vector_space0) vec_spce_ax2: assumes "u\V" "v\V" + shows "u +\<^sub>V v = v +\<^sub>V u" + using mAbGr assms unfolding IsCommutative_def by simp - assumes vAbGr: "IsAgroup(V,A\<^sub>V) \ (A\<^sub>V {is commutative on} V)" +text\The zero vector is a vector.\ - assumes vSpce: "IsAction(R,A,M,V,A\<^sub>V,H)" +lemma (in vector_space0) vec_spce_ax3a: shows "\ \ V" + using vspce_mod.zero_in_mod by simp - fixes vAdd (infixl "+\<^sub>V" 80) - defines vAdd_def [simp]: "v\<^sub>1 +\<^sub>V v\<^sub>2 \ A\<^sub>V`\v\<^sub>1,v\<^sub>2\" +text\The zero vector is the neutral element of addition of vectors.\ - fixes scal (infix "\\<^sub>S" 90) - defines scal_def [simp]: "s \\<^sub>S v \ (H`(s))`(v)" +lemma (in vector_space0) vec_spce_ax3b: assumes "v\V" shows "v +\<^sub>V \ = v" + using assms vspce_mod.zero_neutral by simp + +text\The additive inverse of a vector is a vector.\ + +lemma (in vector_space0) vec_spce_ax4a: assumes "v\V" shows "(\v) \ V" + using assms vspce_mod.mod_ab_gr.inverse_in_group by simp + +text\Sum of of a vector and it's additive inverse is the zero vector.\ + +lemma (in vector_space0) vec_spce_ax4b: assumes "v\V" + shows "v +\<^sub>V (\v) = \" + using assms vspce_mod.mod_ab_gr.group0_2_L6 by simp + +text\Scalar multiplication and field multiplication are "compatible" (as Wikipedia calls it). \ + +lemma (in vector_space0) vec_spce_ax5: assumes "x\K" "y\K" "v\V" + shows "x\\<^sub>S(y\\<^sub>Sv) = (x\y)\\<^sub>Sv" + using assms vspce_mod.module_ax3 by simp + +text\Multiplying the identity element of the field by a vector gives the vector.\ +lemma (in vector_space0) vec_spce_ax6: assumes "v\V" shows "\\\<^sub>Sv = v" + using assms vspce_mod.module_ax4 by simp -text\We indeed talk about modules in the \module0\ context.\ +text\Scalar multiplication is distributive with respect to vector addition.\ -lemma (in module0) module_in_module0: shows "IsModule(R,A,M,V,A\<^sub>V,H)" - using ringAssum vAbGr vSpce unfolding IsModule_def by simp +lemma (in vector_space0) vec_spce_ax7: assumes "x\K" "u\V" "v\V" + shows "x\\<^sub>S(u+\<^sub>Vv) = x\\<^sub>Su +\<^sub>V x\\<^sub>Sv" + using assms vspce_mod.module_ax1 by simp -text\Theorems proven in the \ring_homo\ context are valid in the \module0\ context, as - applied to ring $R$ and the ring of endomorphisms of the vector group. \ +text\Scalar multiplication is distributive with respect to field addition.\ -lemma (in module0) ring_homo_in_module0: - shows "ring_homo(R,A,M,End(V,A\<^sub>V),EndAdd(V,A\<^sub>V),EndMult(V,A\<^sub>V),H)" -proof +lemma (in vector_space0) vec_spce_ax8: assumes "x\K" "y\K" "v\V" + shows "(x\y)\\<^sub>Sv = x\\<^sub>Sv +\<^sub>V y\\<^sub>Sv" + using assms vspce_mod.module_ax2 by simp end