Documentation

TauCeti.RepresentationTheory.GrothendieckGroup.Finrank

The dimension homomorphism on the Grothendieck group of finite-length modules #

Let A be a finite-dimensional algebra over a field k. Every finitely generated A-module is then finite-dimensional over k, and the k-dimension is additive in short exact sequences, so it descends to a homomorphism TauCeti.finrankK0 : G₀(mod A) →+ ℤ out of the exact Grothendieck group of TauCeti.finiteModulesExactStructure. It is the invariant that turns a relation in G₀(mod A) into an identity between dimensions, and in particular it detects the zero module.

Read in the simple-class basis of TauCeti/RepresentationTheory/GrothendieckGroup/SimpleBasis.lean, the dimension of a class is the sum of its Jordan--Hölder multiplicities weighted by the dimensions of the simple modules. When every simple module is isomorphic to one fixed line the dimension is an isomorphism G₀(mod A) ≃+ ℤ.

The finite-dimensionality of A over k is essential and not cosmetic: Module.finrank has a junk value on an infinite-dimensional space, so without it the function below is not additive. The same restriction appears, for the same reason, in TauCeti.pathAlgebraDimensionVectorK0.

Main definitions #

Main results #

References #

The dimension homomorphism #

source
theorem TauCeti.finiteDimensional_fgModuleCat_obj (k : Type u) [Field k] (A : Type u) [Ring A] [Algebra k A] [FiniteDimensional k A] (M : FGModuleCat A) :
FiniteDimensional k ↑M.obj

A finitely generated module over a finite-dimensional algebra is finite-dimensional over the base field. This is what makes Module.finrank over the base field an honest invariant of such a module rather than a junk value.

source
noncomputable def TauCeti.finrankK0 (k : Type u) [Field k] (A : Type u) [Ring A] [Algebra k A] [FiniteDimensional k A] :
ExactK0 (finiteModulesExactStructure A) →+ ℤ

The dimension homomorphism on the Grothendieck group of the finitely generated modules over a finite-dimensional algebra: on the class of M it is dim_k M.

