topzari1.miz



    begin

    reserve R for commutative Ring;

    reserve A,B for non degenerated commutative Ring;

    reserve h for Function of A, B;

    reserve I0,I,I1,I2 for Ideal of A;

    reserve J,J1,J2 for proper Ideal of A;

    reserve p for prime Ideal of A;

    reserve S,S1 for non empty Subset of A;

    reserve E,E1,E2 for Subset of A;

    reserve a,b,f for Element of A;

    reserve n for Nat;

    reserve x,o,o1 for object;

    

     Lm1: x in ( Ideals A) iff x is Ideal of A

    proof

      thus x in ( Ideals A) implies x is Ideal of A

      proof

        assume x in ( Ideals A);

        then x in the set of all I where I be Ideal of A by RING_2:def 3;

        then

        consider x0 be Ideal of A such that

         A3: x0 = x;

        thus thesis by A3;

      end;

      assume x is Ideal of A;

      then x in the set of all I where I be Ideal of A;

      hence thesis by RING_2:def 3;

    end;

    definition

      let A, S;

      :: TOPZARI1:def1

      func Ideals (A,S) -> Subset of ( Ideals A) equals { I where I be Ideal of A : S c= I };

      coherence

      proof

        set C = { I where I be Ideal of A : S c= I };

        now

          let x be object;

          assume x in C;

          then ex I be Ideal of A st x = I & S c= I;

          hence x in ( Ideals A) by Lm1;

        end;

        then C c= ( Ideals A);

        hence thesis;

      end;

    end

    registration

      let A, S;

      cluster ( Ideals (A,S)) -> non empty;

      coherence

      proof

        set I = ( [#] A);

        reconsider I as Subset of A;

        I in ( Ideals (A,S));

        hence thesis;

      end;

    end

    theorem :: TOPZARI1:1

    

     Th2: ( Ideals (A,S)) = ( Ideals (A,(S -Ideal )))

    proof

      thus ( Ideals (A,S)) c= ( Ideals (A,(S -Ideal )))

      proof

        let x be object;

        assume x in ( Ideals (A,S));

        then

        consider y be Ideal of A such that

         A2: x = y and

         A3: S c= y;

        (S -Ideal ) c= (y -Ideal ) by A3, IDEAL_1: 57;

        then (S -Ideal ) c= y by IDEAL_1: 44;

        hence thesis by A2;

      end;

      let x be object;

      assume x in ( Ideals (A,(S -Ideal )));

      then

      consider y be Ideal of A such that

       A8: x = y and

       A9: (S -Ideal ) c= y;

      S c= (S -Ideal ) by IDEAL_1:def 14;

      then S c= y by A9;

      hence thesis by A8;

    end;

    definition

      let A be unital non empty multLoopStr_0, a be Element of A;

      :: TOPZARI1:def2

      attr a is nilpotent means ex k be non zero Nat st (a |^ k) = ( 0. A);

    end

    registration

      let A be unital non empty multLoopStr_0;

      cluster ( 0. A) -> nilpotent;

      coherence

      proof

        (( 0. A) |^ 1) = ( 0. A) by BINOM: 8;

        hence thesis;

      end;

    end

    registration

      let A be unital non empty multLoopStr_0;

      cluster nilpotent for Element of A;

      existence

      proof

        take ( 0. A);

        thus thesis;

      end;

    end

    registration

      let A;

      cluster ( 1. A) -> non nilpotent;

      coherence

      proof

        set a = ( 1. A);

        for n be Nat holds (a |^ n) = a

        proof

          defpred P[ Nat] means (a |^ $1) = ( 1. A);

           A1:

          now

            let n be Nat;

            assume

             A2: P[n];

            (a |^ (n + 1)) = ((a |^ n) * (a |^ 1)) by BINOM: 10

            .= a by BINOM: 8, A2;

            hence P[(n + 1)];

          end;

          (a |^ 0 ) = ( 1_ A) by BINOM: 8

          .= a;

          then

           A3: P[ 0 ];

          thus for n be Nat holds P[n] from NAT_1:sch 2( A3, A1);

        end;

        hence thesis;

      end;

    end

    definition

      let A, J, f;

      :: TOPZARI1:def3

      func multClSet (J,f) -> Subset of A equals the set of all (f |^ i) where i be Nat;

      coherence

      proof

         the set of all (f |^ i) where i be Nat c= the carrier of A

        proof

          let x be object;

          assume x in the set of all (f |^ i) where i be Nat;

          then

          consider k be Nat such that

           A2: x = (f |^ k);

          thus thesis by A2;

        end;

        hence thesis;

      end;

    end

    registration

      let A, J, f;

      cluster ( multClSet (J,f)) -> multiplicatively-closed;

      coherence

      proof

        

         A2: (f |^ 0 ) = ( 1_ A) by BINOM: 8;

        

         A4: ( 1. A) in ( multClSet (J,f)) by A2;

        for v,u be Element of A st v in ( multClSet (J,f)) & u in ( multClSet (J,f)) holds (v * u) in ( multClSet (J,f))

        proof

          let v,u be Element of A;

          assume that

           A5: v in ( multClSet (J,f)) and

           A6: u in ( multClSet (J,f));

          consider n1 be Nat such that

           A7: v = (f |^ n1) by A5;

          consider n2 be Nat such that

           A8: u = (f |^ n2) by A6;

          (v * u) = (f |^ (n1 + n2)) by BINOM: 10, A8, A7;

          hence thesis;

        end;

        hence thesis by A4, C0SP1:def 4;

      end;

    end

    theorem :: TOPZARI1:2

    

     Lm4: for n be Nat holds (( 1. A) |^ n) = ( 1. A)

    proof

      defpred P[ Nat] means (( 1. A) |^ $1) = ( 1. A);

       A1:

      now

        let n be Nat;

        assume

         A2: P[n];

        (( 1. A) |^ (n + 1)) = ((( 1. A) |^ n) * (( 1. A) |^ 1)) by BINOM: 10

        .= ( 1. A) by BINOM: 8, A2;

        hence P[(n + 1)];

      end;

      (( 1. A) |^ 0 ) = ( 1_ A) by BINOM: 8;

      then

       A3: P[ 0 ];

      thus for n be Nat holds P[n] from NAT_1:sch 2( A3, A1);

    end;

    theorem :: TOPZARI1:3

    

     Lm5: not ( 1. A) in ( sqrt J)

    proof

      assume ( 1. A) in ( sqrt J);

      then ( 1. A) in { a where a be Element of A : ex n be Element of NAT st (a |^ n) in J } by IDEAL_1:def 24;

      then

      consider a be Element of A such that

       A3: ( 1. A) = a and

       A4: ex n be Element of NAT st (a |^ n) in J;

      consider n1 be Element of NAT such that

       A5: (a |^ n1) in J by A4;

      ( 1. A) = (a |^ n1) by A3, Lm4;

      hence contradiction by IDEAL_1: 19, A5;

    end;

    theorem :: TOPZARI1:4

    

     Lm6: ( multClSet (J,( 1. A))) = {( 1. A)}

    proof

      thus ( multClSet (J,( 1. A))) c= {( 1. A)}

      proof

        let x be object;

        assume x in ( multClSet (J,( 1. A)));

        then

        consider n1 be Nat such that

         A3: x = (( 1. A) |^ n1);

        x = ( 1. A) by A3, Lm4;

        hence thesis by TARSKI:def 1;

      end;

      let x be object;

      assume x in {( 1. A)};

      then x = ( 1. A) by TARSKI:def 1;

      hence thesis by C0SP1:def 4;

    end;

    definition

      let A, J, f;

      :: TOPZARI1:def4

      func Ideals (A,J,f) -> Subset of ( Ideals A) equals { I where I be Subset of A : I is proper Ideal of A & J c= I & (I /\ ( multClSet (J,f))) = {} };

      coherence

      proof

        set C = { I where I be Subset of A : I is proper Ideal of A & J c= I & (I /\ ( multClSet (J,f))) = {} };

        C c= ( Ideals A)

        proof

          let x be object;

          assume x in C;

          then

          consider I be Subset of A such that

           A1: x = I and

           A2: I is proper Ideal of A and J c= I & (I /\ ( multClSet (J,f))) = {} ;

          thus x in ( Ideals A) by A1, A2, Lm1;

        end;

        hence thesis;

      end;

    end

    theorem :: TOPZARI1:5

    

     Th7: for A, J, f st not f in ( sqrt J) holds J in ( Ideals (A,J,f))

    proof

      let A, J, f;

      assume

       A1: not f in ( sqrt J);

      set I = J;

      (I /\ ( multClSet (J,f))) = {}

      proof

        assume (I /\ ( multClSet (J,f))) <> {} ;

        then

        consider x be object such that

         A4: x in (I /\ ( multClSet (J,f))) by XBOOLE_0:def 1;

        x in I & x in ( multClSet (J,f)) by A4, XBOOLE_0:def 4;

        then

        consider n1 be Nat such that

         A5: x = (f |^ n1);

        reconsider n1 as Element of NAT by ORDINAL1:def 12;

        ( sqrt J) = { a where a be Element of A : ex n be Element of NAT st (a |^ n) in J } by IDEAL_1:def 24;

        then not (f |^ n1) in J by A1;

        hence contradiction by A4, A5, XBOOLE_0:def 4;

      end;

      hence thesis;

    end;

    theorem :: TOPZARI1:6

    

     Th8: for A, J, f st not f in ( sqrt J) holds ( Ideals (A,J,f)) has_upper_Zorn_property_wrt ( RelIncl ( Ideals (A,J,f)))

    proof

      let A, J, f;

      assume

       A1: not f in ( sqrt J);

      set S = ( Ideals (A,J,f));

      set P = ( RelIncl S);

      

       A2: ( field P) = S by WELLORD2:def 1;

      for Y be set st Y c= S & (P |_2 Y) is being_linear-order holds ex x be set st x in S & for y be set st y in Y holds [y, x] in P

      proof

        let Y be set such that

         A3: Y c= S and

         A4: (P |_2 Y) is being_linear-order;

        per cases ;

          suppose

           A5: Y is empty;

          take x = J;

          thus thesis by A5, A1, Th7;

        end;

          suppose Y is non empty;

          then

          consider e be object such that

           A6: e in Y;

          take x = ( union Y);

          for a be object st a in x holds a in the carrier of A

          proof

            let a be object;

            assume a in x;

            then

            consider Z be set such that

             A7: a in Z and

             A8: Z in Y by TARSKI:def 4;

            Z in S by A3, A8;

            then ex A1 be Subset of A st Z = A1 & A1 is proper Ideal of A & J c= A1 & (A1 /\ ( multClSet (J,f))) = {} ;

            hence thesis by A7;

          end;

          then x c= the carrier of A;

          then

          reconsider B = x as Subset of A;

          

           A9: B is left-ideal

          proof

            let p,a be Element of A;

            assume a in B;

            then

            consider Aa be set such that

             A10: a in Aa and

             A11: Aa in Y by TARSKI:def 4;

            Aa in S by A3, A11;

            then

            consider Ia be Subset of A such that

             A12: Aa = Ia and

             A13: Ia is proper Ideal of A and J c= Ia and (Ia /\ ( multClSet (J,f))) = {} ;

            (p * a) in Ia & Ia c= B by A10, A11, A12, A13, IDEAL_1:def 2, ZFMISC_1: 74;

            hence thesis;

          end;

          

           A14: B is proper

          proof

            assume B is non proper;

            then

            consider Aa be set such that

             A16: ( 1. A) in Aa and

             A17: Aa in Y by TARSKI:def 4;

            Aa in S by A3, A17;

            then ex Ia be Subset of A st Aa = Ia & Ia is proper Ideal of A & J c= Ia & (Ia /\ ( multClSet (J,f))) = {} ;

            hence contradiction by A16, IDEAL_1: 19;

          end;

          

           A18: B is add-closed

          proof

            

             A19: ( field (P |_2 Y)) = Y by A2, A3, ORDERS_1: 71;

            let a,b be Element of A;

             A20:

            now

              let A1 be Ideal of A;

              assume a in A1 & b in A1;

              then

               A21: (a + b) in A1 by IDEAL_1:def 1;

              assume A1 in Y;

              hence (a + b) in B by A21, TARSKI:def 4;

            end;

            assume a in B;

            then

            consider Aa be set such that

             A22: a in Aa and

             A23: Aa in Y by TARSKI:def 4;

            Aa in S by A3, A23;

            then

             A24: ex Ia be Subset of A st Aa = Ia & Ia is proper Ideal of A & J c= Ia & (Ia /\ ( multClSet (J,f))) = {} ;

            assume b in B;

            then

            consider Ab be set such that

             A25: b in Ab and

             A26: Ab in Y by TARSKI:def 4;

             [Aa, Ab] in (P |_2 Y) or [Ab, Aa] in (P |_2 Y) or Aa = Ab by A4, A23, A26, A19, RELAT_2:def 6, RELAT_2:def 14;

            then [Aa, Ab] in P or [Ab, Aa] in P or Aa = Ab by XBOOLE_0:def 4;

            then

             A27: Aa c= Ab or Ab c= Aa by A3, A23, A26, WELLORD2:def 1;

            Ab in S by A3, A26;

            then ex Ib be Subset of A st Ab = Ib & Ib is proper Ideal of A & J c= Ib & (Ib /\ ( multClSet (J,f))) = {} ;

            hence (a + b) in B by A22, A23, A25, A26, A20, A24, A27;

          end;

          e in S by A3, A6;

          then

          consider A1 be Subset of A such that

           A28: A1 = e and

           A29: A1 is proper Ideal of A and

           A30: J c= A1 and (A1 /\ ( multClSet (J,f))) = {} ;

          ex q be object st q in A1 by XBOOLE_0:def 1, A29;

          then

           A32: B is non empty & J c= B by A6, A28, A30, TARSKI:def 4;

          

           A33: (B /\ ( multClSet (J,f))) = {}

          proof

            assume (B /\ ( multClSet (J,f))) <> {} ;

            then

            consider y be object such that

             A35: y in (B /\ ( multClSet (J,f))) by XBOOLE_0:def 1;

            y in B & y in ( multClSet (J,f)) by A35, XBOOLE_0:def 4;

            then

            consider Aa be set such that

             A36: y in Aa and

             A37: Aa in Y by TARSKI:def 4;

            Aa in S by A3, A37;

            then

            consider Ia be Subset of A such that

             A38: Aa = Ia and Ia is proper Ideal of A & J c= Ia and

             A39: (Ia /\ ( multClSet (J,f))) = {} ;

            y in ( multClSet (J,f)) by A35, XBOOLE_0:def 4;

            hence contradiction by A39, A38, A36, XBOOLE_0:def 4;

          end;

          thus

           A41: x in S by A9, A14, A18, A32, A33;

          let y be set;

          assume

           A42: y in Y;

          then y c= x by ZFMISC_1: 74;

          hence thesis by A3, A41, A42, WELLORD2:def 1;

        end;

      end;

      hence thesis;

    end;

    theorem :: TOPZARI1:7

    

     Th9: for f, J st not f in ( sqrt J) holds ex m be prime Ideal of A st not f in m & J c= m

    proof

      let f, J;

      assume

       A1: not f in ( sqrt J);

      set S = ( Ideals (A,J,f));

      set P = ( RelIncl S);

      

       A2: ( field P) = S by WELLORD2:def 1;

      P partially_orders S by WELLORD2: 19, WELLORD2: 21, WELLORD2: 20;

      then

      consider I be set such that

       A3: I is_maximal_in P by A1, A2, Th8, ORDERS_1: 63;

      I in S by WELLORD2:def 1, A3;

      then

      consider p be Subset of A such that

       A4: p = I and

       A6: p is proper Ideal of A and

       A7: J c= p and

       A8: (p /\ ( multClSet (J,f))) = {} ;

      (f |^ 1) = f by BINOM: 8;

      then f in ( multClSet (J,f));

      then

       A11: not f in p by A8, XBOOLE_0:def 4;

      p is quasi-prime Ideal of A

      proof

        for x,y be Element of A st not x in p & not y in p holds not (x * y) in p

        proof

          let x,y be Element of A;

          assume that

           A12: not x in p and

           A13: not y in p;

          assume

           A14: (x * y) in p;

          

           A15: p c< (p + ( {x} -Ideal ))

          proof

            ( {x} -Ideal ) c= (p + ( {x} -Ideal )) by A6, IDEAL_1: 74;

            hence thesis by A6, A12, IDEAL_1: 66, IDEAL_1: 73;

          end;

          

           A17: p c< (p + ( {y} -Ideal ))

          proof

            ( {y} -Ideal ) c= (p + ( {y} -Ideal )) by A6, IDEAL_1: 74;

            hence thesis by A6, A13, IDEAL_1: 66, IDEAL_1: 73;

          end;

          set J2 = (p + ( {x} -Ideal ));

          

           A19: not ((p + ( {x} -Ideal )) in ( Ideals (A,J,f)))

          proof

            assume

             A20: (p + ( {x} -Ideal )) in ( Ideals (A,J,f));

            then

             A21: J2 in ( field P) by WELLORD2:def 1;

            J2 <> I & [I, J2] in P by A2, A3, A4, A15, A20, WELLORD2:def 1;

            hence contradiction by A3, A21;

          end;

          

           A22: not ((p + ( {y} -Ideal )) in ( Ideals (A,J,f)))

          proof

            assume

             A23: (p + ( {y} -Ideal )) in ( Ideals (A,J,f));

            set J2 = (p + ( {y} -Ideal ));

            

             A24: J2 in ( field P) by WELLORD2:def 1, A23;

            J2 <> I & [I, J2] in P by A2, A3, A4, A17, A23, WELLORD2:def 1;

            hence contradiction by A3, A24;

          end;

          reconsider q = (p + ( {x} -Ideal )) as Subset of A;

          

           A26: p c= (p + ( {x} -Ideal )) by A6, IDEAL_1: 73;

          

           A27: not (q is proper Ideal of A) or not (J c= q) or not ((q /\ ( multClSet (J,f))) = {} ) by A19;

          

           A28: ex n be Nat st (f |^ n) in (p + ( {x} -Ideal ))

          proof

            per cases by A7, A26, A27;

              suppose

               A29: not ((p + ( {x} -Ideal )) is proper Ideal of A);

              reconsider q1 = (p + ( {x} -Ideal )) as Ideal of A by A6;

              

               A30: q1 = the carrier of A by A29, SUBSET_1:def 6;

              reconsider n = 1 as Nat;

              (f |^ n) in q by A30;

              hence thesis;

            end;

              suppose not ((q /\ ( multClSet (J,f))) = {} );

              then

              consider h be object such that

               A32: h in (q /\ ( multClSet (J,f))) by XBOOLE_0:def 1;

              h in q & h in ( multClSet (J,f)) by A32, XBOOLE_0:def 4;

              then

              consider n1 be Nat such that

               A33: h = (f |^ n1);

              (f |^ n1) in q by A33, A32, XBOOLE_0:def 4;

              hence thesis;

            end;

          end;

          reconsider q = (p + ( {y} -Ideal )) as Subset of A;

          p c= (p + ( {y} -Ideal )) by A6, IDEAL_1: 73;

          then

           A36: J c= q by A7;

          

           A37: ex m be Nat st (f |^ m) in (p + ( {y} -Ideal ))

          proof

            per cases by A22, A36;

              suppose

               A38: not ((p + ( {y} -Ideal )) is proper Ideal of A);

              reconsider q1 = (p + ( {y} -Ideal )) as Ideal of A by A6;

              

               A39: q1 = the carrier of A by A38, SUBSET_1:def 6;

              reconsider m = 1 as Nat;

              (f |^ m) in q by A39;

              hence thesis;

            end;

              suppose (q /\ ( multClSet (J,f))) <> {} ;

              then

              consider h be object such that

               A41: h in (q /\ ( multClSet (J,f))) by XBOOLE_0:def 1;

              h in q & h in ( multClSet (J,f)) by A41, XBOOLE_0:def 4;

              then

              consider n1 be Nat such that

               A42: h = (f |^ n1);

              (f |^ n1) in q by A41, XBOOLE_0:def 4, A42;

              hence thesis;

            end;

          end;

          reconsider p as Ideal of A by A6;

          consider n be Nat such that

           A43: (f |^ n) in (p + ( {x} -Ideal )) by A28;

          consider m be Nat such that

           A44: (f |^ m) in (p + ( {y} -Ideal )) by A37;

          (f |^ n) in { (a + b) where a,b be Element of A : a in p & b in ( {x} -Ideal ) } by A43, IDEAL_1:def 19;

          then

          consider p1,x1 be Element of A such that

           A45: (f |^ n) = (p1 + x1) and

           A46: p1 in p and

           A47: x1 in ( {x} -Ideal );

          (f |^ m) in { (a + b) where a,b be Element of A : a in p & b in ( {y} -Ideal ) } by A44, IDEAL_1:def 19;

          then

          consider p2,y2 be Element of A such that

           A48: (f |^ m) = (p2 + y2) and

           A49: p2 in p and

           A50: y2 in ( {y} -Ideal );

          x1 in the set of all (x * a) where a be Element of A by A47, IDEAL_1: 64;

          then

          consider a be Element of A such that

           A51: x1 = (x * a);

          y2 in the set of all (y * a) where a be Element of A by A50, IDEAL_1: 64;

          then

          consider b be Element of A such that

           A52: y2 = (y * b);

          

           A53: (((p1 + x1) * p2) + (p1 * y2)) in p

          proof

            reconsider a = (p1 + x1) as Element of A;

            

             A54: (a * p2) in p by A49, IDEAL_1:def 2;

            (p1 * y2) in p by A46, IDEAL_1:def 3;

            hence thesis by A54, IDEAL_1:def 1;

          end;

          

           A56a: (x1 * y2) in ( {(x * y)} -Ideal )

          proof

            

             A57: (x1 * y2) = (a * (x * (y * b))) by GROUP_1:def 3, A52, A51

            .= (((x * y) * b) * a) by GROUP_1:def 3

            .= ((x * y) * (b * a)) by GROUP_1:def 3;

            ((x * y) * (b * a)) in the set of all ((x * y) * r) where r be Element of A;

            hence thesis by A57, IDEAL_1: 64;

          end;

          

           A59: (f |^ (n + m)) = ((f |^ n) * (f |^ m)) by BINOM: 10

          .= (((p1 + x1) * p2) + ((p1 + x1) * y2)) by VECTSP_1:def 7, A45, A48

          .= (((p1 + x1) * p2) + ((p1 * y2) + (x1 * y2))) by VECTSP_1:def 7

          .= ((((p1 + x1) * p2) + (p1 * y2)) + (x1 * y2)) by RLVECT_1:def 3;

          reconsider s = (((p1 + x1) * p2) + (p1 * y2)), t = (x1 * y2) as Element of A;

          (s + t) in { (u + v) where u,v be Element of A : u in p & v in ( {(x * y)} -Ideal ) } by A53, A56a;

          then

           A61: (f |^ (n + m)) in (p + ( {(x * y)} -Ideal )) by A59, IDEAL_1:def 19;

          reconsider n1 = (n + m) as Nat;

          

           A63: (f |^ (n + m)) in ( multClSet (J,f));

          

           A64: not (p + ( {(x * y)} -Ideal )) in ( Ideals (A,J,f))

          proof

            assume (p + ( {(x * y)} -Ideal )) in ( Ideals (A,J,f));

            then

            consider q be Subset of A such that

             A66: q = (p + ( {(x * y)} -Ideal )) and q is proper Ideal of A & J c= q and

             A67: (q /\ ( multClSet (J,f))) = {} ;

            thus contradiction by A61, A63, XBOOLE_0:def 4, A67, A66;

          end;

          (p -Ideal ) = p by IDEAL_1: 44;

          then ( {(x * y)} -Ideal ) c= p by IDEAL_1: 67, A14;

          then p = (p + ( {(x * y)} -Ideal )) by IDEAL_1: 74, IDEAL_1: 75;

          hence contradiction by A3, A4, A64, WELLORD2:def 1;

        end;

        then for a,b be Element of A st (a * b) in p holds a in p or b in p;

        hence thesis by A6, RING_1:def 1;

      end;

      hence thesis by A6, A7, A11;

    end;

    theorem :: TOPZARI1:8

    

     Th10: ex m be maximal Ideal of A st J c= m

    proof

      

       A1: not ( 1. A) in ( sqrt J) by Lm5;

      set S = ( Ideals (A,J,( 1. A)));

      set P = ( RelIncl S);

      

       A2: ( field P) = S by WELLORD2:def 1;

      P partially_orders S by WELLORD2: 19, WELLORD2: 20, WELLORD2: 21;

      then

      consider I be set such that

       A3: I is_maximal_in P by A1, A2, Th8, ORDERS_1: 63;

      I in S by WELLORD2:def 1, A3;

      then

      consider p be Subset of A such that

       A4: p = I and

       A5: p is proper Ideal of A and

       A6: J c= p and (p /\ ( multClSet (J,( 1. A)))) = {} ;

      for q be Ideal of A st p c= q holds q = p or q is non proper

      proof

        let q be Ideal of A;

        assume

         A7: p c= q;

        per cases ;

          suppose

           A8: q is proper;

          

           A9: ( multClSet (J,( 1. A))) = {( 1. A)} by Lm6;

          

           A10: (q /\ ( multClSet (J,( 1. A)))) = {}

          proof

            assume (q /\ ( multClSet (J,( 1. A)))) <> {} ;

            then

            consider y be object such that

             A12: y in (q /\ ( multClSet (J,( 1. A)))) by XBOOLE_0:def 1;

            

             A13: y in q & y in ( multClSet (J,( 1. A))) by A12, XBOOLE_0:def 4;

            ( 1. A) in q by A9, A13, TARSKI:def 1;

            hence contradiction by A8, IDEAL_1: 19;

          end;

          J c= q by A6, A7;

          then

           A14: q in S by A8, A10;

           [p, q] in P by A2, A3, A4, A7, A14, WELLORD2:def 1;

          hence thesis by A2, A3, A4, A14;

        end;

          suppose q is non proper;

          hence thesis;

        end;

      end;

      then p is quasi-maximal;

      hence thesis by A5, A6;

    end;

    theorem :: TOPZARI1:9

    

     Th11: ex m be prime Ideal of A st J c= m

    proof

      ex m be maximal Ideal of A st J c= m by Th10;

      hence thesis;

    end;

    theorem :: TOPZARI1:10

    a is NonUnit of A implies ex m be maximal Ideal of A st a in m

    proof

      assume a is NonUnit of A;

      then ( {a} -Ideal ) <> ( [#] A) by RING_2: 20;

      then ( {a} -Ideal ) is proper;

      then

      consider m be maximal Ideal of A such that

       A2: ( {a} -Ideal ) c= m by Th10;

      a in m by A2, IDEAL_1: 66;

      hence thesis;

    end;

    begin

    definition

      let R be commutative Ring;

      :: TOPZARI1:def5

      func Spectrum R -> Subset-Family of R equals

      : Def3: { I where I be Ideal of R : I is quasi-prime & I <> ( [#] R) } if R is non degenerated

      otherwise {} ;

      coherence

      proof

        thus R is non degenerated implies { I where I be Ideal of R : I is quasi-prime & I <> ( [#] R) } is Subset of ( bool the carrier of R)

        proof

          set X = { I where I be Ideal of R : I is quasi-prime & I <> ( [#] R) };

          X c= ( bool the carrier of R)

          proof

            let x be object;

            assume x in X;

            then ex I be Ideal of R st x = I & I is quasi-prime & I <> ( [#] R);

            hence thesis;

          end;

          hence thesis;

        end;

        thus thesis by XBOOLE_1: 2;

      end;

      consistency ;

    end

    definition

      let A;

      :: original: Spectrum

      redefine

      :: TOPZARI1:def6

      func Spectrum A -> Subset-Family of A equals the set of all I where I be prime Ideal of A;

      correctness

      proof

        set C = { I where I be Ideal of A : I is quasi-prime & I <> ( [#] A) };

        

         A1: x in ( Spectrum A) implies x in the set of all I where I be prime Ideal of A

        proof

          assume x in ( Spectrum A);

          then x in C by Def3;

          then

          consider I be Ideal of A such that

           A3: x = I and

           A4: I is quasi-prime and

           A5: I <> ( [#] A);

          

           A6: I is proper Ideal of A by A5, SUBSET_1:def 6;

          reconsider I as quasi-prime Ideal of A by A4;

          I in the set of all I where I be prime Ideal of A by A6;

          hence thesis by A3;

        end;

        x in the set of all I where I be prime Ideal of A implies x in ( Spectrum A)

        proof

          assume x in the set of all I where I be prime Ideal of A;

          then

          consider I be prime Ideal of A such that

           A8: I = x;

          reconsider I as non empty Subset of A;

          I in C;

          hence thesis by A8, Def3;

        end;

        hence thesis by TARSKI: 2, A1;

      end;

    end

    registration

      let A;

      cluster ( Spectrum A) -> non empty;

      coherence

      proof

        set m = the maximal Ideal of A;

        reconsider m as Subset of A;

        m in ( Spectrum A);

        hence thesis;

      end;

    end

    definition

      let R;

      :: TOPZARI1:def7

      func m-Spectrum R -> Subset-Family of R equals

      : Def4: { I where I be Ideal of R : I is quasi-maximal & I <> ( [#] R) } if R is non degenerated

      otherwise {} ;

      coherence

      proof

        thus R is non degenerated implies { I where I be Ideal of R : I is quasi-maximal & I <> ( [#] R) } is Subset of ( bool the carrier of R)

        proof

          set X = { I where I be Ideal of R : I is quasi-maximal & I <> ( [#] R) };

          X c= ( bool the carrier of R)

          proof

            let x be object;

            assume x in X;

            then ex I be Ideal of R st x = I & I is quasi-maximal & I <> ( [#] R);

            hence thesis;

          end;

          hence thesis;

        end;

        thus thesis by XBOOLE_1: 2;

      end;

      consistency ;

    end

    definition

      let A;

      :: original: m-Spectrum

      redefine

      :: TOPZARI1:def8

      func m-Spectrum A -> Subset-Family of the carrier of A equals the set of all I where I be maximal Ideal of A;

      correctness

      proof

        set C = { I where I be Ideal of A : I is quasi-maximal & I <> ( [#] A) };

        

         A2: x in ( m-Spectrum A) implies x in the set of all I where I be maximal Ideal of A

        proof

          assume x in ( m-Spectrum A);

          then x in C by Def4;

          then

          consider I be Ideal of A such that

           A4: x = I and

           A5: I is quasi-maximal and

           A6: I <> ( [#] A);

          I is proper by A6;

          hence thesis by A4, A5;

        end;

        x in the set of all I where I be maximal Ideal of A implies x in ( m-Spectrum A)

        proof

          assume x in the set of all I where I be maximal Ideal of A;

          then

          consider I be maximal Ideal of A such that

           A9: I = x;

          I in C;

          hence thesis by A9, Def4;

        end;

        hence thesis by TARSKI: 2, A2;

      end;

    end

    registration

      let A;

      cluster ( m-Spectrum A) -> non empty;

      coherence

      proof

        set m = the maximal Ideal of A;

        m in ( m-Spectrum A);

        hence thesis;

      end;

    end

    begin

    definition

      let A;

      :: TOPZARI1:def9

      attr A is local means ex m be Ideal of A st ( m-Spectrum A) = {m};

    end

    definition

      let A;

      :: TOPZARI1:def10

      attr A is semi-local means ( m-Spectrum A) is finite;

    end

    theorem :: TOPZARI1:11

    

     Th15: x in I & I is proper Ideal of A implies x is NonUnit of A

    proof

      assume that

       A1: x in I and

       A2: I is proper Ideal of A;

      assume

       A3: not x is NonUnit of A;

      reconsider x as Element of A by A1;

      ( {x} -Ideal ) = ( [#] A) by A3, RING_2: 20;

      then ( [#] A) = I by A1, RING_2: 4;

      hence contradiction by A2;

    end;

    theorem :: TOPZARI1:12

    

     Th16: (for m1,m2 be object st m1 in ( m-Spectrum A) & m2 in ( m-Spectrum A) holds m1 = m2) implies A is local

    proof

      assume

       A1: for m1,m2 be object st m1 in ( m-Spectrum A) & m2 in ( m-Spectrum A) holds m1 = m2;

      reconsider m = the maximal Ideal of A as maximal Ideal of A;

      

       A3: o = m implies o in ( m-Spectrum A);

      m in ( m-Spectrum A);

      then o in ( m-Spectrum A) implies o = m by A1;

      then ( m-Spectrum A) = {m} by A3, TARSKI:def 1;

      hence thesis;

    end;

    theorem :: TOPZARI1:13

    

     Th17: (for x holds x in (( [#] A) \ J) implies x is Unit of A) implies A is local

    proof

      assume

       A1: (for x holds x in (( [#] A) \ J) implies x is Unit of A);

      consider m1 be maximal Ideal of A such that

       A2: J c= m1 by Th10;

      

       A3: for m be maximal Ideal of A holds m = m1

      proof

        let m be maximal Ideal of A;

        o in m implies o in m1

        proof

          assume

           A4: o in m;

          then o is NonUnit of A by Th15;

          then not o in (( [#] A) \ J) by A1;

          then o in J by A4, XBOOLE_0:def 5;

          hence thesis by A2;

        end;

        then m c= m1;

        hence thesis by RING_1:def 3;

      end;

      for o1,o2 be object st o1 in ( m-Spectrum A) & o2 in ( m-Spectrum A) holds o1 = o2

      proof

        let o1,o2 be object;

        assume that

         A8: o1 in ( m-Spectrum A) and

         A9: o2 in ( m-Spectrum A);

        consider x1 be maximal Ideal of A such that

         A10: x1 = o1 by A8;

        consider x2 be maximal Ideal of A such that

         A11: x2 = o2 by A9;

        o1 = m1 by A10, A3

        .= o2 by A3, A11;

        hence thesis;

      end;

      hence thesis by Th16;

    end;

    reserve m for maximal Ideal of A;

    theorem :: TOPZARI1:14

    

     Th18: a in (( [#] A) \ m) implies (( {a} -Ideal ) + m) = ( [#] A)

    proof

      assume

       A1: a in (( [#] A) \ m);

      

       A2: a in ( {a} -Ideal ) by IDEAL_1: 66;

      ( 0. A) in m by IDEAL_1: 3;

      then

       A4: (a + ( 0. A)) in { (x + y) where x,y be Element of A : x in ( {a} -Ideal ) & y in m } by A2;

      reconsider a as Element of A;

      

       A5: a in (( {a} -Ideal ) + m) by A4, IDEAL_1:def 19;

      (( {a} -Ideal ) + m) = m or (( {a} -Ideal ) + m) is non proper by IDEAL_1: 74, RING_1:def 3;

      hence thesis by A1, A5, XBOOLE_0:def 5;

    end;

    theorem :: TOPZARI1:15

    (for a holds a in m implies (( 1. A) + a) is Unit of A) implies A is local

    proof

      assume

       A1: (for a holds a in m implies (( 1. A) + a) is Unit of A);

      for x holds x in (( [#] A) \ m) implies x is Unit of A

      proof

        let x;

        assume

         A2: x in (( [#] A) \ m);

        then

        reconsider a0 = x as Element of A;

        (( {a0} -Ideal ) + m) = ( [#] A) by A2, Th18;

        then ( 1. A) in (( {a0} -Ideal ) + m);

        then ( 1. A) in { (p + q) where p,q be Element of A : p in ( {a0} -Ideal ) & q in m } by IDEAL_1:def 19;

        then

        consider p,q be Element of A such that

         A3: ( 1. A) = (p + q) and

         A4: p in ( {a0} -Ideal ) and

         A5: q in m;

        

         A6: ( {a0} -Ideal ) = the set of all (a0 * s) where s be Element of A by IDEAL_1: 64;

        consider s be Element of A such that

         A7: p = (a0 * s) by A4, A6;

        (( 1. A) + ( - q)) = ((a0 * s) + (( - q) + q)) by RLVECT_1:def 3, A3, A7

        .= ((a0 * s) + ( 0. A)) by RLVECT_1: 5

        .= (a0 * s);

        then (a0 * s) is Unit of A by A1, A5, IDEAL_1: 13;

        then ( {(a0 * s)} -Ideal ) = ( [#] A) by RING_2: 20;

        then

         A9: ( 1. A) in ( {(a0 * s)} -Ideal );

        ( {(a0 * s)} -Ideal ) = the set of all ((a0 * s) * t) where t be Element of A by IDEAL_1: 64;

        then

        consider t1 be Element of A such that

         A11: ( 1. A) = ((a0 * s) * t1) by A9;

        

         A12: (a0 * (s * t1)) = ( 1. A) by A11, GROUP_1:def 3;

        reconsider t = (s * t1) as Element of A;

        ( 1. A) in ( {a0} -Ideal ) by A6, A12;

        then not ( {a0} -Ideal ) is proper by IDEAL_1: 19;

        then ( {a0} -Ideal ) = ( [#] A);

        hence thesis by RING_2: 20;

      end;

      hence thesis by Th17;

    end;

    definition

      let R;

      let E be Subset of R;

      :: TOPZARI1:def11

      func PrimeIdeals (R,E) -> Subset of ( Spectrum R) equals

      : Def5: { p where p be Ideal of R : p is quasi-prime & p <> ( [#] R) & E c= p } if R is non degenerated

      otherwise {} ;

      coherence

      proof

        set X = { p where p be Ideal of R : p is quasi-prime & p <> ( [#] R) & E c= p };

        thus R is non degenerated implies { p where p be Ideal of R : p is quasi-prime & p <> ( [#] R) & E c= p } is Subset of ( Spectrum R)

        proof

          assume

           A1: R is non degenerated;

          X c= ( Spectrum R)

          proof

            let x be object;

            assume x in X;

            then

            consider p be Ideal of R such that

             A3: x = p and

             A4: p is quasi-prime and

             A5: p <> ( [#] R) and E c= p;

            p in { p where p be Ideal of R : p is quasi-prime & p <> ( [#] R) } by A4, A5;

            hence thesis by A3, A1, Def3;

          end;

          hence thesis;

        end;

        thus thesis by XBOOLE_1: 2;

      end;

      consistency ;

    end

    definition

      let A;

      let E be Subset of A;

      :: original: PrimeIdeals

      redefine

      :: TOPZARI1:def12

      func PrimeIdeals (A,E) -> Subset of ( Spectrum A) equals { p where p be prime Ideal of A : E c= p };

      correctness

      proof

        set C = { p where p be Ideal of A : p is quasi-prime & p <> ( [#] A) & E c= p };

        

         A1: x in ( PrimeIdeals (A,E)) implies x in { p where p be prime Ideal of A : E c= p }

        proof

          assume x in ( PrimeIdeals (A,E));

          then

           A3: x in C by Def5;

          consider I be Ideal of A such that

           A4: x = I and

           A5: I is quasi-prime and

           A6: I <> ( [#] A) and

           A7: E c= I by A3;

          reconsider I as prime Ideal of A by A5, A6, RING_1:def 2, SUBSET_1:def 6;

          I in { p where p be prime Ideal of A : E c= p } by A7;

          hence thesis by A4;

        end;

        x in { p where p be prime Ideal of A : E c= p } implies x in ( PrimeIdeals (A,E))

        proof

          assume x in { p where p be prime Ideal of A : E c= p };

          then

          consider I be prime Ideal of A such that

           A9: I = x and

           A10: E c= I;

          I in C by A10;

          hence thesis by A9, Def5;

        end;

        hence thesis by TARSKI: 2, A1;

      end;

    end

    registration

      let A, J;

      cluster ( PrimeIdeals (A,J)) -> non empty;

      coherence

      proof

        consider m be prime Ideal of A such that

         A1: J c= m by Th11;

        m in ( PrimeIdeals (A,J)) by A1;

        hence thesis;

      end;

    end

    

     Th21: ( PrimeIdeals (A, {( 0. A)})) = ( Spectrum A)

    proof

      ( Spectrum A) c= ( PrimeIdeals (A, {( 0. A)}))

      proof

        let x;

        assume x in ( Spectrum A);

        then

        consider J be prime Ideal of A such that

         A3: J = x;

         {( 0. A)} c= J by IDEAL_1: 2, ZFMISC_1: 31;

        hence thesis by A3;

      end;

      hence thesis;

    end;

    

     Th22: x in ( Spectrum A) implies x is prime Ideal of A

    proof

      assume x in ( Spectrum A);

      then

      consider x1 be prime Ideal of A such that

       A2: x1 = x;

      thus thesis by A2;

    end;

    reserve p for prime Ideal of A;

    reserve k for non zero Nat;

    theorem :: TOPZARI1:16

    

     Th23: not a in p implies not (a |^ k) in p

    proof

      assume

       A1: not a in p;

       not (a |^ k) in p

      proof

        defpred P[ Nat] means not (a |^ $1) in p;

        

         A2: P[1] by A1, BINOM: 8;

        

         A3: for k holds P[k] implies P[(k + 1)]

        proof

          let k;

          assume

           A4: P[k];

          

           A5: (a |^ (k + 1)) = ((a |^ k) * (a |^ 1)) by BINOM: 10;

           not (a |^ 1) in p by A1, BINOM: 8;

          hence thesis by A4, A5, RING_1:def 1;

        end;

        for k holds P[k] from NAT_1:sch 10( A2, A3);

        hence thesis;

      end;

      hence thesis;

    end;

    

     Lm24: (a |^ n) in p implies n <> 0

    proof

      assume

       A1: (a |^ n) in p;

      assume n = 0 ;

      then (a |^ n) = ( 1_ A) by BINOM: 8;

      then

       A5: {( 1. A)} c= p by A1, TARSKI:def 1;

      (p -Ideal ) = p by IDEAL_1: 44;

      then ( {( 1. A)} -Ideal ) c= p by A5, IDEAL_1: 57;

      then the carrier of A = p by IDEAL_1: 51;

      then p is non proper;

      hence contradiction;

    end;

    begin

    definition

      let A;

      :: TOPZARI1:def13

      func nilrad A -> Subset of A equals the set of all a where a be nilpotent Element of A;

      coherence

      proof

        set M = the set of all a where a be nilpotent Element of A;

        M c= the carrier of A

        proof

          let x be object;

          assume x in M;

          then ex a be nilpotent Element of A st a = x;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    

     Lm25: a is nilpotent implies a in ( sqrt {( 0. A)})

    proof

      set N = { a where a be Element of A : ex n be Element of NAT st (a |^ n) in {( 0. A)} };

      assume a is nilpotent;

      then

      consider n be non zero Nat such that

       A2: (a |^ n) = ( 0. A);

      

       A3: {( 0. A)} = ( {( 0. A)} -Ideal ) by IDEAL_1: 47;

      reconsider n as Element of NAT by ORDINAL1:def 12;

      reconsider s = a as Element of A;

      (s |^ n) in {( 0. A)} by A2, A3, IDEAL_1: 66;

      then a in N;

      hence a in ( sqrt {( 0. A)}) by IDEAL_1:def 24;

    end;

    

     Lm26: (a |^ n) in {( 0. A)} implies n <> 0

    proof

      assume

       A1: (a |^ n) in {( 0. A)};

      assume n = 0 ;

      then ( 1_ A) in {( 0. A)} by A1, BINOM: 8;

      hence contradiction by TARSKI:def 1;

    end;

    theorem :: TOPZARI1:17

    

     Th27: ( nilrad A) = ( sqrt {( 0. A)})

    proof

      set N = { a where a be Element of A : ex n be Element of NAT st (a |^ n) in {( 0. A)} };

      

       A1: for a be object st a in ( nilrad A) holds a in ( sqrt {( 0. A)})

      proof

        let a be object;

        assume a in ( nilrad A);

        then

        consider s be nilpotent Element of A such that

         A3: s = a;

        thus thesis by A3, Lm25;

      end;

      for a be object st a in ( sqrt {( 0. A)}) holds a in ( nilrad A)

      proof

        let a be object;

        assume a in ( sqrt {( 0. A)});

        then a in N by IDEAL_1:def 24;

        then

        consider s be Element of A such that

         A7: s = a & ex n be Element of NAT st (s |^ n) in {( 0. A)};

        consider n be Element of NAT such that

         A8: (s |^ n) in {( 0. A)} by A7;

        

         A9: (s |^ n) = ( 0. A) by A8, TARSKI:def 1;

        n is non zero Nat by A8, Lm26;

        then s is nilpotent by A9;

        hence thesis by A7;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    registration

      let A;

      cluster ( nilrad A) -> non empty;

      coherence

      proof

        ( sqrt {( 0. A)}) is non empty;

        hence thesis by Th27;

      end;

    end

    registration

      let A;

      cluster ( nilrad A) -> add-closed;

      coherence

      proof

        reconsider S = ( sqrt {( 0. A)}) as Ideal of A;

        S = ( nilrad A) by Th27;

        hence thesis;

      end;

    end

    registration

      let A;

      cluster ( nilrad A) -> left-ideal right-ideal;

      coherence

      proof

        reconsider S = ( sqrt {( 0. A)}) as Ideal of A;

        S = ( nilrad A) by Th27;

        hence thesis;

      end;

    end

    theorem :: TOPZARI1:18

    

     Th28: ( sqrt J) = ( meet ( PrimeIdeals (A,J)))

    proof

      for x be object st x in ( sqrt J) holds x in ( meet ( PrimeIdeals (A,J)))

      proof

        let x be object;

        assume x in ( sqrt J);

        then x in { a where a be Element of A : ex n be Element of NAT st (a |^ n) in J } by IDEAL_1:def 24;

        then

        consider y be Element of A such that

         A2: y = x and

         A3: ex n be Element of NAT st (y |^ n) in J;

        consider k be Element of NAT such that

         A4: (y |^ k) in J by A3;

        y in ( meet ( PrimeIdeals (A,J)))

        proof

          for Y be set holds Y in ( PrimeIdeals (A,J)) implies y in Y

          proof

            let Y be set;

            Y in ( PrimeIdeals (A,J)) implies y in Y

            proof

              assume Y in ( PrimeIdeals (A,J));

              then

              consider Y1 be prime Ideal of A such that

               A6: Y1 = Y and

               A7: J c= Y1;

              reconsider k as non zero Nat by A4, A7, Lm24;

              (y |^ k) in Y1 by A4, A7;

              hence thesis by A6, Th23;

            end;

            hence thesis;

          end;

          hence thesis by SETFAM_1:def 1;

        end;

        hence thesis by A2;

      end;

      then

       A9: ( sqrt J) c= ( meet ( PrimeIdeals (A,J)));

      set N1 = ( meet ( PrimeIdeals (A,J)));

      for x be object st not x in ( sqrt J) holds not x in N1

      proof

        let x be object;

        assume

         A10: not x in ( sqrt J);

        per cases ;

          suppose x in A;

          then

          reconsider x1 = x as Element of A;

          consider p be prime Ideal of A such that

           A12: not x1 in p and

           A13: J c= p by A10, Th9;

          p in ( PrimeIdeals (A,J)) by A13;

          hence thesis by A12, SETFAM_1:def 1;

        end;

          suppose

           A15: not x in A;

           not x in N1

          proof

            assume

             A16: x in N1;

            consider m be prime Ideal of A such that

             A17: J c= m by Th11;

            m in ( PrimeIdeals (A,J)) by A17;

            then x in m by A16, SETFAM_1:def 1;

            hence contradiction by A15;

          end;

          hence thesis;

        end;

      end;

      then ( meet ( PrimeIdeals (A,J))) c= ( sqrt J);

      hence thesis by A9;

    end;

    theorem :: TOPZARI1:19

    ( nilrad A) = ( meet ( Spectrum A))

    proof

      reconsider I = {( 0. A)} as proper Ideal of A by SUBSET_1:def 6;

      ( nilrad A) = ( sqrt {( 0. A)}) by Th27

      .= ( meet ( PrimeIdeals (A,I))) by Th28

      .= ( meet ( Spectrum A)) by Th21;

      hence thesis;

    end;

    theorem :: TOPZARI1:20

    

     Th30: I c= ( sqrt I)

    proof

      let x be object;

      assume

       A1: x in I;

      then

      reconsider x as Element of A;

      (x |^ 1) in I by A1, BINOM: 8;

      then x in { a where a be Element of A : ex n be Element of NAT st (a |^ n) in I };

      hence thesis by IDEAL_1:def 24;

    end;

    theorem :: TOPZARI1:21

    I c= J implies ( sqrt I) c= ( sqrt J)

    proof

      assume

       A1: I c= J;

      let s be object;

      assume

       A2: s in ( sqrt I);

      then

      reconsider s as Element of A;

      s in { a where a be Element of A : ex n be Element of NAT st (a |^ n) in I } by A2, IDEAL_1:def 24;

      then

      consider s1 be Element of A such that

       A3: s1 = s and

       A4: ex n be Element of NAT st (s1 |^ n) in I;

      consider n1 be Element of NAT such that

       A5: (s1 |^ n1) in I by A4;

      n1 <> 0

      proof

        assume n1 = 0 ;

        then (s1 |^ n1) = ( 1_ A) by BINOM: 8;

        hence contradiction by A1, A5, IDEAL_1: 19;

      end;

      then

      reconsider n1 as non zero Nat;

      s1 in { a where a be Element of A : ex n be Element of NAT st (a |^ n) in J } by A1, A5;

      hence thesis by A3, IDEAL_1:def 24;

    end;

    definition

      let A;

      :: TOPZARI1:def14

      func J-Rad A -> Subset of A equals ( meet ( m-Spectrum A));

      coherence ;

    end

    begin

    theorem :: TOPZARI1:22

    

     Th32: ( PrimeIdeals (A,S)) c= ( Ideals (A,S))

    proof

      let x be object;

      assume x in ( PrimeIdeals (A,S));

      then

      consider x1 be prime Ideal of A such that

       A2: x1 = x and

       A3: S c= x1;

      thus thesis by A2, A3;

    end;

    theorem :: TOPZARI1:23

    

     Th33: ( PrimeIdeals (A,S)) = (( Ideals (A,S)) /\ ( Spectrum A))

    proof

      thus ( PrimeIdeals (A,S)) c= (( Ideals (A,S)) /\ ( Spectrum A))

      proof

        let x be object;

        assume

         A2: x in ( PrimeIdeals (A,S));

        then

        consider x1 be prime Ideal of A such that

         A3: x1 = x and S c= x1;

        

         A4: x in ( Spectrum A) by A3;

        x in ( Ideals (A,S)) by A2, Th32, TARSKI:def 3;

        hence thesis by A4, XBOOLE_0:def 4;

      end;

      let x be object;

      assume x in (( Ideals (A,S)) /\ ( Spectrum A));

      then

       A8: x in ( Ideals (A,S)) & x in ( Spectrum A) by XBOOLE_0:def 4;

      then

      consider x1 be Ideal of A such that

       A10: x1 = x and

       A11: S c= x1;

      x1 is prime Ideal of A by A8, Th22, A10;

      hence thesis by A10, A11;

    end;

    theorem :: TOPZARI1:24

    

     Th34: ( PrimeIdeals (A,S)) = ( PrimeIdeals (A,(S -Ideal )))

    proof

      ( PrimeIdeals (A,S)) = (( Ideals (A,S)) /\ ( Spectrum A)) by Th33

      .= (( Ideals (A,(S -Ideal ))) /\ ( Spectrum A)) by Th2

      .= ( PrimeIdeals (A,(S -Ideal ))) by Th33;

      hence thesis;

    end;

    theorem :: TOPZARI1:25

    

     Th35: I c= p implies ( sqrt I) c= p

    proof

      assume

       A1: I c= p;

      let s be object;

      assume

       A2: s in ( sqrt I);

      then

      reconsider s as Element of A;

      s in { a where a be Element of A : ex n be Element of NAT st (a |^ n) in I } by A2, IDEAL_1:def 24;

      then

      consider s1 be Element of A such that

       A3: s1 = s and

       A4: ex n be Element of NAT st (s1 |^ n) in I;

      consider n1 be Element of NAT such that

       A5: (s1 |^ n1) in I by A4;

      n1 <> 0

      proof

        assume n1 = 0 ;

        then (s1 |^ n1) = ( 1_ A) by BINOM: 8;

        hence contradiction by A1, A5, IDEAL_1: 19;

      end;

      then

      reconsider n1 as non zero Nat;

      (s1 |^ n1) in p by A1, A5;

      hence thesis by A3, Th23;

    end;

    theorem :: TOPZARI1:26

    

     Th36: ( sqrt I) c= p implies I c= p

    proof

      assume

       A1: ( sqrt I) c= p;

      I c= ( sqrt I) by Th30;

      hence thesis by A1;

    end;

    theorem :: TOPZARI1:27

    

     Th37: ( PrimeIdeals (A,( sqrt (S -Ideal )))) = ( PrimeIdeals (A,(S -Ideal )))

    proof

      thus ( PrimeIdeals (A,( sqrt (S -Ideal )))) c= ( PrimeIdeals (A,(S -Ideal )))

      proof

        let p be object;

        assume p in ( PrimeIdeals (A,( sqrt (S -Ideal ))));

        then

        consider p1 be prime Ideal of A such that

         A3: p1 = p and

         A4: ( sqrt (S -Ideal )) c= p1;

        (S -Ideal ) c= p1 by A4, Th36;

        hence p in ( PrimeIdeals (A,(S -Ideal ))) by A3;

      end;

      let p be object;

      assume p in ( PrimeIdeals (A,(S -Ideal )));

      then

      consider p1 be prime Ideal of A such that

       A7: p1 = p and

       A8: (S -Ideal ) c= p1;

      ( sqrt (S -Ideal )) c= p1 by A8, Th35;

      hence p in ( PrimeIdeals (A,( sqrt (S -Ideal )))) by A7;

    end;

    theorem :: TOPZARI1:28

    

     Th38: E2 c= E1 implies ( PrimeIdeals (A,E1)) c= ( PrimeIdeals (A,E2))

    proof

      assume

       A1: E2 c= E1;

      let x;

      assume x in ( PrimeIdeals (A,E1));

      then

      consider x1 be prime Ideal of A such that

       A3: x1 = x and

       A4: E1 c= x1;

      E2 c= x1 by A1, A4;

      hence thesis by A3;

    end;

    theorem :: TOPZARI1:29

    ( PrimeIdeals (A,J1)) = ( PrimeIdeals (A,J2)) iff ( sqrt J1) = ( sqrt J2)

    proof

      thus ( PrimeIdeals (A,J1)) = ( PrimeIdeals (A,J2)) implies ( sqrt J1) = ( sqrt J2)

      proof

        assume

         A2: ( PrimeIdeals (A,J1)) = ( PrimeIdeals (A,J2));

        ( sqrt J1) = ( meet ( PrimeIdeals (A,J1))) by Th28

        .= ( sqrt J2) by Th28, A2;

        hence thesis;

      end;

      assume

       A3: ( sqrt J1) = ( sqrt J2);

      ( PrimeIdeals (A,J1)) = ( PrimeIdeals (A,(J1 -Ideal ))) by IDEAL_1: 44

      .= ( PrimeIdeals (A,( sqrt (J1 -Ideal )))) by Th37

      .= ( PrimeIdeals (A,( sqrt J1))) by IDEAL_1: 44

      .= ( PrimeIdeals (A,( sqrt (J2 -Ideal )))) by A3, IDEAL_1: 44

      .= ( PrimeIdeals (A,(J2 -Ideal ))) by Th37

      .= ( PrimeIdeals (A,J2)) by IDEAL_1: 44;

      hence thesis;

    end;

    theorem :: TOPZARI1:30

    

     Th40: (I1 *' I2) c= p implies I1 c= p or I2 c= p

    proof

       not (I1 c= p or I2 c= p) implies not ((I1 *' I2) c= p)

      proof

        assume

         A1: not (I1 c= p or I2 c= p);

        then

        consider x1 be object such that

         A2: x1 in I1 and

         A3: not x1 in p;

        consider x2 be object such that

         A4: x2 in I2 and

         A5: not x2 in p by A1;

        reconsider x1 as Element of A by A2;

        reconsider x2 as Element of A by A4;

        reconsider x = (x1 * x2) as Element of the carrier of A;

        reconsider seq = <*x*> as FinSequence of the carrier of A;

        

         A6: ( Sum seq) = x by BINOM: 3;

        

         A8: for i be Element of NAT st 1 <= i & i <= ( len seq) holds ex a,b be Element of A st (seq . i) = (a * b) & a in I1 & b in I2

        proof

          let i be Element of NAT ;

          assume that

           A9: 1 <= i and

           A10: i <= ( len seq);

          

           A11: i <= 1 by A10, FINSEQ_1: 40;

          (seq . i) = (seq . 1) by A9, XXREAL_0: 1, A11

          .= (x1 * x2) by FINSEQ_1: 40;

          hence thesis by A2, A4;

        end;

        

         A12: ( Sum seq) in { ( Sum s) where s be FinSequence of the carrier of A : for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of A st (s . i) = (a * b) & a in I1 & b in I2 } by A8;

        (x1 * x2) in (I1 *' I2) by A6, A12, IDEAL_1:def 21;

        hence thesis by A3, A5, RING_1:def 1;

      end;

      hence thesis;

    end;

    theorem :: TOPZARI1:31

    

     Th41A: ( PrimeIdeals (A, {( 1. A)})) = {}

    proof

      assume ( PrimeIdeals (A, {( 1. A)})) <> {} ;

      then

      consider p be object such that

       A2: p in ( PrimeIdeals (A, {( 1. A)})) by XBOOLE_0:def 1;

      consider p1 be prime Ideal of A such that p1 = p and

       A3: {( 1. A)} c= p1 by A2;

      ( 1. A) in {( 1. A)} by TARSKI:def 1;

      hence contradiction by A3, IDEAL_1: 19;

    end;

    

     Th41: ex E be non empty Subset of A st {} = ( PrimeIdeals (A,E))

    proof

      take {( 1. A)};

      thus thesis by Th41A;

    end;

    theorem :: TOPZARI1:32

    ( Spectrum A) = ( PrimeIdeals (A, {( 0. A)})) by Th21;

    

     Th42: ex E be non empty Subset of A st ( Spectrum A) = ( PrimeIdeals (A,E))

    proof

      take {( 0. A)};

      thus thesis by Th21;

    end;

    theorem :: TOPZARI1:33

    

     Th43: for E1,E2 be non empty Subset of A holds ex E3 be non empty Subset of A st (( PrimeIdeals (A,E1)) \/ ( PrimeIdeals (A,E2))) = ( PrimeIdeals (A,E3))

    proof

      let E1,E2 be non empty Subset of A;

      set F1 = ( PrimeIdeals (A,E1));

      set F2 = ( PrimeIdeals (A,E2));

      set I1 = (E1 -Ideal );

      set I2 = (E2 -Ideal );

      reconsider I3 = (I1 *' I2) as Ideal of A;

      

       A4: ( PrimeIdeals (A,E1)) = ( PrimeIdeals (A,I1)) by Th34;

      

       A5: ( PrimeIdeals (A,I3)) c= (( PrimeIdeals (A,I1)) \/ ( PrimeIdeals (A,I2)))

      proof

        let x be object;

        assume x in ( PrimeIdeals (A,I3));

        then

        consider x1 be prime Ideal of A such that

         A7: x1 = x and

         A8: I3 c= x1;

        

         A9: I1 c= x1 or I2 c= x1 by A8, Th40;

        x1 in { p where p be prime Ideal of A : I1 c= p } or x1 in { p where p be prime Ideal of A : I2 c= p } by A9;

        hence thesis by A7, XBOOLE_0:def 3;

      end;

      

       A11: (( PrimeIdeals (A,I1)) \/ ( PrimeIdeals (A,I2))) c= ( PrimeIdeals (A,I3))

      proof

        

         A12: (I1 *' I2) c= (I1 /\ I2) by IDEAL_1: 79;

        (I1 /\ I2) c= I1 by XBOOLE_1: 17;

        then

         A13: (I1 *' I2) c= I1 by A12;

        (I1 /\ I2) c= I2 by XBOOLE_1: 17;

        then (I1 *' I2) c= I2 by A12;

        then

         A14: ( PrimeIdeals (A,I2)) c= ( PrimeIdeals (A,(I1 *' I2))) by Th38;

        ( PrimeIdeals (A,I1)) c= ( PrimeIdeals (A,(I1 *' I2))) by A13, Th38;

        hence thesis by A14, XBOOLE_1: 8;

      end;

      ( PrimeIdeals (A,I3)) = (( PrimeIdeals (A,E1)) \/ ( PrimeIdeals (A,E2))) by A4, A5, A11, Th34;

      hence thesis;

    end;

    theorem :: TOPZARI1:34

    

     Th44: for G be Subset-Family of ( Spectrum A) st for S be set st S in G holds (ex E be non empty Subset of A st S = ( PrimeIdeals (A,E))) holds ex F be non empty Subset of A st ( Intersect G) = ( PrimeIdeals (A,F))

    proof

      let G be Subset-Family of ( Spectrum A);

      assume

       A1: for S be set st S in G holds (ex E be non empty Subset of A st S = ( PrimeIdeals (A,E)));

      per cases ;

        suppose

         A2: G <> {} ;

        then

        consider o such that

         A3: o in G by XBOOLE_0:def 1;

        reconsider o as set by A3;

        consider E be non empty Subset of A such that

         A4: o = ( PrimeIdeals (A,E)) by A1, A3;

        

         A5: ( meet G) = ( Intersect G) by A2, SETFAM_1:def 9;

        defpred X[ set] means ex Z be non empty Subset of A st $1 = Z & ex D be set st D in G & D = ( PrimeIdeals (A,Z));

        consider SFE be set such that

         A6: for x be set holds x in SFE iff x in ( bool the carrier of A) & X[x] from XFAMILY:sch 1;

        SFE c= ( bool the carrier of A) by A6;

        then

        reconsider SFE as non empty Subset-Family of the carrier of A by A3, A4, A6;

        E c= ( union SFE) by ZFMISC_1: 74, A3, A4, A6;

        then

         A8: ( union SFE) is non empty Subset of A;

        

         A9: x in ( Intersect G) implies x in ( PrimeIdeals (A,( union SFE)))

        proof

          assume

           A10: x in ( Intersect G);

          then

           A11: x in ( meet G) by A2, SETFAM_1:def 9;

          reconsider x as prime Ideal of A by A10, Th22;

          ( union SFE) c= x

          proof

            let o1;

            assume o1 in ( union SFE);

            then

            consider Y be set such that

             A13: o1 in Y and

             A14: Y in SFE by TARSKI:def 4;

            consider Z be non empty Subset of A such that

             A15: Z = Y and

             A16: ex D be set st D in G & D = ( PrimeIdeals (A,Z)) by A6, A14;

            consider D be set such that

             A17: D in G and

             A18: D = ( PrimeIdeals (A,Z)) by A16;

            x in D by A17, A11, SETFAM_1:def 1;

            then

            consider x1 be prime Ideal of A such that

             A19: x1 = x and

             A20: Z c= x1 by A18;

            thus thesis by A13, A15, A20, A19;

          end;

          hence thesis;

        end;

        x in ( PrimeIdeals (A,( union SFE))) implies x in ( Intersect G)

        proof

          assume

           A23: x in ( PrimeIdeals (A,( union SFE)));

          for Y be set holds Y in G implies x in Y

          proof

            let Y be set;

            assume

             A24: Y in G;

            then

            consider E be non empty Subset of A such that

             A25: Y = ( PrimeIdeals (A,E)) by A1;

            E c= ( union SFE) by A6, A24, A25, ZFMISC_1: 74;

            then ( PrimeIdeals (A,( union SFE))) c= ( PrimeIdeals (A,E)) by Th38;

            hence thesis by A25, A23;

          end;

          hence thesis by A2, A5, SETFAM_1:def 1;

        end;

        hence thesis by A8, A9, TARSKI: 2;

      end;

        suppose G = {} ;

        then ( Intersect G) = ( Spectrum A) by SETFAM_1:def 9;

        hence thesis by Th42;

      end;

    end;

    definition

      let A;

      :: TOPZARI1:def15

      func ZariskiTS (A) -> strict TopSpace means

      : Def7: the carrier of it = ( Spectrum A) & for F be Subset of it holds F is closed iff (ex E be non empty Subset of A st F = ( PrimeIdeals (A,E)));

      existence

      proof

        defpred C[ set] means ex Z be non empty Subset of A st $1 = ( PrimeIdeals (A,Z));

        

         A1: for F1,F2 be set st C[F1] & C[F2] holds C[(F1 \/ F2)] by Th43;

        

         A2: for G be Subset-Family of ( Spectrum A) st for S be set st S in G holds C[S] holds C[( Intersect G)] by Th44;

        

         A3: C[ {} ] & C[( Spectrum A)] by Th41, Th42;

        consider T be strict TopSpace such that

         A4: the carrier of T = ( Spectrum A) & for E be Subset of T holds E is closed iff C[E] from TOPGEN_3:sch 1( A3, A1, A2);

        take T;

        thus the carrier of T = ( Spectrum A) by A4;

        let F be Subset of T;

        thus thesis by A4;

      end;

      correctness

      proof

        let T1,T2 be strict TopSpace such that

         A5: the carrier of T1 = ( Spectrum A) and

         A6: for F be Subset of T1 holds F is closed iff ex Z1 be non empty Subset of A st F = ( PrimeIdeals (A,Z1)) and

         A7: the carrier of T2 = ( Spectrum A) and

         A8: for F be Subset of T2 holds F is closed iff ex Z2 be non empty Subset of A st F = ( PrimeIdeals (A,Z2));

        now

          let F be set;

          F is closed Subset of T1 iff ex Z1 be non empty Subset of A st F = ( PrimeIdeals (A,Z1)) by A5, A6;

          hence F is closed Subset of T1 iff F is closed Subset of T2 by A7, A8;

        end;

        hence thesis by TOPGEN_3: 6;

      end;

    end

    registration

      let A;

      cluster ( ZariskiTS A) -> non empty;

      coherence

      proof

        ( [#] ( ZariskiTS A)) = ( Spectrum A) by Def7;

        hence thesis;

      end;

    end

    

     Lm44: for P be Point of ( ZariskiTS A) holds P is prime Ideal of A

    proof

      let P be Point of ( ZariskiTS A);

      P in ( [#] ( ZariskiTS A));

      then P in ( Spectrum A) by Def7;

      hence thesis by Th22;

    end;

    theorem :: TOPZARI1:35

    

     Th45: for P,Q be Point of ( ZariskiTS A) st P <> Q holds ex V be Subset of ( ZariskiTS A) st V is open & (P in V & not Q in V or Q in V & not P in V)

    proof

      let P,Q be Point of ( ZariskiTS A);

      reconsider P1 = P, Q1 = Q as prime Ideal of A by Lm44;

      assume P <> Q;

      per cases ;

        suppose not Q c= P;

        then (Q \ P) <> {} by XBOOLE_1: 37;

        then

        consider x such that

         A3: x in (Q \ P) by XBOOLE_0:def 1;

        x in Q1 by A3;

        then

        reconsider x as Element of A;

        ( PrimeIdeals (A,( {x} -Ideal ))) is closed Subset of ( ZariskiTS A) by Def7;

        then

        reconsider W = (( [#] ( ZariskiTS A)) \ ( PrimeIdeals (A,( {x} -Ideal )))) as open Subset of ( ZariskiTS A) by PRE_TOPC:def 3;

        

         A5: not x in P by XBOOLE_0:def 5, A3;

        

         A6: not P in ( PrimeIdeals (A,( {x} -Ideal )))

        proof

          assume P in ( PrimeIdeals (A,( {x} -Ideal )));

          then

          consider P0 be prime Ideal of A such that

           A8: P = P0 and

           A9: ( {x} -Ideal ) c= P0;

          thus contradiction by A5, IDEAL_1: 66, A8, A9;

        end;

        ( {x} -Ideal ) c= (Q1 -Ideal ) by A3, ZFMISC_1: 31, IDEAL_1: 57;

        then ( {x} -Ideal ) c= Q1 by IDEAL_1: 44;

        then Q in ( PrimeIdeals (A,( {x} -Ideal )));

        then P in W & not Q in W by A6, XBOOLE_0:def 5;

        hence thesis;

      end;

        suppose Q c= P & Q <> P;

        then Q c< P;

        then

        consider x such that

         A13: x in P and

         A14: not x in Q by XBOOLE_0: 6;

        x in P1 by A13;

        then

        reconsider x as Element of A;

        ( PrimeIdeals (A,( {x} -Ideal ))) is closed Subset of ( ZariskiTS A) by Def7;

        then

        reconsider W = (( [#] ( ZariskiTS A)) \ ( PrimeIdeals (A,( {x} -Ideal )))) as open Subset of ( ZariskiTS A) by PRE_TOPC:def 3;

        

         A16: not Q in ( PrimeIdeals (A,( {x} -Ideal )))

        proof

          assume Q in ( PrimeIdeals (A,( {x} -Ideal )));

          then

          consider Q0 be prime Ideal of A such that

           A18: Q = Q0 and

           A19: ( {x} -Ideal ) c= Q0;

          thus contradiction by A14, IDEAL_1: 66, A18, A19;

        end;

        ( {x} -Ideal ) c= (P1 -Ideal ) by A13, ZFMISC_1: 31, IDEAL_1: 57;

        then ( {x} -Ideal ) c= P1 by IDEAL_1: 44;

        then P in ( PrimeIdeals (A,( {x} -Ideal )));

        then Q in W & not P in W by A16, XBOOLE_0:def 5;

        hence thesis;

      end;

    end;

    registration

      cluster degenerated for commutative Ring;

      existence

      proof

        take the trivial commutative Ring;

        thus thesis;

      end;

    end

    registration

      let R be degenerated commutative Ring;

      cluster ( ADTS ( Spectrum R)) -> T_0;

      coherence

      proof

        ( ADTS ( Spectrum R)) is empty by Def3;

        hence thesis;

      end;

    end

    registration

      let A;

      cluster ( ZariskiTS A) -> T_0;

      coherence

      proof

        for P,Q be Point of ( ZariskiTS A) st P <> Q holds ex V be Subset of ( ZariskiTS A) st V is open & (P in V & not Q in V or Q in V & not P in V) by Th45;

        hence thesis by T_0TOPSP:def 7;

      end;

    end

    begin

    reserve M0 for Ideal of B;

    

     Lm48: for x,y be Element of the carrier of A, h st h is RingHomomorphism & x in (h " M0) & y in (h " M0) holds (x + y) in (h " M0)

    proof

      let x,y be Element of the carrier of A;

      let h;

      assume that

       A1: h is RingHomomorphism and

       A2: x in (h " M0) and

       A3: y in (h " M0);

      

       A4: (h . x) in M0 by A2, FUNCT_1:def 7;

      

       A5: (h . y) in M0 by A3, FUNCT_1:def 7;

      reconsider a = x, b = y as Element of A;

      

       A6: h is additive by A1;

      ((h . x) + (h . y)) in M0 by A4, A5, IDEAL_1:def 1;

      then

       A8: (h . (x + y)) in M0 by A6;

      (x + y) in A;

      then (x + y) in ( dom h) by FUNCT_2:def 1;

      hence thesis by A8, FUNCT_1:def 7;

    end;

    

     Lm49: for r,x be Element of A, h st h is RingHomomorphism & x in (h " M0) holds (r * x) in (h " M0)

    proof

      let r,x be Element of A;

      let h;

      assume that

       A1: h is RingHomomorphism and

       A2: x in (h " M0);

      (h . x) in M0 by A2, FUNCT_1:def 7;

      then

       A5: ((h . r) * (h . x)) in M0 by IDEAL_1:def 2;

      h is multiplicative by A1;

      then

       A6: (h . (r * x)) in M0 by A5;

      (r * x) in A;

      then (r * x) in ( dom h) by FUNCT_2:def 1;

      hence thesis by A6, FUNCT_1:def 7;

    end;

    theorem :: TOPZARI1:36

    

     Th50: h is RingHomomorphism implies (h " M0) is Ideal of A

    proof

      assume

       A1: h is RingHomomorphism;

      then

       A2: (h " M0) is add-closed by Lm48;

      

       A3: (h " M0) is left-ideal by A1, Lm49;

      

       A6: ( dom h) = the carrier of A by FUNCT_2:def 1;

      (h . ( 0. A)) = ( 0. B) by A1, RING_2: 6;

      then (h . ( 0. A)) in M0 by IDEAL_1: 2;

      then ( 0. A) in (h " M0) by A6, FUNCT_1:def 7;

      hence thesis by A2, A3;

    end;

    reserve M0 for prime Ideal of B;

    theorem :: TOPZARI1:37

    

     Th51: h is RingHomomorphism implies (h " M0) is prime Ideal of A

    proof

      assume

       A1: h is RingHomomorphism;

      

       A2: for x,y be Element of A st (x * y) in (h " M0) holds x in (h " M0) or y in (h " M0)

      proof

        let x,y be Element of A;

        assume (x * y) in (h " M0);

        then (x * y) in ( dom h) & (h . (x * y)) in M0 by FUNCT_1:def 7;

        then

         A4: ((h . x) * (h . y)) in M0 by A1, GROUP_6:def 6;

        

         A5: ( dom h) = the carrier of A by FUNCT_2:def 1;

        x in (h " M0) or y in (h " M0)

        proof

          per cases by A4, RING_1:def 1;

            suppose (h . x) in M0;

            hence thesis by A5, FUNCT_1:def 7;

          end;

            suppose (h . y) in M0;

            hence thesis by A5, FUNCT_1:def 7;

          end;

        end;

        hence thesis;

      end;

      (h " M0) <> the carrier of A

      proof

        assume

         A9: (h " M0) = the carrier of A;

        

         A10: h is unity-preserving by A1;

        ( 1. B) in M0 by A9, FUNCT_1:def 7, A10;

        hence contradiction by IDEAL_1: 19;

      end;

      then (h " M0) is proper quasi-prime by A2;

      hence thesis by A1, Th50;

    end;

    definition

      let A, B, h;

      assume

       A0: h is RingHomomorphism;

      :: TOPZARI1:def16

      func Spec h -> Function of ( ZariskiTS B), ( ZariskiTS A) means

      : Def9: for x be Point of ( ZariskiTS B) holds (it . x) = (h " x);

      existence

      proof

        defpred P[ Point of ( ZariskiTS B), object] means $2 = (h " $1);

        

         A1: for x be Point of ( ZariskiTS B) holds ex y be Point of ( ZariskiTS A) st P[x, y]

        proof

          let x be Point of ( ZariskiTS B);

          x is prime Ideal of B by Lm44;

          then (h " x) is prime Ideal of A by A0, Th51;

          then (h " x) in ( Spectrum A);

          then

          reconsider y = (h " x) as Point of ( ZariskiTS A) by Def7;

           P[x, y];

          hence thesis;

        end;

        consider f be Function of ( ZariskiTS B), ( ZariskiTS A) such that

         A2: for x be Point of ( ZariskiTS B) holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        thus thesis by A2;

      end;

      uniqueness

      proof

        let f,g be Function of ( ZariskiTS B), ( ZariskiTS A);

        assume that

         A3: for x be Point of ( ZariskiTS B) holds (f . x) = (h " x) and

         A4: for x be Point of ( ZariskiTS B) holds (g . x) = (h " x);

        now

          let x be Point of ( ZariskiTS B);

          (f . x) = (h " x) by A3;

          hence (f . x) = (g . x) by A4;

        end;

        hence thesis;

      end;

    end

    theorem :: TOPZARI1:38

    

     Th52: h is RingHomomorphism implies (( Spec h) " ( PrimeIdeals (A,E))) = ( PrimeIdeals (B,(h .: E)))

    proof

      assume

       A1: h is RingHomomorphism;

      thus (( Spec h) " ( PrimeIdeals (A,E))) c= ( PrimeIdeals (B,(h .: E)))

      proof

        let x;

        assume

         A3: x in (( Spec h) " ( PrimeIdeals (A,E)));

        then

         A4: x in ( dom ( Spec h)) & (( Spec h) . x) in ( PrimeIdeals (A,E)) by FUNCT_1:def 7;

        reconsider x1 = x as Point of ( ZariskiTS B) by A3;

        (h " x1) in { p where p be prime Ideal of A : E c= p } by A1, Def9, A4;

        then

        consider q be prime Ideal of A such that

         A6: q = (h " x1) and

         A7: E c= q;

        

         A8: (h .: E) c= (h .: (h " x1)) by A6, A7, RELAT_1: 123;

        (h .: (h " x1)) c= x1 by FUNCT_1: 75;

        then

         A9: (h .: E) c= x1 by A8;

        x1 in the carrier of ( ZariskiTS B);

        then x1 in ( Spectrum B) by Def7;

        then x1 is prime Ideal of B by Th22;

        hence thesis by A9;

      end;

      let x;

      assume x in ( PrimeIdeals (B,(h .: E)));

      then

      consider q be prime Ideal of B such that

       A12: x = q and

       A13: (h .: E) c= q;

      

       A14: (h " (h .: E)) c= (h " q) by A13, RELAT_1: 143;

      E c= (h " (h .: E)) by FUNCT_2: 42;

      then

       A15: E c= (h " q) by A14;

      (h " q) is prime Ideal of A by A1, Th51;

      then

       A17: (h " q) in ( PrimeIdeals (A,E)) by A15;

      

       A18: ( dom ( Spec h)) = the carrier of ( ZariskiTS B) by FUNCT_2:def 1;

      q in ( Spectrum B);

      then

      reconsider q1 = q as Point of ( ZariskiTS B) by Def7;

      (( Spec h) . q1) in ( PrimeIdeals (A,E)) by A17, A1, Def9;

      hence thesis by A12, A18, FUNCT_1:def 7;

    end;

    theorem :: TOPZARI1:39

    h is RingHomomorphism implies ( Spec h) is continuous

    proof

      assume

       A1: h is RingHomomorphism;

      for P1 be Subset of ( ZariskiTS A) st P1 is closed holds (( Spec h) " P1) is closed

      proof

        let P1 be Subset of ( ZariskiTS A);

        assume P1 is closed;

        then

        consider E be non empty Subset of A such that

         A3: P1 = ( PrimeIdeals (A,E)) by Def7;

        

         A4: ( dom h) = the carrier of A by FUNCT_2:def 1;

        (( Spec h) " P1) = ( PrimeIdeals (B,(h .: E))) by A3, A1, Th52;

        then

        consider E1 be non empty Subset of B such that E1 = (h .: E) and

         A5: (( Spec h) " P1) = ( PrimeIdeals (B,E1)) by A4;

        thus thesis by A5, Def7;

      end;

      hence thesis by PRE_TOPC:def 6;

    end;