Extⁿ over the dual numbers is free of rank one in every degree

Let k be a commutative ring, let A = k[ε] be the dual numbers k[ε]/(ε²), and let S = A/(ε) be the residue module of A -- its residue field when k is a field -- viewed as an A-module through the constant-term projection. The multiplications

⋯ ⟶ A --ε--> A --ε--> A ⟶ S ⟶ 0

form a projective resolution of S, and every differential of Hom_A(-, S) applied to it is zero, because ε annihilates S. Hence Extⁿ_A(S, S) ≅ k as a k-module, for every n. The free and residue modules, quotient map, and finite-generation instance work over arbitrary rings.

Main definitions

• TauCeti.dualNumberFree and TauCeti.dualNumberResidue: the rank-one free module A and the residue module S = A/(ε), as objects of ModuleCat A.
• TauCeti.dualNumberProjectiveResolution: the ε-periodic projective resolution of S, whose terms are identified with A by TauCeti.dualNumberProjectiveResolutionXIso.
• TauCeti.extDualNumberResidueSuccEquiv: the k-linear equivalence Hom_A(A, S) ≃ₗ[k] Extⁿ⁺¹(S, S) read off that resolution.
• TauCeti.extDualNumberResidueEquiv: the k-linear equivalence Extⁿ(S, S) ≃ₗ[k] k, for every n.
• TauCeti.finrank_ext_dualNumberResidue: over a field, every Extⁿ(S, S) is one-dimensional.

References

• Charles A. Weibel, An Introduction to Homological Algebra, Cambridge Studies in Advanced Mathematics 38, Cambridge University Press (1994), Section 2.5 and Chapter 4.

The two modules

@[reducible, inline]

noncomputable abbrev TauCeti.dualNumberFree (k : Type u) [Ring k] : ModuleCat (DualNumber k)

The rank-one free module over the dual numbers k[ε].

Equations

• TauCeti.dualNumberFree k = ↧(DualNumber k)

@[reducible, inline]

noncomputable abbrev TauCeti.dualNumberResidue (k : Type u) [Ring k] : ModuleCat (DualNumber k)

The quotient k[ε]/(ε) of the dual numbers, as a k[ε]-module: the underlying k-module is k, and ε acts by zero. When k is a field this is the residue field of k[ε].

Equations

• TauCeti.dualNumberResidue k = (ModuleCat.restrictScalars { toFun := TrivSqZeroExt.fst, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }).obj ↧k

noncomputable def TauCeti.dualNumberResidueEquiv (k : Type u) [Ring k] : ↑(dualNumberResidue k) ≃ₗ[k] k

The quotient k[ε]/(ε) is k as a k-module.

Equations

