Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### Opposite Rings, Modules and Their Morphisms

by
Michal Muzalewski

MML identifier: MOD_4
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, RELAT_1, VECTSP_1, OPPCAT_1, RLVECT_1, ARYTM_1, FUNCSDOM,
VECTSP_2, LATTICES, BINOP_1, PRE_TOPC, INCSP_1, MOD_1, ORDINAL4, GROUP_6,
MOD_4;
notation XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, DOMAIN_1,
STRUCT_0, MOD_1, BINOP_1, RLVECT_1, VECTSP_1, FUNCSDOM, VECTSP_2,
GRCAT_1, FUNCT_4, PRE_TOPC, RINGCAT1;
constructors DOMAIN_1, BINOP_1, GRCAT_1, RINGCAT1, VECTSP_2, MEMBERED,
PARTFUN1, XBOOLE_0;
clusters VECTSP_1, VECTSP_2, STRUCT_0, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1,
XBOOLE_0;
requirements SUBSET, BOOLE;

begin :: Funkcje przeciwne

reserve A,B,C for non empty set,
f for Function of [:A,B:],C;

definition let A,B,C,f;
redefine func ~f -> Function of [:B,A:],C;
end;

theorem :: MOD_4:1
for x being Element of A, y being Element of B holds
f.(x,y) = ~f.(y,x);

begin :: Pierscienie przeciwne

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 mult of K),
the unity of K,
the Zero of K #);
end;

definition let K;
cluster opp(K) -> non empty;
end;

definition 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 LoopStr of opp(K) = the LoopStr 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
opp(opp(K)) = the doubleLoopStr of K;

theorem :: MOD_4:4
right_complementable (non empty doubleLoopStr) holds
0.K = 0.opp(K)
& 1_ K = 1_ 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;

theorem :: MOD_4:5
for K being Ring holds opp(K) is strict Ring;

definition let K be Ring;
cluster opp(K) -> Abelian add-associative right_zeroed right_complementable
well-unital distributive;
end;

theorem :: MOD_4:6
for K being Ring holds opp(K) is Ring;

definition let K be Ring;
cluster opp(K) -> associative;
end;

theorem :: MOD_4:7
for K being Skew-Field holds opp(K) is Skew-Field;

definition let K be Skew-Field;
cluster opp(K) -> non degenerated Field-like associative Abelian
end;

theorem :: MOD_4:8
for K being Field holds opp(K) is strict Field;

definition let K be Field;
cluster opp(K) -> strict Field-like;
end;

begin :: Moduly przeciwne

reserve V for non empty VectSpStr 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 add of V, the Zero of V, o #);
end;

definition let K,V;
cluster opp(V) -> non empty;
end;

