:: Opposite Rings, Modules and their Morphisms
:: by Micha{\l} Muzalewski
::
:: Received June 22, 1992
:: Copyright (c) 1992-2016 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, SUBSET_1, 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;