Graded vector spaces

Let k be a field. We use Mathlib's canonical category GradedObjectWithShift (-1) (ModuleCat k) of ℤ-graded vector spaces. Its canonical shift shiftEquiv _ 1 moves every piece up by one degree, (V{1})ᵢ = V_{i-1}, and is a k-linear autoequivalence; the pointwise abelian and linear structures come from TauCeti.CategoryTheory.GradedObject.

The one-dimensional space M = k placed in degree 0 is projective, its morphisms into V are the degree-zero piece V₀, and it is not isomorphic to any of its shifts M{j} with j ≠ 0. Forgetting the grading is Mathlib's GradedObject.total, the functor U taking the direct sum ⨁ᵢ Vᵢ of the pieces; it is invariant under the shift, {1} ⋙ U ≅ U, and U M ≅ k.

Main definitions

• TauCeti.GradedVectorSpace k and TauCeti.GradedVectorSpace.shift k: the category of ℤ-graded vector spaces and its grading shift, abbreviations for Mathlib's canonical GradedObjectWithShift (-1) (ModuleCat k) and shiftEquiv _ 1.
• TauCeti.GradedVectorSpace.unit k: the field k placed in degree 0, given by Mathlib's canonical GradedObject.single₀ applied to k.
• TauCeti.GradedVectorSpace.homUnitLinearEquiv: morphisms out of unit k are the degree-zero piece of the target.
• TauCeti.GradedVectorSpace.shiftCompTotalIso ({1} ⋙ U ≅ U) and TauCeti.GradedVectorSpace.totalObjUnitIso (U M ≅ k), for U = GradedObject.total ℤ _.

Main results

• TauCeti.GradedVectorSpace.nonempty_iso_shift_pow_obj: (V{j})ᵢ ≅ V_{i-j}.
• TauCeti.GradedVectorSpace.finrank_hom_unit_shift_pow: dim_k Hom(M, M{j}) is 1 for j = 0 and 0 otherwise; consequently M{j} ≇ M for j ≠ 0 (TauCeti.GradedVectorSpace.isEmpty_iso_unit_shift_pow).

References

• Zsuzsanna Dancso and Anthony Licata, "Koszul algebras and flow lattices", Journal of Combinatorial Theory, Series A 185 (2022), Section 2.2, for the shift convention.

@[reducible, inline]

abbrev TauCeti.GradedVectorSpace (k : Type u) [Field k] : Type (u + 1)

The category of ℤ-graded vector spaces over k: Mathlib's canonical category of graded objects GradedObjectWithShift (-1) (ModuleCat k), whose shift raises every degree by one.

Equations

• TauCeti.GradedVectorSpace k = CategoryTheory.GradedObjectWithShift (-1) (ModuleCat k)

@[reducible, inline]

abbrev TauCeti.GradedVectorSpace.shift (k : Type u) [Field k] : GradedVectorSpace k ≌ GradedVectorSpace k

The grading shift V ↦ V{1} on graded vector spaces, (V{1})ᵢ = V_{i-1}: Mathlib's canonical shift by 1, a k-linear autoequivalence.

Equations

• TauCeti.GradedVectorSpace.shift k = CategoryTheory.shiftEquiv (TauCeti.GradedVectorSpace k) 1

theorem TauCeti.GradedVectorSpace.nonempty_iso_shift_pow_obj (k : Type u) [Field k] (j : ℤ) (V : GradedVectorSpace k) (i : ℤ) : Nonempty ((shift k ^ j).functor.obj V i ≅ V (i - j))

The iterated shift reindexes the grading: the piece of V{j} in degree i is isomorphic to the piece of V in degree i - j.

noncomputable def TauCeti.GradedVectorSpace.unit (k : Type u) [Field k] : GradedVectorSpace k

The graded vector space k placed in degree 0, defined as Mathlib's canonical single-degree graded object. It is characterized by unitObjZeroIso and isZero_unit_obj.

Equations

• TauCeti.GradedVectorSpace.unit k = (CategoryTheory.GradedObject.single₀ ℤ).obj ↧k

noncomputable def TauCeti.GradedVectorSpace.unitObjZeroIso (k : Type u) [Field k] : unit k 0 ≅ ↧k

The piece of unit k in degree 0 is the field k, as an object of ModuleCat k.

Equations

• TauCeti.GradedVectorSpace.unitObjZeroIso k = CategoryTheory.GradedObject.singleObjApplyIso 0 ↧k

noncomputable def TauCeti.GradedVectorSpace.unitObjZeroLinearEquiv (k : Type u) [Field k] : ↑(unit k 0) ≃ₗ[k] k

The piece of unit k in degree 0 is the field k.

Equations

• TauCeti.GradedVectorSpace.unitObjZeroLinearEquiv k = (TauCeti.GradedVectorSpace.unitObjZeroIso k).toLinearEquiv

