Decomposing a ring by its connected components

Let R be a commutative ring for which the connected-components quotient of its prime spectrum is discrete. Each connected component is selected by a canonical idempotent. This discreteness holds in particular when the prime spectrum is locally connected or has finitely many connected components. In the finite case, these idempotents form a complete orthogonal family and decompose R as the product of the corresponding quotient rings.

Unlike PrimeSpectrum.connectedComponentIdempotent, which is indexed by a point of the spectrum, PrimeSpectrum.connectedComponentsIdempotent is indexed by the component itself. Its characteristic formula says that its basic open is exactly the fibre of the quotient map to connected components. The complete-orthogonal theorem is therefore independent of any choice of representative point.

The product decomposition assumes only Finite (ConnectedComponents (PrimeSpectrum R)) and constructs a Fintype internally for the finite sum.

Main declarations

• PrimeSpectrum.connectedComponentsIdempotent: the idempotent selecting a connected component.
• PrimeSpectrum.basicOpen_connectedComponentsIdempotent: its basic open is the corresponding fibre of the quotient map.
• PrimeSpectrum.completeOrthogonalIdempotents_connectedComponentsIdempotent: the component idempotents are complete and pairwise orthogonal.
• PrimeSpectrum.ringEquivPiQuotientConnectedComponentsIdeal: the canonical product decomposition into the component quotient rings.

References

• The Stacks Project, Tag 00EE, Idempotents and clopen subsets.
• J. S. Milne, Algebraic Groups (2017), Section 2.a.

This supplies the idempotent decomposition needed for the identity component and component group in Layer 3 of the ReductiveGroups roadmap; it does not itself assert compatibility with base change.

noncomputable def PrimeSpectrum.connectedComponentsIdempotent {R : Type u} [CommRing R] [DiscreteTopology (ConnectedComponents (PrimeSpectrum R))] : ConnectedComponents (PrimeSpectrum R) → R

The canonical idempotent indexed by a connected component of Spec R.

It corresponds under the idempotent--clopen equivalence to the fibre of the quotient map over the given component.

Equations

• PrimeSpectrum.connectedComponentsIdempotent C = ↑(PrimeSpectrum.isIdempotentElemEquivClopens.symm { carrier := ConnectedComponents.mk ⁻¹' {C}, isClopen' := ⋯ })

theorem PrimeSpectrum.isIdempotentElem_connectedComponentsIdempotent {R : Type u} [CommRing R] [DiscreteTopology (ConnectedComponents (PrimeSpectrum R))] (C : ConnectedComponents (PrimeSpectrum R)) : IsIdempotentElem (connectedComponentsIdempotent C)

Every component-indexed idempotent is idempotent.

theorem PrimeSpectrum.basicOpen_connectedComponentsIdempotent {R : Type u} [CommRing R] [DiscreteTopology (ConnectedComponents (PrimeSpectrum R))] (C : ConnectedComponents (PrimeSpectrum R)) : ↑(basicOpen (connectedComponentsIdempotent C)) = ConnectedComponents.mk ⁻¹' {C}

The basic open of a component-indexed idempotent is the fibre of the quotient map over that component.

@[simp]

