Cotangent spaces of augmented algebras

For an augmentation f : A →ₐ[R] R, if the augmentation ideal is finitely generated over A, then its cotangent space is finite over R.

Main declarations

• TauCeti.AlgHom.finite_cotangent_ker_of_fg: finite generation of the augmentation ideal gives finiteness of its cotangent space over the base.
• TauCeti.AlgHom.finite_cotangent_ker: the noetherian specialization.

References

• Mathlib's Algebra.Extension.Cotangent.finite provides the generic cotangent-space finiteness result used here.

theorem TauCeti.AlgHom.finite_cotangent_ker_of_fg {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (f : A →ₐ[R] R) (h : (RingHom.ker f.toRingHom).FG) : Module.Finite R (RingHom.ker f.toRingHom).Cotangent

The cotangent space of an augmentation with finitely generated kernel is finite over the base.

theorem TauCeti.AlgHom.finite_cotangent_ker {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (f : A →ₐ[R] R) [IsNoetherianRing A] : Module.Finite R (RingHom.ker f.toRingHom).Cotangent

The cotangent space at an augmented point of a noetherian algebra is finite over the base.

The augmentation hypothesis is encoded by the codomain of f: because f is an R-algebra homomorphism, it is a retraction of algebraMap R A.