Instances For
    source
    @[simp]
    theorem TauCeti.finrankK0_of (k : Type u) [Field k] (A : Type u) [Ring A] [Algebra k A] [FiniteDimensional k A] (M : FGModuleCat A) :
    (finrankK0 k A) (ExactK0.of M) = ↑(Module.finrank k ↑M.obj)

    The dimension homomorphism sends the class of a module to its dimension over the base field.

    source
    theorem TauCeti.finrankK0_unique (k : Type u) [Field k] (A : Type u) [Ring A] [Algebra k A] [FiniteDimensional k A] (f : ExactK0 (finiteModulesExactStructure A) →+ ℤ) (hf : ∀ (M : FGModuleCat A), f (ExactK0.of M) = ↑(Module.finrank k ↑M.obj)) :
    f = finrankK0 k A

    The dimension homomorphism is the only homomorphism to ℤ returning the dimension on object classes.

    source
    theorem TauCeti.finrankK0_of_nonneg (k : Type u) [Field k] (A : Type u) [Ring A] [Algebra k A] [FiniteDimensional k A] (M : FGModuleCat A) :
    0 ≤ (finrankK0 k A) (ExactK0.of M)

    Object classes have nonnegative dimension.

    source
    theorem TauCeti.finrankK0_of_eq_zero_iff (k : Type u) [Field k] (A : Type u) [Ring A] [Algebra k A] [FiniteDimensional k A] (M : FGModuleCat A) :
    (finrankK0 k A) (ExactK0.of M) = 0 ↔ Subsingleton ↑M.obj

    The dimension homomorphism detects the zero module: the class of M has dimension zero exactly when M is the zero module.

    source
    theorem TauCeti.finrankK0_of_pos (k : Type u) [Field k] (A : Type u) [Ring A] [Algebra k A] [FiniteDimensional k A] (M : FGModuleCat A) (hM : Nontrivial ↑M.obj) :
    0 < (finrankK0 k A) (ExactK0.of M)

    A nonzero module has a class of positive dimension.

    source
    @[simp]
    theorem TauCeti.finrankK0_finiteModulesK0Restrict (k : Type u) [Field k] (A : Type u) [Ring A] [Algebra k A] [FiniteDimensional k A] {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (f : A →+* B) (hfk : f.comp (algebraMap k A) = algebraMap k B) (x : ExactK0 (finiteModulesExactStructure B)) :
    (finrankK0 k A) ((f.finiteModulesK0Restrict ⋯) x) = (finrankK0 k B) x

    Restriction of scalars preserves dimension. Restricting scalars along a ring homomorphism f : A →+* B of finite-dimensional k-algebras compatible with the structure maps does not change the k-dimension of a class.

    The dimension homomorphism in the simple-class basis #

    source
    theorem TauCeti.finrankK0_eq_sum_jordanHolderCoordinate_mul (k : Type u) [Field k] (A : Type u) [Ring A] [Algebra k A] [FiniteDimensional k A] [IsArtinianRing A] {I : Type v} (S : I → FGModuleCat A) [∀ (i : I), IsSimpleModule A ↑(S i)] (hnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[A] ↑(S j))) (hexhaustive : IsExhaustiveSimpleFamily S) [Fintype I] (x : ExactK0 (finiteModulesExactStructure A)) :
    (finrankK0 k A) x = ∑ i : I, (jordanHolderCoordinate A ↑(S i)) x * ↑(Module.finrank k ↑(S i).obj)

    The dimension of a class is its Jordan--Hölder expansion weighted by the dimensions of the simple modules. For the class of a module this is the statement that the dimension of a module is the sum of the dimensions of its composition factors.

    Algebras whose simple modules are all isomorphic to one line #

    source
    theorem TauCeti.eq_finrankK0_smul_of_finrank_eq_one (k : Type u) [Field k] (A : Type u) [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FGModuleCat A) (hexhaustive : IsExhaustiveSimpleFamily fun (x : Unit) => S) (hdim : Module.finrank k ↑S.obj = 1) (x : ExactK0 (finiteModulesExactStructure A)) :
    x = (finrankK0 k A) x • ExactK0.of S

    Every class is an integer multiple of the class of S when every simple module is isomorphic to S and S is a line. The multiple is then the dimension itself. Simplicity of S is not needed: exhaustiveness of the one-member family already says that S is the only simple module up to isomorphism, which is what the composition-series induction behind TauCeti.span_range_exactK0OfFamily_eq_top consumes.

    source
    theorem TauCeti.finrankK0_bijective_of_finrank_eq_one (k : Type u) [Field k] (A : Type u) [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FGModuleCat A) (hexhaustive : IsExhaustiveSimpleFamily fun (x : Unit) => S) (hdim : Module.finrank k ↑S.obj = 1) :
    Function.Bijective ⇑(finrankK0 k A)

    The dimension homomorphism is bijective when every simple module is isomorphic to the line S.

    source
    noncomputable def TauCeti.finrankK0Equiv (k : Type u) [Field k] (A : Type u) [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FGModuleCat A) (hexhaustive : IsExhaustiveSimpleFamily fun (x : Unit) => S) (hdim : Module.finrank k ↑S.obj = 1) :
    ExactK0 (finiteModulesExactStructure A) ≃+ ℤ

    G₀(mod A) ≃+ ℤ when every simple module is isomorphic to the line S, the isomorphism being the dimension. The group algebra of a finite ℓ-group over a field of characteristic ℓ, whose only simple module is the trivial one, is an instance.

    Instances For
      source
      @[simp]
      theorem TauCeti.finrankK0Equiv_apply (k : Type u) [Field k] (A : Type u) [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FGModuleCat A) (hexhaustive : IsExhaustiveSimpleFamily fun (x : Unit) => S) (hdim : Module.finrank k ↑S.obj = 1) (x : ExactK0 (finiteModulesExactStructure A)) :
      (finrankK0Equiv k A S hexhaustive hdim) x = (finrankK0 k A) x
      source
      @[simp]
      theorem TauCeti.finrankK0Equiv_symm_apply (k : Type u) [Field k] (A : Type u) [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FGModuleCat A) (hexhaustive : IsExhaustiveSimpleFamily fun (x : Unit) => S) (hdim : Module.finrank k ↑S.obj = 1) (n : ℤ) :
      (finrankK0Equiv k A S hexhaustive hdim).symm n = n • ExactK0.of S