let A be non degenerated commutative Ring; :: thesis: for q being proper Ideal of A st sqrt q is maximal holds
A / q is local
let q be proper Ideal of A; :: thesis: ( sqrt q is maximal implies A / q is local )
set m = sqrt q;
set E = { I where I is Ideal of (A / q) : ( I is quasi-maximal & I <> [#] (A / q) ) } ;
assume A1: sqrt q is maximal ; :: thesis: A / q is local
A2: (canHom q) .: (sqrt q) = nilrad (A / q) by Th37;
for m1, m2 being object st m1 in m-Spectrum (A / q) & m2 in m-Spectrum (A / q) holds
m1 = m2
proof
let m1, m2 be object ; :: thesis: ( m1 in m-Spectrum (A / q) & m2 in m-Spectrum (A / q) implies m1 = m2 )
assume ( m1 in m-Spectrum (A / q) & m2 in m-Spectrum (A / q) ) ; :: thesis: m1 = m2
then A4: ( m1 in { I where I is Ideal of (A / q) : ( I is quasi-maximal & I <> [#] (A / q) ) } & m2 in { I where I is Ideal of (A / q) : ( I is quasi-maximal & I <> [#] (A / q) ) } ) by TOPZARI1:def 7;
then consider M1 being Ideal of (A / q) such that
A5: M1 = m1 and
A6: ( M1 is quasi-maximal & M1 <> [#] (A / q) ) ;
consider M2 being Ideal of (A / q) such that
A7: M2 = m2 and
A8: ( M2 is quasi-maximal & M2 <> [#] (A / q) ) by A4;
A9: M1 is proper by A6;
A10: M2 is proper by A8;
set S = { I where I is Ideal of (A / q) : ( I is quasi-prime & I <> [#] (A / q) ) } ;
H: Spectrum (A / q) = { I where I is prime Ideal of (A / q) : verum } by TOPZARI1:def 6;
then M1 in Spectrum (A / q) by A6, A9;
then meet (Spectrum (A / q)) c= M1 by SETFAM_1:3;
then A11: nilrad (A / q) c= M1 by TOPZARI1:19;
set M = nilrad (A / q);
nilrad (A / q) is maximal by A1, TOPZARI1:20, Th30, A2;
then A12: ( nilrad (A / q) is proper & nilrad (A / q) is quasi-maximal ) ;
then A13: ( M1 = nilrad (A / q) or not M1 is proper ) by A11;
M2 in Spectrum (A / q) by H, A8, A10;
then meet (Spectrum (A / q)) c= M2 by SETFAM_1:3;
then nilrad (A / q) c= M2 by TOPZARI1:19;
then A15: ( M2 = nilrad (A / q) or not M2 is proper ) by A12;
m1 = m2
proof
assume A16: m1 <> m2 ; :: thesis: contradiction
per cases ( ( M1 = nilrad (A / q) & M2 = nilrad (A / q) ) or ( M1 = nilrad (A / q) & M2 = [#] (A / q) ) or ( M1 = [#] (A / q) & M2 = nilrad (A / q) ) or ( M1 = [#] (A / q) & M2 = [#] (A / q) ) ) by A13, A15;
suppose ( M1 = nilrad (A / q) & M2 = nilrad (A / q) ) ; :: thesis: contradiction
hence contradiction by A16, A5, A7; :: thesis: verum
end;
suppose ( M1 = nilrad (A / q) & M2 = [#] (A / q) ) ; :: thesis: contradiction
hence contradiction by A8; :: thesis: verum
end;
suppose ( M1 = [#] (A / q) & M2 = nilrad (A / q) ) ; :: thesis: contradiction
hence contradiction by A6; :: thesis: verum
end;
suppose ( M1 = [#] (A / q) & M2 = [#] (A / q) ) ; :: thesis: contradiction
hence contradiction by A16, A5, A7; :: thesis: verum
end;
end;
end;
hence m1 = m2 ; :: thesis: verum
end;
hence A / q is local by TOPZARI1:12; :: thesis: verum