The idempotent cutting out a connected component

When Spec R is locally connected, the connected component of a point x is clopen. The idempotent--clopen correspondence therefore supplies a canonical idempotent eₓ : R whose basic open is that component. Equivalently, the ideal (1 - eₓ) cuts out the component as a closed subset, and the spectrum of R / (1 - eₓ) is homeomorphic to it.

The construction is stated under the natural topological hypothesis LocallyConnectedSpace (PrimeSpectrum R). In particular it applies to Noetherian rings, for which Tau Ceti already supplies the locally connected instance.

Main declarations

• PrimeSpectrum.quotientHomeomorphZeroLocus: the spectrum of a quotient is homeomorphic to the zero locus of the quotient ideal.
• PrimeSpectrum.connectedComponentIdempotent: the idempotent selecting the component of a point.
• PrimeSpectrum.map_connectedComponentIdempotent: an automorphism transports component idempotents along the induced map on prime spectra.
• PrimeSpectrum.connectedComponentIdeal: the ideal generated by its complementary idempotent.
• PrimeSpectrum.map_connectedComponentIdeal: an automorphism transports component ideals.
• PrimeSpectrum.apply_mem_connectedComponentIdeal_iff: the corresponding elementwise membership equivalence.
• PrimeSpectrum.primeSpectrumQuotientHomeomorphConnectedComponent: the spectrum of the quotient by that ideal is the selected connected component.

References

• The Stacks Project, Tag 00EE, for the idempotent--clopen correspondence.
• J. S. Milne, Algebraic Groups (2017), Section 2.a, for the identity-component construction.

This ordinary connected-component construction is a commutative-algebra prerequisite for the geometric identity component in Layer 3 of the ReductiveGroups roadmap; it does not itself assert compatibility with base change.

theorem PrimeSpectrum.range_comap_quotientMk_eq_zeroLocus {R : Type u} [CommRing R] (I : Ideal R) : Set.range (comap (Ideal.Quotient.mk I)) = zeroLocus ↑I

The image of the spectrum of a quotient is the zero locus of the quotient ideal.

noncomputable def PrimeSpectrum.quotientHomeomorphZeroLocus {R : Type u} [CommRing R] (I : Ideal R) : PrimeSpectrum (R ⧸ I) ≃ₜ ↑(zeroLocus ↑I)

The spectrum of R / I is homeomorphic to the zero locus of I in Spec R.

Equations

• PrimeSpectrum.quotientHomeomorphZeroLocus I = ⋯.toHomeomorph.trans (Homeomorph.setCongr ⋯)

@[simp]

theorem PrimeSpectrum.quotientHomeomorphZeroLocus_apply_coe {R : Type u} [CommRing R] (I : Ideal R) (y : PrimeSpectrum (R ⧸ I)) : ↑((quotientHomeomorphZeroLocus I) y) = comap (Ideal.Quotient.mk I) y

After coercion to PrimeSpectrum R, the quotient-spectrum homeomorphism sends a point to its contraction along the quotient map.

