Grothendieck groups, Cartan maps, and Euler forms

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

DefinitionThe resolution theorem#

For a resolving property P of an exact category, the inclusion of the full subcategory on P induces an isomorphism of exact Grothendieck groups. Its inverse sends the class of an object to the alternating class of any finite P-resolution of it, by TauCeti.ExactStructure.IsResolving.resolutionEquiv_symm_of.

TauCeti.ExactStructure.IsResolving.resolutionEquiv.{w, v, u} {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C]
  (E : TauCeti.ExactStructure C) (P : CategoryTheory.ObjectProperty C) [E.IsResolving P]
  [CategoryTheory.EssentiallySmall.{w, v, u} C] :
  TauCeti.ExactK0 (E.resolvingSubcategory P) ≃+ TauCeti.ExactK0 E

Lean

Formalized in Tau Ceti as TauCeti.ExactStructure.IsResolving.resolutionEquiv.

Sources

• Tau Ceti documentation: TauCeti.ExactStructure.IsResolving.resolutionEquiv
• Source of TauCeti.ExactStructure.IsResolving.resolutionEquiv in TauCeti/CategoryTheory/GrothendieckGroup/Resolving.lean
• Tau Ceti roadmap status: Grothendieck groups, Cartan maps, and Euler forms

LeanTauCeti.ExactStructure.IsResolving.resolutionEquiv

Uses 2 · Used by 2

Proof usesThe dual Noether isomorphism · The Noether isomorphism for exact categories

Used byEquivalence invariance of the resolution theorem · The graded resolution theorem

TheoremCartan-matrix unimodularity#

If every finitely generated module admits a finite resolution by finitely generated projectives, the Cartan determinant is 1 or -1. No positivity of its sign is asserted.