theorem PrimeSpectrum.connectedComponentsIdempotent_mk {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (x : PrimeSpectrum R) : connectedComponentsIdempotent (ConnectedComponents.mk x) = x.connectedComponentIdempotent

On a component represented by x, the component-indexed idempotent is the point-indexed component idempotent of x.

theorem PrimeSpectrum.mem_basicOpen_connectedComponentsIdempotent {R : Type u} [CommRing R] [DiscreteTopology (ConnectedComponents (PrimeSpectrum R))] (C : ConnectedComponents (PrimeSpectrum R)) (x : PrimeSpectrum R) : x ∈ basicOpen (connectedComponentsIdempotent C) ↔ ConnectedComponents.mk x = C

A point belongs to the basic open selected by a component exactly when it lies in that component.

theorem PrimeSpectrum.connectedComponentsIdempotent_mul_eq_zero {R : Type u} [CommRing R] [DiscreteTopology (ConnectedComponents (PrimeSpectrum R))] {C D : ConnectedComponents (PrimeSpectrum R)} (hCD : C ≠ D) : connectedComponentsIdempotent C * connectedComponentsIdempotent D = 0

Distinct connected components have orthogonal component-indexed idempotents.

theorem PrimeSpectrum.orthogonalIdempotents_connectedComponentsIdempotent {R : Type u} [CommRing R] [DiscreteTopology (ConnectedComponents (PrimeSpectrum R))] : OrthogonalIdempotents connectedComponentsIdempotent

The component-indexed idempotents are pairwise orthogonal.

noncomputable def PrimeSpectrum.connectedComponentsIdeal {R : Type u} [CommRing R] [DiscreteTopology (ConnectedComponents (PrimeSpectrum R))] (C : ConnectedComponents (PrimeSpectrum R)) : Ideal R

The ideal generated by the complement of the idempotent indexed by C.

Equations

• PrimeSpectrum.connectedComponentsIdeal C = Ideal.span {1 - PrimeSpectrum.connectedComponentsIdempotent C}

@[simp]

theorem PrimeSpectrum.connectedComponentsIdeal_mk {R : Type u} [CommRing R] [LocallyConnectedSpace (PrimeSpectrum R)] (x : PrimeSpectrum R) : connectedComponentsIdeal (ConnectedComponents.mk x) = x.connectedComponentIdeal

At a component represented by x, the component-indexed ideal is the point-indexed connected component ideal of x.

@[simp]

theorem PrimeSpectrum.quotientMk_connectedComponentsIdempotent_eq_one {R : Type u} [CommRing R] [DiscreteTopology (ConnectedComponents (PrimeSpectrum R))] (C : ConnectedComponents (PrimeSpectrum R)) : (Ideal.Quotient.mk (connectedComponentsIdeal C)) (connectedComponentsIdempotent C) = 1

A component-indexed idempotent becomes one in its component quotient.

@[simp]

theorem PrimeSpectrum.zeroLocus_connectedComponentsIdeal {R : Type u} [CommRing R] [DiscreteTopology (ConnectedComponents (PrimeSpectrum R))] (C : ConnectedComponents (PrimeSpectrum R)) : zeroLocus ↑(connectedComponentsIdeal C) = ConnectedComponents.mk ⁻¹' {C}

The zero locus of a component-indexed ideal is the corresponding fibre of the quotient map to connected components.

noncomputable def PrimeSpectrum.primeSpectrumQuotientHomeomorphConnectedComponentsFiber {R : Type u} [CommRing R] [DiscreteTopology (ConnectedComponents (PrimeSpectrum R))] (C : ConnectedComponents (PrimeSpectrum R)) : PrimeSpectrum (R ⧸ connectedComponentsIdeal C) ≃ₜ ↑(ConnectedComponents.mk ⁻¹' {C})

The spectrum of a component quotient is homeomorphic to the corresponding fibre of the quotient map to connected components.

Equations

• PrimeSpectrum.primeSpectrumQuotientHomeomorphConnectedComponentsFiber C = (PrimeSpectrum.quotientHomeomorphZeroLocus (PrimeSpectrum.connectedComponentsIdeal C)).trans (Homeomorph.setCongr ⋯)

instance PrimeSpectrum.connectedSpace_quotient_connectedComponentsIdeal {R : Type u} [CommRing R] [DiscreteTopology (ConnectedComponents (PrimeSpectrum R))] (C : ConnectedComponents (PrimeSpectrum R)) : ConnectedSpace (PrimeSpectrum (R ⧸ connectedComponentsIdeal C))

The spectrum of a component-indexed quotient is connected.

instance PrimeSpectrum.nontrivial_quotient_connectedComponentsIdeal {R : Type u} [CommRing R] [DiscreteTopology (ConnectedComponents (PrimeSpectrum R))] (C : ConnectedComponents (PrimeSpectrum R)) : Nontrivial (R ⧸ connectedComponentsIdeal C)

A component-indexed quotient is nontrivial.

@[simp]

theorem PrimeSpectrum.primeSpectrumQuotientHomeomorphConnectedComponentsFiber_apply_coe {R : Type u} [CommRing R] [DiscreteTopology (ConnectedComponents (PrimeSpectrum R))] (C : ConnectedComponents (PrimeSpectrum R)) (y : PrimeSpectrum (R ⧸ connectedComponentsIdeal C)) : ↑((primeSpectrumQuotientHomeomorphConnectedComponentsFiber C) y) = comap (Ideal.Quotient.mk (connectedComponentsIdeal C)) y

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

theorem PrimeSpectrum.completeOrthogonalIdempotents_connectedComponentsIdempotent {R : Type u} [CommRing R] [Fintype (ConnectedComponents (PrimeSpectrum R))] : CompleteOrthogonalIdempotents connectedComponentsIdempotent

The idempotents indexed by the connected components of Spec R form a complete orthogonal family.

noncomputable def PrimeSpectrum.ringEquivPiQuotientConnectedComponentsIdeal {R : Type u} [CommRing R] [Finite (ConnectedComponents (PrimeSpectrum R))] : R ≃+* ((C : ConnectedComponents (PrimeSpectrum R)) → R ⧸ connectedComponentsIdeal C)

A ring with finitely many connected components in its prime spectrum is canonically isomorphic to the product of its component-indexed quotient rings.

Equations

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

@[simp]

theorem PrimeSpectrum.ringEquivPiQuotientConnectedComponentsIdeal_apply {R : Type u} [CommRing R] [Finite (ConnectedComponents (PrimeSpectrum R))] (r : R) (C : ConnectedComponents (PrimeSpectrum R)) : ringEquivPiQuotientConnectedComponentsIdeal r C = (Ideal.Quotient.mk (connectedComponentsIdeal C)) r

The product decomposition sends an element to its class in each component-indexed quotient.