Documentation

TauCeti.Algebra.Homology.Ext.GradedDualNumbers

Bigraded Ext over the graded dual numbers #

Let k be a commutative ring and grade the dual numbers A = k[ε] with ε in degree two (TauCeti.dualNumberIntegerGrade). The residue module S = A/(ε) is concentrated in degree zero. Multiplication by ε raises degrees by two, so the ungraded periodic resolution of S becomes the graded projective resolution

⋯ ⟶ A{4} --ε--> A{2} --ε--> A ⟶ S ⟶ 0

whose nth term A{2n} is generated in internal degree 2n. Its differentials take values in A₊ = (ε), so it is minimal, and graded Hom from it into any internal shift of S has zero differentials. Hence Extⁿ(S, S{j}) is the degree-2n piece of S{j}, that is the degree 2n - j piece of S. Over a field this gives

dim_k Extⁿ(S, S{j}) = 1 if j = 2n, and 0 otherwise.

Thus every cohomological degree carries exactly one internal degree, and no cohomological degree vanishes. This is the graded refinement of TauCeti.finrank_ext_dualNumberResidue.

Main definitions #

Main results #

References #

source
@[reducible, inline]
noncomputable abbrev TauCeti.dualNumberGradedResidue (k : Type u) [CommRing k] :
GradedModuleCat (dualNumberIntegerGrade k)

The graded residue module S = k[ε]/(ε), concentrated in degree zero: the graded head A / A₊ of the regular module A.

Instances For
    source
    noncomputable def TauCeti.dualNumberGradedResolution (k : Type u) [CommRing k] :
    GradedProjectiveResolution (dualNumberIntegerGrade k) (dualNumberGradedResidue k).grading

    The ε-periodic graded projective resolution ⋯ ⟶ A{4} ⟶ A{2} ⟶ A ⟶ S ⟶ 0 of the graded residue module, for ε in degree two. Every differential is multiplication by ε, and the nth term is A{2n} (TauCeti.dualNumberGradedResolution_termObj).

    Instances For
      source
      theorem TauCeti.dualNumberGradedResolution_termObj (k : Type u) [CommRing k] (n : ℕ) :
      (dualNumberGradedResolution k).termObj n = GradedModuleCat.regular.shiftObj (2 * ↑n)

      The nth term of the periodic graded resolution is the shifted regular module A{2n}.

      source
      theorem TauCeti.dualNumberGradedResolution_differential_hom_one (k : Type u) [CommRing k] (n : ℕ) :
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((dualNumberGradedResolution k).differential n) (CategoryTheory.eqToHom ⋯))).hom 1 = DualNumber.eps

      Every differential of the periodic graded resolution, read through TauCeti.dualNumberGradedResolution_termObj as a map A{2n + 2} ⟶ A{2n}, sends 1 to ε.

      source
      theorem TauCeti.dualNumberGradedResolution_augmentation_hom_one (k : Type u) [CommRing k] :
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (dualNumberGradedResolution k).augmentation).hom 1 = (gradedPositiveMulQuotientMk ⋯) ⟨1, ⋯⟩

      The augmentation of the periodic graded resolution, read through TauCeti.dualNumberGradedResolution_termObj as a map A ⟶ S, sends 1 to the class of 1.

      source
      theorem TauCeti.isMinimal_dualNumberGradedResolution (k : Type u) [CommRing k] :
      (dualNumberGradedResolution k).IsMinimal

      The periodic graded resolution is minimal: every differential is multiplication by ε, which has positive degree.

      source
      theorem TauCeti.dualNumberGradedResidue_piece_eq_bot (k : Type u) [CommRing k] {p : ℤ} (hp : p ≠ 0) :
      (dualNumberGradedResidue k).grading.piece ℤ p = ⊥

      The graded residue module vanishes outside degree zero.

      source
      theorem TauCeti.positive_smul_top_shiftObj_dualNumberGradedResidue_eq_bot (k : Type u) [CommRing k] (j : ℤ) :
      (⨆ (i : ℤ), ⨆ (_ : 0 < i), dualNumberIntegerGrade k i) • ⊤ = ⊥

      Positive-degree scalars annihilate every internal shift of the graded residue module.

      source
      noncomputable def TauCeti.extDualNumberGradedResidueShiftEquiv (k : Type u) [CommRing k] [CategoryTheory.HasExt (GradedModuleCat (dualNumberIntegerGrade k))] (n : ℕ) (j : ℤ) :
      CategoryTheory.Abelian.Ext (dualNumberGradedResidue k) ((dualNumberGradedResidue k).shiftObj j) n ≃ₗ[k] ↥((dualNumberGradedResidue k).grading.piece ℤ (2 * ↑n - j))

      Extⁿ(S, S{j}) is the degree-(2n - j) piece of S, for the graded residue module S of the dual numbers with ε in degree two: the minimal periodic resolution identifies it with graded Hom from A{2n} to S{j}, that is with the degree-2n piece of S{j}.

      Instances For
        source
        theorem TauCeti.extDualNumberGradedResidueShiftEquiv_symm_apply (k : Type u) [CommRing k] [CategoryTheory.HasExt (GradedModuleCat (dualNumberIntegerGrade k))] (n : ℕ) (j : ℤ) (m : ↥((dualNumberGradedResidue k).grading.piece ℤ (2 * ↑n - j))) :
        (extDualNumberGradedResidueShiftEquiv k n j).symm m = (⋯.extLinearEquiv ⋯ n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((((dualNumberGradedResidue k).shiftObj j).regularShiftHomEquiv (2 * ↑n)).symm ⟨↑m, ⋯⟩))

        The inverse of TauCeti.extDualNumberGradedResidueShiftEquiv sends m ∈ S_{2n - j} to the class, computed by the minimal periodic resolution, of the graded map A{2n} ⟶ S{j} sending 1 to m.

        source
        theorem TauCeti.finrank_dualNumberGradedResidue_piece (k : Type u) [Field k] (p : ℤ) :
        Module.finrank k ↥((dualNumberGradedResidue k).grading.piece ℤ p) = if p = 0 then 1 else 0

        The graded residue module is one-dimensional, concentrated in degree zero.

        source
        theorem TauCeti.finrank_ext_dualNumberGradedResidue_shiftObj (k : Type u) [Field k] [CategoryTheory.HasExt (GradedModuleCat (dualNumberIntegerGrade k))] (n : ℕ) (j : ℤ) :
        Module.finrank k (CategoryTheory.Abelian.Ext (dualNumberGradedResidue k) ((dualNumberGradedResidue k).shiftObj j) n) = if j = 2 * ↑n then 1 else 0

        dim_k Extⁿ(S, S{j}) is 1 if j = 2n and 0 otherwise, for the graded residue field S of the dual numbers with ε in degree two. Each cohomological degree contributes exactly one internal degree, and none vanishes.