:: Opposite Rings, Modules and their Morphisms :: by Micha{\l} Muzalewski :: :: Received June 22, 1992 :: Copyright (c) 1992-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, FUNCT_1, ZFMISC_1, RELAT_1, SUBSET_1, ALGSTR_0, ARYTM_0, STRUCT_0, MESFUNC1, SUPINF_2, VECTSP_1, RLVECT_1, ARYTM_3, ARYTM_1, GROUP_1, BINOP_1, LATTICES, FUNCSDOM, VECTSP_2, MSSUBFAM, FDIFF_1, GRCAT_1, GROUP_6, FUNCT_2, MOD_4; notations XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, DOMAIN_1, STRUCT_0, ALGSTR_0, BINOP_1, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_2, GRCAT_1, FUNCT_4, GROUP_6, RINGCAT1; constructors DOMAIN_1, VECTSP_2, GRCAT_1, GROUP_6, RINGCAT1, FUNCOP_1, RELSET_1, FUNCT_4; registrations XBOOLE_0, RELSET_1, STRUCT_0, VECTSP_1, VECTSP_2, ALGSTR_0, GRCAT_1, FUNCT_2, RINGCAT1, FUNCT_1; requirements SUBSET, BOOLE; begin :: Opposite Functions registration let G be non empty addMagma; cluster id G -> bijective; end; reserve A,B,C for non empty set, f for Function of [:A,B:],C; theorem :: MOD_4:1 for x being Element of A, y being Element of B holds f.(x,y) = ~f .(y,x); begin :: Opposite Rings reserve K for non empty doubleLoopStr; definition let K; func opp K -> strict doubleLoopStr equals :: MOD_4:def 1 doubleLoopStr (# the carrier of K, the addF of K, ~(the multF of K), 1.K, 0.K #); end; registration let K; cluster opp(K) -> non empty; end; registration let K be well-unital non empty doubleLoopStr; cluster opp(K) -> well-unital; end; registration let K be add-associative right_complementable right_zeroed non empty doubleLoopStr; cluster opp K -> add-associative right_zeroed right_complementable; end; theorem :: MOD_4:2 the addLoopStr of opp(K) = the addLoopStr of K & (K is add-associative right_zeroed right_complementable implies comp opp K = comp K) & for x being set holds x is Scalar of opp(K) iff x is Scalar of K; theorem :: MOD_4:3 (for K being unital non empty doubleLoopStr holds 1.K = 1.opp(K)) & for K being add-associative right_zeroed right_complementable non empty doubleLoopStr holds 0.K = 0.opp(K) & for x,y,z,u being (Scalar of K), a,b,c,d being Scalar of opp(K) st x = a & y = b & z = c & u = d holds x+y = a+b & x*y = b*a & -x = -a & (x+y)+z = (a+b)+c & x+(y+z) = a+(b+c) & (x*y)*z = c*(b*a) & x*( y*z) = (c*b)*a & x*(y+z) = (b+c)*a & (y+z)*x = a*(b+c) & x*y+z*u = b*a+d*c; registration let K be Abelian non empty doubleLoopStr; cluster opp K -> Abelian; end; registration let K be add-associative non empty doubleLoopStr; cluster opp K -> add-associative; end; registration let K be right_zeroed non empty doubleLoopStr; cluster opp K -> right_zeroed; end; registration let K be right_complementable non empty doubleLoopStr; cluster opp K -> right_complementable; end; registration let K be associative non empty doubleLoopStr; cluster opp K -> associative; end; registration let K be distributive non empty doubleLoopStr; cluster opp K -> distributive; end; theorem :: MOD_4:4 for K being Ring holds opp(K) is strict Ring; theorem :: MOD_4:5 for K being Skew-Field holds opp(K) is Skew-Field; registration let K be Skew-Field; cluster opp(K) -> non degenerated almost_left_invertible associative Abelian add-associative right_zeroed right_complementable unital distributive; end; theorem :: MOD_4:6 for K being Field holds opp(K) is strict Field; registration let K be Field; cluster opp(K) -> almost_left_invertible; end; begin :: Opposite Modules reserve V for non empty ModuleStr over K; definition let K,V; func opp(V) -> strict RightModStr over opp(K) means :: MOD_4:def 2 for o being Function of [:the carrier of V, the carrier of opp(K):], the carrier of V st o = ~(the lmult of V) holds it = RightModStr (# the carrier of V, the addF of V, 0.V, o #); end; registration let K,V; cluster opp(V) -> non empty; end; theorem :: MOD_4:7 the addLoopStr of opp(V) = the addLoopStr of V & for x being set holds x is Vector of V iff x is Vector of opp(V); definition let K,V; let o be Function of [:the carrier of K, the carrier of V:], the carrier of V; func opp(o) -> Function of [:the carrier of opp(V), the carrier of opp(K):], the carrier of opp(V) equals :: MOD_4:def 3 ~o; end; theorem :: MOD_4:8 the rmult of opp(V) = opp(the lmult of V); reserve W for non empty RightModStr over K; definition let K,W; func opp(W) -> strict ModuleStr over opp(K) means :: MOD_4:def 4 for o being Function of [:the carrier of opp(K), the carrier of W:], the carrier of W st o = ~(the rmult of W) holds it = ModuleStr (# the carrier of W, the addF of W, 0. W, o #); end; registration let K,W; cluster opp(W) -> non empty; end; theorem :: MOD_4:9 the addLoopStr of opp(W) = the addLoopStr of W & for x being set holds x is Vector of W iff x is Vector of opp(W); definition let K,W; let o be Function of [:the carrier of W, the carrier of K:], the carrier of W; func opp(o) -> Function of [:the carrier of opp(K), the carrier of opp(W):], the carrier of opp(W) equals :: MOD_4:def 5 ~o; end; theorem :: MOD_4:10 the lmult of opp(W) = opp(the rmult of W); theorem :: MOD_4:11 for o being Function of [:the carrier of K, the carrier of V:], the carrier of V, x being Scalar of K, y being Scalar of opp(K), v being Vector of V, w being Vector of opp(V) st x=y & v=w holds (opp(o)).(w,y) = o.(x,v); theorem :: MOD_4:12 for K,L being Ring, V being non empty ModuleStr over K for W being non empty RightModStr over L for x being Scalar of K, y being Scalar of L , v being Vector of V, w being Vector of W st L=opp(K) & W=opp(V) & x=y & v=w holds w*y = x*v; theorem :: MOD_4:13 for K,L being Ring, V being non empty ModuleStr over K for W being non empty RightModStr over L for v1,v2 being Vector of V, w1,w2 being Vector of W st W=opp(V) & v1=w1 & v2=w2 holds w1+w2=v1+v2; theorem :: MOD_4:14 for o being Function of [:the carrier of W, the carrier of K:], the carrier of W, x being Scalar of K, y being Scalar of opp(K), v being Vector of W, w being Vector of opp(W) st x=y & v=w holds (opp(o)).(y,w) = o.(v,x); theorem :: MOD_4:15 for K,L being Ring, V being non empty ModuleStr over K for W being non empty RightModStr over L for x being Scalar of K, y being Scalar of L , v being Vector of V, w being Vector of W st V=opp(W) & x=y & v=w holds w*y = x*v; theorem :: MOD_4:16 for K,L being Ring, V being non empty ModuleStr over K for W being non empty RightModStr over L for v1,v2 being Vector of V, w1,w2 being Vector of W st V=opp(W) & v1=w1 & v2=w2 holds w1+w2=v1+v2; theorem :: MOD_4:17 for K being strict non empty doubleLoopStr, V being non empty ModuleStr over K holds opp(opp(V)) = the ModuleStr of V; theorem :: MOD_4:18 for K being strict non empty doubleLoopStr, W being non empty RightModStr over K holds opp(opp(W)) = the RightModStr of W; theorem :: MOD_4:19 for K being Ring, V being LeftMod of K holds opp V is strict RightMod of opp K; registration let K be Ring, V be LeftMod of K; cluster opp(V) -> Abelian add-associative right_zeroed right_complementable RightMod-like; end; theorem :: MOD_4:20 for K being Ring, W being RightMod of K holds opp W is strict LeftMod of opp K; registration let K be Ring, W be RightMod of K; cluster opp(W) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital; end; begin :: Ring Morphisms definition let K,L be non empty multMagma; let IT be Function of K,L; attr IT is antimultiplicative means :: MOD_4:def 6 for x,y being Scalar of K holds IT.(x*y) = IT.y*IT.x; end; definition let K,L be non empty doubleLoopStr; let IT be Function of K,L; attr IT is antilinear means :: MOD_4:def 7 IT is additive antimultiplicative unity-preserving; end; definition let K,L be non empty doubleLoopStr; let IT be Function of K,L; attr IT is monomorphism means :: MOD_4:def 8 IT is linear one-to-one; attr IT is antimonomorphism means :: MOD_4:def 9 IT is antilinear one-to-one; attr IT is epimorphism means :: MOD_4:def 10 IT is linear onto; attr IT is antiepimorphism means :: MOD_4:def 11 IT is antilinear onto; end; definition let K,L be non empty doubleLoopStr; let IT be Function of K,L; attr IT is isomorphism means :: MOD_4:def 12 IT is monomorphism onto; attr IT is antiisomorphism means :: MOD_4:def 13 IT is antimonomorphism onto; end; registration let K,L be non empty doubleLoopStr; cluster antilinear -> additive antimultiplicative unity-preserving for Function of K,L; cluster additive antimultiplicative unity-preserving -> antilinear for Function of K,L; cluster monomorphism -> linear one-to-one for Function of K,L; cluster linear one-to-one -> monomorphism for Function of K,L; cluster antimonomorphism -> antilinear one-to-one for Function of K,L; cluster antilinear one-to-one -> antimonomorphism for Function of K,L; cluster epimorphism -> linear onto for Function of K,L; cluster linear onto -> epimorphism for Function of K,L; cluster antiepimorphism -> antilinear onto for Function of K,L; cluster antilinear onto -> antiepimorphism for Function of K,L; cluster isomorphism -> monomorphism onto for Function of K,L; cluster monomorphism onto -> isomorphism for Function of K,L; cluster antiisomorphism -> antimonomorphism onto for Function of K,L; cluster antimonomorphism onto -> antiisomorphism for Function of K,L; end; definition let K be non empty doubleLoopStr; let IT be Function of K,K; attr IT is endomorphism means :: MOD_4:def 14 IT is linear; attr IT is antiendomorphism means :: MOD_4:def 15 IT is antilinear; end; registration let K be non empty doubleLoopStr; cluster endomorphism -> linear for Function of K,K; cluster linear -> endomorphism for Function of K,K; cluster antiendomorphism -> antilinear for Function of K,K; cluster antilinear -> antiendomorphism for Function of K,K; end; reserve J for Function of K,K; theorem :: MOD_4:21 J is isomorphism iff J is additive & (for x,y being Scalar of K holds J.(x*y) = J.x*J.y) & J.(1_K) = 1_K & J is one-to-one onto; theorem :: MOD_4:22 J is antiisomorphism iff J is additive & (for x,y being Scalar of K holds J.(x*y) = J.y*J.x) & J.(1_K) = 1_K & J is one-to-one & J is onto; registration let K; cluster id K -> isomorphism; end; reserve K,L for Ring; reserve J for Function of K,L; reserve x,y for Scalar of K; theorem :: MOD_4:23 J is linear implies J.(0.K) = 0.L & J.(-x) = -J.x & J.(x-y) = J.x-J.y; theorem :: MOD_4:24 J is antilinear implies J.(0.K) = 0.L & J.(-x) = -J.x & J.(x-y) = J.x- J.y; theorem :: MOD_4:25 for K being Ring holds id K is antiisomorphism iff K is comRing; theorem :: MOD_4:26 for K being Skew-Field holds id K is antiisomorphism iff K is Field; begin :: Opposite Morphisms definition let K,L be non empty doubleLoopStr, J be Function of K,L; func opp(J) -> Function of K,opp(L) equals :: MOD_4:def 16 J; end; reserve K,L for add-associative right_zeroed right_complementable non empty doubleLoopStr; reserve J for Function of K,L; reserve K for add-associative right_zeroed right_complementable non empty doubleLoopStr; reserve L for add-associative right_zeroed right_complementable well-unital non empty doubleLoopStr; reserve J for Function of K,L; ::$CT theorem :: MOD_4:28 J is linear iff opp(J) is antilinear; theorem :: MOD_4:29 J is antilinear iff opp(J) is linear; theorem :: MOD_4:30 J is monomorphism iff opp(J) is antimonomorphism; theorem :: MOD_4:31 J is antimonomorphism iff opp(J) is monomorphism; theorem :: MOD_4:32 J is epimorphism iff opp(J) is antiepimorphism; theorem :: MOD_4:33 J is antiepimorphism iff opp(J) is epimorphism; theorem :: MOD_4:34 J is isomorphism iff opp(J) is antiisomorphism; theorem :: MOD_4:35 J is antiisomorphism iff opp(J) is isomorphism; reserve K for add-associative right_zeroed right_complementable well-unital non empty doubleLoopStr; reserve J for Function of K,K; theorem :: MOD_4:36 J is endomorphism iff opp(J) is antilinear; theorem :: MOD_4:37 J is antiendomorphism iff opp(J) is linear; theorem :: MOD_4:38 J is isomorphism iff opp(J) is antiisomorphism; theorem :: MOD_4:39 J is antiisomorphism iff opp(J) is isomorphism; begin :: Morphisms of Groups definition let G,H be AddGroup; mode Homomorphism of G,H is additive Function of G,H; end; definition let G be AddGroup; mode Endomorphism of G is Homomorphism of G,G; end; registration let G be AddGroup; cluster bijective for Endomorphism of G; end; definition let G be AddGroup; mode Automorphism of G is bijective Endomorphism of G; end; reserve G,H for AddGroup; reserve f for Homomorphism of G,H; reserve x,y for Element of G; theorem :: MOD_4:40 f.(0.G) = 0.H & f.(-x) = -f.x & f.(x-y) = f.x-f.y; begin :: Semilinear Maps reserve G,H for AbGroup; reserve f for Homomorphism of G,H; reserve x,y for Element of G; reserve K,L for Ring; reserve J for Function of K,L; reserve V for LeftMod of K; reserve W for LeftMod of L; definition let K,L,J,V,W; mode Homomorphism of J,V,W -> Function of V,W means :: MOD_4:def 17 (for x,y being Vector of V holds it.(x+y) = it.x+it.y) & for a being Scalar of K, x being Vector of V holds it.(a*x) = J.a*it.x; end; theorem :: MOD_4:41 ZeroMap(V,W) is Homomorphism of J,V,W; reserve J for Function of K,K; reserve f for Homomorphism of J,V,V; reserve W for LeftMod of K; definition let K,J,V; mode Endomorphism of J,V is Homomorphism of J,V,V; end; definition let K,V,W; mode Homomorphism of V,W is Homomorphism of (id K),V,W; end; theorem :: MOD_4:42 for f being Function of V,W holds f is Homomorphism of V,W iff (for x, y being Vector of V holds f.(x+y) = f.x+f.y) & for a being Scalar of K, x being Vector of V holds f.(a*x) = a*f.x; definition let K,V; mode Endomorphism of V is Homomorphism of V,V; end;