:: Opposite Rings, Modules and their Morphisms
:: by Micha{\l} Muzalewski
::
:: Received June 22, 1992
:: Copyright (c) 1992-2026 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;
definitions RLVECT_1, STRUCT_0, GROUP_1, GROUP_6, RINGCAT1, VECTSP_1,
ALGSTR_0;
equalities STRUCT_0, GRCAT_1, VECTSP_1, ALGSTR_0;
expansions GROUP_1, GROUP_6, VECTSP_1;
theorems FUNCT_1, FUNCT_2, VECTSP_1, VECTSP_2, FUNCT_4, RLVECT_1, RELAT_1,
GROUP_1, FUNCOP_1, GROUP_6, ALGSTR_0, STRUCT_0;
begin :: Opposite Functions
registration let G be non empty 1-sorted;
cluster id G -> bijective;
coherence
proof
set f = id G;
rng f = the carrier of G by RELAT_1:45; then
f is one-to-one onto by FUNCT_2:def 3;
hence thesis;
end;
end;
reserve A,B,C for non empty set,
f for Function of [:A,B:],C;
theorem
for x being Element of A, y being Element of B holds f.(x,y) = ~f .(y,x)
by FUNCT_4:def 8;
begin :: Opposite Rings
reserve K for non empty doubleLoopStr;
definition let K;
func opp K -> strict doubleLoopStr equals
doubleLoopStr
(# the carrier of K, the addF of K, ~(the multF of K), 1.K, 0.K #);
correctness;
end;
registration let K;
cluster opp(K) -> non empty;
coherence;
end;
Lm1: for K being well-unital non empty doubleLoopStr for h, e being Element
of opp K st e = 1.K holds h * e = h & e * h = h
proof
let K be well-unital non empty doubleLoopStr;
let h, e be Element of opp K;
assume
A1: e = 1.K;
reconsider a = h, b = e as Element of K;
thus h * e = b * a by FUNCT_4:def 8
.= h by A1;
thus e * h = a * b by FUNCT_4:def 8
.= h by A1;
end;
registration
let K be well-unital non empty doubleLoopStr;
cluster opp(K) -> well-unital;
coherence
by Lm1;
end;
Lm2: now
let K be add-associative right_zeroed right_complementable non empty
doubleLoopStr;
set L = opp(K);
thus for x,y,z being Scalar of L holds (x+y)+z = x+(y+z) & x+(0.L) = x
proof
let x,y,z be Scalar of L;
reconsider a = x, b = y, c = z as Scalar of K;
thus (x+y)+z = (a+b)+c .= a+(b+c) by RLVECT_1:def 3
.= x+(y+z);
thus x+(0.L) = a + 0.K .= x by RLVECT_1:def 4;
end;
end;
registration
let K be add-associative right_complementable right_zeroed non empty
doubleLoopStr;
cluster opp K -> add-associative right_zeroed right_complementable;
coherence
proof
thus for x,y,z be Element of opp K holds x + (y + z) = x + y + z by Lm2;
thus for x be Element of opp K holds x + 0.opp K = x by Lm2;
let a be Element of opp K;
reconsider x = a as Element of K;
reconsider y = -x as Element of opp K;
take y;
thus a+y = x+-x .= 0.opp K by RLVECT_1:5;
end;
end;
Lm3: for K being add-associative right_zeroed right_complementable non empty
doubleLoopStr for x,y being Scalar of K, a,b being Scalar of opp(K) st x = a &
y = b holds x+y = a+b & x*y = b*a & -x = -a
proof
let K be add-associative right_zeroed right_complementable non empty
doubleLoopStr;
let x,y be Scalar of K,a,b be Scalar of opp(K) such that
A1: x = a and
A2: y = b;
thus x+y = a+b by A1,A2;
thus x*y = b*a by A1,A2,FUNCT_4:def 8;
reconsider c = -a as Element of K;
c+x = -a+a by A1
.= 0.opp K by RLVECT_1:5
.= 0.K;
hence thesis by RLVECT_1:6;
end;
theorem
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
proof
thus the addLoopStr of opp(K) = the addLoopStr of K;
hereby
assume
A1: K is add-associative right_zeroed right_complementable;
A2: for x be object st x in the carrier of K
holds (comp opp K).x = (comp K). x
proof
let x be object;
assume x in the carrier of K;
then reconsider y = x as Element of K;
reconsider z = y as Element of opp K;
A3: -y = -z by A1,Lm3;
thus (comp opp K).x = -z by VECTSP_1:def 13
.= (comp K).x by A3,VECTSP_1:def 13;
end;
dom comp opp K = the carrier of K & dom comp K = the carrier of K by
FUNCT_2:def 1;
hence comp opp K = comp K by A2,FUNCT_1:2;
end;
let x be set;
thus thesis;
end;
Lm4: for K being non empty doubleLoopStr 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)+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
proof
let K be non empty doubleLoopStr;
let x,y,z,u be Scalar of K, a,b,c,d be Scalar of opp(K);
assume that
A1: x = a & y = b & z = c and
A2: u = d;
x*y = b*a & y*z = c*b by A1,FUNCT_4:def 8;
hence thesis by A1,A2,FUNCT_4:def 8;
end;
theorem
(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
by Lm3,Lm4;
registration
let K be Abelian non empty doubleLoopStr;
cluster opp K -> Abelian;
coherence
proof
let x,y be Element of opp K;
reconsider a=x, b=y as Element of K;
thus x+y = a+b .= b+a
.= y+x;
end;
end;
registration
let K be add-associative non empty doubleLoopStr;
cluster opp K -> add-associative;
coherence
proof
let x,y,z be Element of opp K;
reconsider a = x, b = y, c = z as Element of K;
thus (x+y)+z = (a+b)+c .= a+(b+c) by RLVECT_1:def 3
.= x+(y+z);
end;
end;
registration
let K be right_zeroed non empty doubleLoopStr;
cluster opp K -> right_zeroed;
coherence
proof
let x be Element of opp K;
reconsider a = x as Element of K;
thus x+0.opp K = a+0.K .= x by RLVECT_1:def 4;
end;
end;
registration
let K be right_complementable non empty doubleLoopStr;
cluster opp K -> right_complementable;
coherence
proof
let x be Element of opp K;
reconsider a = x as Element of K;
consider b being Element of K such that
A1: a + b = 0.K by ALGSTR_0:def 11;
reconsider y = b as Element of opp K;
take y;
thus thesis by A1;
end;
end;
registration
let K be associative non empty doubleLoopStr;
cluster opp K -> associative;
coherence
proof
let x,y,z be Element of opp K;
reconsider a = x, b = y, c = z as Element of K;
thus (x*y)*z = c*(b*a) by Lm4
.= c*b*a by GROUP_1:def 3
.= x*(y*z) by Lm4;
end;
end;
registration
let K be distributive non empty doubleLoopStr;
cluster opp K -> distributive;
coherence
proof
let x,y,z be Element of opp K;
reconsider a = x, b = y, c = z as Element of K;
thus x*(y+z) = (b+c)*a by Lm4
.= b*a+c*a by VECTSP_1:def 7
.= x*y+x*z by Lm4;
thus (y+z)*x = a*(b+c) by Lm4
.= a*b+a*c by VECTSP_1:def 7
.= y*x+z*x by Lm4;
end;
end;
theorem
for K being Ring holds opp(K) is strict Ring;
theorem Th5:
for K being Skew-Field holds opp(K) is Skew-Field
proof
let K be Skew-Field;
set L = opp(K);
for x being Scalar of L holds (x <> 0.L implies ex y be Scalar of L st y
*x = 1_L) & 0.L <> 1_L
proof
let x be Scalar of L;
x <> 0.L implies ex y be Scalar of L st y*x = 1_L
proof
reconsider a = x as Scalar of K;
assume x <> 0.L;
then consider b being Scalar of K such that
A1: a*b = 1_K by VECTSP_2:6;
reconsider y = b as Scalar of opp(K);
take y;
thus thesis by A1,Lm3;
end;
hence thesis;
end;
hence thesis by STRUCT_0:def 8,VECTSP_1:def 9;
end;
registration
let K be Skew-Field;
cluster opp(K) -> non degenerated almost_left_invertible associative Abelian
add-associative right_zeroed right_complementable unital distributive;
coherence by Th5;
end;
Lm5: for F being commutative non empty doubleLoopStr, x,y being Element of F
holds x*y = y*x;
theorem
for K being Field holds opp(K) is strict Field
proof
let K be Field;
set L = opp(K);
for x,y being Scalar of L holds x*y = y*x
proof
let x,y be Scalar of L;
reconsider a = x, b = y as Scalar of K;
b*a = x*y by Lm3;
hence thesis by Lm3;
end;
hence thesis by GROUP_1:def 12;
end;
registration let K be Field;
cluster opp(K) -> almost_left_invertible;
coherence;
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
:Def2:
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 #);
existence
proof
reconsider o = ~(the lmult of V) as Function of [:the carrier of V, the
carrier of opp(K):], the carrier of V;
take RightModStr (#the carrier of V, the addF of V, 0.V, o#);
thus thesis;
end;
uniqueness
proof
reconsider o = ~(the lmult of V) as Function of [:the carrier of V, the
carrier of opp(K):], the carrier of V;
let M1,M2 be strict RightModStr over opp(K) such that
A1: 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 M1 = RightModStr (# the
carrier of V, the addF of V, 0.V, o #) and
A2: 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 M2 = RightModStr (# the
carrier of V, the addF of V, 0.V, o #);
thus M1 = RightModStr (# the carrier of V, the addF of V, 0.V, o #) by A1
.= M2 by A2;
end;
end;
registration let K,V;
cluster opp(V) -> non empty;
coherence
proof
reconsider o = ~(the lmult of V) as Function of [:the carrier of V,the
carrier of opp(K):], the carrier of V;
opp V = RightModStr (# the carrier of V, the addF of V, 0.V, o #) by Def2;
hence the carrier of opp V is non empty;
end;
end;
theorem Th7:
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)
proof
reconsider p = ~(the lmult of V) as Function of [:the carrier of V, the
carrier of opp(K):], the carrier of V;
A1: opp(V) = RightModStr (# the carrier of V, the addF of V, 0.V, p #) by Def2;
hence the addLoopStr of opp(V) = the addLoopStr of V;
let x be set;
thus thesis by A1;
end;
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
~o;
coherence
proof
the addLoopStr of opp(V) = the addLoopStr of V by Th7;
hence thesis;
end;
end;
theorem Th8:
the rmult of opp(V) = opp(the lmult of V)
proof
reconsider p = ~(the lmult of V) as Function of [:the carrier of V, the
carrier of opp(K):], the carrier of V;
opp(V) = RightModStr (# the carrier of V, the addF of V, 0.V, p #) by Def2;
hence thesis;
end;
reserve W for non empty RightModStr over K;
definition let K,W;
func opp(W) -> strict ModuleStr over opp(K) means :Def4:
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 #);
existence
proof
reconsider o = ~(the rmult of W) as Function of [:the carrier of opp(K ),
the carrier of W:], the carrier of W;
take ModuleStr (#the carrier of W, the addF of W, 0.W, o#);
thus thesis;
end;
uniqueness
proof
reconsider o = ~(the rmult of W) as Function of [:the carrier of opp(K),
the carrier of W:], the carrier of W;
let M1,M2 be strict ModuleStr over opp(K) such that
A1: 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 M1 = ModuleStr (# the
carrier of W, the addF of W, 0.W, o #) and
A2: 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 M2 = ModuleStr (# the
carrier of W, the addF of W, 0.W, o #);
thus M1 = ModuleStr (# the carrier of W, the addF of W, 0.W, o #) by A1
.= M2 by A2;
end;
end;
registration let K,W;
cluster opp(W) -> non empty;
coherence
proof
reconsider o = ~(the rmult of W) as Function of [:the carrier of opp(K),
the carrier of W:], the carrier of W;
opp W = ModuleStr (#the carrier of W, the addF of W, 0.W, o#) by Def4;
hence the carrier of opp W is non empty;
end;
end;
theorem Th9:
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)
proof
reconsider p = ~(the rmult of W) as Function of [:the carrier of opp(K), the
carrier of W:], the carrier of W;
A1: opp(W) = ModuleStr (# the carrier of W, the addF of W, 0.W, p #) by Def4;
hence the addLoopStr of opp(W) = the addLoopStr of W;
let x be set;
thus thesis by A1;
end;
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
~o;
coherence
proof
the addLoopStr of opp(W) = the addLoopStr of W by Th9;
then reconsider
o9 = ~o as Function of [:the carrier of opp(K), the carrier of
opp(W):], the carrier of opp(W);
o9 is Function of [:the carrier of opp(K), the carrier of opp(W):],
the carrier of opp(W);
hence thesis;
end;
end;
theorem Th10:
the lmult of opp(W) = opp(the rmult of W)
proof
reconsider p = ~(the rmult of W) as Function of [:the carrier of opp(K), the
carrier of W:], the carrier of W;
opp(W) = ModuleStr (# the carrier of W, the addF of W, 0.W, p #) by Def4;
hence thesis;
end;
theorem
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)
by FUNCT_4:def 8;
theorem Th12:
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
proof
let K,L be Ring, V be non empty ModuleStr over K;
let W be non empty RightModStr over L;
let x be Scalar of K, y be Scalar of L, v be Vector of V, w be Vector of W
such that
A1: L=opp(K) & W=opp(V) and
A2: x=y & v=w;
set o = the lmult of V;
opp(o) = the rmult of opp(V) by Th8;
hence w*y = (opp(o)).(w,y) by A1,VECTSP_2:def 7
.= x*v by A2,FUNCT_4:def 8;
end;
theorem Th13:
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
proof
let K,L be Ring, V be non empty ModuleStr over K;
A1: the addLoopStr of opp(V) = the addLoopStr of V by Th7;
let W be non empty RightModStr over L, v1,v2 be Vector of V, w1,w2 be Vector
of W;
assume W=opp(V) & v1=w1 & v2=w2;
hence thesis by A1;
end;
theorem
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)
by FUNCT_4:def 8;
theorem Th15:
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
proof
let K,L be Ring, V be non empty ModuleStr over K;
let W be non empty RightModStr over L;
let x be Scalar of K, y be Scalar of L, v be Vector of V, w be Vector of W
such that
A1: V=opp(W) & x=y & v=w;
set o = the rmult of W;
A2: opp(o) = the lmult of opp(W) by Th10;
thus w*y = o.(w,y) by VECTSP_2:def 7
.= x*v by A1,A2,FUNCT_4:def 8;
end;
theorem Th16:
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
proof
let K,L be Ring, V be non empty ModuleStr over K;
let W be non empty RightModStr over L;
A1: the addLoopStr of opp(W) = the addLoopStr of W by Th9;
let v1,v2 be Vector of V, w1,w2 be Vector of W;
assume V=opp(W) & v1=w1 & v2=w2;
hence thesis by A1;
end;
theorem
for K being strict non empty doubleLoopStr, V being non empty
ModuleStr over K holds opp(opp(V)) = the ModuleStr of V
proof
let K be strict non empty doubleLoopStr, V be non empty ModuleStr over K;
set W = opp(V);
A1: opp(opp(K)) = K by FUNCT_4:53;
A2: opp(the rmult of W) = opp(opp(the lmult of V)) by Th8
.= the lmult of V by FUNCT_4:53;
the addLoopStr of opp(W) = the addLoopStr of W by Th9
.= the addLoopStr of V by Th7;
hence thesis by A2,A1,Th10;
end;
theorem
for K being strict non empty doubleLoopStr, W being non empty
RightModStr over K holds opp(opp(W)) = the RightModStr of W
proof
let K be strict non empty doubleLoopStr, W be non empty RightModStr over K;
set V = opp(W);
A1: opp(opp(K)) = K by FUNCT_4:53;
A2: opp(the lmult of V) = opp(opp(the rmult of W)) by Th10
.= the rmult of W by FUNCT_4:53;
the addLoopStr of opp(V) = the addLoopStr of V by Th7
.= the addLoopStr of W by Th9;
hence thesis by A2,A1,Th8;
end;
theorem Th19:
for K being Ring, V being LeftMod of K holds opp V is strict
RightMod of opp K
proof
let K be Ring, V be LeftMod of K;
set R=opp(K);
reconsider W=opp(V) as non empty RightModStr over R;
A1: the addLoopStr of opp V = the addLoopStr of V by Th7;
then
A2: for a,b be Element of opp V for x,y be Element of V st x = a & b = y
holds a + b = x + y;
A3: opp V is Abelian add-associative right_zeroed right_complementable
proof
thus opp V is Abelian
proof
let a,b be Element of opp V;
reconsider x = a, y = b as Element of V by Th7;
thus a + b = y + x by A2
.= b + a by A1;
end;
hereby
let a,b,c be Element of opp V;
reconsider x = a, y = b, z = c as Element of V by Th7;
thus a + b + c = x + y + z by A1
.= x + (y + z) by RLVECT_1:def 3
.= a + (b + c) by A1;
end;
hereby
let a be Element of opp V;
reconsider x = a as Element of V by Th7;
thus a + 0.opp V = x + 0.V by A1
.= a by RLVECT_1:4;
end;
let a be Element of opp V;
reconsider x = a as Element of V by Th7;
consider b being Element of V such that
A4: x + b = 0.V by ALGSTR_0:def 11;
reconsider b9 = b as Element of opp V by Th7;
take b9;
thus thesis by A1,A4;
end;
now
let x,y be Scalar of R, v,w be Vector of W;
reconsider p=v,q=w as Vector of V by Th7;
reconsider a=x,b=y as Scalar of K;
A5: b*p=v*y by Th12;
A6: a*q=w*x by Th12;
A7: a*p=v*x by Th12;
v+w=p+q by Th13;
hence (v+w)*x = a*(p+q) by Th12
.= a*p+a*q by VECTSP_1:def 14
.= v*x+w*x by A7,A6,Th13;
thus v*(x+y) = (a+b)*p by Th12
.= a*p+b*p by VECTSP_1:def 15
.= v*x+v*y by A5,A7,Th13;
thus v*(y*x) = (a*b)*p by Lm3,Th12
.= a*(b*p) by VECTSP_1:def 16
.= (v*y)*x by A5,Th12;
thus v*(1_R) = (1_K)*p by Th12
.= v;
end;
hence thesis by A3,VECTSP_2:def 9;
end;
registration let K be Ring, V be LeftMod of K;
cluster opp(V) -> Abelian add-associative right_zeroed right_complementable
RightMod-like;
coherence by Th19;
end;
theorem Th20:
for K being Ring, W being RightMod of K holds
opp W is strict LeftMod of opp K
proof
let K be Ring, W be RightMod of K;
set R=opp(K);
reconsider V=opp(W) as non empty ModuleStr over R;
A1: the addLoopStr of opp W = the addLoopStr of W by Th9;
then
A2: for a,b be Element of opp W for x,y be Element of W st x = a & b = y
holds a + b = x + y;
A3: opp W is Abelian add-associative right_zeroed right_complementable
proof
thus opp W is Abelian
proof
let a,b be Element of opp W;
reconsider x = a, y = b as Element of W by Th9;
thus a + b = y + x by A2
.= b + a by A1;
end;
hereby
let a,b,c be Element of opp W;
reconsider x = a, y = b, z = c as Element of W by Th9;
thus a + b + c = x + y + z by A1
.= x + (y + z) by RLVECT_1:def 3
.= a + (b + c) by A1;
end;
hereby
let a be Element of opp W;
reconsider x = a as Element of W by Th9;
thus a + 0.opp W = x + 0.W by A1
.= a by RLVECT_1:4;
end;
let a be Element of opp W;
reconsider x = a as Element of W by Th9;
consider b being Element of W such that
A4: x + b = 0.W by ALGSTR_0:def 11;
reconsider b9 = b as Element of opp W by Th9;
take b9;
thus thesis by A1,A4;
end;
now
let x,y be Scalar of R, v,w be Vector of V;
reconsider p=v,q=w as Vector of W by Th9;
reconsider a=x,b=y as Scalar of K;
A5: p*b=y*v by Th15;
A6: q*a=x*w by Th15;
A7: p*a=x*v by Th15;
v+w=p+q by Th16;
hence x*(v+w) = (p+q)*a by Th15
.= p*a+q*a by VECTSP_2:def 9
.= x*v+x*w by A7,A6,Th16;
thus (x+y)*v = p*(a+b) by Th15
.= p*a+p*b by VECTSP_2:def 9
.= x*v+y*v by A5,A7,Th16;
x*y=b*a by Lm3;
hence (x*y)*v = p*(b*a) by Th15
.= (p*b)*a by VECTSP_2:def 9
.= x*(y*v) by A5,Th15;
thus (1_R)*v = p*(1_K) by Th15
.= v by VECTSP_2:def 9;
end;
hence thesis by A3,VECTSP_1:def 14,def 15,def 16,def 17;
end;
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;
coherence by Th20;
end;
begin :: Ring Morphisms
definition
let K,L be non empty multMagma;
let IT be Function of K,L;
attr IT is antimultiplicative means :Def6:
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
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
IT is linear one-to-one;
attr IT is antimonomorphism means
IT is antilinear one-to-one;
attr IT is epimorphism means
IT is linear onto;
attr IT is antiepimorphism means
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
IT is monomorphism onto;
attr IT is antiisomorphism means
IT is antimonomorphism onto;
end;
registration
let K,L be non empty doubleLoopStr;
cluster antilinear -> additive antimultiplicative unity-preserving
for Function of K,L;
coherence;
cluster additive antimultiplicative unity-preserving -> antilinear
for Function of K,L;
coherence;
cluster monomorphism -> linear one-to-one for Function of K,L;
coherence;
cluster linear one-to-one -> monomorphism for Function of K,L;
coherence;
cluster antimonomorphism -> antilinear one-to-one for Function of K,L;
coherence;
cluster antilinear one-to-one -> antimonomorphism for Function of K,L;
coherence;
cluster epimorphism -> linear onto for Function of K,L;
coherence;
cluster linear onto -> epimorphism for Function of K,L;
coherence;
cluster antiepimorphism -> antilinear onto for Function of K,L;
coherence;
cluster antilinear onto -> antiepimorphism for Function of K,L;
coherence;
cluster isomorphism -> monomorphism onto for Function of K,L;
coherence;
cluster monomorphism onto -> isomorphism for Function of K,L;
coherence;
cluster antiisomorphism -> antimonomorphism onto for Function of K,L;
coherence;
cluster antimonomorphism onto -> antiisomorphism for Function of K,L;
coherence;
end;
definition
let K be non empty doubleLoopStr;
let IT be Function of K,K;
attr IT is endomorphism means
IT is linear;
attr IT is antiendomorphism means
IT is antilinear;
end;
registration
let K be non empty doubleLoopStr;
cluster endomorphism -> linear for Function of K,K;
coherence;
cluster linear -> endomorphism for Function of K,K;
coherence;
cluster antiendomorphism -> antilinear for Function of K,K;
coherence;
cluster antilinear -> antiendomorphism for Function of K,K;
coherence;
end;
reserve J for Function of K,K;
theorem
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
proof
thus J is isomorphism implies 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 by GROUP_1:def 13,GROUP_6:def 6;
assume (J is additive & for x,y
being Scalar of K holds J.(x*y) = J.x*J.y )& J.(1_K) = 1_K;
then J is additive multiplicative unity-preserving;
hence thesis;
end;
theorem Th22:
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
proof
thus J is antiisomorphism implies 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 by Def6,GROUP_1:def 13;
assume (J is additive & for x,y
being Scalar of K holds J.(x*y) = J.y*J.x )& J.(1_K) = 1_K;
then J is additive antimultiplicative unity-preserving;
hence thesis;
end;
registration let K;
cluster id K -> isomorphism;
coherence;
end;
reserve K,L for Ring;
reserve J for Function of K,L;
reserve x,y for Scalar of K;
Lm6: J is additive implies J.(0.K) = 0.L
proof
set a = 0.K;
assume
A1: J is additive;
a+a = a by RLVECT_1:4;
then J.a+J.a = J.a by A1
.= J.a+(0.L) by RLVECT_1:4;
hence thesis by RLVECT_1:8;
end;
Lm7: J is linear implies J.(-x) = -J.x
proof
set a = 0.K, b = 0.L, y = J.x;
A1: x+-x = a by RLVECT_1:5;
A2: y+-y = b by RLVECT_1:5;
assume
A3: J is linear;
then y+J.(-x) = J.a by A1,VECTSP_1:def 20
.= b by A3,Lm6;
hence thesis by A2,RLVECT_1:8;
end;
Lm8: J is linear implies J.(x-y) = J.x-J.y
proof
assume
A1: J is linear;
hence J.(x-y) = J.x+J.(-y) by VECTSP_1:def 20
.= J.x-J.y by A1,Lm7;
end;
theorem
J is linear implies J.(0.K) = 0.L & J.(-x) = -J.x & J.(x-y) = J.x-J.y
by Lm6,Lm7,Lm8;
Lm9: J is antilinear implies J.(0.K) = 0.L
proof
set a = 0.K;
A1: a+a = a by RLVECT_1:4;
assume J is antilinear;
then J.a+J.a = J.a by A1,VECTSP_1:def 20
.= J.a+(0.L) by RLVECT_1:4;
hence thesis by RLVECT_1:8;
end;
Lm10: J is antilinear implies J.(-x) = -J.x
proof
assume
A1: J is antilinear;
set a = 0.K, b = 0.L, y = J.x;
A2: y+-y = b by RLVECT_1:5;
x+-x = a by RLVECT_1:5;
then y+J.(-x) = J.a by A1,VECTSP_1:def 20
.= b by A1,Lm9;
hence thesis by A2,RLVECT_1:8;
end;
Lm11: J is antilinear implies J.(x-y) = J.x-J.y
proof
assume
A1: J is antilinear;
hence J.(x-y) = J.x+J.(-y) by VECTSP_1:def 20
.= J.x-J.y by A1,Lm10;
end;
theorem
J is antilinear implies J.(0.K) = 0.L & J.(-x) = -J.x & J.(x-y) = J.x-
J.y by Lm9,Lm10,Lm11;
theorem
for K being Ring holds id K is antiisomorphism iff K is comRing
proof
let K be Ring;
set J = id K;
A1: now
assume
A2: K is comRing;
A3: for x,y being Scalar of K holds J.(x*y) = J.y*J.x
by A2,Lm5;
J.(1_K) = 1_K;
hence J is antiisomorphism by A3,Th22;
end;
now
assume
A4: J is antiisomorphism;
for x,y being Element of K holds x*y = y*x
proof
let x,y be Element of K;
A5: J.y = y;
J.(x*y) = x*y & J.x = x;
hence thesis by A4,A5,Th22;
end;
hence K is comRing by GROUP_1:def 12;
end;
hence thesis by A1;
end;
theorem
for K being Skew-Field holds id K is antiisomorphism iff K is Field
proof
let K be Skew-Field;
set J = id K;
A1: now
assume
A2: K is Field;
A3: for x,y being Scalar of K holds J.(x*y) = J.y*J.x
by A2,GROUP_1:def 12;
J.(1_K) = 1_K;
hence J is antiisomorphism by A3,Th22;
end;
now
assume
A4: J is antiisomorphism;
for x,y being Scalar of K holds x*y = y*x
proof
let x,y be Scalar of K;
A5: J.y = y;
J.(x*y) = x*y & J.x = x;
hence thesis by A4,A5,Th22;
end;
hence K is Field by GROUP_1:def 12;
end;
hence thesis by A1;
end;
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
J;
coherence;
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;
Lm12:
J is linear implies opp J is additive
proof
set J9 = opp J;
assume A1: J is linear;
let x,y be Scalar of K;
thus J9.(x+y) = J.x+J.y by A1,VECTSP_1:def 20
.= J9.x+J9.y;
end;
::$CT
theorem Th27:
J is linear iff opp(J) is antilinear
proof
set J9 = opp(J), L9 = opp(L);
A1: now
assume A2: J is linear;
A3: for x,y being Scalar of K holds J9.(x*y) = J9.y*J9.x
proof
let x,y be Scalar of K;
thus J9.(x*y) = J.x*J.y by A2,GROUP_6:def 6
.= J9.y*J9.x by Lm3;
end;
J9.(1_K) = 1_L by A2,GROUP_1:def 13
.= 1_L9;
then J9 is additive antimultiplicative unity-preserving by Lm12,A3,A2;
hence J9 is antilinear;
end;
now
assume
A4: J9 is antilinear;
A5: for x,y being Scalar of K holds J.(x+y) = J.x+J.y
proof
let x,y be Scalar of K;
thus J.(x+y) = J9.x+J9.y by A4,VECTSP_1:def 20
.= J.x+J.y;
end;
A6: for x,y being Scalar of K holds J.(x*y) = J.x*J.y
proof
let x,y be Scalar of K;
thus J.(x*y) = J9.y*J9.x by A4,Def6
.= J.x*J.y by Lm3;
end;
J.(1_K) = 1_L9 by A4,GROUP_1:def 13
.= 1_L;
then J is additive multiplicative unity-preserving by A5,A6;
hence J is linear;
end;
hence thesis by A1;
end;
theorem Th28:
J is antilinear iff opp(J) is linear
proof
set J9 = opp(J), L9 = opp(L);
hereby
assume
A1: J is antilinear;
A2: J9 is additive
proof
let x,y be Scalar of K;
thus J9.(x+y) = J.x+J.y by A1,VECTSP_1:def 20
.= J9.x+J9.y;
end;
A3: J9 is multiplicative
proof
let x,y be Scalar of K;
thus J9.(x*y) = J.y*J.x by A1,Def6
.= J9.x*J9.y by Lm3;
end;
J9.(1_K) = 1_L by A1,GROUP_1:def 13
.= 1_L9;
then J9 is unity-preserving;
hence J9 is linear by A2,A3;
end;
assume
A4: J9 is additive multiplicative unity-preserving;
hereby
let x,y be Scalar of K;
thus J.(x+y) = J9.x+J9.y by A4
.= J.x+J.y;
end;
hereby
let x,y be Scalar of K;
thus J.(x*y) = J9.x*J9.y by A4
.= J.y*J.x by Lm3;
end;
thus J.(1_K) = 1_L by A4;
end;
theorem Th29:
J is monomorphism iff opp(J) is antimonomorphism by Th27;
theorem Th30:
J is antimonomorphism iff opp(J) is monomorphism by Th28;
theorem
J is epimorphism iff opp(J) is antiepimorphism by Th27;
theorem
J is antiepimorphism iff opp(J) is epimorphism by Th28;
theorem
J is isomorphism iff opp(J) is antiisomorphism by Th29;
theorem
J is antiisomorphism iff opp(J) is isomorphism by Th30;
reserve K for add-associative right_zeroed right_complementable well-unital
non empty doubleLoopStr;
reserve J for Function of K,K;
theorem
J is endomorphism iff opp(J) is antilinear by Th27;
theorem
J is antiendomorphism iff opp(J) is linear by Th28;
theorem
J is isomorphism iff opp(J) is antiisomorphism by Th29;
theorem
J is antiisomorphism iff opp(J) is isomorphism by Th30;
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;
existence
proof
take id G;
thus thesis;
end;
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;
Lm13: f.(0.G) = 0.H
proof
set a = 0.G;
a+a = a by RLVECT_1:def 4;
then f.a+f.a = f.a by VECTSP_1:def 20
.= f.a+(0.H) by RLVECT_1:def 4;
hence thesis by RLVECT_1:8;
end;
Lm14: f.(-x) = -f.x
proof
set a = 0.G, b = 0.H, y = f.x;
x+-x = a by RLVECT_1:def 10;
then y+f.(-x) = f.a by VECTSP_1:def 20
.= b by Lm13;
hence thesis by VECTSP_1:16;
end;
Lm15: f.(x-y) = f.x-f.y
proof
thus f.(x-y) = f.x+f.(-y) by VECTSP_1:def 20
.= f.x-f.y by Lm14;
end;
theorem
f.(0.G) = 0.H & f.(-x) = -f.x & f.(x-y) = f.x-f.y by Lm13,Lm14,Lm15;
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;
Lm16: for x,y being Vector of V holds ZeroMap(V,W).(x+y) = ZeroMap(V,W).x+
ZeroMap(V,W).y
proof
set f = ZeroMap(V,W);
thus for x,y being Vector of V holds f.(x+y) = f.x+f.y
proof
let x,y be Vector of V;
A1: f.y = 0.W by FUNCOP_1:7;
f.(x+y) = 0.W & f.x = 0.W by FUNCOP_1:7;
hence thesis by A1,RLVECT_1:def 4;
end;
end;
Lm17: for a being Scalar of K, x being Vector of V holds ZeroMap(V,W).(a*x) =
J.a*ZeroMap(V,W).x
proof
let a be Scalar of K, x be Vector of V;
set z = ZeroMap(V,W);
z.(a*x) = 0.W & z.(x) = 0.W by FUNCOP_1:7;
hence thesis by VECTSP_1:14;
end;
definition let K,L,J,V,W;
mode Homomorphism of J,V,W -> Function of V,W means :Def17:
(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;
existence
proof
take ZeroMap(V,W);
thus thesis by Lm16,Lm17;
end;
end;
theorem
ZeroMap(V,W) is Homomorphism of J,V,W
proof
set z = ZeroMap(V,W);
( for x,y being Vector of V holds z.(x+y) = z.x+z.y)& for a being Scalar
of K, x being Vector of V holds z.(a*x) = J.a*z.x by Lm16,Lm17;
hence thesis by Def17;
end;
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
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
proof
let f be Function of V,W;
set J = id K;
A1: (for a being Scalar of K, x being Vector of V holds f.(a*x) = a*f.x)
implies
for a be Scalar of K, x be Vector of V holds f.(a*x) = J.a*f.x;
now
assume
A2: for a being Scalar of K, x being Vector of V holds f.(a*x) = J.a*f .x;
let a be Scalar of K, x be Vector of V;
J.a = a;
hence f.(a*x) = a*f.x by A2;
end;
hence thesis by A1,Def17;
end;
definition let K,V;
mode Endomorphism of V is Homomorphism of V,V;
end;