The Zariski cotangent space at an augmentation point

For an augmented commutative algebra f : H →ₐ[k] k, the augmentation determines a k-rational point of Spec H. Its prime ideal is ker f. The stalk of Spec H at this point is the localization of H at ker f, so localization of cotangent spaces gives a canonical equivalence

ker(f) / ker(f)² ≃ₗ[k] 𝔪_f / 𝔪_f².

This file supplies the affine-scheme comparison used to identify the augmentation cotangent space of a commutative bialgebra with the Zariski cotangent space at its augmentation point.

Main declarations

• AlgHom.kernelResidueFieldAlgEquiv: the canonical identification of its residue field with k.
• AlgHom.kernelCotangentLinearEquivZariski: the kernel cotangent space is the Zariski cotangent space at the augmentation point.

References

• J. S. Milne, Algebraic Groups (2017), §10.a.

@[instance_reducible]

noncomputable instance AlgHom.kernelStalkAlgebra {k : Type u} [Field k] {H : Type v} [CommRing H] [Algebra k H] (f : H →ₐ[k] k) : Algebra H ↑((AlgebraicGeometry.Spec ↧H).presheaf.stalk (TauCeti.AlgHom.kernelPoint f))

The stalk at an augmentation point is an H-algebra through the germ map.

Equations

• f.kernelStalkAlgebra = AlgebraicGeometry.StructureSheaf.stalkAlgebra H (TauCeti.AlgHom.kernelPoint f)

@[instance_reducible]

noncomputable instance AlgHom.kernelStalkBaseAlgebra {k : Type u} [Field k] {H : Type v} [CommRing H] [Algebra k H] (f : H →ₐ[k] k) : Algebra k ↑((AlgebraicGeometry.Spec ↧H).presheaf.stalk (TauCeti.AlgHom.kernelPoint f))

The stalk at an augmentation point is a k-algebra through k → H.

Equations

• f.kernelStalkBaseAlgebra = Algebra.restrictScalars k H ↑((AlgebraicGeometry.Spec ↧H).presheaf.stalk (TauCeti.AlgHom.kernelPoint f))

instance AlgHom.kernelStalkIsScalarTower {k : Type u} [Field k] {H : Type v} [CommRing H] [Algebra k H] (f : H →ₐ[k] k) : IsScalarTower k H ↑((AlgebraicGeometry.Spec ↧H).presheaf.stalk (TauCeti.AlgHom.kernelPoint f))

Scalar extension from k through H to the stalk at an augmentation point is compatible.

instance AlgHom.kernelStalkIsLocalization {k : Type u} [Field k] {H : Type v} [CommRing H] [Algebra k H] (f : H →ₐ[k] k) : IsLocalization.AtPrime (↑((AlgebraicGeometry.Spec ↧H).presheaf.stalk (TauCeti.AlgHom.kernelPoint f))) (RingHom.ker ↑f)

The stalk at an augmentation point is the localization of H at the augmentation kernel.

noncomputable def AlgHom.kernelResidueFieldAlgEquiv {k : Type u} [Field k] {H : Type v} [CommRing H] [Algebra k H] (f : H →ₐ[k] k) : k ≃ₐ[k] IsLocalRing.ResidueField ↑((AlgebraicGeometry.Spec ↧H).presheaf.stalk (TauCeti.AlgHom.kernelPoint f))

The ground field is canonically the residue field at an augmentation point, as a k-algebra.

Equations

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

noncomputable def AlgHom.kernelCotangentLinearEquivZariski {k : Type u} [Field k] {H : Type v} [CommRing H] [Algebra k H] (f : H →ₐ[k] k) : (RingHom.ker ↑f).Cotangent ≃ₗ[k] TauCeti.AlgebraicGeometry.ZariskiCotangentSpace (AlgebraicGeometry.Spec ↧H) (TauCeti.AlgHom.kernelPoint f)

The cotangent space of an augmentation kernel is canonically the Zariski cotangent space of the affine spectrum at the corresponding point.

This is the cotangent form of the comparison between augmentation-valued derivations and the scheme-theoretic tangent space at the augmentation point.

Equations

• f.kernelCotangentLinearEquivZariski = LinearEquiv.restrictScalars k (RingHom.ker ↑f).cotangentLocalizationEquiv

@[simp]

theorem AlgHom.kernelCotangentLinearEquivZariski_toCotangent {k : Type u} [Field k] {H : Type v} [CommRing H] [Algebra k H] (f : H →ₐ[k] k) (a : ↥(RingHom.ker ↑f)) : f.kernelCotangentLinearEquivZariski ((RingHom.ker ↑f).toCotangent a) = (IsLocalRing.maximalIdeal ↑((AlgebraicGeometry.Spec ↧H).presheaf.stalk (TauCeti.AlgHom.kernelPoint f))).toCotangent ⟨(algebraMap H ↑((AlgebraicGeometry.Spec ↧H).presheaf.stalk (TauCeti.AlgHom.kernelPoint f))) ↑a, ⋯⟩

On an element of the augmentation kernel, the cotangent comparison is induced by the map from the coordinate ring to its stalk.

instance AlgHom.kernelCotangentIsScalarTower {k : Type u} [Field k] {H : Type v} [CommRing H] [Algebra k H] (f : H →ₐ[k] k) : IsScalarTower k (IsLocalRing.ResidueField ↑((AlgebraicGeometry.Spec ↧H).presheaf.stalk (TauCeti.AlgHom.kernelPoint f))) (TauCeti.AlgebraicGeometry.ZariskiCotangentSpace (AlgebraicGeometry.Spec ↧H) (TauCeti.AlgHom.kernelPoint f))

The ground-field action on the Zariski cotangent space factors through the residue field.

theorem AlgHom.finrank_kernelCotangent_eq_finrank_zariskiCotangentSpace {k : Type u} [Field k] {H : Type v} [CommRing H] [Algebra k H] (f : H →ₐ[k] k) : Module.finrank k (RingHom.ker ↑f).Cotangent = Module.finrank k (TauCeti.AlgebraicGeometry.ZariskiCotangentSpace (AlgebraicGeometry.Spec ↧H) (TauCeti.AlgHom.kernelPoint f))

The cotangent space of an augmentation kernel and the Zariski cotangent space at its point have the same dimension over the ground field.