Grothendieck Group

Results named in Tau Ceti's TauCeti.RepresentationTheory.GrothendieckGroup modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremArtin's identity in G₀(k[G]) over every field, written as induction of the unit from subgroups#

No division by the group order is required.

TauCeti.natCard_nsmul_one_eq_sum_artinCoeff_indK0.{u} (k G : Type u) [Field k] [Group G]
  [Finite G] :
  Nat.card G • 1 = ∑ᶠ (C : Subgroup G), (C.artinCoeff * ↑(Nat.card ↥C)) • (TauCeti.indK0 k C) 1
Lean

Formalized in Tau Ceti as TauCeti.natCard_nsmul_one_eq_sum_artinCoeff_indK0.

Sources
LeanTauCeti.natCard_nsmul_one_eq_sum_artinCoeff_indK0
Uses 3 · Used by 1
Proof usesArtin's signed permutation identity in the exact Grothendieck group over every field · The dual Noether isomorphism · The Noether isomorphism for exact categories
Used byArtin's induction identity for every virtual class over every field

TheoremArtin's induction identity for every virtual class over every field#

Multiplying by |G| expresses a class as the Artin-coefficient sum of its induced restrictions.

TauCeti.natCard_nsmul_eq_sum_artinCoeff_indK0_resK0.{u} (k G : Type u) [Field k] [Group G]
  [Finite G] (x : TauCeti.ExactK0 (TauCeti.finiteModulesExactStructure (MonoidAlgebra k G))) :
  Nat.card G • x =
    ∑ᶠ (C : Subgroup G),
      (C.artinCoeff * ↑(Nat.card ↥C)) • (TauCeti.indK0 k C) ((TauCeti.resK0 k C.subtype) x)
Lean

Formalized in Tau Ceti as TauCeti.natCard_nsmul_eq_sum_artinCoeff_indK0_resK0.

Sources
LeanTauCeti.natCard_nsmul_eq_sum_artinCoeff_indK0_resK0
Uses 3 · Used by 2
Proof usesArtin's identity in G₀(k[G]) over every field, written as induction of the unit from subgroups · The dual Noether isomorphism · The Noether isomorphism for exact categories
Used byModular-Artin reduction of the local Euler characteristic formula · The modular Artin theorem with multiplier |G|

TheoremArtin's signed permutation identity in the exact Grothendieck group over every field# 

TauCeti.natCard_nsmul_permK0_quotient_top_eq_sum_artinCoeff.{u} (k G : Type u) [Field k] [Group G]
  [Finite G] :
  Nat.card G • TauCeti.permK0 k G (G ⧸ ⊤) =
    ∑ᶠ (C : Subgroup G), (C.artinCoeff * ↑(Nat.card ↥C)) • TauCeti.permK0 k G (G ⧸ C)
Lean

Formalized in Tau Ceti as TauCeti.natCard_nsmul_permK0_quotient_top_eq_sum_artinCoeff.

Sources
LeanTauCeti.natCard_nsmul_permK0_quotient_top_eq_sum_artinCoeff
Uses 3 · Used by 1
Proof usesArtin's identity for fixed points · The dual Noether isomorphism · The Noether isomorphism for exact categories
Used byArtin's identity in G₀(k[G]) over every field, written as induction of the unit from subgroups

TheoremThe Cartan path-count formula#

The multiplicity of Sᵢ in the vertex projective Pⱼ is the number of oriented paths from j to i. With simples in rows and projectives in columns, these are the entries of the Cartan matrix of a finite acyclic path algebra.

TauCeti.jordanHolderMultiplicity_vertexProjectiveModuleFG_eq_card_path.{v, w} (k : Type (max v w))
  (Q : Type v) [Field k] [Quiver Q] [Finite Q] [FiniteDimensional k (TauCeti.pathAlgebra k Q)]
  (i j : Q) :
  TauCeti.jordanHolderMultiplicity (TauCeti.pathAlgebra k Q)
      ↑(TauCeti.vertexProjectiveModuleFG k Q j) ↑(TauCeti.vertexSimpleModuleFG k Q i) =
    Nat.card (Quiver.Path j i)
Lean

Formalized in Tau Ceti as TauCeti.jordanHolderMultiplicity_vertexProjectiveModuleFG_eq_card_path.

Sources
LeanTauCeti.jordanHolderMultiplicity_vertexProjectiveModuleFG_eq_card_path
Uses 2
Proof usesThe dual Noether isomorphism · The Noether isomorphism for exact categories

TheoremThe general-field Cartan/Ext-Euler identity#

Let P i ⟶ S i be projective covers of simple modules. If every pair of finitely generated modules is Euler-admissible, then Cᵀ * E = diagonal (fun i ↦ dim_k End_A(S i)), where C i j = [P j : S i] is the Cartan matrix and E is the Ext-Euler matrix in the simple-class basis.

TauCeti.cartanMatrix_transpose_mul_extEulerMatrix_eq_diagonal.{u, v, u_1} {k : Type u_1} [Field k]
  {A : Type u} [Ring A] [Algebra k A] [IsArtinianRing A] {I : Type v} [Fintype I] [DecidableEq I]
  (P : I → (TauCeti.finiteProjectiveModules A).FullSubcategory) (S : I → FGModuleCat A)
  [hS : ∀ (i : I), IsSimpleModule A ↑(S i)]
  (hind : ∀ (i : I), TauCeti.IsIndecomposableModule A ↑(P i).obj)
  (hPnoniso : Pairwise fun i j => IsEmpty (↑(P i).obj ≃ₗ[A] ↑(P j).obj))
  (hPexhaustive : TauCeti.IsExhaustiveIndecomposableProjectiveFamily P)
  (hSnoniso : Pairwise fun i j => IsEmpty (↑(S i) ≃ₗ[A] ↑(S j)))
  (hSexhaustive : TauCeti.IsExhaustiveSimpleFamily S) {f : (i : I) → ↑(P i).obj →ₗ[A] ↑(S i).obj}
  (hf : ∀ (i : I), TauCeti.IsProjectiveCover (f i))
  (hadm : TauCeti.IsEulerAdmissibleOn k (ModuleCat.isFG A) (ModuleCat.isFG A)) :
  (TauCeti.cartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive).transpose *
      TauCeti.extEulerMatrix (ModuleCat.isFG A) (ModuleCat.isFG A) ⋯ ⋯ hadm
        ((TauCeti.simpleClassBasis S hSnoniso hSexhaustive).map
          (TauCeti.finiteModulesExactK0Equiv A).toIntLinearEquiv)
        ((TauCeti.simpleClassBasis S hSnoniso hSexhaustive).map
          (TauCeti.finiteModulesExactK0Equiv A).toIntLinearEquiv) =
    Matrix.diagonal fun i => ↑(Module.finrank k (Module.End A ↑(S i).obj))
Lean

Formalized in Tau Ceti as TauCeti.cartanMatrix_transpose_mul_extEulerMatrix_eq_diagonal.

Sources
LeanTauCeti.cartanMatrix_transpose_mul_extEulerMatrix_eq_diagonal
Uses 4
Proof usesThe dual Noether isomorphism · The Krull-Schmidt theorem · The Noether isomorphism for exact categories · Schur's lemma, vanishing form

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.