FIELD_2: On Monomorphisms and Subfields

:: On Monomorphisms and Subfields
:: by Christoph Schwarzweller
::
:: Received May 27, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users

definition

let R be Ring;
let S be R -monomorphic Ring;
let f be Monomorphism of R,S;
:: original: "
redefine func f " -> Function of (rng f),R;
coherence

proof end;

end;

theorem Th1: :: FIELD_2:1

for R being Ring
for S being b₁ -monomorphic Ring
for f being Monomorphism of R,S
for a, b being Element of rng f holds
( (f ") . (a + b) = ((f ") . a) + ((f ") . b) & (f ") . (a * b) = ((f ") . a) * ((f ") . b) )

proof end;

theorem Th2: :: FIELD_2:2

for R being Ring
for S being b₁ -monomorphic Ring
for f being Monomorphism of R,S
for a being Element of rng f holds
( (f ") . a = 0. R iff a = 0. S )

proof end;

theorem Th3: :: FIELD_2:3

for R being Ring
for S being b₁ -monomorphic Ring
for f being Monomorphism of R,S holds
( (f ") . (1. S) = 1. R & (f ") . (0. S) = 0. R )

proof end;

theorem :: FIELD_2:4

for R being Ring
for S being b₁ -monomorphic Ring
for f being Monomorphism of R,S holds
( f " is one-to-one & f " is onto )

proof end;

theorem Th4: :: FIELD_2:5

for R being Ring
for S being b₁ -monomorphic Ring
for f being Monomorphism of R,S
for a being Element of R holds
( f . a = 0. S iff a = 0. R )

proof end;

theorem Th5: :: FIELD_2:6

for K being Field
for F being b₁ -monomorphic Field
for f being Monomorphism of K,F
for a being Element of K st a <> 0. K holds
f . (a ") = (f . a) "

proof end;

notation

let R, S be Ring;
synonym R,S are_disjoint for R misses S;

end;

definition

let R, S be Ring;

redefine pred R misses S means :: FIELD_2:def 1
([#] R) /\ ([#] S) = {} ;

compatibility by TSEP_1:def 3, XBOOLE_0:def 7;

end;

:: deftheorem defines are_disjoint FIELD_2:def 1 :

definition

let R be Ring;
let S be R -monomorphic Ring;
let f be Monomorphism of R,S;

func carr f -> non empty set equals :: FIELD_2:def 2
(([#] S) \ (rng f)) \/ ([#] R);

coherence ;

end;

:: deftheorem defines carr FIELD_2:def 2 :

Lm1: for R being Ring
for S being b₁ -monomorphic Ring
for f being Monomorphism of R,S
for a being Element of carr f st not a in [#] R holds
( a in [#] S & not a in rng f )

proof end;

Lm2: for R being Ring
for S being b₁ -monomorphic Ring
for f being Monomorphism of R,S
for a, b being Element of carr f st not a in [#] R & b in [#] R holds
the addF of S . (a,(f . b)) in ([#] S) \ (rng f)

proof end;

Lm3: for R being Ring
for S being b₁ -monomorphic Ring
for f being Monomorphism of R,S
for a, b being Element of carr f st a in [#] R & not b in [#] R holds
the addF of S . ((f . a),b) in ([#] S) \ (rng f)

proof end;

Lm4: for K being Field
for T being b₁ -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of carr f st not a in [#] K & b in [#] K & b <> 0. K holds
the multF of T . (a,(f . b)) in ([#] T) \ (rng f)

proof end;

Lm5: for K being Field
for T being b₁ -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of carr f st not b in [#] K & a in [#] K & a <> 0. K holds
the multF of T . ((f . a),b) in ([#] T) \ (rng f)

proof end;

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::::::::: f: R >--> S,
::::::::: addemb(f,x,y): R x R -> (S\ rng f) \/ R
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition

let R be Ring;
let S be R -monomorphic Ring;
let f be Monomorphism of R,S;
let a, b be Element of carr f;

func addemb (f,a,b) -> Element of carr f equals :defaddf: :: FIELD_2:def 3
the addF of R . (a,b) if ( a in [#] R & b in [#] R )
the addF of S . ((f . a),b) if ( a in [#] R & not b in [#] R )
the addF of S . (a,(f . b)) if ( b in [#] R & not a in [#] R )
(f ") . ( the addF of S . (a,b)) if ( not a in [#] R & not b in [#] R & the addF of S . (a,b) in rng f )
otherwise the addF of S . (a,b);

coherence

proof end;

consistency ;

end;

:: deftheorem defaddf defines addemb FIELD_2:def 3 :

definition

let R be Ring;
let S be R -monomorphic Ring;
let f be Monomorphism of R,S;

func addemb f -> BinOp of (carr f) means :defadd: :: FIELD_2:def 4
for a, b being Element of carr f holds it . (a,b) = addemb (f,a,b);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defadd defines addemb FIELD_2:def 4 :

definition

let K be Field;
let T be K -monomorphic comRing;
let f be Monomorphism of K,T;
let a, b be Element of carr f;

func multemb (f,a,b) -> Element of carr f equals :defmultf: :: FIELD_2:def 5
the multF of K . (a,b) if ( a in [#] K & b in [#] K )
0. K if ( a = 0. K or b = 0. K )
the multF of T . ((f . a),b) if ( a in [#] K & a <> 0. K & not b in [#] K )
the multF of T . (a,(f . b)) if ( b in [#] K & b <> 0. K & not a in [#] K )
(f ") . ( the multF of T . (a,b)) if ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f )
otherwise the multF of T . (a,b);

coherence

proof end;

consistency

proof end;

end;

:: deftheorem defmultf defines multemb FIELD_2:def 5 :

definition

let K be Field;
let T be K -monomorphic comRing;
let f be Monomorphism of K,T;

func multemb f -> BinOp of (carr f) means :defmult: :: FIELD_2:def 6
for a, b being Element of carr f holds it . (a,b) = multemb (f,a,b);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defmult defines multemb FIELD_2:def 6 :

definition

let K be Field;
let T be K -monomorphic comRing;
let f be Monomorphism of K,T;

func embField f -> strict doubleLoopStr means :defemb: :: FIELD_2:def 7
( the carrier of it = carr f & the addF of it = addemb f & the multF of it = multemb f & the OneF of it = 1. K & the ZeroF of it = 0. K );

existence

proof end;

uniqueness ;

end;

:: deftheorem defemb defines embField FIELD_2:def 7 :

registration

let K be Field;
let T be K -monomorphic comRing;
let f be Monomorphism of K,T;

cluster embField f -> non degenerated strict ;

coherence

proof end;

end;

Lm6: for K being Field
for T being b₁ -monomorphic comRing
for f being Monomorphism of K,T st K,T are_disjoint holds
for a, b being Element of (embField f) st a in [#] K & not b in [#] K holds
for a1, b1 being Element of carr f st a1 = a & b1 = b holds
( a + b = the addF of T . ((f . a1),b1) & b + a = the addF of T . (b1,(f . a1)) & not a + b in [#] K & not b + a in [#] K )

proof end;

Lm7: for K being Field
for T being b₁ -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of (embField f)
for a1, b1 being Element of K st a1 = a & b1 = b holds
( a + b = a1 + b1 & b + a = b1 + a1 )

proof end;

Lm8: for K being Field
for T being b₁ -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of (embField f)
for a1, b1 being Element of T st K,T are_disjoint & not a in [#] K & not b in [#] K & not the addF of T . (a,b) in rng f & a1 = a & b1 = b holds
( a + b = a1 + b1 & b + a = b1 + a1 & not a + b in [#] K & not b + a in [#] K )

proof end;

Lm9: for K being Field
for T being b₁ -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of (embField f)
for a1, b1 being Element of T st not a in [#] K & not b in [#] K & the addF of T . (a,b) in rng f & a1 = a & b1 = b holds
( a + b = (f ") . (a1 + b1) & b + a = (f ") . (b1 + a1) & a + b in [#] K & b + a in [#] K )

proof end;

Lm10: for K being Field
for T being b₁ -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of (embField f)
for a1, b1 being Element of carr f st K,T are_disjoint & a in [#] K & a <> 0. K & not b in [#] K & a1 = a & b1 = b holds
( a * b = the multF of T . ((f . a1),b1) & b * a = the multF of T . (b1,(f . a1)) & not a * b in [#] K & not b * a in [#] K )

proof end;

Lm11: for K being Field
for T being b₁ -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of (embField f)
for a1, b1 being Element of K st a1 = a & b1 = b holds
( a * b = a1 * b1 & b * a = b1 * a1 )

proof end;

Lm12: for K being Field
for T being b₁ -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of (embField f)
for a1, b1 being Element of T st K,T are_disjoint & not a in [#] K & not b in [#] K & not the multF of T . (a,b) in rng f & a1 = a & b1 = b holds
( a * b = a1 * b1 & b * a = b1 * a1 & not a * b in [#] K & not b * a in [#] K )

proof end;

Lm13: for K being Field
for T being b₁ -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of (embField f)
for a1, b1 being Element of T st not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f & a1 = a & b1 = b holds
( a * b = (f ") . (a1 * b1) & b * a = (f ") . (b1 * a1) & a * b in [#] K & b * a in [#] K )

proof end;

registration

let K be Field;
let T be K -monomorphic comRing;
let f be Monomorphism of K,T;

cluster embField f -> strict Abelian right_zeroed ;

coherence

proof end;

end;

theorem Th6: :: FIELD_2:7

for K being Field
for T being b₁ -monomorphic comRing
for f being Monomorphism of K,T st K,T are_disjoint holds
embField f is add-associative

proof end;

theorem Th7: :: FIELD_2:8

for K being Field
for T being b₁ -monomorphic comRing
for f being Monomorphism of K,T st K,T are_disjoint holds
embField f is right_complementable

proof end;

registration

let K be Field;
let T be K -monomorphic comRing;
let f be Monomorphism of K,T;

cluster embField f -> strict commutative well-unital ;

coherence

proof end;

end;

theorem Th8: :: FIELD_2:9

for K being Field
for F being b₁ -monomorphic Field
for f being Monomorphism of K,F st K,F are_disjoint holds
embField f is associative

proof end;

theorem Th9: :: FIELD_2:10

for K being Field
for T being b₁ -monomorphic comRing
for f being Monomorphism of K,T st K,T are_disjoint holds
embField f is distributive

proof end;

theorem Th10: :: FIELD_2:11

for K being Field
for F being b₁ -monomorphic Field
for f being Monomorphism of K,F st K,F are_disjoint holds
embField f is almost_left_invertible

proof end;

theorem :: FIELD_2:12

for K being Field
for F being b₁ -monomorphic Field
for f being Monomorphism of K,F st K,F are_disjoint holds
embField f is Field by Th6, Th8, Th9, Th7, Th10;

definition

let K be Field;
let F be K -monomorphic Field;
let f be Monomorphism of K,F;

func emb_iso f -> Function of (embField f),F means :defiso: :: FIELD_2:def 8
( ( for a being Element of (embField f) st not a in K holds
it . a = a ) & ( for a being Element of (embField f) st a in K holds
it . a = f . a ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defiso defines emb_iso FIELD_2:def 8 :

registration

let K be Field;
let F be K -monomorphic Field;
let f be Monomorphism of K,F;

cluster emb_iso f -> unity-preserving ;

coherence

proof end;

end;

theorem Th11: :: FIELD_2:13

for K being Field
for F being b₁ -monomorphic Field
for f being Monomorphism of K,F st K,F are_disjoint holds
emb_iso f is additive

proof end;

theorem Th12: :: FIELD_2:14

for K being Field
for F being b₁ -monomorphic Field
for f being Monomorphism of K,F st K,F are_disjoint holds
emb_iso f is multiplicative

proof end;

registration

let K be Field;
let F be K -monomorphic Field;
let f be Monomorphism of K,F;

cluster emb_iso f -> one-to-one ;

coherence

proof end;

end;

theorem Th13: :: FIELD_2:15

for K being Field
for F being b₁ -monomorphic Field
for f being Monomorphism of K,F st K,F are_disjoint holds
emb_iso f is onto

proof end;

theorem Th14: :: FIELD_2:16

for K being Field
for F being b₁ -monomorphic Field
for f being Monomorphism of K,F st K,F are_disjoint holds
F, embField f are_isomorphic

proof end;

theorem Th15: :: FIELD_2:17

for K being Field
for F being b₁ -monomorphic Field
for f being Monomorphism of K,F
for E being Field st E = embField f holds
K is Subfield of E

proof end;

theorem Th16: :: FIELD_2:18

for K being Field
for F being b₁ -monomorphic Field st K,F are_disjoint holds
ex E being Field st
( E,F are_isomorphic & K is Subfield of E )

proof end;

theorem :: FIELD_2:19

for K, F being Field st K,F are_disjoint holds
( F is K -monomorphic iff ex E being Field st
( E,F are_isomorphic & K is Subfield of E ) )

proof end;