noncomputable def PrimeSpectrum.connectedComponentIdempotent {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (x : PrimeSpectrum R) : R

The idempotent whose basic open is the connected component of x in Spec R.

It is the inverse image of the clopen connected component under Mathlib's order equivalence between idempotents and clopen subsets of the prime spectrum.

Equations

• x.connectedComponentIdempotent = ↑(PrimeSpectrum.isIdempotentElemEquivClopens.symm { carrier := connectedComponent x, isClopen' := ⋯ })

theorem PrimeSpectrum.isIdempotentElem_connectedComponentIdempotent {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (x : PrimeSpectrum R) : IsIdempotentElem x.connectedComponentIdempotent

The element selecting a connected component is idempotent.

theorem PrimeSpectrum.basicOpen_connectedComponentIdempotent {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (x : PrimeSpectrum R) : ↑(basicOpen x.connectedComponentIdempotent) = connectedComponent x

The basic open of the component idempotent is exactly the connected component.

@[simp]

theorem PrimeSpectrum.connectedComponentIdempotent_notMem_asIdeal {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (x : PrimeSpectrum R) : x.connectedComponentIdempotent ∉ x.asIdeal

The component idempotent does not belong to the prime ideal defining the selected point.

theorem PrimeSpectrum.eq_connectedComponentIdempotent_iff {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] {e : R} (he : IsIdempotentElem e) (x : PrimeSpectrum R) : e = x.connectedComponentIdempotent ↔ ↑(basicOpen e) = connectedComponent x

An idempotent is the component idempotent exactly when its basic open is the selected connected component.

theorem PrimeSpectrum.map_connectedComponentIdempotent {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (e : R ≃+* R) (x : PrimeSpectrum R) : e x.connectedComponentIdempotent = (comap (↑e.symm) x).connectedComponentIdempotent

A ring automorphism transports the component idempotent along its inverse action on the prime spectrum.

theorem PrimeSpectrum.map_connectedComponentIdempotent_eq_self {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (e : R ≃+* R) (x : PrimeSpectrum R) (hx : comap (↑e) x = x) : e x.connectedComponentIdempotent = x.connectedComponentIdempotent

A ring automorphism whose induced map on the prime spectrum fixes x also fixes the component idempotent of x.

@[simp]

theorem PrimeSpectrum.connectedComponentIdempotent_eq_one {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] [ConnectedSpace (PrimeSpectrum R)] (x : PrimeSpectrum R) : x.connectedComponentIdempotent = 1

If the whole prime spectrum is connected, its component idempotent is one.

noncomputable def PrimeSpectrum.connectedComponentIdeal {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (x : PrimeSpectrum R) : Ideal R

The ideal generated by the complementary idempotent 1 - eₓ. Its zero locus is the connected component of x.

Equations

• x.connectedComponentIdeal = Ideal.span {1 - x.connectedComponentIdempotent}

theorem PrimeSpectrum.map_connectedComponentIdeal {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (e : R ≃+* R) (x : PrimeSpectrum R) : Ideal.map e x.connectedComponentIdeal = (comap (↑e.symm) x).connectedComponentIdeal

A ring automorphism transports the ideal cutting out a connected component along its inverse action on the prime spectrum.

theorem PrimeSpectrum.map_connectedComponentIdeal_eq_self {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (e : R ≃+* R) (x : PrimeSpectrum R) (hx : comap (↑e) x = x) : Ideal.map e x.connectedComponentIdeal = x.connectedComponentIdeal

A ring automorphism whose induced map on the prime spectrum fixes x also fixes the ideal cutting out the connected component of x.

theorem PrimeSpectrum.apply_mem_connectedComponentIdeal_iff {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (e : R ≃+* R) (x : PrimeSpectrum R) {r : R} : e r ∈ (comap (↑e.symm) x).connectedComponentIdeal ↔ r ∈ x.connectedComponentIdeal

Applying a ring automorphism transports membership to the component ideal at the inverse image of the point.

theorem PrimeSpectrum.apply_mem_connectedComponentIdeal_iff_of_comap_eq_self {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (e : R ≃+* R) (x : PrimeSpectrum R) (hx : comap (↑e) x = x) {r : R} : e r ∈ x.connectedComponentIdeal ↔ r ∈ x.connectedComponentIdeal

A ring automorphism fixing x preserves membership in the ideal cutting out the connected component of x.

theorem PrimeSpectrum.mem_connectedComponentIdeal_iff {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] {x : PrimeSpectrum R} {r : R} : r ∈ x.connectedComponentIdeal ↔ ∃ (a : R), a * (1 - x.connectedComponentIdempotent) = r

Membership in the component ideal means being a multiple of its complementary idempotent.

@[simp]

theorem PrimeSpectrum.quotientMk_connectedComponentIdempotent_eq_one {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (x : PrimeSpectrum R) : (Ideal.Quotient.mk x.connectedComponentIdeal) x.connectedComponentIdempotent = 1

The component idempotent becomes one in the quotient by the component ideal.

@[simp]

theorem PrimeSpectrum.zeroLocus_connectedComponentIdeal {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (x : PrimeSpectrum R) : zeroLocus ↑x.connectedComponentIdeal = connectedComponent x

The zero locus of the component ideal is exactly the connected component of the point.

theorem PrimeSpectrum.connectedComponentIdeal_le_asIdeal {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (x : PrimeSpectrum R) : x.connectedComponentIdeal ≤ x.asIdeal

The component ideal is contained in the prime ideal defining the selected point.

noncomputable def PrimeSpectrum.primeSpectrumQuotientHomeomorphConnectedComponent {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (x : PrimeSpectrum R) : PrimeSpectrum (R ⧸ x.connectedComponentIdeal) ≃ₜ ↑(connectedComponent x)

The spectrum of R / (1 - eₓ) is homeomorphic to the connected component of x.

The homeomorphism is induced by contraction along the quotient map.

Equations

• x.primeSpectrumQuotientHomeomorphConnectedComponent = (PrimeSpectrum.quotientHomeomorphZeroLocus x.connectedComponentIdeal).trans (Homeomorph.setCongr ⋯)

instance PrimeSpectrum.connectedSpace_quotient_connectedComponentIdeal {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (x : PrimeSpectrum R) : ConnectedSpace (PrimeSpectrum (R ⧸ x.connectedComponentIdeal))

The spectrum of the component quotient is connected.

instance PrimeSpectrum.nontrivial_quotient_connectedComponentIdeal {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (x : PrimeSpectrum R) : Nontrivial (R ⧸ x.connectedComponentIdeal)

The quotient by the component ideal is nontrivial.

@[simp]

theorem PrimeSpectrum.primeSpectrumQuotientHomeomorphConnectedComponent_apply_coe {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (x : PrimeSpectrum R) (y : PrimeSpectrum (R ⧸ x.connectedComponentIdeal)) : ↑(x.primeSpectrumQuotientHomeomorphConnectedComponent y) = comap (Ideal.Quotient.mk x.connectedComponentIdeal) y

After coercion to PrimeSpectrum R, the quotient-spectrum homeomorphism sends a point to its contraction along the quotient map.