Irreducibility of prime spectrum

In this file we show some results on irreducibility of the prime spectrum of a ring.

theorem PrimeSpectrum.preirreducibleSpace_iff {R : Type u_2} [CommSemiring R] : PreirreducibleSpace (PrimeSpectrum R) ↔ (minimalPrimes R).Subsingleton

Spec R is preirreducible if and only if R has at most one minimal prime.

theorem PrimeSpectrum.irreducibleSpace_iff {R : Type u_2} [CommSemiring R] : IrreducibleSpace (PrimeSpectrum R) ↔ Nontrivial R ∧ (minimalPrimes R).Subsingleton

Spec R is irreducible if and only if R has a unique minimal prime.

theorem PrimeSpectrum.irreducibleSpace_iff_of_ringEquiv {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) : IrreducibleSpace (PrimeSpectrum R) ↔ IrreducibleSpace (PrimeSpectrum S)

theorem Ideal.IsPrime.nontrivial {R : Type u_2} [Semiring R] {I : Ideal R} (hI : I.IsPrime) : Nontrivial R

theorem RingHom.isIntegral_algebraMap_iff {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] : (algebraMap R S).IsIntegral ↔ Algebra.IsIntegral R S

theorem Algebra.TensorProduct.isIntegral_includeRight (R : Type u_2) (S : Type u_3) (T : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra.IsIntegral R T] : includeRight.IsIntegral

theorem PrimeSpectrum.irreducibleSpace_of_isSeparable {k : Type u} {R : Type u_1} [Field k] [CommRing R] [Algebra k R] (H : ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra k K] [Module.Finite k K] [Algebra.IsSeparable k K], IrreducibleSpace (PrimeSpectrum (TensorProduct k K R))) (Ω : Type u) [Field Ω] [Algebra k Ω] [Algebra.IsSeparable k Ω] : IrreducibleSpace (PrimeSpectrum (TensorProduct k Ω R))

If Spec (K ⊗[k] R) is irreducible for every finite, separable extension K of k, the same holds for Spec (Ω ⊗[k] R) for every separable extension Ω of k.

theorem PrimeSpectrum.comap_quotientMk_surjective_of_le_nilradical {R : Type u_2} [CommRing R] (I : Ideal R) (hle : I ≤ nilradical R) : Function.Surjective ⇑(comap (Ideal.Quotient.mk I))

theorem PrimeSpectrum.irreducibleSpace_iff_of_isPurelyInseparable (k : Type u_2) (R : Type u_3) [CommRing R] [Field k] [Algebra k R] (K : Type u_4) [Field K] [Algebra k K] (L : Type u_5) [Field L] [Algebra k L] [Algebra K L] [IsScalarTower k K L] [IsPurelyInseparable K L] : IrreducibleSpace (PrimeSpectrum (TensorProduct k K R)) ↔ IrreducibleSpace (PrimeSpectrum (TensorProduct k L R))

theorem PrimeSpectrum.irreducibleSpace_iff_of_isAlgClosure_of_isSepClosure (k : Type u_2) (R : Type u_3) [CommRing R] [Field k] [Algebra k R] (K : Type u_4) [Field K] [Algebra k K] [IsSepClosure k K] (L : Type u_5) [Field L] [Algebra k L] [IsAlgClosure k L] : IrreducibleSpace (PrimeSpectrum (TensorProduct k K R)) ↔ IrreducibleSpace (PrimeSpectrum (TensorProduct k L R))

theorem PrimeSpectrum.irreducibleSpace_iff_of_isAlgClosure_of_isSepClosed (k : Type u_2) (R : Type u_3) [CommRing R] [Field k] [Algebra k R] [IsSepClosed k] (L : Type u_4) [Field L] [Algebra k L] [IsAlgClosure k L] : IrreducibleSpace (PrimeSpectrum R) ↔ IrreducibleSpace (PrimeSpectrum (TensorProduct k L R))

noncomputable def PrimeSpectrum.algEquiv_residueField_of_isAlgClosed {k : Type u} {R : Type u_1} [Field k] [CommRing R] [Algebra k R] [IsAlgClosed k] [Algebra.FiniteType k R] (p : PrimeSpectrum R) [hp : p.asIdeal.IsMaximal] : k ≃ₐ[k] p.asIdeal.ResidueField

Equations

• One or more equations did not get rendered due to their size.

theorem minimalPrimes_eq_singleton_nilradical {R : Type u_2} [CommRing R] [IrreducibleSpace (PrimeSpectrum R)] : minimalPrimes R = {nilradical R}

theorem isDomain_iff_isReduced_and_irreducibleSpace {R : Type u_2} [CommRing R] : IsDomain R ↔ IsReduced R ∧ IrreducibleSpace (PrimeSpectrum R)

A ring is a domain if and only if it is reduced and its prime spectrum is irreducible.

noncomputable def homeomorph_ofClosedDenseEmbedding {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (hfc : Topology.IsClosedEmbedding f) (hfd : DenseRange f) : X ≃ₜ Y

Equations

• homeomorph_ofClosedDenseEmbedding f hfc hfd = IsHomeomorph.homeomorph f ⋯

theorem geo_reduced_iff_reduce_alg_closed {k : Type u_2} {R : Type u_3} [Field k] [IsAlgClosed k] [CommRing R] [Algebra k R] [IsReduced R] : Algebra.IsGeometricallyReduced k R

theorem PrimeSpectrum.irreducibleSpace_tensorProduct_of_isAlgClosed {k : Type u} {R : Type u_1} [Field k] [CommRing R] [Algebra k R] [IsAlgClosed k] {S : Type u_2} [CommRing S] [Algebra k S] (hR : IrreducibleSpace (PrimeSpectrum R)) (hS : IrreducibleSpace (PrimeSpectrum S)) : IrreducibleSpace (PrimeSpectrum (TensorProduct k R S))

Stacks Tag 00I7 (For algebraically closed fields.)

theorem PrimeSpectrum.irreducibleSpace_tensorProduct_of_isSepClosed {k : Type u} {R : Type u_1} [Field k] [CommRing R] [Algebra k R] [IsSepClosed k] {S : Type u_2} [CommRing S] [Algebra k S] (hR : IrreducibleSpace (PrimeSpectrum R)) (hS : IrreducibleSpace (PrimeSpectrum S)) : IrreducibleSpace (PrimeSpectrum (TensorProduct k R S))

Stacks Tag 00I7

theorem PrimeSpectrum.irreducibleSpace_of_faithfullyFlat {R : Type u_1} [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S] [IrreducibleSpace (PrimeSpectrum S)] : IrreducibleSpace (PrimeSpectrum R)

theorem Module.FaithfullyFlat.of_isBaseChange {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module S N] [Module R N] [IsScalarTower R S N] {f : M →ₗ[R] N} (hf : IsBaseChange S f) [FaithfullyFlat R M] : FaithfullyFlat S N

theorem PrimeSpectrum.irreducibleSpace_of_isScalarTower {k : Type u} {R : Type u_1} [Field k] [CommRing R] [Algebra k R] (K : Type u_2) (L : Type u_3) [Field K] [Field L] [Algebra k K] [Algebra k L] [Algebra K L] [IsScalarTower k K L] [IrreducibleSpace (PrimeSpectrum (TensorProduct k L R))] : IrreducibleSpace (PrimeSpectrum (TensorProduct k K R))