theorem TauCeti.GradedVectorSpace.isZero_unit_obj (k : Type u) [Field k] {i : ℤ} (hi : i ≠ 0) : CategoryTheory.Limits.IsZero (unit k i)

The pieces of unit k away from degree 0 vanish.

noncomputable def TauCeti.GradedVectorSpace.homUnitLinearEquiv (k : Type u) [Field k] (V : GradedVectorSpace k) : (unit k ⟶ V) ≃ₗ[k] ↑(V 0)

Morphisms out of unit k are the degree-zero piece of the target: a morphism is determined by the image of 1 in degree 0.

Equations

• TauCeti.GradedVectorSpace.homUnitLinearEquiv k V = (TauCeti.GradedVectorSpace.homUnitHomLinearEquiv✝ k V).trans (ModuleCat.homLinearEquiv.trans (LinearMap.ringLmapEquivSelf k k ↑(V 0)))

@[simp]

theorem TauCeti.GradedVectorSpace.homUnitLinearEquiv_apply (k : Type u) [Field k] {V : GradedVectorSpace k} (f : unit k ⟶ V) : (homUnitLinearEquiv k V) f = (ModuleCat.Hom.hom (f 0)) ((unitObjZeroLinearEquiv k).symm 1)

homUnitLinearEquiv evaluates the degree-zero component of a morphism at 1 ∈ k.

@[simp]

theorem TauCeti.GradedVectorSpace.homUnitLinearEquiv_symm_apply_zero (k : Type u) [Field k] {V : GradedVectorSpace k} (v : ↑(V 0)) : (homUnitLinearEquiv k V).symm v 0 = CategoryTheory.CategoryStruct.comp (unitObjZeroIso k).hom (ModuleCat.ofHom (LinearMap.toSpanSingleton k (↑(V 0)) v))

The degree-zero component of the morphism out of unit k corresponding to v ∈ V₀ is the identification unit k 0 ≅ k followed by c ↦ c • v.

instance TauCeti.GradedVectorSpace.instProjectiveUnit (k : Type u) [Field k] : CategoryTheory.Projective (unit k)

unit k is projective because epimorphisms of graded objects are componentwise epimorphisms and the one-dimensional module k is projective.

theorem TauCeti.GradedVectorSpace.finiteDimensional_unit_obj (k : Type u) [Field k] (i : ℤ) : FiniteDimensional k ↑(unit k i)

Every piece of unit k is finite-dimensional.

@[simp]

theorem TauCeti.GradedVectorSpace.finrank_unit_obj (k : Type u) [Field k] (i : ℤ) : Module.finrank k ↑(unit k i) = if i = 0 then 1 else 0

The piece of unit k in degree i has dimension 1 if i = 0 and 0 otherwise.

theorem TauCeti.GradedVectorSpace.nonempty_linearEquiv_hom_unit_shift_pow (k : Type u) [Field k] (j : ℤ) : Nonempty ((unit k ⟶ (shift k ^ j).functor.obj (unit k)) ≃ₗ[k] ↑(unit k (-j)))

The morphisms from M = unit k to its shift M{j} are the piece of M in degree -j.

@[simp]

theorem TauCeti.GradedVectorSpace.finrank_hom_unit_shift_pow (k : Type u) [Field k] (j : ℤ) : Module.finrank k (unit k ⟶ (shift k ^ j).functor.obj (unit k)) = if j = 0 then 1 else 0

The degree-zero morphisms Hom(M, M{j}) between M = unit k and its shifts: they form a one-dimensional space for j = 0 and vanish otherwise.

theorem TauCeti.GradedVectorSpace.isEmpty_iso_unit_shift_pow (k : Type u) [Field k] {j : ℤ} (hj : j ≠ 0) : IsEmpty (unit k ≅ (shift k ^ j).functor.obj (unit k))

The shifts of M = unit k are genuinely different: M{j} is not isomorphic to M for j ≠ 0, since there are no nonzero morphisms M ⟶ M{j} while M has nonzero endomorphisms.

Totalizing the grading

noncomputable def TauCeti.GradedVectorSpace.shiftCompTotalIso (k : Type u) [Field k] : (shift k).functor.comp (CategoryTheory.GradedObject.total ℤ (ModuleCat k)) ≅ CategoryTheory.GradedObject.total ℤ (ModuleCat k)

Totalizing the grading is invariant under the shift: {1} ⋙ U ≅ U. Both functors are left adjoint to the constant functor.

Equations

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

noncomputable def TauCeti.GradedVectorSpace.totalObjUnitIso (k : Type u) [Field k] : (CategoryTheory.GradedObject.total ℤ (ModuleCat k)).obj (unit k) ≅ ↧k

The total space underlying M = unit k is k.

Equations

• TauCeti.GradedVectorSpace.totalObjUnitIso k = TauCeti.GradedVectorSpace.coproductUnitIso✝ k