@[reducible, inline]
The Zariski cotangent space at a point, defined as the cotangent space of the local ring R
(i.e. 𝔪/𝔪² viewed as a vector space over the residue field).
Instances For
@[reducible, inline]
abbrev
ZariskiCotangentSpace.tangentSpace
(k : Type u_1)
[Field k]
(R : Type u_2)
[CommRing R]
[IsLocalRing R]
[Algebra k R]
:
Type u_2
The Zariski tangent space at a point, defined as the space of k-derivations from the
local ring R to its residue field (Definition 35, Lecture 18).
Instances For
theorem
ZariskiCotangentSpace.tangentSpace_dual_cotangentSpace
(k : Type u_1)
[Field k]
(R : Type u_2)
[CommRing R]
[IsLocalRing R]
[Algebra k R]
:
Nonempty (tangentSpace k R ≃ₗ[k] Module.Dual k (cotangentSpace R))
The tangent space is the k-linear dual of the cotangent space: there exists a
linear equivalence between tangentSpace k R and Module.Dual k (cotangentSpace R).