The tangent space of an abelian variety at the identity

The identity of an abelian variety A/K is a section Spec K ⟶ A of its structure morphism, so the residue field κ(0) at the identity point is canonically the ground field; that identification is AbelianVariety.zeroResidueFieldRingEquiv, built in TauCeti.AlgebraicGeometry.AbelianVariety.Basic. It must be made explicit, because κ(0) and K are not definitionally equal.

This file uses it to regard the Zariski tangent space at the identity as a vector space over the ground field, and computes its dimension: it is the dimension of the abelian variety. Indeed A is smooth over K, so its local ring at the identity is regular and its cotangent space 𝔪₀ / 𝔪₀² has dimension the Krull dimension of that local ring; and since the identity is a closed point of the integral scheme A, locally of finite type over K, that local ring has the dimension of A.

Main declarations

• AbelianVariety.TangentSpace A is T₀A, the Zariski tangent space at the identity together with its K-vector-space structure;
• AbelianVariety.finrank_tangentSpace_eq_finrank_cotangentSpace computes its dimension as the dimension of 𝔪₀ / 𝔪₀² over κ(0);
• AbelianVariety.finrank_tangentSpace_eq_dim: dim_K T₀A = dim A.

For an affine group scheme the same tangent space is described in Hopf-algebra terms elsewhere in the library: TauCeti.Bialgebra.CotangentSpace in TauCeti.Algebra.AlgebraicGroup.Tangent.Cotangent is the augmentation ideal modulo its square, and TauCeti.Algebra.AlgebraicGroup.Tangent.Basic describes the tangent space at the identity by counit-valued derivations. The construction here is the scheme-level Zariski tangent space at a point, which applies to an abelian variety, and no comparison between the two is made.

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.finrank_residueField_stalk_zeroPoint {K : Type u} [Field K] (A : AbelianVariety K) : Module.finrank K (IsLocalRing.ResidueField ↑(A.toScheme.presheaf.stalk A.zeroPoint)) = 1

The residue field at the identity has dimension one over the ground field, since the structure map of the K-algebra κ(0) is the bijection zeroResidueFieldRingEquiv.symm.

instance TauCeti.AlgebraicGeometry.AbelianVariety.finiteDimensional_residueField_stalk_zeroPoint {K : Type u} [Field K] (A : AbelianVariety K) : FiniteDimensional K (IsLocalRing.ResidueField ↑(A.toScheme.presheaf.stalk A.zeroPoint))

The residue field at the identity is a finite-dimensional K-vector space.

def TauCeti.AlgebraicGeometry.AbelianVariety.TangentSpace {K : Type u} [Field K] (A : AbelianVariety K) : Type u

The tangent space T₀A of an abelian variety at its identity: the Zariski tangent space of the underlying scheme at zeroPoint, carrying the K-vector-space structure transported along zeroResidueFieldRingEquiv.

This is a type synonym rather than an abbreviation, so that the residue-field action, the ground-field action and their scalar tower are declared together on one type — the arrangement Mathlib recommends, and the reason Module.compHom is registered here rather than on the underlying Module.Dual. The equivalence tangentSpaceLinearEquiv is the public interface to the underlying Zariski tangent space.

Equations

• A.TangentSpace = TauCeti.AlgebraicGeometry.ZariskiTangentSpace A.toScheme A.zeroPoint

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.AbelianVariety.tangentSpaceAddCommGroup {K : Type u} [Field K] (A : AbelianVariety K) : AddCommGroup A.TangentSpace

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.AbelianVariety.tangentSpaceModuleResidueField {K : Type u} [Field K] (A : AbelianVariety K) : Module (IsLocalRing.ResidueField ↑(A.toScheme.presheaf.stalk A.zeroPoint)) A.TangentSpace

Equations

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

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.tangentSpaceLinearEquiv {K : Type u} [Field K] (A : AbelianVariety K) : A.TangentSpace ≃ₗ[IsLocalRing.ResidueField ↑(A.toScheme.presheaf.stalk A.zeroPoint)] ZariskiTangentSpace A.toScheme A.zeroPoint

The canonical residue-field-linear identification of T₀A with the underlying Zariski tangent space.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.tangentSpaceLinearEquiv_apply {K : Type u} [Field K] (A : AbelianVariety K) (v : A.TangentSpace) : A.tangentSpaceLinearEquiv v ≍ v

The canonical equivalence sends a tangent vector to its underlying Zariski tangent vector.

noncomputable def TauCeti.AlgebraicGeometry.AbelianVariety.tangentSpaceEval {K : Type u} [Field K] (A : AbelianVariety K) (v : A.TangentSpace) (m : ZariskiCotangentSpace A.toScheme A.zeroPoint) : IsLocalRing.ResidueField ↑(A.toScheme.presheaf.stalk A.zeroPoint)

