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

Received June 22, 1992

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 add 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
for K being add-associative right_zeroed
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
add-associative right_zeroed right_complementable well-unital distributive;
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

reserve G,H for AddGroup;

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;
```