Documentation

TauCeti.RepresentationTheory.GrothendieckGroup.CartanMatrix

Projective-simple coordinates and the Cartan matrix #

Let R be an Artinian ring, and choose exhaustive families (P i) and (S i) of pairwise nonisomorphic indecomposable projective and simple modules, indexed so that P i is a projective cover of S i. The corresponding bases of K₀(proj R) and G₀(mod R) are in perfect integral pairing: pairing [P i] with [M] reads the Jordan--Hölder multiplicity [M : S i].

The matrix of the Cartan map in these bases therefore has entry

C i j = [P j : S i].

Thus columns record projectives in the simple basis. This convention is important for left modules: the row index is the simple module and the column index is the projective module.

Main definitions #

Main results #

References #

The projective-simple multiplicity pairing #

source
noncomputable def TauCeti.projectiveSimplePairing {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (P : I → (finiteProjectiveModules R).FullSubcategory) (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) :
ExactK0 (finiteProjectiveModulesExactStructure R) →ₗ[ℤ] ExactK0 (finiteModulesExactStructure R) →ₗ[ℤ] ℤ

The projective-simple multiplicity pairing. This is the coordinate-dual pairing between the chosen projective and simple bases, indexed by the common type I, so pairing [P i] with a module class reads its S i Jordan--Hölder coordinate.

It has its representation-theoretic meaning when P i is a projective cover of S i; the construction itself only uses the common indexing, so no cover maps are required.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.projectiveSimplePairing_of_left {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (P : I → (finiteProjectiveModules R).FullSubcategory) (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) (i : I) (x : ExactK0 (finiteModulesExactStructure R)) :
    ((projectiveSimplePairing P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive) (ExactK0.of (P i))) x = (jordanHolderCoordinate R ↑(S i)) x

    Pairing with the class of P i is the Jordan--Hölder coordinate attached to S i.

    source
    theorem TauCeti.projectiveSimplePairing_of_of {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (P : I → (finiteProjectiveModules R).FullSubcategory) (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) (i : I) (M : FGModuleCat R) :
    ((projectiveSimplePairing P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive) (ExactK0.of (P i))) (ExactK0.of M) = ↑(jordanHolderMultiplicity R ↑M ↑(S i))

    On object classes, the projective-simple pairing is Jordan--Hölder multiplicity.

    source
    theorem TauCeti.projectiveSimplePairing_basis {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (P : I → (finiteProjectiveModules R).FullSubcategory) (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) [DecidableEq I] (i j : I) :
    ((projectiveSimplePairing P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive) (ExactK0.of (P i))) (ExactK0.of (S j)) = if i = j then 1 else 0

    The selected projective and simple basis classes pair as a Kronecker delta.

    source
    theorem TauCeti.projectiveSimplePairing_isPerfPair {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (P : I → (finiteProjectiveModules R).FullSubcategory) (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) [Finite I] :
    (projectiveSimplePairing P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive).IsPerfPair

    For a finite indexing type, the integral projective-simple multiplicity pairing is perfect: it identifies either Grothendieck group with the integral dual of the other.

    The Cartan matrix #

    source
    noncomputable def TauCeti.cartanMatrix {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (P : I → (finiteProjectiveModules R).FullSubcategory) (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) [Fintype I] :
    Matrix I I ℤ

    The Cartan matrix of the selected projective and simple families: the matrix of the Cartan map K₀(proj R) → G₀(mod R) in the indecomposable-projective basis on the source and the simple-class basis on the target. Rows are indexed by simples and columns by projectives.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.cartanMatrix_apply {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (P : I → (finiteProjectiveModules R).FullSubcategory) (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) [Fintype I] (i j : I) :
      cartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive i j = ↑(jordanHolderMultiplicity R ↑{ obj := (P j).obj, property := ⋯ } ↑(S i))

      Cartan-matrix entries are composition multiplicities: the (i,j) entry is the Jordan--Hölder multiplicity [P j : S i].

      source
      theorem TauCeti.cartanMatrix_apply_eq_projectiveSimplePairing {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (P : I → (finiteProjectiveModules R).FullSubcategory) (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] (hind : ∀ (i : I), IsIndecomposableModule R ↑(P i).obj) (hPnoniso : Pairwise fun (i j : I) => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj)) (hPexhaustive : IsExhaustiveIndecomposableProjectiveFamily P) (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) [Fintype I] (i j : I) :
      cartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive i j = ((projectiveSimplePairing P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive) (ExactK0.of (P i))) ((cartanMap R) (ExactK0.of (P j)))

      A Cartan-matrix entry is obtained by pairing the corresponding projective basis vector with the image under the Cartan map of the column projective.

      source
      theorem TauCeti.cartanMap_of_eq_sum {R : Type u} [Ring R] [IsArtinianRing R] {I : Type v} (P : I → (finiteProjectiveModules R).FullSubcategory) (S : I → FGModuleCat R) [hS : ∀ (i : I), IsSimpleModule R ↑(S i)] (hSnoniso : Pairwise fun (i j : I) => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j))) (hSexhaustive : IsExhaustiveSimpleFamily S) [Fintype I] (j : I) :
      (cartanMap R) (ExactK0.of (P j)) = ∑ i : I, ↑(jordanHolderMultiplicity R ↑{ obj := (P j).obj, property := ⋯ } ↑(S i)) • ExactK0.of (S i)

      Columns of the Cartan matrix are projective composition-factor vectors. The image of [P j] under the Cartan map is the sum of the simple basis vectors with coefficients [P j : S i].