TauCeti.cartanMatrix_det_eq_one_or_neg_one.{u, v} {R : Type u} [Ring R] [IsArtinianRing R]
  {I : Type v} [Fintype I] [DecidableEq I]
  (P : I → (TauCeti.finiteProjectiveModules R).FullSubcategory) (S : I → FGModuleCat R)
  [∀ (i : I), IsSimpleModule R ↑(S i)]
  (hind : ∀ (i : I), TauCeti.IsIndecomposableModule R ↑(P i).obj)
  (hPnoniso : Pairwise fun i j => IsEmpty (↑(P i).obj ≃ₗ[R] ↑(P j).obj))
  (hPexhaustive : TauCeti.IsExhaustiveIndecomposableProjectiveFamily P)
  (hSnoniso : Pairwise fun i j => IsEmpty (↑(S i) ≃ₗ[R] ↑(S j)))
  (hSexhaustive : TauCeti.IsExhaustiveSimpleFamily S)
  (h :
    ModuleCat.isFG R ≤
      (TauCeti.ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution
        (TauCeti.finiteProjectiveModules R)) :
  (TauCeti.cartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive).det = 1 ∨
    (TauCeti.cartanMatrix P S hind hPnoniso hPexhaustive hSnoniso hSexhaustive).det = -1

Lean

Formalized in Tau Ceti as TauCeti.cartanMatrix_det_eq_one_or_neg_one.

Sources

• Tau Ceti documentation: TauCeti.cartanMatrix_det_eq_one_or_neg_one
• Source of TauCeti.cartanMatrix_det_eq_one_or_neg_one in TauCeti/RepresentationTheory/GrothendieckGroup/UnimodularCartanMatrix.lean
• Tau Ceti roadmap status: Grothendieck groups, Cartan maps, and Euler forms

LeanTauCeti.cartanMatrix_det_eq_one_or_neg_one

Uses 5

Proof usesThe dual Noether isomorphism · The Krull-Schmidt theorem · The Noether isomorphism for exact categories · The resolution theorem for modules · The resolution theorem for modules admitting finite resolutions by finitely generated projectives

TheoremThe graded Cartan matrix of the dual numbers is 1 + q², with ε in degree two, in the bases [A] and [S]#

the regular module has the graded composition factors S and S{2}. At q = 1 this is the ungraded Cartan matrix 2 of TauCeti.cartanMatrix_dualNumber.

TauCeti.gradedCartanMatrix_dualNumber.{u} (k : Type u) [Field k] :
  TauCeti.gradedCartanMatrix (TauCeti.dualNumberIntegerGrade k)
      (TauCeti.dualNumberGradedProjectiveBasis k) (TauCeti.dualNumberGradedResidueBasis k) =
    Matrix.of fun x x_1 => 1 + LaurentPolynomial.T 2

Lean

Formalized in Tau Ceti as TauCeti.gradedCartanMatrix_dualNumber.

Sources

• Tau Ceti documentation: TauCeti.gradedCartanMatrix_dualNumber
• Source of TauCeti.gradedCartanMatrix_dualNumber in TauCeti/RepresentationTheory/GrothendieckGroup/GradedDualNumbers.lean
• Tau Ceti roadmap status: Grothendieck groups, Cartan maps, and Euler forms

LeanTauCeti.gradedCartanMatrix_dualNumber

Uses 6

Statement usesThe graded Cartan matrix in a projective basis bP and a module basis bM · The graded projectives A eᵢ form a basis of K₀^gr(proj A)

Proof usesThe dual Noether isomorphism · Jacobson's lemma · The Noether isomorphism for exact categories · TauCeti.isLocalRing_end_of_indecomposable

DefinitionTauCeti.gradedCartanEquiv#

If every finite graded module admits a finite graded-projective resolution, the graded Cartan map is an isomorphism of ℤ[q,q⁻¹]-modules.

TauCeti.gradedCartanEquiv.{uk, uA} {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A]
  (𝒜 : ℤ → Submodule k A) [DirectSum.Decomposition 𝒜]
  (h :
    TauCeti.gradedFiniteModules 𝒜 ≤
      (TauCeti.gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution
        (TauCeti.gradedFiniteProjectiveModules 𝒜)) :
  TauCeti.LaurentK0 (TauCeti.gradedFiniteProjectiveModulesExactStructure 𝒜) ≃ₗ[LaurentPolynomial ℤ]
    TauCeti.LaurentK0 (TauCeti.gradedFiniteModulesExactStructure 𝒜)

Lean

Formalized in Tau Ceti as TauCeti.gradedCartanEquiv.

Sources

• Tau Ceti documentation: TauCeti.gradedCartanEquiv
• Source of TauCeti.gradedCartanEquiv in TauCeti/Algebra/Category/GradedModuleCat/CartanMap/Resolution.lean
• Tau Ceti roadmap status: Grothendieck groups, Cartan maps, and Euler forms

LeanTauCeti.gradedCartanEquiv

Uses 4

Statement usesThe graded resolution theorem

Proof usesThe dual Noether isomorphism · The Noether isomorphism for exact categories · The resolution theorem for finite projective resolutions

TheoremThe q-Euler matrix of a path algebra is the inverse of its conjugate-transposed graded Cartan matrix#

χ_q(Sᵢ, Sⱼ) is the (i, j) entry of ((C.map invert)ᵀ)⁻¹, where C is the graded Cartan matrix in the bases of graded vertex projectives and graded vertex simples.

TauCeti.PathAlgebra.gradedExtEulerForm_gradedVertexSimpleClassBasis_eq_inv.{u, v, w} (k : Type w)
  (Q : Type u) [Field k] [Quiver Q] [Fintype Q] [DecidableEq Q]
  [Module.Finite k (TauCeti.pathAlgebra k Q)]
  [CategoryTheory.HasExt (TauCeti.GradedModuleCat (TauCeti.PathAlgebra.integerGrade k Q))]
  (i j : Q) :
  ((TauCeti.PathAlgebra.gradedExtEulerForm k Q)
        ((TauCeti.PathAlgebra.gradedVertexSimpleClassBasis k Q) i))
      ((TauCeti.PathAlgebra.gradedVertexSimpleClassBasis k Q) j) =
    ((TauCeti.gradedCartanMatrix (TauCeti.PathAlgebra.integerGrade k Q)
                (TauCeti.PathAlgebra.gradedVertexProjectiveClassBasis k Q)
                (TauCeti.PathAlgebra.gradedVertexSimpleClassBasis k Q)).map
            ⇑LaurentPolynomial.invert).transpose⁻¹
      i j

Lean

Formalized in Tau Ceti as TauCeti.PathAlgebra.gradedExtEulerForm_gradedVertexSimpleClassBasis_eq_inv.

Sources

• Tau Ceti documentation: TauCeti.PathAlgebra.gradedExtEulerForm_gradedVertexSimpleClassBasis_eq_inv
• Source of TauCeti.PathAlgebra.gradedExtEulerForm_gradedVertexSimpleClassBasis_eq_inv in TauCeti/RepresentationTheory/Quiver/PathAlgebra/GradedExtEuler/CartanMatrix.lean
• Tau Ceti roadmap status: Grothendieck groups, Cartan maps, and Euler forms

LeanTauCeti.PathAlgebra.gradedExtEulerForm_gradedVertexSimpleClassBasis_eq_inv

Uses 7

Statement usesThe graded Cartan matrix in a projective basis bP and a module basis bM · The graded projectives A eᵢ form a basis of K₀^gr(proj A)

Proof usesThe dual Noether isomorphism · The graded first-arrow Euler formula · Jacobson's lemma · The Noether isomorphism for exact categories · TauCeti.isLocalRing_end_of_indecomposable

TheoremThe graded quiver q-Euler form at q = 1 is the ungraded Ext-Euler pairing#

On G₀^gr(mod kQ) specialized at q = 1, the q-Euler form is the Ext-Euler pairing on G₀(mod kQ) of the classes with their grading forgotten.

TauCeti.PathAlgebra.laurentSpecialize_gradedExtEulerForm_eq_extEulerPairing.{u, v}
  (k : Type (max u v)) (Q : Type u) [Field k] [Quiver Q] [Finite Q]
  [FiniteDimensional k (TauCeti.pathAlgebra k Q)]
  [CategoryTheory.HasExt (TauCeti.GradedModuleCat (TauCeti.PathAlgebra.integerGrade k Q))]
  (x y :
    TauCeti.LaurentSpecialization 1
      (TauCeti.LaurentK0
        (TauCeti.gradedFiniteModulesExactStructure (TauCeti.PathAlgebra.integerGrade k Q)))) :
  (((TauCeti.PathAlgebra.gradedExtEulerForm k Q).laurentSpecialize ⋯) x) y =
    ((TauCeti.extEulerPairing ⋯ ⋯ ⋯)
        ((TauCeti.finiteModulesExactK0Equiv (TauCeti.pathAlgebra k Q))
          ((TauCeti.gradedFiniteModulesForgetK0 (TauCeti.PathAlgebra.integerGrade k Q)) x)))
      ((TauCeti.finiteModulesExactK0Equiv (TauCeti.pathAlgebra k Q))
        ((TauCeti.gradedFiniteModulesForgetK0 (TauCeti.PathAlgebra.integerGrade k Q)) y))

Lean

Formalized in Tau Ceti as TauCeti.PathAlgebra.laurentSpecialize_gradedExtEulerForm_eq_extEulerPairing.

Sources

• Tau Ceti documentation: TauCeti.PathAlgebra.laurentSpecialize_gradedExtEulerForm_eq_extEulerPairing
• Source of TauCeti.PathAlgebra.laurentSpecialize_gradedExtEulerForm_eq_extEulerPairing in TauCeti/RepresentationTheory/Quiver/PathAlgebra/GradedExtEuler/ForgetGrading.lean
• Tau Ceti roadmap status: Grothendieck groups, Cartan maps, and Euler forms

LeanTauCeti.PathAlgebra.laurentSpecialize_gradedExtEulerForm_eq_extEulerPairing

Uses 2

Proof usesThe dual Noether isomorphism · The Noether isomorphism for exact categories

TheoremBigraded Ext detects linear resolutions over a semisimple degree-zero part#

Suppose that A is finite-dimensional and nonnegatively graded, with semisimple degree-zero part. For an exhaustive family of finite simple modules concentrated in degree zero, every simple admits a linear graded projective resolution if and only if every entry of the full bigraded Ext Poincare matrix has diagonal support.

Unlike TauCeti.forall_isLinear_iff_bigradedExtPoincareMatrix_isDiagonal, this statement does not take a preselected family of minimal resolutions: their existence, with finite-dimensional terms, follows from semisimplicity of the degree-zero part.

TauCeti.forall_exists_isLinear_iff_bigradedExtPoincareMatrix_isDiagonal.{uk, uA, uI} {k : Type uk}
  [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜]
  [CategoryTheory.HasExt (TauCeti.GradedModuleCat 𝒜)] {I : Type uI} [IsSemisimpleRing ↥(𝒜 0)]
  [Module.Finite k A] (S : I → (TauCeti.gradedFiniteModules 𝒜).FullSubcategory)
  (hS : TauCeti.IsExhaustiveGradedSimpleFamily S)
  (hSzero : ∀ (i : I) (p : ℤ), p ≠ 0 → (S i).obj.grading.piece ℤ p = ⊥)
  (h :
    TauCeti.IsGradedEulerAdmissibleOn (TauCeti.gradedFiniteModules 𝒜)
      (TauCeti.gradedFiniteModules 𝒜))
  (hneg : ∀ p < 0, 𝒜 p = ⊥) {b : ℕ}
  (hb :
    ∀ (i j : I),
      TauCeti.IsGradedExtBoundedBy (TauCeti.GradedModuleCat.shift 𝒜) (S i).obj (S j).obj b) :
  (∀ (i : I), ∃ r, r.IsLinear) ↔
    ∀ (i j : I),
      TauCeti.Bigraded.IsDiagonal (TauCeti.bigradedExtPoincareMatrix (fun i => (S i).obj) ⋯ b i j)

Lean

Formalized in Tau Ceti as TauCeti.forall_exists_isLinear_iff_bigradedExtPoincareMatrix_isDiagonal.

Sources

• Tau Ceti documentation: TauCeti.forall_exists_isLinear_iff_bigradedExtPoincareMatrix_isDiagonal
• Source of TauCeti.forall_exists_isLinear_iff_bigradedExtPoincareMatrix_isDiagonal in TauCeti/Algebra/Category/GradedModuleCat/LinearResolution/Poincare.lean
• Tau Ceti roadmap status: Grothendieck groups, Cartan maps, and Euler forms

LeanTauCeti.forall_exists_isLinear_iff_bigradedExtPoincareMatrix_isDiagonal

Uses 1

Statement usesTauCeti.GradedProjectiveResolution.IsLinear

TheoremThe Cartan--Poincare identity over a semisimple degree-zero part#

If A is finite-dimensional and nonnegatively graded, its degree-zero part is semisimple, the chosen simples are concentrated in degree zero, and their full bigraded Ext Poincare matrix is diagonal, then C^T * P(-q) = diagonal (fun i ↦ gdim(eᵢ • Sᵢ)).

The diagonal entries are nonzero and need not be one; for projective covers of degree-zero simples they are the constants dim_k End_A(Sᵢ). The semisimplicity hypothesis supplies minimal projective resolutions with finite-dimensional terms, so no resolutions or minimality witnesses occur in the public statement.

TauCeti.cartan_poincare_of_bigradedExtPoincareMatrix_isDiagonal_of_semisimple.{uk, uA, uI}
  {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A}
  [GradedAlgebra 𝒜] [CategoryTheory.HasExt (TauCeti.GradedModuleCat 𝒜)] {I : Type uI}
  [Module.Finite k A] [Fintype I] [DecidableEq I]
  (S : I → (TauCeti.gradedFiniteModules 𝒜).FullSubcategory) {e : I → A}
  (he : ∀ (i : I), IsIdempotentElem (e i)) (he₀ : ∀ (i : I), e i ∈ 𝒜 0)
  (hI : ∀ (i : I), Ideal.IsHomogeneous 𝒜 (Ideal.span {e i}))
  (hne : Pairwise fun i j => TauCeti.GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0)
  (hself : ∀ (i : I), TauCeti.GradedModuleCat.smulGradedDimension (e i) (S i).obj ≠ 0)
  (hS : TauCeti.IsExhaustiveGradedSimpleFamily S)
  (bP :
    Module.Basis I (LaurentPolynomial ℤ)
      (TauCeti.LaurentK0 (TauCeti.gradedFiniteProjectiveModulesExactStructure 𝒜)))
  (hbP :
    ∀ (i : I),
      bP i =
        TauCeti.LaurentK0.of (TauCeti.gradedFiniteProjectiveModulesExactStructure 𝒜)
          { obj := TauCeti.GradedModuleCat.ofIdeal 𝒜 (Ideal.span {e i}) ⋯, property := ⋯ })
  [IsSemisimpleRing ↥(𝒜 0)]
  (h :
    TauCeti.IsGradedEulerAdmissibleOn (TauCeti.gradedFiniteModules 𝒜)
      (TauCeti.gradedFiniteModules 𝒜))
  (hneg : ∀ p < 0, 𝒜 p = ⊥) (hconc : ∀ (i : I) (p : ℤ), p ≠ 0 → (S i).obj.grading.piece ℤ p = ⊥)
  {b : ℕ}
  (hb :
    ∀ (i j : I),
      TauCeti.IsGradedExtBoundedBy (TauCeti.GradedModuleCat.shift 𝒜) (S i).obj (S j).obj b)
  (hdiag :
    ∀ (i j : I),
      TauCeti.Bigraded.IsDiagonal
        (TauCeti.bigradedExtPoincareMatrix (fun i => (S i).obj) ⋯ b i j)) :
  (TauCeti.gradedCartanMatrix 𝒜 bP
          (TauCeti.gradedSimpleClassBasisOfNeZero S he he₀ hne hself hS)).transpose *
      (TauCeti.diagonalExtPoincareMatrix k (fun i => (S i).obj) b).map
        ⇑(Polynomial.eval₂RingHom LaurentPolynomial.C (-LaurentPolynomial.T 1)) =
    Matrix.diagonal fun i => TauCeti.GradedModuleCat.smulGradedDimension (e i) (S i).obj

Lean

Formalized in Tau Ceti as TauCeti.cartan_poincare_of_bigradedExtPoincareMatrix_isDiagonal_of_semisimple.

Sources

• Tau Ceti documentation: TauCeti.cartan_poincare_of_bigradedExtPoincareMatrix_isDiagonal_of_semisimple
• Source of TauCeti.cartan_poincare_of_bigradedExtPoincareMatrix_isDiagonal_of_semisimple in TauCeti/Algebra/Category/GradedModuleCat/CartanMap/ExtEuler/Linearity.lean
• Tau Ceti roadmap status: Grothendieck groups, Cartan maps, and Euler forms

LeanTauCeti.cartan_poincare_of_bigradedExtPoincareMatrix_isDiagonal_of_semisimple

Uses 5

Statement usesThe graded Cartan matrix in a projective basis bP and a module basis bM

Proof usesThe dual Noether isomorphism · The general-field Cartan--Poincaré identity · The Noether isomorphism for exact categories · TauCeti.GradedProjectiveResolution.IsLinear

DefinitionThe graded Cartan matrix in a projective basis bP and a module basis bM#

the matrix of the Laurent-linear graded Cartan map. Rows are indexed by bM and columns by bP.

TauCeti.gradedCartanMatrix.{uk, uA, uI, uJ} {k : Type uk} [CommRing k] {A : Type uA} [Ring A]
  [Algebra k A] (𝒜 : ℤ → Submodule k A) {I : Type uI} {J : Type uJ} [Fintype I] [Finite J]
  (bP :
    Module.Basis I (LaurentPolynomial ℤ)
      (TauCeti.LaurentK0 (TauCeti.gradedFiniteProjectiveModulesExactStructure 𝒜)))
  (bM :
    Module.Basis J (LaurentPolynomial ℤ)
      (TauCeti.LaurentK0 (TauCeti.gradedFiniteModulesExactStructure 𝒜))) :
  Matrix J I (LaurentPolynomial ℤ)

Lean

Formalized in Tau Ceti as TauCeti.gradedCartanMatrix.

Sources

• Tau Ceti documentation: TauCeti.gradedCartanMatrix
• Source of TauCeti.gradedCartanMatrix in TauCeti/Algebra/Category/GradedModuleCat/CartanMap/Matrix.lean
• Tau Ceti roadmap status: Grothendieck groups, Cartan maps, and Euler forms

LeanTauCeti.gradedCartanMatrix

Uses 2 · Used by 6

Proof usesThe dual Noether isomorphism · The Noether isomorphism for exact categories

Used byThe general-field Cartan--Poincaré identity · The Cartan--Poincare identity over a semisimple degree-zero part · The graded Cartan matrix of the dual numbers is 1 + q², with ε in degree two, in the bases [A] and [S] · The q-Euler matrix of a path algebra is the inverse of its conjugate-transposed graded Cartan matrix · The weighted graded Cartan coefficient formula · TauCeti.gradedCartanMatrix_zigzagAlgebra

DefinitionThe graded projectives A eᵢ form a basis of K₀^gr(proj A)#

The graded projectives A eᵢ form a basis of K₀^gr(proj A) over ℤ[q,q⁻¹], for a nonnegatively graded finite-dimensional algebra whose degree-zero piece is spanned by a complete family of orthogonal nonzero idempotents eᵢ. Its basis vector at i is the class [A eᵢ]. This is the projective counterpart of the head basis TauCeti.gradedIdempotentHeadBasis, and the case of TauCeti.gradedIdempotentProjectiveBasisOfPrimitive where each eᵢ is primitive by TauCeti.isPrimitiveIdempotent_of_gradeZero_le_span and the A eᵢ are pairwise nonisomorphic by TauCeti.isEmpty_linearEquiv_span_singleton_of_gradeZero_le_span.

TauCeti.gradedIdempotentProjectiveBasis.{uk, uA, uI} {k : Type uk} [Field k] {A : Type uA} [Ring A]
  [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} [Fintype I] {e : I → A}
  (he : CompleteOrthogonalIdempotents e) (he₀ : ∀ (i : I), e i ∈ 𝒜 0)
  (hI : ∀ (i : I), Ideal.IsHomogeneous 𝒜 (Ideal.span {e i})) [Module.Finite k A]
  (hneg : ∀ p < 0, 𝒜 p = ⊥) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e))
  (hne : ∀ (i : I), e i ≠ 0) :
  Module.Basis I (LaurentPolynomial ℤ)
    (TauCeti.LaurentK0 (TauCeti.gradedFiniteProjectiveModulesExactStructure 𝒜))

