![]() |
Metamath
Proof Explorer Theorem List (p. 332 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lmat22det 33101 | The determinant of a literal 2x2 complex matrix. (Contributed by Thierry Arnoux, 1-Sep-2020.) |
β’ π = (litMatββ¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ Β· = (.rβπ ) & β’ β = (-gβπ ) & β’ π = (Baseβπ ) & β’ π½ = ((1...2) maDet π ) & β’ (π β π β Ring) β β’ (π β (π½βπ) = ((π΄ Β· π·) β (πΆ Β· π΅))) | ||
Theorem | mdetpmtr1 33102* | The determinant of a matrix with permuted rows is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π· = (π maDet π ) & β’ πΊ = (Baseβ(SymGrpβπ)) & β’ π = (pmSgnβπ) & β’ π = (β€RHomβπ ) & β’ Β· = (.rβπ ) & β’ πΈ = (π β π, π β π β¦ ((πβπ)ππ)) β β’ (((π β CRing β§ π β Fin) β§ (π β π΅ β§ π β πΊ)) β (π·βπ) = (((π β π)βπ) Β· (π·βπΈ))) | ||
Theorem | mdetpmtr2 33103* | The determinant of a matrix with permuted columns is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π· = (π maDet π ) & β’ πΊ = (Baseβ(SymGrpβπ)) & β’ π = (pmSgnβπ) & β’ π = (β€RHomβπ ) & β’ Β· = (.rβπ ) & β’ πΈ = (π β π, π β π β¦ (ππ(πβπ))) β β’ (((π β CRing β§ π β Fin) β§ (π β π΅ β§ π β πΊ)) β (π·βπ) = (((π β π)βπ) Β· (π·βπΈ))) | ||
Theorem | mdetpmtr12 33104* | The determinant of a matrix with permuted rows and columns is the determinant of the original matrix multiplied by the product of the signs of the permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π· = (π maDet π ) & β’ πΊ = (Baseβ(SymGrpβπ)) & β’ π = (pmSgnβπ) & β’ π = (β€RHomβπ ) & β’ Β· = (.rβπ ) & β’ πΈ = (π β π, π β π β¦ ((πβπ)π(πβπ))) & β’ (π β π β CRing) & β’ (π β π β Fin) & β’ (π β π β π΅) & β’ (π β π β πΊ) & β’ (π β π β πΊ) β β’ (π β (π·βπ) = ((πβ((πβπ) Β· (πβπ))) Β· (π·βπΈ))) | ||
Theorem | mdetlap1 33105* | A Laplace expansion of the determinant of a matrix, using the adjunct (cofactor) matrix. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π· = (π maDet π ) & β’ πΎ = (π maAdju π ) & β’ Β· = (.rβπ ) β β’ ((π β CRing β§ π β π΅ β§ πΌ β π) β (π·βπ) = (π Ξ£g (π β π β¦ ((πΌππ) Β· (π(πΎβπ)πΌ))))) | ||
Theorem | madjusmdetlem1 33106* | Lemma for madjusmdet 33110. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π΅ = (Baseβπ΄) & β’ π΄ = ((1...π) Mat π ) & β’ π· = ((1...π) maDet π ) & β’ πΎ = ((1...π) maAdju π ) & β’ Β· = (.rβπ ) & β’ π = (β€RHomβπ ) & β’ πΈ = ((1...(π β 1)) maDet π ) & β’ (π β π β β) & β’ (π β π β CRing) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β π΅) & β’ πΊ = (Baseβ(SymGrpβ(1...π))) & β’ π = (pmSgnβ(1...π)) & β’ π = (πΌ(((1...π) minMatR1 π )βπ)π½) & β’ π = (π β (1...π), π β (1...π) β¦ ((πβπ)π(πβπ))) & β’ (π β π β πΊ) & β’ (π β π β πΊ) & β’ (π β (πβπ) = πΌ) & β’ (π β (πβπ) = π½) & β’ (π β (πΌ(subMat1βπ)π½) = (π(subMat1βπ)π)) β β’ (π β (π½(πΎβπ)πΌ) = ((πβ((πβπ) Β· (πβπ))) Β· (πΈβ(πΌ(subMat1βπ)π½)))) | ||
Theorem | madjusmdetlem2 33107* | Lemma for madjusmdet 33110. (Contributed by Thierry Arnoux, 26-Aug-2020.) |
β’ π΅ = (Baseβπ΄) & β’ π΄ = ((1...π) Mat π ) & β’ π· = ((1...π) maDet π ) & β’ πΎ = ((1...π) maAdju π ) & β’ Β· = (.rβπ ) & β’ π = (β€RHomβπ ) & β’ πΈ = ((1...(π β 1)) maDet π ) & β’ (π β π β β) & β’ (π β π β CRing) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β π΅) & β’ π = (π β (1...π) β¦ if(π = 1, πΌ, if(π β€ πΌ, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π, if(π β€ π, (π β 1), π))) β β’ ((π β§ π β (1...(π β 1))) β if(π < πΌ, π, (π + 1)) = ((π β β‘π)βπ)) | ||
Theorem | madjusmdetlem3 33108* | Lemma for madjusmdet 33110. (Contributed by Thierry Arnoux, 27-Aug-2020.) |
β’ π΅ = (Baseβπ΄) & β’ π΄ = ((1...π) Mat π ) & β’ π· = ((1...π) maDet π ) & β’ πΎ = ((1...π) maAdju π ) & β’ Β· = (.rβπ ) & β’ π = (β€RHomβπ ) & β’ πΈ = ((1...(π β 1)) maDet π ) & β’ (π β π β β) & β’ (π β π β CRing) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β π΅) & β’ π = (π β (1...π) β¦ if(π = 1, πΌ, if(π β€ πΌ, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π, if(π β€ π, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π½, if(π β€ π½, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π, if(π β€ π, (π β 1), π))) & β’ π = (π β (1...π), π β (1...π) β¦ (((π β β‘π)βπ)π((π β β‘π)βπ))) & β’ (π β π β π΅) β β’ (π β (πΌ(subMat1βπ)π½) = (π(subMat1βπ)π)) | ||
Theorem | madjusmdetlem4 33109* | Lemma for madjusmdet 33110. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π΅ = (Baseβπ΄) & β’ π΄ = ((1...π) Mat π ) & β’ π· = ((1...π) maDet π ) & β’ πΎ = ((1...π) maAdju π ) & β’ Β· = (.rβπ ) & β’ π = (β€RHomβπ ) & β’ πΈ = ((1...(π β 1)) maDet π ) & β’ (π β π β β) & β’ (π β π β CRing) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β π΅) & β’ π = (π β (1...π) β¦ if(π = 1, πΌ, if(π β€ πΌ, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π, if(π β€ π, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π½, if(π β€ π½, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π, if(π β€ π, (π β 1), π))) β β’ (π β (π½(πΎβπ)πΌ) = ((πβ(-1β(πΌ + π½))) Β· (πΈβ(πΌ(subMat1βπ)π½)))) | ||
Theorem | madjusmdet 33110 | Express the cofactor of the matrix, i.e. the entries of its adjunct matrix, using determinant of submatrices. (Contributed by Thierry Arnoux, 23-Aug-2020.) |
β’ π΅ = (Baseβπ΄) & β’ π΄ = ((1...π) Mat π ) & β’ π· = ((1...π) maDet π ) & β’ πΎ = ((1...π) maAdju π ) & β’ Β· = (.rβπ ) & β’ π = (β€RHomβπ ) & β’ πΈ = ((1...(π β 1)) maDet π ) & β’ (π β π β β) & β’ (π β π β CRing) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β π΅) β β’ (π β (π½(πΎβπ)πΌ) = ((πβ(-1β(πΌ + π½))) Β· (πΈβ(πΌ(subMat1βπ)π½)))) | ||
Theorem | mdetlap 33111* | Laplace expansion of the determinant of a square matrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π΅ = (Baseβπ΄) & β’ π΄ = ((1...π) Mat π ) & β’ π· = ((1...π) maDet π ) & β’ πΎ = ((1...π) maAdju π ) & β’ Β· = (.rβπ ) & β’ π = (β€RHomβπ ) & β’ πΈ = ((1...(π β 1)) maDet π ) & β’ (π β π β β) & β’ (π β π β CRing) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β π΅) β β’ (π β (π·βπ) = (π Ξ£g (π β (1...π) β¦ ((πβ(-1β(πΌ + π))) Β· ((πΌππ) Β· (πΈβ(πΌ(subMat1βπ)π))))))) | ||
Theorem | ist0cld 33112* | The predicate "is a T0 space", using closed sets. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
β’ (π β π΅ = βͺ π½) & β’ (π β π· = (Clsdβπ½)) β β’ (π β (π½ β Kol2 β (π½ β Top β§ βπ₯ β π΅ βπ¦ β π΅ (βπ β π· (π₯ β π β π¦ β π) β π₯ = π¦)))) | ||
Theorem | txomap 33113* | Given two open maps πΉ and πΊ, π» mapping pairs of sets, is also an open map for the product topology. (Contributed by Thierry Arnoux, 29-Dec-2019.) |
β’ (π β πΉ:πβΆπ) & β’ (π β πΊ:πβΆπ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β π β (TopOnβπ)) & β’ ((π β§ π₯ β π½) β (πΉ β π₯) β πΏ) & β’ ((π β§ π¦ β πΎ) β (πΊ β π¦) β π) & β’ (π β π΄ β (π½ Γt πΎ)) & β’ π» = (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) β β’ (π β (π» β π΄) β (πΏ Γt π)) | ||
Theorem | qtopt1 33114* | If every equivalence class is closed, then the quotient space is T1 . (Contributed by Thierry Arnoux, 5-Jan-2020.) |
β’ π = βͺ π½ & β’ (π β π½ β Fre) & β’ (π β πΉ:πβontoβπ) & β’ ((π β§ π₯ β π) β (β‘πΉ β {π₯}) β (Clsdβπ½)) β β’ (π β (π½ qTop πΉ) β Fre) | ||
Theorem | qtophaus 33115* | If an open map's graph in the product space (π½ Γt π½) is closed, then its quotient topology is Hausdorff. (Contributed by Thierry Arnoux, 4-Jan-2020.) |
β’ π = βͺ π½ & β’ βΌ = (β‘πΉ β πΉ) & β’ π» = (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) & β’ (π β π½ β Haus) & β’ (π β πΉ:πβontoβπ) & β’ ((π β§ π₯ β π½) β (πΉ β π₯) β (π½ qTop πΉ)) & β’ (π β βΌ β (Clsdβ(π½ Γt π½))) β β’ (π β (π½ qTop πΉ) β Haus) | ||
Theorem | circtopn 33116* | The topology of the unit circle is generated by open intervals of the polar coordinate. (Contributed by Thierry Arnoux, 4-Jan-2020.) |
β’ πΌ = (0[,](2 Β· Ο)) & β’ π½ = (topGenβran (,)) & β’ πΉ = (π₯ β β β¦ (expβ(i Β· π₯))) & β’ πΆ = (β‘abs β {1}) β β’ (π½ qTop πΉ) = (TopOpenβ(πΉ βs βfld)) | ||
Theorem | circcn 33117* | The function gluing the real line into the unit circle is continuous. (Contributed by Thierry Arnoux, 5-Jan-2020.) |
β’ πΌ = (0[,](2 Β· Ο)) & β’ π½ = (topGenβran (,)) & β’ πΉ = (π₯ β β β¦ (expβ(i Β· π₯))) & β’ πΆ = (β‘abs β {1}) β β’ πΉ β (π½ Cn (π½ qTop πΉ)) | ||
Theorem | reff 33118* | For any cover refinement, there exists a function associating with each set in the refinement a set in the original cover containing it. This is sometimes used as a definition of refinement. Note that this definition uses the axiom of choice through ac6sg 10487. (Contributed by Thierry Arnoux, 12-Jan-2020.) |
β’ (π΄ β π β (π΄Refπ΅ β (βͺ π΅ β βͺ π΄ β§ βπ(π:π΄βΆπ΅ β§ βπ£ β π΄ π£ β (πβπ£))))) | ||
Theorem | locfinreflem 33119* | A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf, it is expressed by exposing a function π from the original cover π, which is taken as the index set. The solution is constructed by building unions, so the same method can be used to prove a similar theorem about closed covers. (Contributed by Thierry Arnoux, 29-Jan-2020.) |
β’ π = βͺ π½ & β’ (π β π β π½) & β’ (π β π = βͺ π) & β’ (π β π β π½) & β’ (π β πRefπ) & β’ (π β π β (LocFinβπ½)) β β’ (π β βπ((Fun π β§ dom π β π β§ ran π β π½) β§ (ran πRefπ β§ ran π β (LocFinβπ½)))) | ||
Theorem | locfinref 33120* | A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf, it is expressed by exposing a function π from the original cover π, which is taken as the index set. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
β’ π = βͺ π½ & β’ (π β π β π½) & β’ (π β π = βͺ π) & β’ (π β π β π½) & β’ (π β πRefπ) & β’ (π β π β (LocFinβπ½)) β β’ (π β βπ(π:πβΆπ½ β§ ran πRefπ β§ ran π β (LocFinβπ½))) | ||
Syntax | ccref 33121 | The "every open cover has an π΄ refinement" predicate. |
class CovHasRefπ΄ | ||
Definition | df-cref 33122* | Define a statement "every open cover has an π΄ refinement" , where π΄ is a property for refinements like "finite", "countable", "point finite" or "locally finite". (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ CovHasRefπ΄ = {π β Top β£ βπ¦ β π« π(βͺ π = βͺ π¦ β βπ§ β (π« π β© π΄)π§Refπ¦)} | ||
Theorem | iscref 33123* | The property that every open cover has an π΄ refinement for the topological space π½. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ π = βͺ π½ β β’ (π½ β CovHasRefπ΄ β (π½ β Top β§ βπ¦ β π« π½(π = βͺ π¦ β βπ§ β (π« π½ β© π΄)π§Refπ¦))) | ||
Theorem | crefeq 33124 | Equality theorem for the "every open cover has an A refinement" predicate. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π΄ = π΅ β CovHasRefπ΄ = CovHasRefπ΅) | ||
Theorem | creftop 33125 | A space where every open cover has an π΄ refinement is a topological space. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π½ β CovHasRefπ΄ β π½ β Top) | ||
Theorem | crefi 33126* | The property that every open cover has an π΄ refinement for the topological space π½. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ π = βͺ π½ β β’ ((π½ β CovHasRefπ΄ β§ πΆ β π½ β§ π = βͺ πΆ) β βπ§ β (π« π½ β© π΄)π§RefπΆ) | ||
Theorem | crefdf 33127* | A formulation of crefi 33126 easier to use for definitions. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ π = βͺ π½ & β’ π΅ = CovHasRefπ΄ & β’ (π§ β π΄ β π) β β’ ((π½ β π΅ β§ πΆ β π½ β§ π = βͺ πΆ) β βπ§ β π« π½(π β§ π§RefπΆ)) | ||
Theorem | crefss 33128 | The "every open cover has an π΄ refinement" predicate respects inclusion. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π΄ β π΅ β CovHasRefπ΄ β CovHasRefπ΅) | ||
Theorem | cmpcref 33129 | Equivalent definition of compact space in terms of open cover refinements. Compact spaces are topologies with finite open cover refinements. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ Comp = CovHasRefFin | ||
Theorem | cmpfiref 33130* | Every open cover of a Compact space has a finite refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
β’ π = βͺ π½ β β’ ((π½ β Comp β§ π β π½ β§ π = βͺ π) β βπ£ β π« π½(π£ β Fin β§ π£Refπ)) | ||
Syntax | cldlf 33131 | Extend class notation with the class of all LindelΓΆf spaces. |
class Ldlf | ||
Definition | df-ldlf 33132 | Definition of a LindelΓΆf space. A LindelΓΆf space is a topological space in which every open cover has a countable subcover. Definition 1 of [BourbakiTop2] p. 195. (Contributed by Thierry Arnoux, 30-Jan-2020.) |
β’ Ldlf = CovHasRef{π₯ β£ π₯ βΌ Ο} | ||
Theorem | ldlfcntref 33133* | Every open cover of a LindelΓΆf space has a countable refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
β’ π = βͺ π½ β β’ ((π½ β Ldlf β§ π β π½ β§ π = βͺ π) β βπ£ β π« π½(π£ βΌ Ο β§ π£Refπ)) | ||
Syntax | cpcmp 33134 | Extend class notation with the class of all paracompact topologies. |
class Paracomp | ||
Definition | df-pcmp 33135 | Definition of a paracompact topology. A topology is said to be paracompact iff every open cover has an open refinement that is locally finite. The definition 6 of [BourbakiTop1] p. I.69. also requires the topology to be Hausdorff, but this is dropped here. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ Paracomp = {π β£ π β CovHasRef(LocFinβπ)} | ||
Theorem | ispcmp 33136 | The predicate "is a paracompact topology". (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π½ β Paracomp β π½ β CovHasRef(LocFinβπ½)) | ||
Theorem | cmppcmp 33137 | Every compact space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π½ β Comp β π½ β Paracomp) | ||
Theorem | dispcmp 33138 | Every discrete space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π β π β π« π β Paracomp) | ||
Theorem | pcmplfin 33139* | Given a paracompact topology π½ and an open cover π, there exists an open refinement π£ that is locally finite. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
β’ π = βͺ π½ β β’ ((π½ β Paracomp β§ π β π½ β§ π = βͺ π) β βπ£ β π« π½(π£ β (LocFinβπ½) β§ π£Refπ)) | ||
Theorem | pcmplfinf 33140* | Given a paracompact topology π½ and an open cover π, there exists an open refinement ran π that is locally finite, using the same index as the original cover π. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
β’ π = βͺ π½ β β’ ((π½ β Paracomp β§ π β π½ β§ π = βͺ π) β βπ(π:πβΆπ½ β§ ran πRefπ β§ ran π β (LocFinβπ½))) | ||
The prime ideals of a ring π can be endowed with the Zariski topology. This is done by defining a function π which maps ideals of π to closed sets (see for example zarcls0 33147 for the definition of π). The closed sets of the topology are in the range of π (see zartopon 33156). The correspondence with the open sets is made in zarcls 33153. As proved in zart0 33158, the Zariski topology is T0 , but generally not T1 . | ||
Syntax | crspec 33141 | Extend class notation with the spectrum of a ring. |
class Spec | ||
Definition | df-rspec 33142 | Define the spectrum of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
β’ Spec = (π β Ring β¦ ((IDLsrgβπ) βΎs (PrmIdealβπ))) | ||
Theorem | rspecval 33143 | Value of the spectrum of the ring π . Notation 1.1.1 of [EGA] p. 80. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
β’ (π β Ring β (Specβπ ) = ((IDLsrgβπ ) βΎs (PrmIdealβπ ))) | ||
Theorem | rspecbas 33144 | The prime ideals form the base of the spectrum of a ring. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
β’ π = (Specβπ ) β β’ (π β Ring β (PrmIdealβπ ) = (Baseβπ)) | ||
Theorem | rspectset 33145* | Topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
β’ π = (Specβπ ) & β’ πΌ = (LIdealβπ ) & β’ π½ = ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) β β’ (π β Ring β π½ = (TopSetβπ)) | ||
Theorem | rspectopn 33146* | The topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 4-Jun-2024.) |
β’ π = (Specβπ ) & β’ πΌ = (LIdealβπ ) & β’ π = (PrmIdealβπ ) & β’ π½ = ran (π β πΌ β¦ {π β π β£ Β¬ π β π}) β β’ (π β Ring β π½ = (TopOpenβπ)) | ||
Theorem | zarcls0 33147* | The closure of the identity ideal in the Zariski topology. Proposition 1.1.2(i) of [EGA] p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
β’ π = (π β (LIdealβπ ) β¦ {π β (PrmIdealβπ ) β£ π β π}) & β’ π = (PrmIdealβπ ) & β’ 0 = (0gβπ ) β β’ (π β Ring β (πβ{ 0 }) = π) | ||
Theorem | zarcls1 33148* | The unit ideal π΅ is the only ideal whose closure in the Zariski topology is the empty set. Stronger form of the Proposition 1.1.2(i) of [EGA] p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
β’ π = (π β (LIdealβπ ) β¦ {π β (PrmIdealβπ ) β£ π β π}) & β’ π΅ = (Baseβπ ) β β’ ((π β CRing β§ πΌ β (LIdealβπ )) β ((πβπΌ) = β β πΌ = π΅)) | ||
Theorem | zarclsun 33149* | The union of two closed sets of the Zariski topology is closed. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
β’ π = (π β (LIdealβπ ) β¦ {π β (PrmIdealβπ ) β£ π β π}) β β’ ((π β CRing β§ π β ran π β§ π β ran π) β (π βͺ π) β ran π) | ||
Theorem | zarclsiin 33150* | In a Zariski topology, the intersection of the closures of a family of ideals is the closure of the span of their union. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
β’ π = (π β (LIdealβπ ) β¦ {π β (PrmIdealβπ ) β£ π β π}) & β’ πΎ = (RSpanβπ ) β β’ ((π β Ring β§ π β (LIdealβπ ) β§ π β β ) β β© π β π (πβπ) = (πβ(πΎββͺ π))) | ||
Theorem | zarclsint 33151* | The intersection of a family of closed sets is closed in the Zariski topology. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
β’ π = (π β (LIdealβπ ) β¦ {π β (PrmIdealβπ ) β£ π β π}) β β’ ((π β CRing β§ π β ran π β§ π β β ) β β© π β ran π) | ||
Theorem | zarclssn 33152* | The closed points of Zariski topology are the maximal ideals. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
β’ π = (π β (LIdealβπ ) β¦ {π β (PrmIdealβπ ) β£ π β π}) & β’ π΅ = (LIdealβπ ) β β’ ((π β CRing β§ π β π΅) β ({π} = (πβπ) β π β (MaxIdealβπ ))) | ||
Theorem | zarcls 33153* | The open sets of the Zariski topology are the complements of the closed sets. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
β’ π = (Specβπ ) & β’ π½ = (TopOpenβπ) & β’ π = (PrmIdealβπ ) & β’ π = (π β (LIdealβπ ) β¦ {π β π β£ π β π}) β β’ (π β Ring β π½ = {π β π« π β£ (π β π ) β ran π}) | ||
Theorem | zartopn 33154* | The Zariski topology is a topology, and its closed sets are images by π of the ideals of π . (Contributed by Thierry Arnoux, 16-Jun-2024.) |
β’ π = (Specβπ ) & β’ π½ = (TopOpenβπ) & β’ π = (PrmIdealβπ ) & β’ π = (π β (LIdealβπ ) β¦ {π β π β£ π β π}) β β’ (π β CRing β (π½ β (TopOnβπ) β§ ran π = (Clsdβπ½))) | ||
Theorem | zartop 33155 | The Zariski topology is a topology. Proposition 1.1.2 of [EGA] p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
β’ π = (Specβπ ) & β’ π½ = (TopOpenβπ) β β’ (π β CRing β π½ β Top) | ||
Theorem | zartopon 33156 | The points of the Zariski topology are the prime ideals. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
β’ π = (Specβπ ) & β’ π½ = (TopOpenβπ) & β’ π = (PrmIdealβπ ) β β’ (π β CRing β π½ β (TopOnβπ)) | ||
Theorem | zar0ring 33157 | The Zariski Topology of the trivial ring. (Contributed by Thierry Arnoux, 1-Jul-2024.) |
β’ π = (Specβπ ) & β’ π½ = (TopOpenβπ) & β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ (β―βπ΅) = 1) β π½ = {β }) | ||
Theorem | zart0 33158 | The Zariski topology is T0 . Corollary 1.1.8 of [EGA] p. 81. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
β’ π = (Specβπ ) & β’ π½ = (TopOpenβπ) β β’ (π β CRing β π½ β Kol2) | ||
Theorem | zarmxt1 33159 | The Zariski topology restricted to maximal ideals is T1 . (Contributed by Thierry Arnoux, 16-Jun-2024.) |
β’ π = (Specβπ ) & β’ π½ = (TopOpenβπ) & β’ π = (MaxIdealβπ ) & β’ π = (π½ βΎt π) β β’ (π β CRing β π β Fre) | ||
Theorem | zarcmplem 33160* | Lemma for zarcmp 33161. (Contributed by Thierry Arnoux, 2-Jul-2024.) |
β’ π = (Specβπ ) & β’ π½ = (TopOpenβπ) & β’ π = (π β (LIdealβπ ) β¦ {π β (PrmIdealβπ ) β£ π β π}) β β’ (π β CRing β π½ β Comp) | ||
Theorem | zarcmp 33161 | The Zariski topology is compact. Proposition 1.1.10(ii) of [EGA], p. 82. (Contributed by Thierry Arnoux, 2-Jul-2024.) |
β’ π = (Specβπ ) & β’ π½ = (TopOpenβπ) β β’ (π β CRing β π½ β Comp) | ||
Theorem | rspectps 33162 | The spectrum of a ring π is a topological space. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
β’ π = (Specβπ ) β β’ (π β CRing β π β TopSp) | ||
Theorem | rhmpreimacnlem 33163* | Lemma for rhmpreimacn 33164. (Contributed by Thierry Arnoux, 7-Jul-2024.) |
β’ π = (Specβπ ) & β’ π = (Specβπ) & β’ π΄ = (PrmIdealβπ ) & β’ π΅ = (PrmIdealβπ) & β’ π½ = (TopOpenβπ) & β’ πΎ = (TopOpenβπ) & β’ πΊ = (π β π΅ β¦ (β‘πΉ β π)) & β’ (π β π β CRing) & β’ (π β π β CRing) & β’ (π β πΉ β (π RingHom π)) & β’ (π β ran πΉ = (Baseβπ)) & β’ (π β πΌ β (LIdealβπ )) & β’ π = (π β (LIdealβπ ) β¦ {π β π΄ β£ π β π}) & β’ π = (π β (LIdealβπ) β¦ {π β π΅ β£ π β π}) β β’ (π β (πβ(πΉ β πΌ)) = (β‘πΊ β (πβπΌ))) | ||
Theorem | rhmpreimacn 33164* | The function mapping a prime ideal to its preimage by a surjective ring homomorphism is continuous, when considering the Zariski topology. Corollary 1.2.3 of [EGA], p. 83. Notice that the direction of the continuous map πΊ is reverse: the original ring homomorphism πΉ goes from π to π, but the continuous map πΊ goes from π΅ to π΄. This mapping is also called "induced map on prime spectra" or "pullback on primes". (Contributed by Thierry Arnoux, 8-Jul-2024.) |
β’ π = (Specβπ ) & β’ π = (Specβπ) & β’ π΄ = (PrmIdealβπ ) & β’ π΅ = (PrmIdealβπ) & β’ π½ = (TopOpenβπ) & β’ πΎ = (TopOpenβπ) & β’ πΊ = (π β π΅ β¦ (β‘πΉ β π)) & β’ (π β π β CRing) & β’ (π β π β CRing) & β’ (π β πΉ β (π RingHom π)) & β’ (π β ran πΉ = (Baseβπ)) β β’ (π β πΊ β (πΎ Cn π½)) | ||
Syntax | cmetid 33165 | Extend class notation with the class of metric identifications. |
class ~Met | ||
Syntax | cpstm 33166 | Extend class notation with the metric induced by a pseudometric. |
class pstoMet | ||
Definition | df-metid 33167* | Define the metric identification relation for a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
β’ ~Met = (π β βͺ ran PsMet β¦ {β¨π₯, π¦β© β£ ((π₯ β dom dom π β§ π¦ β dom dom π) β§ (π₯ππ¦) = 0)}) | ||
Definition | df-pstm 33168* | Define the metric induced by a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
β’ pstoMet = (π β βͺ ran PsMet β¦ (π β (dom dom π / (~Metβπ)), π β (dom dom π / (~Metβπ)) β¦ βͺ {π§ β£ βπ₯ β π βπ¦ β π π§ = (π₯ππ¦)})) | ||
Theorem | metidval 33169* | Value of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
β’ (π· β (PsMetβπ) β (~Metβπ·) = {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π) β§ (π₯π·π¦) = 0)}) | ||
Theorem | metidss 33170 | As a relation, the metric identification is a subset of a Cartesian product. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
β’ (π· β (PsMetβπ) β (~Metβπ·) β (π Γ π)) | ||
Theorem | metidv 33171 | π΄ and π΅ identify by the metric π· if their distance is zero. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
β’ ((π· β (PsMetβπ) β§ (π΄ β π β§ π΅ β π)) β (π΄(~Metβπ·)π΅ β (π΄π·π΅) = 0)) | ||
Theorem | metideq 33172 | Basic property of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
β’ ((π· β (PsMetβπ) β§ (π΄(~Metβπ·)π΅ β§ πΈ(~Metβπ·)πΉ)) β (π΄π·πΈ) = (π΅π·πΉ)) | ||
Theorem | metider 33173 | The metric identification is an equivalence relation. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
β’ (π· β (PsMetβπ) β (~Metβπ·) Er π) | ||
Theorem | pstmval 33174* | Value of the metric induced by a pseudometric π·. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
β’ βΌ = (~Metβπ·) β β’ (π· β (PsMetβπ) β (pstoMetβπ·) = (π β (π / βΌ ), π β (π / βΌ ) β¦ βͺ {π§ β£ βπ₯ β π βπ¦ β π π§ = (π₯π·π¦)})) | ||
Theorem | pstmfval 33175 | Function value of the metric induced by a pseudometric π· (Contributed by Thierry Arnoux, 11-Feb-2018.) |
β’ βΌ = (~Metβπ·) β β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β ([π΄] βΌ (pstoMetβπ·)[π΅] βΌ ) = (π΄π·π΅)) | ||
Theorem | pstmxmet 33176 | The metric induced by a pseudometric is a full-fledged metric on the equivalence classes of the metric identification. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
β’ βΌ = (~Metβπ·) β β’ (π· β (PsMetβπ) β (pstoMetβπ·) β (βMetβ(π / βΌ ))) | ||
Theorem | hauseqcn 33177 | In a Hausdorff topology, two continuous functions which agree on a dense set agree everywhere. (Contributed by Thierry Arnoux, 28-Dec-2017.) |
β’ π = βͺ π½ & β’ (π β πΎ β Haus) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β πΊ β (π½ Cn πΎ)) & β’ (π β (πΉ βΎ π΄) = (πΊ βΎ π΄)) & β’ (π β π΄ β π) & β’ (π β ((clsβπ½)βπ΄) = π) β β’ (π β πΉ = πΊ) | ||
Theorem | elunitge0 33178 | An element of the closed unit interval is positive. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 20-Dec-2016.) |
β’ (π΄ β (0[,]1) β 0 β€ π΄) | ||
Theorem | unitssxrge0 33179 | The closed unit interval is a subset of the set of the extended nonnegative reals. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
β’ (0[,]1) β (0[,]+β) | ||
Theorem | unitdivcld 33180 | Necessary conditions for a quotient to be in the closed unit interval. (somewhat too strong, it would be sufficient that A and B are in RR+) (Contributed by Thierry Arnoux, 20-Dec-2016.) |
β’ ((π΄ β (0[,]1) β§ π΅ β (0[,]1) β§ π΅ β 0) β (π΄ β€ π΅ β (π΄ / π΅) β (0[,]1))) | ||
Theorem | iistmd 33181 | The closed unit interval forms a topological monoid under multiplication. (Contributed by Thierry Arnoux, 25-Mar-2017.) |
β’ πΌ = ((mulGrpββfld) βΎs (0[,]1)) β β’ πΌ β TopMnd | ||
Theorem | unicls 33182 | The union of the closed set is the underlying set of the topology. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
β’ π½ β Top & β’ π = βͺ π½ β β’ βͺ (Clsdβπ½) = π | ||
Theorem | tpr2tp 33183 | The usual topology on (β Γ β) is the product topology of the usual topology on β. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
β’ π½ = (topGenβran (,)) β β’ (π½ Γt π½) β (TopOnβ(β Γ β)) | ||
Theorem | tpr2uni 33184 | The usual topology on (β Γ β) is the product topology of the usual topology on β. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
β’ π½ = (topGenβran (,)) β β’ βͺ (π½ Γt π½) = (β Γ β) | ||
Theorem | xpinpreima 33185 | Rewrite the cartesian product of two sets as the intersection of their preimage by 1st and 2nd, the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
β’ (π΄ Γ π΅) = ((β‘(1st βΎ (V Γ V)) β π΄) β© (β‘(2nd βΎ (V Γ V)) β π΅)) | ||
Theorem | xpinpreima2 33186 | Rewrite the cartesian product of two sets as the intersection of their preimage by 1st and 2nd, the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
β’ ((π΄ β πΈ β§ π΅ β πΉ) β (π΄ Γ π΅) = ((β‘(1st βΎ (πΈ Γ πΉ)) β π΄) β© (β‘(2nd βΎ (πΈ Γ πΉ)) β π΅))) | ||
Theorem | sqsscirc1 33187 | The complex square of side π· is a subset of the complex circle of radius π·. (Contributed by Thierry Arnoux, 25-Sep-2017.) |
β’ ((((π β β β§ 0 β€ π) β§ (π β β β§ 0 β€ π)) β§ π· β β+) β ((π < (π· / 2) β§ π < (π· / 2)) β (ββ((πβ2) + (πβ2))) < π·)) | ||
Theorem | sqsscirc2 33188 | The complex square of side π· is a subset of the complex disc of radius π·. (Contributed by Thierry Arnoux, 25-Sep-2017.) |
β’ (((π΄ β β β§ π΅ β β) β§ π· β β+) β (((absβ(ββ(π΅ β π΄))) < (π· / 2) β§ (absβ(ββ(π΅ β π΄))) < (π· / 2)) β (absβ(π΅ β π΄)) < π·)) | ||
Theorem | cnre2csqlem 33189* | Lemma for cnre2csqima 33190. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
β’ (πΊ βΎ (β Γ β)) = (π» β πΉ) & β’ πΉ Fn (β Γ β) & β’ πΊ Fn V & β’ (π₯ β (β Γ β) β (πΊβπ₯) β β) & β’ ((π₯ β ran πΉ β§ π¦ β ran πΉ) β (π»β(π₯ β π¦)) = ((π»βπ₯) β (π»βπ¦))) β β’ ((π β (β Γ β) β§ π β (β Γ β) β§ π· β β+) β (π β (β‘(πΊ βΎ (β Γ β)) β (((πΊβπ) β π·)(,)((πΊβπ) + π·))) β (absβ(π»β((πΉβπ) β (πΉβπ)))) < π·)) | ||
Theorem | cnre2csqima 33190* | Image of a centered square by the canonical bijection from (β Γ β) to β. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
β’ πΉ = (π₯ β β, π¦ β β β¦ (π₯ + (i Β· π¦))) β β’ ((π β (β Γ β) β§ π β (β Γ β) β§ π· β β+) β (π β ((((1st βπ) β π·)(,)((1st βπ) + π·)) Γ (((2nd βπ) β π·)(,)((2nd βπ) + π·))) β ((absβ(ββ((πΉβπ) β (πΉβπ)))) < π· β§ (absβ(ββ((πΉβπ) β (πΉβπ)))) < π·))) | ||
Theorem | tpr2rico 33191* | For any point of an open set of the usual topology on (β Γ β) there is an open square which contains that point and is entirely in the open set. This is square is actually a ball by the (πβ+β) norm π. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
β’ π½ = (topGenβran (,)) & β’ πΊ = (π’ β β, π£ β β β¦ (π’ + (i Β· π£))) & β’ π΅ = ran (π₯ β ran (,), π¦ β ran (,) β¦ (π₯ Γ π¦)) β β’ ((π΄ β (π½ Γt π½) β§ π β π΄) β βπ β π΅ (π β π β§ π β π΄)) | ||
Theorem | cnvordtrestixx 33192* | The restriction of the 'greater than' order to an interval gives the same topology as the subspace topology. (Contributed by Thierry Arnoux, 1-Apr-2017.) |
β’ π΄ β β* & β’ ((π₯ β π΄ β§ π¦ β π΄) β (π₯[,]π¦) β π΄) β β’ ((ordTopβ β€ ) βΎt π΄) = (ordTopβ(β‘ β€ β© (π΄ Γ π΄))) | ||
Theorem | prsdm 33193 | Domain of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = ((leβπΎ) β© (π΅ Γ π΅)) β β’ (πΎ β Proset β dom β€ = π΅) | ||
Theorem | prsrn 33194 | Range of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = ((leβπΎ) β© (π΅ Γ π΅)) β β’ (πΎ β Proset β ran β€ = π΅) | ||
Theorem | prsss 33195 | Relation of a subproset. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = ((leβπΎ) β© (π΅ Γ π΅)) β β’ ((πΎ β Proset β§ π΄ β π΅) β ( β€ β© (π΄ Γ π΄)) = ((leβπΎ) β© (π΄ Γ π΄))) | ||
Theorem | prsssdm 33196 | Domain of a subproset relation. (Contributed by Thierry Arnoux, 12-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = ((leβπΎ) β© (π΅ Γ π΅)) β β’ ((πΎ β Proset β§ π΄ β π΅) β dom ( β€ β© (π΄ Γ π΄)) = π΄) | ||
Theorem | ordtprsval 33197* | Value of the order topology for a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = ((leβπΎ) β© (π΅ Γ π΅)) & β’ πΈ = ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦ β€ π₯}) & β’ πΉ = ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯ β€ π¦}) β β’ (πΎ β Proset β (ordTopβ β€ ) = (topGenβ(fiβ({π΅} βͺ (πΈ βͺ πΉ))))) | ||
Theorem | ordtprsuni 33198* | Value of the order topology. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = ((leβπΎ) β© (π΅ Γ π΅)) & β’ πΈ = ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π¦ β€ π₯}) & β’ πΉ = ran (π₯ β π΅ β¦ {π¦ β π΅ β£ Β¬ π₯ β€ π¦}) β β’ (πΎ β Proset β π΅ = βͺ ({π΅} βͺ (πΈ βͺ πΉ))) | ||
Theorem | ordtcnvNEW 33199 | The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015.) (Revised by Thierry Arnoux, 13-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = ((leβπΎ) β© (π΅ Γ π΅)) β β’ (πΎ β Proset β (ordTopββ‘ β€ ) = (ordTopβ β€ )) | ||
Theorem | ordtrestNEW 33200 | The subspace topology of an order topology is in general finer than the topology generated by the restricted order, but we do have inclusion in one direction. (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = ((leβπΎ) β© (π΅ Γ π΅)) β β’ ((πΎ β Proset β§ π΄ β π΅) β (ordTopβ( β€ β© (π΄ Γ π΄))) β ((ordTopβ β€ ) βΎt π΄)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |