:: On Monomorphisms and Subfields :: by Christoph Schwarzweller :: :: Received May 27, 2019 :: Copyright (c) 2019-2021 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 SUBSET, BOOLE; 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;