Lean

Formalized in Tau Ceti as TauCeti.gradedIdempotentProjectiveBasis.

Sources

• Tau Ceti documentation: TauCeti.gradedIdempotentProjectiveBasis
• Source of TauCeti.gradedIdempotentProjectiveBasis in TauCeti/Algebra/Category/GradedModuleCat/CartanMap/Idempotent/Projective/Basic.lean
• Tau Ceti roadmap status: Grothendieck groups, Cartan maps, and Euler forms

LeanTauCeti.gradedIdempotentProjectiveBasis

Uses 4 · Used by 2

Proof usesThe dual Noether isomorphism · Jacobson's lemma · The Noether isomorphism for exact categories · TauCeti.isLocalRing_end_of_indecomposable

Used byThe graded Cartan matrix of the dual numbers is 1 + q², with ε in degree two, in the bases [A] and [S] · The q-Euler matrix of a path algebra is the inverse of its conjugate-transposed graded Cartan matrix

DefinitionTauCeti.GradedProjectiveResolution.IsLinear#

A graded projective resolution is linear if its term in homological degree n is generated by its homogeneous piece of internal degree n.

TauCeti.GradedProjectiveResolution.IsLinear.{uk, uA, uM, u_1} {k : Type uk} {A : Type uA}
  [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M : Type uM} [AddCommGroup M]
  [_root_.Module k M] [_root_.Module A M] {G : TauCeti.InternalGrading k M ℤ}
  (r : TauCeti.GradedProjectiveResolution 𝒜 G) : Prop

