:: Valuation Theory, Part {I} :: by Grzegorz Bancerek , Hidetsune Kobayashi and Artur Korni{\l}owicz :: :: Received April 7, 2011 :: Copyright (c) 2011-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 INT_1, VECTSP_1, FUNCT_1, ARYTM_3, ZFMISC_1, RELAT_1, RLVECT_1, FUNCOP_1, ARYTM_1, BINOP_1, FUNCSDOM, REALSET1, LATTICES, GROUP_1, ORDINAL2, IDEAL_1, FINSEQ_1, SUBSET_1, VECTSP_2, FUNCT_3, NUMBERS, GROUP_4, STRUCT_0, RLSUB_1, XXREAL_2, ALGSTR_0, XCMPLX_0, REALSET2, NAT_1, REAL_1, INT_2, XXREAL_0, TARSKI, XREAL_0, XBOOLE_0, NEWTON, CARD_FIL, RMOD_2, CARD_1, SUPINF_2, MESFUNC1, PARTFUN1, COMPLEX1, MEMBERED, MSSUBFAM, FVALUAT1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, XXREAL_0, XREAL_0, XXREAL_2, XXREAL_3, XCMPLX_0, REAL_1, INT_1, MEMBERED, SUPINF_2, EXTREAL1, INT_2, MESFUNC1, FINSEQ_1, FINSEQ_4, REALSET1, BINOP_1, STRUCT_0, ALGSTR_0, RLVECT_1, GRCAT_1, GROUP_1, YELLOW_9, VECTSP_1, VECTSP_2, REALSET2, RMOD_2, IDEAL_1, RING_1; constructors REAL_1, FINSEQ_4, SUPINF_2, EXTREAL1, MESFUNC1, RMOD_2, YELLOW_9, RING_1, BINOM, FUNCOP_1, REALSET2, RELSET_1, GRCAT_1, NEWTON; registrations RELSET_1, VECTSP_1, INT_1, XREAL_0, ALGSTR_1, VECTSP_2, STRUCT_0, NAT_1, SUBSET_1, WAYBEL_2, XBOOLE_0, RMOD_2, XCMPLX_0, IDEAL_1, RING_1, XXREAL_0, NUMBERS, MEMBERED, ORDINAL1, ALGSTR_0, XXREAL_3, REALSET2, FINSEQ_1; requirements NUMERALS, ARITHM, REAL, BOOLE, SUBSET; begin :: Extended reals reserve x, y, z, s for ExtReal; reserve i, j for Integer; reserve n, m for Nat; theorem :: FVALUAT1:1 x = -x implies x = 0; theorem :: FVALUAT1:2 x + x = 0 implies x = 0; theorem :: FVALUAT1:3 0 <= x & x <= y & 0 <= s & s <= z implies x*s <= y*z; theorem :: FVALUAT1:4 y <> +infty & 0 < x & 0 < y implies 0 < x / y; theorem :: FVALUAT1:5 y <> +infty & x < 0 & 0 < y implies x / y < 0; theorem :: FVALUAT1:6 y <> -infty & 0 < x & y < 0 implies x / y < 0; theorem :: FVALUAT1:7 x in REAL & y in REAL or z in REAL implies (x + y) / z = x/z + y/z; theorem :: FVALUAT1:8 y <> +infty & y <> -infty & y <> 0 implies x / y * y = x; theorem :: FVALUAT1:9 y <> -infty & y <> +infty & x <> 0 & y <> 0 implies x / y <> 0; definition let x be object; attr x is ext-integer means :: FVALUAT1:def 1 x is integer or x = +infty; end; registration cluster ext-integer -> ext-real for object; end; registration cluster +infty -> ext-integer; cluster -infty -> non ext-integer; cluster 1. -> ext-integer positive real; cluster integer -> ext-integer for object; cluster real ext-integer -> integer for object; end; registration cluster real ext-integer positive for Element of ExtREAL; cluster positive for ext-integer object; end; definition mode ExtInt is ext-integer object; end; reserve x, y, v, u for ExtInt; theorem :: FVALUAT1:10 x < y implies x + 1 <= y; theorem :: FVALUAT1:11 -infty < x; definition let X be ext-real-membered set; given i0 being positive ExtInt such that i0 in X; func least-positive(X) -> positive ExtInt means :: FVALUAT1:def 2 it in X & for i being positive ExtInt st i in X holds it <= i; end; definition let f be Relation; attr f is e.i.-valued means :: FVALUAT1:def 3 for x being set st x in rng f holds x is ext-integer; end; registration cluster e.i.-valued for Function; end; registration let A be set; cluster e.i.-valued for Function of A, ExtREAL; end; registration let f be e.i.-valued Function, x be set; cluster f.x -> ext-integer; end; begin :: Structures theorem :: FVALUAT1:12 for K being distributive left_unital add-associative right_zeroed right_complementable non empty doubleLoopStr holds (-1.K) * (-1.K) = 1.K; definition let K be non empty doubleLoopStr; let S be Subset of K; let n be Nat; func S |^ n -> Subset of K means :: FVALUAT1:def 4 it = the carrier of K if n = 0 otherwise ex f being FinSequence of bool the carrier of K st it = f.len f & len f = n & f.1 = S & for i being Nat st i in dom f & i+1 in dom f holds f.(i+1) = S *' (f/.i); end; reserve D for non empty doubleLoopStr, A for Subset of D; theorem :: FVALUAT1:13 A |^ 1 = A; theorem :: FVALUAT1:14 A |^ 2 = A *' A; registration let R be Ring; let S be Ideal of R; let n be Nat; cluster S|^n -> non empty add-closed left-ideal right-ideal; end; definition let G be non empty doubleLoopStr, g be Element of G, i be Integer; func g |^ i -> Element of G equals :: FVALUAT1:def 5 power(G).(g,|.i.|) if 0 <= i otherwise /(power(G).(g,|.i.|)); end; definition let G be non empty doubleLoopStr, g be Element of G, n be Nat; redefine func g |^ n equals :: FVALUAT1:def 6 power(G).(g,n); end; reserve K for Field-like non degenerated associative add-associative right_zeroed right_complementable distributive Abelian non empty doubleLoopStr, a, b, c for Element of K; theorem :: FVALUAT1:15 a |^ (n + m) = (a |^ n) * (a |^ m); theorem :: FVALUAT1:16 a <> 0.K implies a|^i <> 0.K; begin :: Valuation definition let K be doubleLoopStr; attr K is having_valuation means :: FVALUAT1:def 7 ex f being e.i.-valued Function of K, ExtREAL st f.0.K = +infty & (for a being Element of K st a <> 0.K holds f.a in INT) & (for a,b being Element of K holds f.(a*b) = f.a + f.b) & (for a being Element of K st 0 <= f.a holds 0 <= f.(1.K+a)) & ex a being Element of K st f.a <> 0 & f.a <> +infty; end; definition let K be doubleLoopStr such that K is having_valuation; mode Valuation of K -> e.i.-valued Function of K, ExtREAL means :: FVALUAT1:def 8 it.0.K = +infty & (for a being Element of K st a <> 0.K holds it.a in INT) & (for a,b being Element of K holds it.(a*b) = it.a + it.b) & (for a being Element of K st 0 <= it.a holds 0 <= it.(1.K+a)) & ex a being Element of K st it.a <> 0 & it.a <> +infty; end; reserve v for Valuation of K; theorem :: FVALUAT1:17 K is having_valuation implies v.1.K = 0; theorem :: FVALUAT1:18 K is having_valuation & a <> 0.K implies v.a <> +infty; theorem :: FVALUAT1:19 K is having_valuation implies v.-1.K = 0; theorem :: FVALUAT1:20 K is having_valuation implies v.-a = v.a; theorem :: FVALUAT1:21 K is having_valuation & a <> 0.K implies v.(a") = -v.a; theorem :: FVALUAT1:22 K is having_valuation & b <> 0.K implies v.(a/b) = v.a - v.b; theorem :: FVALUAT1:23 K is having_valuation & a <> 0.K & b <> 0.K implies v.(a/b) = -v.(b/a); theorem :: FVALUAT1:24 K is having_valuation & b <> 0.K & 0 <= v.(a/b) implies v.b <= v.a; theorem :: FVALUAT1:25 K is having_valuation & a <> 0.K & b <> 0.K & v.(a/b) <= 0 implies 0 <= v.(b/a); theorem :: FVALUAT1:26 K is having_valuation & b <> 0.K & v.(a/b) <= 0 implies v.a <= v.b; theorem :: FVALUAT1:27 K is having_valuation implies min(v.a,v.b) <= v.(a+b); theorem :: FVALUAT1:28 K is having_valuation & v.a < v.b implies v.a = v.(a+b); theorem :: FVALUAT1:29 K is having_valuation & a <> 0.K implies v.(a|^i) = i * v.a; theorem :: FVALUAT1:30 K is having_valuation & 0 <= v.(1.K+a) implies 0 <= v.a; theorem :: FVALUAT1:31 K is having_valuation & 0 <= v.(1.K-a) implies 0 <= v.a; theorem :: FVALUAT1:32 K is having_valuation & a <> 0.K & v.a <= v.b implies 0 <= v.(b/a); theorem :: FVALUAT1:33 K is having_valuation implies +infty in rng v; theorem :: FVALUAT1:34 v.a = 1 implies least-positive(rng v) = 1; theorem :: FVALUAT1:35 K is having_valuation implies least-positive(rng v) is integer; theorem :: FVALUAT1:36 K is having_valuation implies for x being Element of K st x <> 0.K ex i being Integer st v.x = i * least-positive(rng v); definition let K, v; assume K is having_valuation; func Pgenerator(v) -> Element of K equals :: FVALUAT1:def 9 the Element of v"{least-positive(rng v)}; end; definition let K, v; assume K is having_valuation; func normal-valuation(v) -> Valuation of K means :: FVALUAT1:def 10 v.a = (it.a) * least-positive(rng v); end; theorem :: FVALUAT1:37 K is having_valuation implies (v.a = 0 iff normal-valuation(v).a = 0); theorem :: FVALUAT1:38 K is having_valuation implies (v.a = +infty iff normal-valuation(v).a = +infty); theorem :: FVALUAT1:39 K is having_valuation implies (v.a = v.b iff normal-valuation(v).a = normal-valuation(v).b); theorem :: FVALUAT1:40 K is having_valuation implies (v.a is positive iff normal-valuation(v).a is positive); theorem :: FVALUAT1:41 K is having_valuation implies (0 <= v.a iff 0 <= normal-valuation(v).a); theorem :: FVALUAT1:42 K is having_valuation implies (v.a is non negative iff normal-valuation(v).a is non negative); theorem :: FVALUAT1:43 K is having_valuation implies normal-valuation(v).Pgenerator(v) = 1; theorem :: FVALUAT1:44 K is having_valuation & 0 <= v.a implies normal-valuation(v).a <= v.a; theorem :: FVALUAT1:45 K is having_valuation & v.a = 1 implies normal-valuation(v) = v; theorem :: FVALUAT1:46 K is having_valuation implies normal-valuation(normal-valuation(v)) = normal-valuation(v); begin :: Valuation Ring definition let K be non empty doubleLoopStr; let v be Valuation of K; func NonNegElements v -> set equals :: FVALUAT1:def 11 {x where x is Element of K: 0 <= v.x}; end; theorem :: FVALUAT1:47 for K being non empty doubleLoopStr, v being Valuation of K, a being Element of K holds a in NonNegElements v iff 0 <= v.a; theorem :: FVALUAT1:48 for K being non empty doubleLoopStr, v being Valuation of K holds NonNegElements v c= the carrier of K; theorem :: FVALUAT1:49 for K being non empty doubleLoopStr, v being Valuation of K holds K is having_valuation implies 0.K in NonNegElements v; theorem :: FVALUAT1:50 K is having_valuation implies 1.K in NonNegElements v; definition let K, v such that K is having_valuation; func ValuatRing v -> strict commutative non degenerated Ring means :: FVALUAT1:def 12 the carrier of it = NonNegElements v & the addF of it = (the addF of K) | [:NonNegElements v,NonNegElements v:] & the multF of it = (the multF of K) | [:NonNegElements v,NonNegElements v:] & the ZeroF of it = 0.K & the OneF of it = 1.K; end; theorem :: FVALUAT1:51 K is having_valuation implies for x being Element of ValuatRing v holds x is Element of K; theorem :: FVALUAT1:52 K is having_valuation implies (0 <= v.a iff a is Element of ValuatRing v); theorem :: FVALUAT1:53 K is having_valuation implies for S being Subset of ValuatRing v holds 0 is LowerBound of v.:S; theorem :: FVALUAT1:54 K is having_valuation implies for x, y being Element of K, x1, y1 being Element of ValuatRing v st x = x1 & y = y1 holds x + y = x1 + y1; theorem :: FVALUAT1:55 K is having_valuation implies for x, y being Element of K, x1, y1 being Element of ValuatRing v st x = x1 & y = y1 holds x * y = x1 * y1; theorem :: FVALUAT1:56 K is having_valuation implies 0.ValuatRing v = 0.K; theorem :: FVALUAT1:57 K is having_valuation implies 1.ValuatRing v = 1.K; theorem :: FVALUAT1:58 K is having_valuation implies for x being Element of K, y being Element of ValuatRing v st x = y holds -x = -y; theorem :: FVALUAT1:59 K is having_valuation implies ValuatRing v is domRing-like; theorem :: FVALUAT1:60 K is having_valuation implies for y being Element of ValuatRing v holds power(K).(y,n) = power(ValuatRing v).(y,n); definition let K, v; assume K is having_valuation; func PosElements v -> Ideal of ValuatRing v equals :: FVALUAT1:def 13 {x where x is Element of K: 0 < v.x}; end; notation let K, v; synonym vp v for PosElements v; end; theorem :: FVALUAT1:61 K is having_valuation implies (a in vp v iff 0 < v.a); theorem :: FVALUAT1:62 K is having_valuation implies 0.K in vp v; theorem :: FVALUAT1:63 K is having_valuation implies not 1.K in vp v; definition let K, v; let S be non empty Subset of K; assume that K is having_valuation and S is Subset of ValuatRing v; func min(S,v) -> Subset of ValuatRing v equals :: FVALUAT1:def 14 v"{inf(v.:S)} /\ S; end; theorem :: FVALUAT1:64 for S being non empty Subset of K st K is having_valuation & S is Subset of ValuatRing v holds min(S,v) c= S; theorem :: FVALUAT1:65 for S being non empty Subset of K st K is having_valuation & S is Subset of ValuatRing v for x being Element of K holds x in min(S,v) iff x in S & for y being Element of K st y in S holds v.x <= v.y; theorem :: FVALUAT1:66 K is having_valuation implies for I being non empty Subset of K, x being Element of ValuatRing v st I is Ideal of ValuatRing v & x in min(I,v) holds I = {x}-Ideal; theorem :: FVALUAT1:67 for R being non empty doubleLoopStr, I being add-closed non empty Subset of R holds I is Preserv of the addF of R; definition let R be Ring; let P be RightIdeal of R; mode Submodule of P -> Submodule of RightModule R means :: FVALUAT1:def 15 the carrier of it = P; end; registration let R be Ring; let P be RightIdeal of R; cluster strict for Submodule of P; end; theorem :: FVALUAT1:68 for R being Ring, P being Ideal of R, M being Submodule of P for a being BinOp of P, z be Element of P for m being Function of [:P,the carrier of R:], P st a = (the addF of R)|[:P,P:] & m = (the multF of R)|[:P,the carrier of R:] & z = the ZeroF of R holds the RightModStr of M = RightModStr(#P,a,z,m#); definition let R be Ring; let M1,M2 be RightMod of R; let h be Function of M1,M2; attr h is scalar-linear means :: FVALUAT1:def 16 for x being Element of M1, r being Element of R holds h.(x*r) = (h.x)*r; end; registration let R be Ring, M1 be RightMod of R, M2 be Submodule of M1; cluster incl(M2,M1) -> additive scalar-linear; end; theorem :: FVALUAT1:69 K is having_valuation & b is Element of ValuatRing v implies v.a <= v.a + v.b; theorem :: FVALUAT1:70 K is having_valuation & a is Element of ValuatRing v implies power(K).(a,n) is Element of ValuatRing v; theorem :: FVALUAT1:71 K is having_valuation implies for x being Element of ValuatRing v st x <> 0.K holds power(K).(x,n) <> 0.K; theorem :: FVALUAT1:72 K is having_valuation & v.a = 0 implies a is Element of ValuatRing v & a" is Element of ValuatRing v; theorem :: FVALUAT1:73 K is having_valuation & a <> 0.K & a is Element of ValuatRing v & a" is Element of ValuatRing v implies v.a = 0; theorem :: FVALUAT1:74 K is having_valuation & v.a = 0 implies for I being Ideal of ValuatRing v holds a in I iff I = the carrier of ValuatRing v; theorem :: FVALUAT1:75 K is having_valuation implies Pgenerator(v) is Element of ValuatRing v; theorem :: FVALUAT1:76 K is having_valuation implies vp(v) is proper; theorem :: FVALUAT1:77 K is having_valuation implies for x being Element of ValuatRing v st not x in vp(v) holds v.x = 0; theorem :: FVALUAT1:78 K is having_valuation implies vp(v) is prime; theorem :: FVALUAT1:79 K is having_valuation implies for I being proper Ideal of ValuatRing v holds I c= vp(v); theorem :: FVALUAT1:80 K is having_valuation implies vp(v) is maximal; theorem :: FVALUAT1:81 K is having_valuation implies for I being maximal Ideal of ValuatRing v holds I = vp(v); theorem :: FVALUAT1:82 K is having_valuation implies NonNegElements(normal-valuation v) = NonNegElements(v); theorem :: FVALUAT1:83 K is having_valuation implies ValuatRing(normal-valuation v) = ValuatRing v;