theorem :: MOD_4:9
the LoopStr of opp(V) = the LoopStr 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:10
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 VectSpStr 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 = VectSpStr
(# the carrier of W, the add of W, the Zero of W, o #);
end;

definition let K,W;
cluster opp(W) -> non empty;
end;

canceled;

theorem :: MOD_4:12
the LoopStr of opp(W) = the LoopStr 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:13
the lmult of opp(W) = opp(the rmult of W);

canceled;

theorem :: MOD_4:15
for o being Function of [:the carrier of K,
the carrier of V:], the carrier of V
holds opp(opp(o)) = o;

theorem :: MOD_4:16
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:17
for K,L being Ring, V being non empty VectSpStr 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:18
for K,L being Ring, V being non empty VectSpStr over K
for W being non empty RightModStr over L for v1,v2 being Vector of V,
w1,w2 being Vector of W
st L=opp(K) & W=opp(V) & v1=w1 & v2=w2
holds w1+w2=v1+v2;

theorem :: MOD_4:19
for o being Function of [:the carrier of W,
the carrier of K:], the carrier of W
holds opp(opp(o)) = o;

theorem :: MOD_4:20
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:21
for K,L being Ring, V being non empty VectSpStr 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 K=opp(L) & V=opp(W) & x=y & v=w
holds w*y = x*v;

theorem :: MOD_4:22
for K,L being Ring, V being non empty VectSpStr over K
for W being non empty RightModStr over L for v1,v2 being Vector of V,
w1,w2 being Vector of W
st K=opp(L) & V=opp(W) & v1=w1 & v2=w2
holds w1+w2=v1+v2;

theorem :: MOD_4:23
for K being strict non empty doubleLoopStr, V being non empty VectSpStr over
K
holds opp(opp(V)) = the VectSpStr of V;

theorem :: MOD_4:24
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:25
for K being Ring, V being LeftMod of K holds
opp V is strict RightMod of opp K;

definition 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:26
for K being Ring, W being RightMod of K holds
opp W is strict LeftMod of opp K;

definition let K be Ring, W be RightMod of K;
cluster opp(W) -> Abelian add-associative right_zeroed right_complementable
VectSp-like;
end;

begin :: Morfizmy pierscieni

definition let K,L be non empty doubleLoopStr;
let IT be map of K,L;
attr IT is antilinear means
:: MOD_4:def 6
(for x,y being Scalar of K holds IT.(x+y) = IT.x+IT.y)
& (for x,y being Scalar of K holds IT.(x*y) = IT.y*IT.x)
& IT.(1_ K) = 1_ L;
end;

definition let K,L be non empty doubleLoopStr;
let IT be map of K,L;
attr IT is monomorphism means
:: MOD_4:def 7
IT is linear & IT is one-to-one;
attr IT is antimonomorphism means
:: MOD_4:def 8
IT is antilinear & IT is one-to-one;
end;

definition let K,L be non empty doubleLoopStr;
let IT be map of K,L;
attr IT is epimorphism means
:: MOD_4:def 9
IT is linear & rng IT = the carrier of L;
attr IT is antiepimorphism means
:: MOD_4:def 10
IT is antilinear & rng IT = the carrier of L;
end;

definition let K,L be non empty doubleLoopStr;
let IT be map of K,L;
attr IT is isomorphism means
:: MOD_4:def 11
IT is monomorphism & rng IT = the carrier of L;
attr IT is antiisomorphism means
:: MOD_4:def 12
IT is antimonomorphism & rng IT = the carrier of L;
end;

reserve J for map of K,K;

definition let K be non empty doubleLoopStr;
let IT be map of K,K;
attr IT is endomorphism means
:: MOD_4:def 13
IT is linear;
attr IT is antiendomorphism means
:: MOD_4:def 14
IT is antilinear;
attr IT is automorphism means
:: MOD_4:def 15
IT is isomorphism;
attr IT is antiautomorphism means
:: MOD_4:def 16
IT is antiisomorphism;
end;

theorem :: MOD_4:27
J is automorphism
iff (for x,y being Scalar of K holds J.(x+y) = J.x+J.y)
& (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
& rng J = the carrier of K;

theorem :: MOD_4:28
J is antiautomorphism iff
(for x,y being Scalar of K holds J.(x+y) = J.x+J.y)
& (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
& rng J = the carrier of K;

theorem :: MOD_4:29
id K is automorphism;

reserve K,L for Ring;
reserve J for map of K,L;
reserve x,y for Scalar of K;

theorem :: MOD_4:30
J is linear implies
J.(0.K) = 0.L
& J.(-x) = -J.x
& J.(x-y) = J.x-J.y;

theorem :: MOD_4:31
J is antilinear implies
J.(0.K) = 0.L
& J.(-x) = -J.x
& J.(x-y) = J.x-J.y;

theorem :: MOD_4:32
for K being Ring holds id K is antiautomorphism iff K is comRing;

theorem :: MOD_4:33
for K being Skew-Field holds id K is antiautomorphism iff K is Field;

begin :: Morfizmy przeciwne do morfizmow pierscieni

definition let K,L be non empty doubleLoopStr,
J be map of K,L;
func opp(J) -> map of K,opp(L) equals
:: MOD_4:def 17
J;
end;

reserve K,L for add-associative right_zeroed right_complementable
(non empty doubleLoopStr);
reserve J for map of K,L;

theorem :: MOD_4:34
opp(opp(J)) = J;

theorem :: MOD_4:35
for K,L being add-associative right_zeroed right_complementable
(non empty doubleLoopStr),
J being map of K,L holds
J is linear iff opp(J) is antilinear;

theorem :: MOD_4:36
J is antilinear iff opp(J) is linear;

theorem :: MOD_4:37
J is monomorphism iff opp(J) is antimonomorphism;

theorem :: MOD_4:38
J is antimonomorphism iff opp(J) is monomorphism;

theorem :: MOD_4:39
J is epimorphism iff opp(J) is antiepimorphism;

theorem :: MOD_4:40
J is antiepimorphism iff opp(J) is epimorphism;

theorem :: MOD_4:41
J is isomorphism iff opp(J) is antiisomorphism;

theorem :: MOD_4:42
J is antiisomorphism iff opp(J) is isomorphism;

reserve J for map of K,K;

theorem :: MOD_4:43
J is endomorphism iff opp(J) is antilinear;

theorem :: MOD_4:44
J is antiendomorphism iff opp(J) is linear;

theorem :: MOD_4:45
J is automorphism iff opp(J) is antiisomorphism;

theorem :: MOD_4:46
J is antiautomorphism iff opp(J) is isomorphism;

begin :: Morfizmy grup i grup abelowych

definition let G,H;
mode Homomorphism of G,H -> map of G,H means
:: MOD_4:def 18
for x,y being Element of G holds it.(x+y) = it.x+it.y;
end;

definition let G,H;
redefine func ZeroMap(G,H) -> Homomorphism of G,H;
end;

reserve f for Homomorphism of G,H;

definition let G,H;
let IT be Homomorphism of G,H;
attr IT is monomorphism means
:: MOD_4:def 19
IT is one-to-one;
end;

definition let G,H;
let IT be Homomorphism of G,H;
attr IT is epimorphism means
:: MOD_4:def 20
rng IT = the carrier of H;
end;

definition let G,H;
let IT be Homomorphism of G,H;
attr IT is isomorphism means
:: MOD_4:def 21
IT is one-to-one & rng IT = the carrier of H;
end;

definition let G;
mode Endomorphism of G is Homomorphism of G,G;
end;

definition let G;
cluster isomorphism Endomorphism of G;
end;

definition let G;
mode Automorphism of G is isomorphism Endomorphism of G;
end;

definition let G;
redefine func id G -> Automorphism of G;
end;

reserve x,y for Element of G;

canceled;

theorem :: MOD_4:48
f.(0.G) = 0.H
& f.(-x) = -f.x
& f.(x-y) = f.x-f.y;

reserve G,H for AbGroup;
reserve f for Homomorphism of G,H;
reserve x,y for Element of G;

theorem :: MOD_4:49
f.(x-y) = f.x-f.y;

begin :: Odwzorowania semiliniowe

reserve K,L for Ring;
reserve J for map of K,L;
reserve V for LeftMod of K;
reserve W for LeftMod of L;

definition let K,L,J,V,W;
canceled;

mode Homomorphism of J,V,W -> map of V,W means
:: MOD_4:def 23

(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:50
ZeroMap(V,W) is Homomorphism of J,V,W;

reserve f for Homomorphism of J,V,W;

definition let K,L,J,V,W,f;
pred f is_monomorphism_wrp J means
:: MOD_4:def 24
f is one-to-one;

pred f is_epimorphism_wrp J means
:: MOD_4:def 25
rng f = the carrier of W;

pred f is_isomorphism_wrp J means
:: MOD_4:def 26
f is one-to-one & rng f = the carrier of W;
end;

reserve J for map of K,K;
reserve f for Homomorphism of J,V,V;

definition let K,J,V;
mode Endomorphism of J,V is Homomorphism of J,V,V;
end;

definition let K,J,V,f;
pred f is_automorphism_wrp J means
:: MOD_4:def 27
f is one-to-one
& rng f = the carrier of V;
end;

reserve W for LeftMod of K;

definition let K,V,W;
mode Homomorphism of V,W is Homomorphism of (id K),V,W;
end;

theorem :: MOD_4:51
for f being map 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,W;
let IT be Homomorphism of V,W;
attr IT is monomorphism means
:: MOD_4:def 28
IT is one-to-one;
attr IT is epimorphism means
:: MOD_4:def 29
rng IT = the carrier of W;
attr IT is isomorphism means
:: MOD_4:def 30
IT is one-to-one & rng IT = the carrier of W;
end;

definition let K,V;
mode Endomorphism of V is Homomorphism of V,V;
end;

definition let K,V;
let IT be Endomorphism of V;
attr IT is automorphism means
:: MOD_4:def 31
IT is one-to-one & rng IT = the carrier of V;
end;
```