Lean

Formalized in Tau Ceti as TauCeti.GradedProjectiveResolution.IsLinear.

Sources

• Tau Ceti documentation: TauCeti.GradedProjectiveResolution.IsLinear
• Source of TauCeti.GradedProjectiveResolution.IsLinear in TauCeti/Algebra/Module/GradedModule/Resolution.lean
• Tau Ceti roadmap status: Grothendieck groups, Cartan maps, and Euler forms

LeanTauCeti.GradedProjectiveResolution.IsLinear

Used by 4

Used byThe general-field Cartan--Poincaré identity · Bigraded Ext detects linear resolutions over a semisimple degree-zero part · The Cartan--Poincare identity over a semisimple degree-zero part · The Koszulity dichotomy for zigzag algebras

TheoremEquivalence invariance of the resolution theorem#

An exact equivalence identifying two resolving properties intertwines both the ambient exact K₀ equivalence and the equivalence of the resolving subcategories with their resolution-theorem comparisons.

TauCeti.ExactStructure.IsResolving.mapEquiv_comp_resolutionEquiv.{w, w', v, v', u, u'} {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C]
  {E : TauCeti.ExactStructure C} {P : CategoryTheory.ObjectProperty C} [E.IsResolving P]
  [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D]
  [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D]
  [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D]
  {E' : TauCeti.ExactStructure D} {P' : CategoryTheory.ObjectProperty D} [E'.IsResolving P']
  (e : C ≌ D) [e.functor.Additive] [e.inverse.Additive] (hF : E.IsConflationExact E' e.functor)
  (hG : E'.IsConflationExact E e.inverse) (h : P'.inverseImage e.functor = P) :
  (TauCeti.ExactK0.mapEquiv e hF hG).toAddMonoidHom.comp
      (TauCeti.ExactStructure.IsResolving.resolutionEquiv E P).toAddMonoidHom =
    (TauCeti.ExactStructure.IsResolving.resolutionEquiv E' P').toAddMonoidHom.comp
      (TauCeti.ExactK0.mapEquiv (e.congrFullSubcategory h) ⋯ ⋯).toAddMonoidHom

Lean

Formalized in Tau Ceti as TauCeti.ExactStructure.IsResolving.mapEquiv_comp_resolutionEquiv.

Sources

• Tau Ceti documentation: TauCeti.ExactStructure.IsResolving.mapEquiv_comp_resolutionEquiv
• Source of TauCeti.ExactStructure.IsResolving.mapEquiv_comp_resolutionEquiv in TauCeti/CategoryTheory/GrothendieckGroup/Resolving.lean

LeanTauCeti.ExactStructure.IsResolving.mapEquiv_comp_resolutionEquiv

Uses 3

Statement usesThe resolution theorem

Proof usesThe dual Noether isomorphism · The Noether isomorphism for exact categories

TheoremThe graded first-arrow Euler formula#

Pairing a vertex simple against a finite-dimensional graded module subtracts the shifted outgoing-arrow coordinates from its own vertex coordinate.

TauCeti.PathAlgebra.gradedExtEuler_gradedVertexSimple.{u, v, w, t} (k : Type w) (Q : Type u)
  [Field k] [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)]
  [CategoryTheory.HasExt (TauCeti.GradedModuleCat (TauCeti.PathAlgebra.integerGrade k Q))] (i : Q)
  (Y : TauCeti.GradedModuleCat (TauCeti.PathAlgebra.integerGrade k Q)) [Module.Finite k Y.carrier]
  (h :
    TauCeti.IsGradedEulerAdmissible k
      (TauCeti.GradedModuleCat.shift (TauCeti.PathAlgebra.integerGrade k Q))
      (TauCeti.PathAlgebra.gradedVertexSimple k Q i) Y) :
  TauCeti.gradedExtEuler k (TauCeti.GradedModuleCat.shift (TauCeti.PathAlgebra.integerGrade k Q))
      h =
    TauCeti.GradedModuleCat.smulGradedDimension (TauCeti.PathAlgebra.vertexIdempotent k i) Y -
      LaurentPolynomial.T (-1) *
        ∑ a,
          TauCeti.GradedModuleCat.smulGradedDimension (TauCeti.PathAlgebra.vertexIdempotent k a.fst)
            Y

Lean

Formalized in Tau Ceti as TauCeti.PathAlgebra.gradedExtEuler_gradedVertexSimple.

Sources

• Tau Ceti documentation: TauCeti.PathAlgebra.gradedExtEuler_gradedVertexSimple
• Source of TauCeti.PathAlgebra.gradedExtEuler_gradedVertexSimple in TauCeti/RepresentationTheory/Quiver/PathAlgebra/GradedExtEuler/Value.lean

LeanTauCeti.PathAlgebra.gradedExtEuler_gradedVertexSimple

Used by 2

Used byThe graded Ringel formula on Grothendieck classes · The q-Euler matrix of a path algebra is the inverse of its conjugate-transposed graded Cartan matrix

TheoremThe graded Ringel formula on Grothendieck classes#

The vertex coordinates are the idempotent graded dimensions, and the source coordinates are conjugated by q ↦ q⁻¹.

TauCeti.PathAlgebra.gradedExtEulerForm_eq_sum.{u, v, w} (k : Type w) (Q : Type u) [Field k]
  [Quiver Q] [Finite Q] [Module.Finite k (TauCeti.pathAlgebra k Q)]
  [CategoryTheory.HasExt (TauCeti.GradedModuleCat (TauCeti.PathAlgebra.integerGrade k Q))]
  [Fintype Q]
  (x y :
    TauCeti.LaurentK0
      (TauCeti.gradedFiniteModulesExactStructure (TauCeti.PathAlgebra.integerGrade k Q))) :
  ((TauCeti.PathAlgebra.gradedExtEulerForm k Q) x) y =
    ∑ i,
        LaurentPolynomial.invert
            (((TauCeti.PathAlgebra.gradedVertexSimpleClassBasis k Q).repr x) i) *
          ((TauCeti.PathAlgebra.gradedVertexSimpleClassBasis k Q).repr y) i -
      LaurentPolynomial.T (-1) *
        ∑ i,
          ∑ j,
            ↑(Nat.card (i ⟶ j)) *
                LaurentPolynomial.invert
                  (((TauCeti.PathAlgebra.gradedVertexSimpleClassBasis k Q).repr x) i) *
              ((TauCeti.PathAlgebra.gradedVertexSimpleClassBasis k Q).repr y) j

Lean

Formalized in Tau Ceti as TauCeti.PathAlgebra.gradedExtEulerForm_eq_sum.

Other forms

The graded Ringel formula for finite-dimensional graded modules. Formalized in Tau Ceti as TauCeti.PathAlgebra.gradedExtEuler_eq_sum_smulGradedDimension.

TauCeti.PathAlgebra.gradedExtEuler_eq_sum_smulGradedDimension.{u, v, w} (k : Type w) (Q : Type u)
  [Field k] [Quiver Q] [Finite Q] [Module.Finite k (TauCeti.pathAlgebra k Q)]
  [CategoryTheory.HasExt (TauCeti.GradedModuleCat (TauCeti.PathAlgebra.integerGrade k Q))]
  [Fintype Q] (X Y : TauCeti.GradedModuleCat (TauCeti.PathAlgebra.integerGrade k Q))
  [Module.Finite k X.carrier] [Module.Finite k Y.carrier]
  (h :
    TauCeti.IsGradedEulerAdmissible k
      (TauCeti.GradedModuleCat.shift (TauCeti.PathAlgebra.integerGrade k Q)) X Y) :
  TauCeti.gradedExtEuler k (TauCeti.GradedModuleCat.shift (TauCeti.PathAlgebra.integerGrade k Q))
      h =
    ∑ i,
        LaurentPolynomial.invert
            (TauCeti.GradedModuleCat.smulGradedDimension (TauCeti.PathAlgebra.vertexIdempotent k i)
              X) *
          TauCeti.GradedModuleCat.smulGradedDimension (TauCeti.PathAlgebra.vertexIdempotent k i) Y -
      LaurentPolynomial.T (-1) *
        ∑ i,
          ∑ j,
            ↑(Nat.card (i ⟶ j)) *
                LaurentPolynomial.invert
                  (TauCeti.GradedModuleCat.smulGradedDimension
                    (TauCeti.PathAlgebra.vertexIdempotent k i) X) *
              TauCeti.GradedModuleCat.smulGradedDimension (TauCeti.PathAlgebra.vertexIdempotent k j)
                Y

Sources

• Tau Ceti documentation: TauCeti.PathAlgebra.gradedExtEulerForm_eq_sum
• Source of TauCeti.PathAlgebra.gradedExtEulerForm_eq_sum in TauCeti/RepresentationTheory/Quiver/PathAlgebra/GradedExtEuler/Pairing.lean

LeanTauCeti.PathAlgebra.gradedExtEulerForm_eq_sum · TauCeti.PathAlgebra.gradedExtEuler_eq_sum_smulGradedDimension

Uses 3

Proof usesThe dual Noether isomorphism · The graded first-arrow Euler formula · The Noether isomorphism for exact categories

TheoremThe weighted graded Cartan coefficient formula#

A coefficient in a column [A f], multiplied by dim_k(eᵢ • (Sᵢ)₀), is the corresponding graded corner dimension.

TauCeti.finrank_smul_simple_piece_zero_mul_coeff_gradedCartanMatrix.{uk, uA, uI, uJ} {k : Type uk}
  [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A}
  {I : Type uI} (S : I → (TauCeti.gradedFiniteModules 𝒜).FullSubcategory) {e : I → A}
  (he : ∀ (i : I), IsIdempotentElem (e i)) (he₀ : ∀ (i : I), e i ∈ 𝒜 0)
  (hne : Pairwise fun i j => TauCeti.GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0)
  (hself : ∀ (i : I), TauCeti.GradedModuleCat.smulGradedDimension (e i) (S i).obj ≠ 0)
  (hS : TauCeti.IsExhaustiveGradedSimpleFamily S) [GradedAlgebra 𝒜] {J : Type uJ} [Fintype J]
  [Finite I]
  (bP :
    Module.Basis J (LaurentPolynomial ℤ)
      (TauCeti.LaurentK0 (TauCeti.gradedFiniteProjectiveModulesExactStructure 𝒜)))
  {f : A} (hf : IsIdempotentElem f) (hF : Ideal.IsHomogeneous 𝒜 (Ideal.span {f})) (j : J)
  (hj :
    bP j =
      TauCeti.LaurentK0.of (TauCeti.gradedFiniteProjectiveModulesExactStructure 𝒜)
        { obj := TauCeti.GradedModuleCat.ofIdeal 𝒜 (Ideal.span {f}) hF, property := ⋯ })
  (i : I) (hconc : ∀ (p : ℤ), p ≠ 0 → (S i).obj.grading.piece ℤ p = ⊥) (p : ℤ) :
  ↑(Module.finrank k ↥(e i • (S i).obj.grading.piece ℤ 0)) *
      (TauCeti.gradedCartanMatrix 𝒜 bP
            (TauCeti.gradedSimpleClassBasisOfNeZero S he he₀ hne hself hS) i j).coeff
        p =
    ↑(Module.finrank k ↥(TauCeti.cornerSubmodule k (e i) f ⊓ 𝒜 p))

Lean

Formalized in Tau Ceti as TauCeti.finrank_smul_simple_piece_zero_mul_coeff_gradedCartanMatrix.

Sources

• Tau Ceti documentation: TauCeti.finrank_smul_simple_piece_zero_mul_coeff_gradedCartanMatrix
• Source of TauCeti.finrank_smul_simple_piece_zero_mul_coeff_gradedCartanMatrix in TauCeti/Algebra/Category/GradedModuleCat/CartanMap/Coefficients.lean

LeanTauCeti.finrank_smul_simple_piece_zero_mul_coeff_gradedCartanMatrix

Uses 3

Statement usesThe graded Cartan matrix in a projective basis bP and a module basis bM

Proof usesThe dual Noether isomorphism · The Noether isomorphism for exact categories

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.