@[reducible, inline]

abbrev ZariskiCotangentSpace (R : Type u) [CommRing R] [IsLocalRing R] : Type u

Zariski cotangent space (Def 35, Lec 18): for a local ring R with maximal ideal m, it is m/m² as a vector space over the residue field.

@[implicit_reducible]

instance ZariskiCotangentSpace.instModule (R : Type u) [CommRing R] [IsLocalRing R] : Module (IsLocalRing.ResidueField R) (ZariskiCotangentSpace R)

The Zariski cotangent space is naturally a module over the residue field.

@[reducible, inline]

abbrev ZariskiTangentSpace (R : Type u) [CommRing R] [IsLocalRing R] : Type u

The Zariski tangent space, defined as the residue-field dual of the Zariski cotangent space; equivalently, derivations R → k.

@[implicit_reducible]

noncomputable instance ZariskiTangentSpace.instModule (R : Type u) [CommRing R] [IsLocalRing R] : Module (IsLocalRing.ResidueField R) (ZariskiTangentSpace R)

Residue-field module structure on the Zariski tangent space.

theorem ZariskiCotangentSpace.eq_maximalIdeal_cotangent (R : Type u) [CommRing R] [IsLocalRing R] : ZariskiCotangentSpace R = (IsLocalRing.maximalIdeal R).Cotangent

Unfolding: the Zariski cotangent space is exactly the cotangent module m/m² of the maximal ideal.

theorem ZariskiTangentSpace.eq_dual (R : Type u) [CommRing R] [IsLocalRing R] : ZariskiTangentSpace R = Module.Dual (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R)

Unfolding: the Zariski tangent space is the residue-field dual of the cotangent space m/m².