:: Embedding Principle for Rings and Abelian Groups
:: by Yasushige Watase
::
:: Received November 21, 2023
:: Copyright (c) 2023-2025 Association of Mizar Users

theorem Th1: :: RING_EMB:1

for a being non empty set ex b being object st
for x being set holds not [x,b] in a

proof end;

theorem Th2: :: RING_EMB:2

for a, b being non empty set ex c being non empty set st
( a /\ c = {} & ex f being Function st
( f is one-to-one & dom f = b & rng f = c ) )

proof end;

:: Apply Embedding Principle to Rings.

theorem Th3: :: RING_EMB:3

for A being Ring
for X being non empty set
for f being Function of A,X
for a, b being Element of X st f is bijective holds
f . ( the addF of A . (((f ") . a),((f ") . b))) is Element of X

proof end;

definition

let A be Ring;
let X be non empty set ;
let f be Function of A,X;
let a, b be Element of X;
assume A1: f is bijective ;

func addemb (f,a,b) -> Element of X equals :Def1: :: RING_EMB:def 1
f . ( the addF of A . (((f ") . a),((f ") . b)));

coherence
f . ( the addF of A . (((f ") . a),((f ") . b))) is Element of X by A1, Th3;

end;

:: deftheorem Def1 defines addemb RING_EMB:def 1 :
for A being Ring
for X being non empty set
for f being Function of A,X
for a, b being Element of X st f is bijective holds
addemb (f,a,b) = f . ( the addF of A . (((f ") . a),((f ") . b)));

theorem Th4: :: RING_EMB:4

for A being Ring
for X being non empty set
for f being Function of A,X
for a, b, c being Element of X st f is bijective holds
addemb (f,a,(addemb (f,b,c))) = addemb (f,(addemb (f,a,b)),c)

proof end;

definition

let A be Ring;
let X be non empty set ;
let f be Function of A,X;

func addemb f -> BinOp of X means :Def2: :: RING_EMB:def 2
for a, b being Element of X holds it . (a,b) = addemb (f,a,b);

existence
ex b₁ being BinOp of X st
for a, b being Element of X holds b₁ . (a,b) = addemb (f,a,b)

proof end;

