:: On Monomorphisms and Subfields
:: by Christoph Schwarzweller
::
:: Received May 27, 2019
:: Copyright (c) 2019 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 ARYTM_3, VECTSP_1, ALGSTR_0, STRUCT_0, SUBSET_1, SUPINF_2,
BINOP_1, TARSKI, MESFUNC1, FUNCSDOM, ZFMISC_1, EC_PF_1, RLVECT_1,
GROUP_1, FUNCT_1, RELAT_1, LATTICES, REALSET1, XBOOLE_0, NUMBERS, RING_3,
VECTSP_2, FUNCT_2, ARYTM_1, MSSUBFAM, MOD_4, QUOFIELD, GROUP_2, WELLORD1,
GROEB_2, FIELD_2, C0SP1, FDIFF_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELSET_1, REALSET1,
PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, VECTSP_1, VECTSP_2, QUOFIELD,
TSEP_1, MOD_4, GROUP_1, GROUP_6, ALGSTR_0, ALGSTR_1, RLVECT_1, RINGCAT1,
C0SP1, EC_PF_1, RING_2, RING_3;
constructors FUNCT_2, FUNCT_1, XBOOLE_0, RELSET_1, REALSET1, STRUCT_0,
QUOFIELD, RLVECT_1, RINGCAT1, RING_3, C0SP1, EC_PF_1, TSEP_1;
registrations XBOOLE_0, RELSET_1, STRUCT_0, VECTSP_1, ALGSTR_0, REALSET1,
RLVECT_1, QUOFIELD, FUNCT_1, FUNCT_2, RELAT_1, MOD_4, RINGCAT1, RING_3;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
begin
reserve R for Ring, S for R-monomorphic Ring,
K for Field, F for K-monomorphic Field,
T for K-monomorphic comRing;
definition
let R,S;
let f be Monomorphism of R,S;
redefine func f" -> Function of rng f,R;
end;
theorem :: FIELD_2:1
for f being Monomorphism of R,S, a,b being Element of rng f
holds f".(a+b) = f".a + f".b & f".(a*b) = f".a * f".b;
theorem :: FIELD_2:2
for f being Monomorphism of R,S, a being Element of rng f
holds f".(a) = 0.R iff a = 0.S;
theorem :: FIELD_2:3
for f being Monomorphism of R,S holds f".(1.S) = 1.R & f".(0.S) = 0.R;
theorem :: FIELD_2:4
for f being Monomorphism of R,S holds f" is one-to-one onto;
theorem :: FIELD_2:5
for f being Monomorphism of R,S, a being Element of R
holds f.a = 0.S iff a = 0.R;
theorem :: FIELD_2:6
for f being Monomorphism of K,F,a being Element of K
st a <> 0.K holds f.(a") = (f.a)";
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,S are_disjoint means
:: FIELD_2:def 1
[#]R /\ [#]S = {};
end;
definition
let R,S;
let f be Monomorphism of R,S;
func carr f -> non empty set equals
:: FIELD_2:def 2
([#]S \ rng f) \/ [#]R;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::::::::: f: R >--> S,
::::::::: addemb(f,x,y): R x R -> (S\ rng f) \/ R
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let R be Ring, 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
:: 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);
end;
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
:: FIELD_2:def 4
for a,b being Element of carr f holds it.(a,b) = addemb(f,a,b);
end;
definition
let K be Field, 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
:: 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);
end;
definition
let K be Field, T be K-monomorphic comRing;
let f be Monomorphism of K,T;
func multemb f -> BinOp of carr f means
:: FIELD_2:def 6
for a,b being Element of carr f holds it.(a,b) = multemb(f,a,b);
end;
definition
let K be Field, T be K-monomorphic comRing;
let f be Monomorphism of K,T;
func embField f -> strict doubleLoopStr means
:: 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;
end;
registration
let K be Field,
T be K-monomorphic comRing;
let f be Monomorphism of K,T;
cluster embField f -> non degenerated;
end;
registration
let K be Field,
T be K-monomorphic comRing;
let f be Monomorphism of K,T;
cluster embField f -> Abelian right_zeroed;
end;
theorem :: FIELD_2:7
for f being Monomorphism of K,T st K,T are_disjoint
holds embField f is add-associative;
theorem :: FIELD_2:8
for f being Monomorphism of K,T st K,T are_disjoint
holds embField f is right_complementable;
registration
let K be Field,
T be K-monomorphic comRing;
let f be Monomorphism of K,T;
cluster embField f -> commutative well-unital;
end;
theorem :: FIELD_2:9
for f being Monomorphism of K,F st K,F are_disjoint
holds embField f is associative;
theorem :: FIELD_2:10
for f being Monomorphism of K,T st K,T are_disjoint
holds embField f is distributive;
theorem :: FIELD_2:11
for f being Monomorphism of K,F st K,F are_disjoint
holds embField f is almost_left_invertible;
theorem :: FIELD_2:12
for f being Monomorphism of K,F st K,F are_disjoint holds
embField f is Field;
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
:: 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);
end;
registration
let K be Field,
F be K-monomorphic Field;
let f be Monomorphism of K,F;
cluster emb_iso f -> unity-preserving;
end;
theorem :: FIELD_2:13
for f being Monomorphism of K,F st K,F are_disjoint
holds emb_iso f is additive;
theorem :: FIELD_2:14
for f being Monomorphism of K,F st K,F are_disjoint
holds emb_iso f is multiplicative;
registration
let K be Field,
F be K-monomorphic Field;
let f be Monomorphism of K,F;
cluster emb_iso f -> one-to-one;
end;
theorem :: FIELD_2:15
for f being Monomorphism of K,F st K,F are_disjoint holds
emb_iso f is onto;
theorem :: FIELD_2:16
for f being Monomorphism of K,F st K,F are_disjoint
holds F, embField f are_isomorphic;
theorem :: FIELD_2:17
for f being Monomorphism of K,F, E being Field st E = embField f holds
K is Subfield of E;
theorem :: FIELD_2:18
K,F are_disjoint implies
ex E being Field st E,F are_isomorphic & K is Subfield of E;
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;