The spectrum point 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 point and its underlying prime ideal.

Main declarations

• TauCeti.AlgHom.kernelPoint: the point cut out by the kernel of an augmentation.
• TauCeti.AlgHom.comap_kernelPoint: contraction of a kernel point is the kernel point of the composite algebra homomorphism.

def TauCeti.AlgHom.kernelPoint {k : Type u} [Field k] {H : Type v} [CommRing H] [Algebra k H] (f : H →ₐ[k] k) : ↥(AlgebraicGeometry.Spec ↧H)

The point of Spec H defined by an augmentation f : H →ₐ[k] k. Its prime ideal is ker f.

Equations

• TauCeti.AlgHom.kernelPoint f = PrimeSpectrum.comap (↑f) (IsLocalRing.closedPoint k)

@[simp]

theorem TauCeti.AlgHom.kernelPoint_asIdeal {k : Type u} [Field k] {H : Type v} [CommRing H] [Algebra k H] (f : H →ₐ[k] k) : (kernelPoint f).asIdeal = RingHom.ker ↑f

The prime ideal of an augmentation point is the kernel of the augmentation.

@[simp]

theorem TauCeti.AlgHom.comap_kernelPoint {k : Type u} [Field k] {H : Type v} [CommRing H] [Algebra k H] (f : H →ₐ[k] k) {A : Type w} [CommRing A] [Algebra k A] (g : A →ₐ[k] H) : PrimeSpectrum.comap (↑g) (kernelPoint f) = kernelPoint (f.comp g)

Contracting a kernel point along an algebra homomorphism gives the kernel point of the composite algebra homomorphism.