uniqueness
for b₁, b₂ being BinOp of X st ( for a, b being Element of X holds b₁ . (a,b) = addemb (f,a,b) ) & ( for a, b being Element of X holds b₂ . (a,b) = addemb (f,a,b) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines addemb RING_EMB:def 2 :
for A being Ring
for X being non empty set
for f being Function of A,X
for b₄ being BinOp of X holds
( b₄ = addemb f iff for a, b being Element of X holds b₄ . (a,b) = addemb (f,a,b) );

theorem Th5: :: RING_EMB:5

for A being Ring
for X being non empty set
for f being Function of A,X
for a, b being Element of X st f is bijective holds
f . ( the multF of A . (((f ") . a),((f ") . b))) is Element of X

proof end;

definition

let A be Ring;
let X be non empty set ;
let f be Function of A,X;
let a, b be Element of X;
assume A1: f is bijective ;

func multemb (f,a,b) -> Element of X equals :Def3: :: RING_EMB:def 3
f . ( the multF of A . (((f ") . a),((f ") . b)));

coherence
f . ( the multF of A . (((f ") . a),((f ") . b))) is Element of X by Th5, A1;

end;

:: deftheorem Def3 defines multemb RING_EMB:def 3 :
for A being Ring
for X being non empty set
for f being Function of A,X
for a, b being Element of X st f is bijective holds
multemb (f,a,b) = f . ( the multF of A . (((f ") . a),((f ") . b)));

definition

let A be Ring;
let X be non empty set ;
let f be Function of A,X;

func multemb f -> BinOp of X means :Def4: :: RING_EMB:def 4
for a, b being Element of X holds it . (a,b) = multemb (f,a,b);

existence
ex b₁ being BinOp of X st
for a, b being Element of X holds b₁ . (a,b) = multemb (f,a,b)

proof end;

uniqueness
for b₁, b₂ being BinOp of X st ( for a, b being Element of X holds b₁ . (a,b) = multemb (f,a,b) ) & ( for a, b being Element of X holds b₂ . (a,b) = multemb (f,a,b) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines multemb RING_EMB:def 4 :
for A being Ring
for X being non empty set
for f being Function of A,X
for b₄ being BinOp of X holds
( b₄ = multemb f iff for a, b being Element of X holds b₄ . (a,b) = multemb (f,a,b) );

definition

let A be Ring;
let X be non empty set ;
let f be Function of A,X;

func emb_Ring f -> non empty strict doubleLoopStr equals :: RING_EMB:def 5
doubleLoopStr(# X,(addemb f),(multemb f),(f . (1. A)),(f . (0. A)) #);

coherence
doubleLoopStr(# X,(addemb f),(multemb f),(f . (1. A)),(f . (0. A)) #) is non empty strict doubleLoopStr ;

end;

:: deftheorem defines emb_Ring RING_EMB:def 5 :
for A being Ring
for X being non empty set
for f being Function of A,X holds emb_Ring f = doubleLoopStr(# X,(addemb f),(multemb f),(f . (1. A)),(f . (0. A)) #);

theorem Th6: :: RING_EMB:6

for A being Ring
for X being non empty set
for f being Function of A,X st f is bijective holds
emb_Ring f is Ring

proof end;

theorem :: RING_EMB:7

for A being comRing
for X being non empty set
for f being Function of A,X st f is bijective holds
emb_Ring f is comRing

proof end;

theorem Th8: :: RING_EMB:8

for A, B being Ring
for i being Function of A,B st i is RingHomomorphism & i = id A holds
A is Subring of B

proof end;

theorem Th9: :: RING_EMB:9

for A, B being Ring
for f being Function of A,B st f is monomorphism & ([#] B) \ (rng f) <> {} holds
ex C being Ring ex X being set ex h being Function ex G being Function of B,C st
( X /\ ([#] A) = {} & h is one-to-one & dom h = ([#] B) \ (rng f) & rng h = X & [#] C = X \/ ([#] A) & A is Subring of C & G is RingIsomorphism & id A = G * f )

proof end;

:: Embedding Principle Applied to AbGroups.

definition

let G be AbGroup;

mode SubAbGr of G -> AbGroup means :Def6: :: RING_EMB:def 6
( the carrier of it c= the carrier of G & the addF of it = the addF of G || the carrier of it & 0. it = 0. G );

existence
ex b₁ being AbGroup st
( the carrier of b₁ c= the carrier of G & the addF of b₁ = the addF of G || the carrier of b₁ & 0. b₁ = 0. G )

proof end;

end;

:: deftheorem Def6 defines SubAbGr RING_EMB:def 6 :
for G, b₂ being AbGroup holds
( b₂ is SubAbGr of G iff ( the carrier of b₂ c= the carrier of G & the addF of b₂ = the addF of G || the carrier of b₂ & 0. b₂ = 0. G ) );

Lm1: for R, S being AbGroup
for f being Homomorphism of R,S holds 0. S in rng f

proof end;

Lm2: for R, S being AbGroup
for f being Homomorphism of R,S holds rng f is Preserv of the addF of S

proof end;

definition

let G, H be AbGroup;
let f be Homomorphism of G,H;

func Image f -> strict addLoopStr means :: RING_EMB:def 7
( the carrier of it = rng f & the addF of it = the addF of H || (rng f) & the ZeroF of it = 0. H );

existence
ex b₁ being strict addLoopStr st
( the carrier of b₁ = rng f & the addF of b₁ = the addF of H || (rng f) & the ZeroF of b₁ = 0. H )

proof end;

uniqueness
for b₁, b₂ being strict addLoopStr st the carrier of b₁ = rng f & the addF of b₁ = the addF of H || (rng f) & the ZeroF of b₁ = 0. H & the carrier of b₂ = rng f & the addF of b₂ = the addF of H || (rng f) & the ZeroF of b₂ = 0. H holds
b₁ = b₂ ;

end;

:: deftheorem defines Image RING_EMB:def 7 :
for G, H being AbGroup
for f being Homomorphism of G,H
for b₄ being strict addLoopStr holds
( b₄ = Image f iff ( the carrier of b₄ = rng f & the addF of b₄ = the addF of H || (rng f) & the ZeroF of b₄ = 0. H ) );

theorem Th10: :: RING_EMB:10

for A being AbGroup
for X being non empty set
for f being Function of A,X
for a, b being Element of X st f is bijective holds
f . ( the addF of A . (((f ") . a),((f ") . b))) is Element of X

proof end;

definition

let A be AbGroup;
let X be non empty set ;
let f be Function of A,X;
let a, b be Element of X;
assume A1: f is bijective ;

func addemb (f,a,b) -> Element of X equals :Def8: :: RING_EMB:def 8
f . ( the addF of A . (((f ") . a),((f ") . b)));

coherence
f . ( the addF of A . (((f ") . a),((f ") . b))) is Element of X by A1, Th10;

end;

:: deftheorem Def8 defines addemb RING_EMB:def 8 :
for A being AbGroup
for X being non empty set
for f being Function of A,X
for a, b being Element of X st f is bijective holds
addemb (f,a,b) = f . ( the addF of A . (((f ") . a),((f ") . b)));

theorem Th11: :: RING_EMB:11

for A being AbGroup
for X being non empty set
for f being Function of A,X
for a, b, c being Element of X st f is bijective holds
addemb (f,a,(addemb (f,b,c))) = addemb (f,(addemb (f,a,b)),c)

proof end;

definition

let A be AbGroup;
let X be non empty set ;
let f be Function of A,X;

func addemb f -> BinOp of X means :Def9: :: RING_EMB:def 9
for a, b being Element of X holds it . (a,b) = addemb (f,a,b);

existence
ex b₁ being BinOp of X st
for a, b being Element of X holds b₁ . (a,b) = addemb (f,a,b)

proof end;

uniqueness
for b₁, b₂ being BinOp of X st ( for a, b being Element of X holds b₁ . (a,b) = addemb (f,a,b) ) & ( for a, b being Element of X holds b₂ . (a,b) = addemb (f,a,b) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines addemb RING_EMB:def 9 :
for A being AbGroup
for X being non empty set
for f being Function of A,X
for b₄ being BinOp of X holds
( b₄ = addemb f iff for a, b being Element of X holds b₄ . (a,b) = addemb (f,a,b) );

definition

let A be AbGroup;
let X be non empty set ;
let f be Function of A,X;

func emb_AbGr f -> non empty strict addLoopStr equals :: RING_EMB:def 10
addLoopStr(# X,(addemb f),(f . (0. A)) #);

coherence
addLoopStr(# X,(addemb f),(f . (0. A)) #) is non empty strict addLoopStr ;

end;

:: deftheorem defines emb_AbGr RING_EMB:def 10 :
for A being AbGroup
for X being non empty set
for f being Function of A,X holds emb_AbGr f = addLoopStr(# X,(addemb f),(f . (0. A)) #);

theorem Th12: :: RING_EMB:12

for A being AbGroup
for X being non empty set
for f being Function of A,X st f is bijective holds
emb_AbGr f is AbGroup

proof end;

theorem Th13: :: RING_EMB:13

for A, B being AbGroup
for i being Homomorphism of A,B st i = id A holds
A is SubAbGr of B

proof end;

theorem :: RING_EMB:14

for A, B being AbGroup
for f being Homomorphism of A,B st f is one-to-one & ([#] B) \ (rng f) <> {} holds
ex C being AbGroup ex X being set ex h being Function ex G being Function of B,C st
( X /\ ([#] A) = {} & h is one-to-one & dom h = ([#] B) \ (rng f) & rng h = X & [#] C = X \/ ([#] A) & A is SubAbGr of C & G is Homomorphism of B,C & id A = G * f )

proof end;

:: Relation with Polynomial Rings

theorem Th15: :: RING_EMB:15

for b being bag of 0 holds
( dom b = {} & b = EmptyBag {} & rng b = 0 & EmptyBag {} = {} --> 0 & Bags {} = {(EmptyBag {})} )

proof end;

theorem :: RING_EMB:16

for R being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for f being Polynomial of 0,R holds
( dom f = Bags 0 & Bags 0 = {{}} & rng f = {(f . (EmptyBag 0))} )

proof end;

theorem Th17: :: RING_EMB:17

for R being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for f being Polynomial of 0,R holds f is Constant

proof end;

theorem :: RING_EMB:18

for R being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for f being Polynomial of 0,R ex a being Element of R st f = a | (0,R)

proof end;

definition

let R be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ;

func 1_1 R -> sequence of R equals :: RING_EMB:def 11
(0_. R) +* (1,(1. R));

coherence
(0_. R) +* (1,(1. R)) is sequence of R ;

end;

:: deftheorem defines 1_1 RING_EMB:def 11 :
for R being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr holds 1_1 R = (0_. R) +* (1,(1. R));

theorem :: RING_EMB:19

for R being non degenerated comRing holds Support (1_1 R) = {1}

proof end;

registration

let R be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ;

cluster 1_1 R -> finite-Support ;

coherence
1_1 R is finite-Support ;

end;

theorem Th20: :: RING_EMB:20

for R being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr holds Leading-Monomial (1_1 R) = 1_1 R

proof end;

theorem :: RING_EMB:21

for R being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for m being Element of R holds eval ((1_1 R),m) = m

proof end;

theorem Th22: :: RING_EMB:22

for R being non degenerated comRing
for p0 being Element of (Polynom-Ring (0,R)) holds p0 is not Polynomial of (Polynom-Ring (0,R))

proof end;

theorem :: RING_EMB:23

for R being non degenerated comRing holds Polynom-Ring (Polynom-Ring (0,R)), Polynom-Ring (1,R) are_isomorphic

proof end;

::ThQ3:
:: for R being non degenerated comRing holds
:: Polynom-Ring(1,R),Polynom-Ring R are_isomorphic
:: proof
:: let R being non degenerated comRing;
:: BSPoly(R) is RingIsomorphism;
:: hence thesis by QUOFIELD:def 23;
:: end;
::ThQ4:
:: for R being non degenerated comRing holds
:: Polynom-Ring(Polynom-Ring(0,R)),Polynom-Ring R are_isomorphic
:: proof
:: let R being non degenerated comRing;
::A1: Polynom-Ring (Polynom-Ring(0,R)),Polynom-Ring(1,R) are_isomorphic by ThQ1;
:: Polynom-Ring(1,R),Polynom-Ring R are_isomorphic by ThQ3;
:: hence thesis by A1,RING_3:44;
:: end;

theorem Th24: :: RING_EMB:24

for R being non degenerated Ring holds ([#] (Polynom-Ring R)) \ (rng (canHom R)) <> {}

proof end;

theorem Th25: :: RING_EMB:25

for R being non degenerated Ring ex PR being non degenerated Ring ex X being set ex h being Function ex G being Function of (Polynom-Ring R),PR st
( R is Subring of PR & G is RingIsomorphism & id R = G * (canHom R) & X /\ ([#] R) = {} & h is one-to-one & dom h = ([#] (Polynom-Ring R)) \ (rng (canHom R)) & rng h = X & [#] PR = X \/ ([#] R) )

proof end;

theorem :: RING_EMB:26

for R being non degenerated comRing holds ([#] (Polynom-Ring (0,R))) /\ ([#] (Polynom-Ring (Polynom-Ring (0,R)))) = {}

proof end;

theorem :: RING_EMB:27

for R being non degenerated Ring ex PR being non degenerated Ring ex X being set ex h being Function ex G being Function of (Polynom-Ring (Polynom-Ring (0,R))),PR st
( Polynom-Ring (0,R) is Subring of PR & G is RingIsomorphism & id (Polynom-Ring (0,R)) = G * (canHom (Polynom-Ring (0,R))) & X /\ ([#] (Polynom-Ring (0,R))) = {} & h is one-to-one & dom h = ([#] (Polynom-Ring (Polynom-Ring (0,R)))) \ (rng (canHom (Polynom-Ring (0,R)))) & rng h = X & [#] PR = X \/ ([#] (Polynom-Ring (0,R))) ) by Th25;

definition

let R be non degenerated comRing;
let A be R -monomorphic comRing;
let x be Element of A;

attr x is indeterminate means :: RING_EMB:def 12
ex g being Function of (Polynom-Ring R),A st
( g is isomorphism & x = g . (1_1 R) );

end;

:: deftheorem defines indeterminate RING_EMB:def 12 :
for R being non degenerated comRing
for A being b₁ -monomorphic comRing
for x being Element of A holds
( x is indeterminate iff ex g being Function of (Polynom-Ring R),A st
( g is isomorphism & x = g . (1_1 R) ) );

theorem :: RING_EMB:28

for R being non degenerated comRing ex X being Element of (Polynom-Ring R) st
( X is indeterminate & X = 1_1 R )

proof end;