Evaluate a tangent vector in T₀A on a Zariski cotangent vector through the canonical identification tangentSpaceLinearEquiv.

Equations

• A.tangentSpaceEval v m = (A.tangentSpaceLinearEquiv v) m

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.tangentSpaceEval_apply {K : Type u} [Field K] (A : AbelianVariety K) (v : A.TangentSpace) (m : ZariskiCotangentSpace A.toScheme A.zeroPoint) : A.tangentSpaceEval v m = (A.tangentSpaceLinearEquiv v) m

Evaluation in T₀A is application of the underlying Zariski tangent vector.

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.AbelianVariety.tangentSpaceModule {K : Type u} [Field K] (A : AbelianVariety K) : Module K A.TangentSpace

Restrict scalars on T₀A from κ(0) to K along the canonical residue-field equivalence.

Equations

• A.tangentSpaceModule = Module.compHom A.TangentSpace A.zeroResidueFieldRingEquiv.symm.toRingHom

instance TauCeti.AlgebraicGeometry.AbelianVariety.isScalarTower_tangentSpace {K : Type u} [Field K] (A : AbelianVariety K) : IsScalarTower K (IsLocalRing.ResidueField ↑(A.toScheme.presheaf.stalk A.zeroPoint)) A.TangentSpace

The ground-field action, the residue-field action, and the tangent-space action form the expected scalar tower.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.tangentSpace_smul_def {K : Type u} [Field K] (A : AbelianVariety K) (k : K) (v : A.TangentSpace) : k • v = A.zeroResidueFieldRingEquiv.symm k • v

Ground-field scalar multiplication on T₀A is restriction of the residue-field action.

Not a simp lemma: with algebraMap_zeroResidueField the right-hand side is the ground-field scalar algebraMap K κ(0) k • v, which Mathlib's algebraMap_smul rewrites back to the left-hand side.

instance TauCeti.AlgebraicGeometry.AbelianVariety.finiteDimensional_tangentSpace_residueField {K : Type u} [Field K] (A : AbelianVariety K) : FiniteDimensional (IsLocalRing.ResidueField ↑(A.toScheme.presheaf.stalk A.zeroPoint)) A.TangentSpace

The tangent space is finite-dimensional over the residue field, since the underlying Zariski tangent space is.

instance TauCeti.AlgebraicGeometry.AbelianVariety.finiteDimensional_tangentSpace {K : Type u} [Field K] (A : AbelianVariety K) : FiniteDimensional K A.TangentSpace

The tangent space of an abelian variety is finite-dimensional over the ground field.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.finrank_residueField_tangentSpace {K : Type u} [Field K] (A : AbelianVariety K) : Module.finrank (IsLocalRing.ResidueField ↑(A.toScheme.presheaf.stalk A.zeroPoint)) A.TangentSpace = Module.finrank (IsLocalRing.ResidueField ↑(A.toScheme.presheaf.stalk A.zeroPoint)) (ZariskiTangentSpace A.toScheme A.zeroPoint)

The residue-field dimension of T₀A is that of the underlying Zariski tangent space: the type synonym carries exactly the residue-field structure of the latter.

theorem TauCeti.AlgebraicGeometry.AbelianVariety.finrank_tangentSpace_eq_finrank_residueField_tangentSpace {K : Type u} [Field K] (A : AbelianVariety K) : Module.finrank K A.TangentSpace = Module.finrank (IsLocalRing.ResidueField ↑(A.toScheme.presheaf.stalk A.zeroPoint)) A.TangentSpace

Computing the dimension of T₀A over K is the same as computing it over the canonically identified residue field κ(0).

theorem TauCeti.AlgebraicGeometry.AbelianVariety.finrank_tangentSpace_eq_finrank_cotangentSpace {K : Type u} [Field K] (A : AbelianVariety K) : Module.finrank K A.TangentSpace = Module.finrank (IsLocalRing.ResidueField ↑(A.toScheme.presheaf.stalk A.zeroPoint)) (ZariskiCotangentSpace A.toScheme A.zeroPoint)

The dimension of the tangent space of an abelian variety over K is the dimension of the cotangent space 𝔪₀ / 𝔪₀² over κ(0).

@[simp]

theorem TauCeti.AlgebraicGeometry.AbelianVariety.finrank_tangentSpace_eq_dim {K : Type u} [Field K] (A : AbelianVariety K) : ↑(Module.finrank K A.TangentSpace) = A.dim

The tangent space of an abelian variety at the identity has dimension the dimension of the abelian variety.