Documentation

TauCeti.Algebra.Category.FGModuleCat.Stable.CyclicHom

Stable morphisms between cyclic modules #

Let A be an algebra over a field k and let a, b : A. A map of right A-modules out of the cyclic module A ⧸ aA is determined by the image m of the generator, which can be any element with m * a = 0. Such a map A ⧸ aA ⟶ A ⧸ bA factors through a projective module exactly when it lifts along the quotient map A ⟶ A ⧸ bA, that is, when m is the class of an element of the left annihilator of a. This gives the dimension of the stable morphism space as the difference

dim {m ∈ A ⧸ bA | m * a = 0} - dim (image in A ⧸ bA of {c ∈ A | c * a = 0}).

For the truncated polynomial algebra A = K[X]/(X ^ n) over a field K, with x the class of X and M_i = A ⧸ (x ^ i), both terms are explicit: the first is min i j and the second is j - min j (n - i) (TauCeti.FGModuleCat.finrank_cyclicModule_hom_root_pow, TauCeti.FGModuleCat.finrank_map_ker_smul_op_root_pow). Hence for i, j ≤ n

dim_K Hom_stable(M_i, M_j) = min (min i j) (min (n - i) (n - j)).

In particular M_n = A has no nonzero stable endomorphisms, and the stable dimensions are unchanged when (i, j) is replaced by (n - i, n - j), as they must be since the syzygy autoequivalence sends M_i to M_(n - i) (TauCeti.FGModuleCat.stableModuleLoopCyclicModuleRootPowIso). No hypothesis on the characteristic of K is used.

Right A-modules are left Aᵐᵒᵖ-modules, so the condition m * a = 0 is written op a • m = 0. The description of maps out of A ⧸ aA by the image of the generator is TauCeti.FGModuleCat.cyclicModuleHomEquiv. The k-vector space structure on morphisms is Mathlib's ModuleCat.linearOverField, inherited by the stable category as a quotient by a morphism ideal.

Main results #

References #

Stable morphisms between cyclic modules #

source
theorem TauCeti.FGModuleCat.stableModuleFunctor_map_cyclicModule_eq_zero_iff {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {a b : A} (f : cyclicModule a ⟶ cyclicModule b) :
(stableModuleFunctor A).map f = 0 ↔ ∃ (c : Aᵐᵒᵖ), MulOpposite.op a * c = 0 ∧ Submodule.Quotient.mk c = (ModuleCat.Hom.hom f.hom) (Submodule.Quotient.mk 1)

A map A ⧸ aA ⟶ A ⧸ bA vanishes in the stable module category exactly when the image of the generator is the class of an element c with op a * c = 0: the map then lifts along the quotient map A ⟶ A ⧸ bA, which is an epimorphism from a projective module.

source
theorem TauCeti.FGModuleCat.finrank_stableModuleHom_cyclicModule_add_finrank {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (k : Type w) [Field k] [Algebra k A] [FiniteDimensional k A] (a b : A) :
Module.finrank k ((stableModuleFunctor A).obj (cyclicModule a) ⟶ (stableModuleFunctor A).obj (cyclicModule b)) + Module.finrank k ↥(Submodule.map (↑k (Submodule.mkQ (Ideal.span {MulOpposite.op b}))) (DistribSMul.toLinearMap k Aᵐᵒᵖ (MulOpposite.op a)).ker) = Module.finrank k ↥(DistribSMul.toLinearMap k (Aᵐᵒᵖ ⧸ Ideal.span {MulOpposite.op b}) (MulOpposite.op a)).ker

Dimension of stable morphisms between cyclic modules. The stable morphisms A ⧸ aA ⟶ A ⧸ bA together with the image in A ⧸ bA of the left annihilator of a have the dimension of the space of elements of A ⧸ bA killed by a, which is the dimension of all morphisms A ⧸ aA ⟶ A ⧸ bA.

The truncated polynomial algebra K[X]/(X ^ n) #

source
theorem TauCeti.FGModuleCat.finrank_stableModuleHom_cyclicModule_root_pow {K : Type u} [Field K] {n i j : ℕ} (hi : i ≤ n) (hj : j ≤ n) :
Module.finrank K ((stableModuleFunctor (AdjoinRoot (Polynomial.X ^ n))).obj (cyclicModule (AdjoinRoot.root (Polynomial.X ^ n) ^ i)) ⟶ (stableModuleFunctor (AdjoinRoot (Polynomial.X ^ n))).obj (cyclicModule (AdjoinRoot.root (Polynomial.X ^ n) ^ j))) = min (min i j) (min (n - i) (n - j))

Stable morphisms between the cyclic modules of K[X]/(X ^ n). With x the class of X and M_i = A ⧸ (x ^ i), the space of stable morphisms M_i ⟶ M_j has dimension min (min i j) (min (n - i) (n - j)) for i, j ≤ n, over any field K.