The connected component defined by an augmentation

An algebra homomorphism from a commutative algebra to its ground field determines a rational point of the algebra's prime spectrum. This file records that the component idempotent maps to one and the factorization of the augmentation through the quotient cutting out that point's connected component when the prime spectrum is locally connected.

Main declarations

• TauCeti.AlgHom.map_connectedComponentIdempotent_kernelPoint_eq_one: the augmentation maps the component idempotent of its kernel point to one.
• TauCeti.AlgHom.kernelPointConnectedComponentAlgHom: the augmentation factored through the quotient cutting out the connected component of its kernel point.
• TauCeti.AlgHom.kernelPoint_comp_connectedComponentQuotient_mem: a point of the component quotient maps into the selected connected component.

References

• J. S. Milne, Algebraic Groups (2017), Section 2.a.
• The Stacks Project, Tags 00EE and 022R.

The connected-component factorization supplies a prerequisite for Layer 3, "Identity component G° and component group π₀(G)", of the ReductiveGroups roadmap. It concerns only the ordinary connected component over the ground field and asserts no compatibility with base change.

@[simp]

theorem TauCeti.AlgHom.map_connectedComponentIdempotent_kernelPoint_eq_one {k : Type u} [Field k] {H : Type v} [CommRing H] [Algebra k H] (f : H →ₐ[k] k) [LocallyConnectedSpace (PrimeSpectrum H)] : f (PrimeSpectrum.connectedComponentIdempotent (kernelPoint f)) = 1

An augmentation takes the idempotent selecting the connected component of its kernel point to one.

theorem TauCeti.AlgHom.connectedComponentIdeal_kernelPoint_le_ker {k : Type u} [Field k] {H : Type v} [CommRing H] [Algebra k H] (f : H →ₐ[k] k) [LocallyConnectedSpace (PrimeSpectrum H)] : PrimeSpectrum.connectedComponentIdeal (kernelPoint f) ≤ RingHom.ker ↑f

The ideal cutting out the connected component of an augmentation's kernel point is contained in the kernel of the augmentation.

noncomputable def TauCeti.AlgHom.kernelPointConnectedComponentAlgHom {k : Type u} [Field k] {H : Type v} [CommRing H] [Algebra k H] (f : H →ₐ[k] k) [LocallyConnectedSpace (PrimeSpectrum H)] : H ⧸ PrimeSpectrum.connectedComponentIdeal (kernelPoint f) →ₐ[k] k

The augmentation factored through the quotient cutting out the connected component of its kernel point.

Equations

• TauCeti.AlgHom.kernelPointConnectedComponentAlgHom f = Ideal.Quotient.liftₐ (PrimeSpectrum.connectedComponentIdeal (TauCeti.AlgHom.kernelPoint f)) f ⋯

@[simp]

theorem TauCeti.AlgHom.kernelPointConnectedComponentAlgHom_comp_mk {k : Type u} [Field k] {H : Type v} [CommRing H] [Algebra k H] (f : H →ₐ[k] k) [LocallyConnectedSpace (PrimeSpectrum H)] : (kernelPointConnectedComponentAlgHom f).comp (Ideal.Quotient.mkₐ k (PrimeSpectrum.connectedComponentIdeal (kernelPoint f))) = f

The factored augmentation composed with the quotient map is the original augmentation.

@[simp]

theorem TauCeti.AlgHom.kernelPointConnectedComponentAlgHom_mk {k : Type u} [Field k] {H : Type v} [CommRing H] [Algebra k H] (f : H →ₐ[k] k) [LocallyConnectedSpace (PrimeSpectrum H)] (h : H) : (kernelPointConnectedComponentAlgHom f) ((Ideal.Quotient.mk (PrimeSpectrum.connectedComponentIdeal (kernelPoint f))) h) = f h

The factored augmentation evaluates a quotient constructor as the original augmentation.

theorem TauCeti.AlgHom.kernelPoint_comp_connectedComponentQuotient_mem {k : Type u} [Field k] {H : Type v} [CommRing H] [Algebra k H] [LocallyConnectedSpace (PrimeSpectrum H)] (z : PrimeSpectrum H) (g : H ⧸ z.connectedComponentIdeal →ₐ[k] k) : kernelPoint (g.comp (Ideal.Quotient.mkₐ k z.connectedComponentIdeal)) ∈ connectedComponent z

A rational point of the quotient cutting out a connected component maps into that component under the quotient map.