• TauCeti.dualNumberResidueEquiv k = { toFun := fun (x : ↑(TauCeti.dualNumberResidue k)) => x, map_add' := ⋯, map_smul' := ⋯, invFun := fun (x : k) => x, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.dualNumberResidueEquiv_apply (k : Type u) [Ring k] (x : ↑(dualNumberResidue k)) : (dualNumberResidueEquiv k) x = x

The identification of k[ε]/(ε) with k is the identity on the underlying elements.

@[simp]

theorem TauCeti.dualNumberResidueEquiv_symm_apply (k : Type u) [Ring k] (x : k) : (dualNumberResidueEquiv k).symm x = x

The inverse identification of k with k[ε]/(ε) is also the identity on elements.

theorem TauCeti.dualNumberResidueEquiv_smul (k : Type u) [Ring k] (a : DualNumber k) (x : ↑(dualNumberResidue k)) : (dualNumberResidueEquiv k) (a • x) = TrivSqZeroExt.fst a * (dualNumberResidueEquiv k) x

The k[ε]-action on k[ε]/(ε) is multiplication by the constant term.

theorem TauCeti.eps_smul_dualNumberResidue (k : Type u) [Ring k] (x : ↑(dualNumberResidue k)) : DualNumber.eps • x = 0

ε annihilates k[ε]/(ε).

noncomputable def TauCeti.dualNumberProj (k : Type u) [Ring k] : dualNumberFree k ⟶ dualNumberResidue k

The quotient map k[ε] ↠ k[ε]/(ε).

Equations

• TauCeti.dualNumberProj k = ModuleCat.ofHom { toFun := TrivSqZeroExt.fst, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.dualNumberProj_apply (k : Type u) [Ring k] (x : DualNumber k) : (ModuleCat.Hom.hom (dualNumberProj k)) x = TrivSqZeroExt.fst x

The quotient map is the constant-term map.

theorem TauCeti.dualNumberProj_surjective (k : Type u) [Ring k] : Function.Surjective ⇑(ModuleCat.Hom.hom (dualNumberProj k))

The quotient map k[ε] ↠ k[ε]/(ε) is surjective.

instance TauCeti.instFiniteDualNumberCarrierDualNumberResidue (k : Type u) [Ring k] : Module.Finite (DualNumber k) ↑(dualNumberResidue k)

The residue module k[ε]/(ε) is a finitely generated k[ε]-module.

instance TauCeti.epi_dualNumberProj (k : Type u) [Ring k] : CategoryTheory.Epi (dualNumberProj k)

The quotient map k[ε] ↠ k[ε]/(ε) is an epimorphism; this is what makes precomposition with it injective on End(k[ε]/(ε)).

The periodic resolution

noncomputable def TauCeti.dualNumberEpsSmul (k : Type u) [CommRing k] : dualNumberFree k ⟶ dualNumberFree k

Multiplication by ε on the rank-one free module.

Equations

• TauCeti.dualNumberEpsSmul k = ModuleCat.ofHom (LinearMap.mulLeft (DualNumber k) DualNumber.eps)

@[simp]

theorem TauCeti.dualNumberEpsSmul_hom (k : Type u) [CommRing k] : ModuleCat.Hom.hom (dualNumberEpsSmul k) = LinearMap.mulLeft (DualNumber k) DualNumber.eps

Multiplication by ε is left multiplication by ε as a linear map.

@[simp]

theorem TauCeti.dualNumberEpsSmul_comp_dualNumberEpsSmul_eq_zero (k : Type u) [CommRing k] : CategoryTheory.CategoryStruct.comp (dualNumberEpsSmul k) (dualNumberEpsSmul k) = 0

ε² = 0, so multiplication by ε squares to zero.

@[simp]

theorem TauCeti.dualNumberEpsSmul_comp_eq_zero (k : Type u) [CommRing k] (f : dualNumberFree k ⟶ dualNumberResidue k) : CategoryTheory.CategoryStruct.comp (dualNumberEpsSmul k) f = 0

Every map from the free module to k[ε]/(ε) kills multiplication by ε: this is the statement that Hom_A(-, S) turns the periodic resolution into a complex with zero differentials.

@[simp]

theorem TauCeti.ker_dualNumberProj (F : Type u) [Field F] : (ModuleCat.Hom.hom (dualNumberProj F)).ker = IsLocalRing.maximalIdeal (DualNumber F)

The kernel of the quotient map F[ε] ↠ F[ε]/(ε) is the maximal ideal of F[ε].

instance TauCeti.instIsSimpleModuleDualNumberCarrierDualNumberResidue (F : Type u) [Field F] : IsSimpleModule (DualNumber F) ↑(dualNumberResidue F)

The residue module F[ε]/(ε) is a simple F[ε]-module.

noncomputable def TauCeti.dualNumberProjectiveResolution (k : Type u) [CommRing k] : CategoryTheory.ProjectiveResolution (dualNumberResidue k)

The ε-periodic projective resolution ⋯ ⟶ A --ε--> A --ε--> A ⟶ S ⟶ 0 of k[ε]/(ε).

Equations

• TauCeti.dualNumberProjectiveResolution k = { complex := TauCeti.dualNumberComplex✝ k, projective := ⋯, hasHomology := ⋯, π := TauCeti.dualNumberComplexπ✝ k, quasiIso := ⋯ }

noncomputable def TauCeti.dualNumberProjectiveResolutionXIso (k : Type u) [CommRing k] (n : ℕ) : (dualNumberProjectiveResolution k).complex.X n ≅ dualNumberFree k

Every term of the periodic resolution is the rank-one free module A.

Equations

• TauCeti.dualNumberProjectiveResolutionXIso k n = CategoryTheory.Iso.refl ((TauCeti.dualNumberProjectiveResolution k).complex.X n)

@[simp]

theorem TauCeti.dualNumberProjectiveResolution_complex_d (k : Type u) [CommRing k] (n : ℕ) : (dualNumberProjectiveResolution k).complex.d (n + 1) n = CategoryTheory.CategoryStruct.comp (dualNumberProjectiveResolutionXIso k (n + 1)).hom (CategoryTheory.CategoryStruct.comp (dualNumberEpsSmul k) (dualNumberProjectiveResolutionXIso k n).inv)

Every differential of the periodic resolution is multiplication by ε, read through TauCeti.dualNumberProjectiveResolutionXIso.

@[simp]

theorem TauCeti.dualNumberProjectiveResolution_π_f_zero (k : Type u) [CommRing k] : CategoryTheory.CategoryStruct.comp (dualNumberProjectiveResolutionXIso k 0).inv ((dualNumberProjectiveResolution k).π.f 0) = dualNumberProj k

The augmentation of the periodic resolution is the quotient map k[ε] ↠ k[ε]/(ε), read through TauCeti.dualNumberProjectiveResolutionXIso.

@[simp]

theorem TauCeti.dualNumberProjectiveResolution_comp_eq_zero (k : Type u) [CommRing k] (p q : ℕ) (f : (dualNumberProjectiveResolution k).complex.X q ⟶ dualNumberResidue k) : CategoryTheory.CategoryStruct.comp ((dualNumberProjectiveResolution k).complex.d p q) f = 0

Every differential of the periodic resolution dies against the residue module.

The Hom spaces

noncomputable def TauCeti.homDualNumberFreeEquiv (k : Type u) [CommRing k] : (dualNumberFree k ⟶ dualNumberResidue k) ≃ₗ[k] k

Hom_A(A, S) is isomorphic to k as a k-module, by evaluation at 1.

Equations

• TauCeti.homDualNumberFreeEquiv k = (ModuleCat.homLinearEquiv.trans (LinearMap.ringLmapEquivSelf (DualNumber k) k ↑(TauCeti.dualNumberResidue k))).trans (TauCeti.dualNumberResidueEquiv k)

@[simp]

theorem TauCeti.homDualNumberFreeEquiv_apply (k : Type u) [CommRing k] (f : dualNumberFree k ⟶ dualNumberResidue k) : (homDualNumberFreeEquiv k) f = (dualNumberResidueEquiv k) ((ModuleCat.Hom.hom f) 1)

Evaluation at 1, read through TauCeti.dualNumberResidueEquiv, is what the composite does.

noncomputable def TauCeti.homDualNumberResidueEquiv (k : Type u) [CommRing k] : (dualNumberResidue k ⟶ dualNumberResidue k) ≃ₗ[k] k

End_A(S) is isomorphic to k as a k-module.

Equations

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

@[simp]

theorem TauCeti.homDualNumberResidueEquiv_apply (k : Type u) [CommRing k] (f : dualNumberResidue k ⟶ dualNumberResidue k) : (homDualNumberResidueEquiv k) f = (dualNumberResidueEquiv k) ((ModuleCat.Hom.hom f) ((ModuleCat.Hom.hom (dualNumberProj k)) 1))

TauCeti.homDualNumberResidueEquiv reads an endomorphism of S off its value on the class of 1, through TauCeti.dualNumberResidueEquiv: precomposing with A ↠ S and evaluating at 1 is the same data as evaluating at the class of 1.

The Ext groups

noncomputable def TauCeti.extDualNumberResidueSuccEquiv (k : Type u) [CommRing k] (n : ℕ) : (dualNumberFree k ⟶ dualNumberResidue k) ≃ₗ[k] CategoryTheory.Abelian.Ext (dualNumberResidue k) (dualNumberResidue k) (n + 1)

In every positive degree the periodic resolution identifies Extⁿ⁺¹_A(S, S) with the Hom-space Hom_A(A, S): no cocycle condition and no coboundary survives.

Equations

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

@[simp]

theorem TauCeti.extDualNumberResidueSuccEquiv_apply (k : Type u) [CommRing k] (n : ℕ) (f : dualNumberFree k ⟶ dualNumberResidue k) : (extDualNumberResidueSuccEquiv k n) f = (dualNumberProjectiveResolution k).extMk (CategoryTheory.CategoryStruct.comp (dualNumberProjectiveResolutionXIso k (n + 1)).hom f) (n + 2) ⋯ ⋯

The class attached to f : A ⟶ S is the one CategoryTheory.ProjectiveResolution.extMk builds out of f, transported to the degree n + 1 term of the resolution.

noncomputable def TauCeti.extDualNumberResidueEquiv (k : Type u) [CommRing k] (n : ℕ) : CategoryTheory.Abelian.Ext (dualNumberResidue k) (dualNumberResidue k) n ≃ₗ[k] k

Extⁿ_A(S, S) ≅ k for every n, where A = k[ε] is the ring of dual numbers and S = A/(ε): the periodic resolution of S has zero Hom(-, S)-differentials.

Equations

• TauCeti.extDualNumberResidueEquiv k 0 = CategoryTheory.Abelian.Ext.linearEquiv₀.trans (TauCeti.homDualNumberResidueEquiv k)
• TauCeti.extDualNumberResidueEquiv k n.succ = (TauCeti.extDualNumberResidueSuccEquiv k n).symm.trans (TauCeti.homDualNumberFreeEquiv k)

@[simp]

theorem TauCeti.extDualNumberResidueEquiv_zero (k : Type u) [CommRing k] (α : CategoryTheory.Abelian.Ext (dualNumberResidue k) (dualNumberResidue k) 0) : (extDualNumberResidueEquiv k 0) α = (homDualNumberResidueEquiv k) (CategoryTheory.Abelian.Ext.linearEquiv₀ α)

In degree 0 the equivalence is the identification Ext⁰(S, S) ≅ End_A(S) ≅ k.

@[simp]

theorem TauCeti.extDualNumberResidueEquiv_succ (k : Type u) [CommRing k] (n : ℕ) (α : CategoryTheory.Abelian.Ext (dualNumberResidue k) (dualNumberResidue k) (n + 1)) : (extDualNumberResidueEquiv k (n + 1)) α = (homDualNumberFreeEquiv k) ((extDualNumberResidueSuccEquiv k n).symm α)

In positive degree the equivalence reads a class off the cocycle representing it, through TauCeti.homDualNumberFreeEquiv.

@[simp]

theorem TauCeti.finrank_ext_dualNumberResidue {k : Type u} [Field k] (n : ℕ) : Module.finrank k (CategoryTheory.Abelian.Ext (dualNumberResidue k) (dualNumberResidue k) n) = 1

Over a field, every Extⁿ(S, S) of the residue field S of k[ε] is one-dimensional.