Grothendieck Group

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

TheoremThe Euler–Poincaré theorem in abelian K₀#

For a cochain complex that is strictly supported in degrees a to b, and any finite range of degrees containing [a, b], the alternating sum of the classes of the terms equals the alternating sum of the classes of the cohomology objects.

TauCeti.AbelianK0.eulerChar_eq_homologyEulerChar.{w, v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  [CategoryTheory.EssentiallySmall.{w, v, u} A] (K : CochainComplex A ℤ) (a b : ℤ)
  [K.IsStrictlyGE a] [K.IsStrictlyLE b] {s : Finset ℤ} (hs : Finset.Icc a b ⊆ s) :
  TauCeti.AbelianK0.eulerChar K s = TauCeti.AbelianK0.homologyEulerChar K s

Lean

Formalized in Tau Ceti as TauCeti.AbelianK0.eulerChar_eq_homologyEulerChar.

Other forms

The Euler–Poincaré theorem for an additive invariant. Formalized in Tau Ceti as TauCeti.AbelianK0.AdditiveInvariant.sum_negOnePow_obj_X_eq_sum_negOnePow_obj_homology.

TauCeti.AbelianK0.AdditiveInvariant.sum_negOnePow_obj_X_eq_sum_negOnePow_obj_homology.{v, u, u_1}
  {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {G : Type u_1}
  [AddCommGroup G] (v : TauCeti.AbelianK0.AdditiveInvariant A G) (K : CochainComplex A ℤ) (a b : ℤ)
  [K.IsStrictlyGE a] [K.IsStrictlyLE b] {s : Finset ℤ} (hs : Finset.Icc a b ⊆ s) :
  ∑ n ∈ s, ↑n.negOnePow • v.obj (K.X n) =
    ∑ n ∈ s, ↑n.negOnePow • v.obj (HomologicalComplex.homology K n)

The Euler–Poincaré theorem in an extension-closed subcategory. Formalized in Tau Ceti as TauCeti.ExactK0.AdditiveInvariant.sum_negOnePow_obj_X_eq_sum_negOnePow_obj_homology.

TauCeti.ExactK0.AdditiveInvariant.sum_negOnePow_obj_X_eq_sum_negOnePow_obj_homology.{v, u, u_1}
  {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  {P : CategoryTheory.ObjectProperty A} [P.ContainsZero] [P.IsClosedUnderBinaryProducts]
  {hP : (TauCeti.ExactStructure.abelian A).IsExtensionClosed P} {G : Type u_1} [AddCommGroup G]
  (v : TauCeti.ExactK0.AdditiveInvariant (TauCeti.ExactStructure.fullSubcategory P hP) G)
  {K : CochainComplex A ℤ} (hB : ∀ (n : ℤ), P (CategoryTheory.Abelian.image (K.d n (n + 1))))
  (hH : ∀ (n : ℤ), P (HomologicalComplex.homology K n)) (a b : ℤ) [K.IsStrictlyGE a]
  [K.IsStrictlyLE b] {s : Finset ℤ} (hs : Finset.Icc a b ⊆ s) :
  ∑ n ∈ s, ↑n.negOnePow • v.obj { obj := K.X n, property := ⋯ } =
    ∑ n ∈ s, ↑n.negOnePow • v.obj { obj := HomologicalComplex.homology K n, property := ⋯ }

The Euler–Poincaré theorem in exact K₀ of an extension-closed subcategory. Formalized in Tau Ceti as TauCeti.ExactK0.sum_negOnePow_of_X_eq_sum_negOnePow_of_homology.

TauCeti.ExactK0.sum_negOnePow_of_X_eq_sum_negOnePow_of_homology.{w, v, u} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A]
  {P : CategoryTheory.ObjectProperty A} [P.ContainsZero] [P.IsClosedUnderBinaryProducts]
  (hP : (TauCeti.ExactStructure.abelian A).IsExtensionClosed P)
  [CategoryTheory.EssentiallySmall.{w, v, u} P.FullSubcategory] (K : CochainComplex A ℤ)
  (hB : ∀ (n : ℤ), P (CategoryTheory.Abelian.image (K.d n (n + 1))))
  (hH : ∀ (n : ℤ), P (HomologicalComplex.homology K n)) (a b : ℤ) [K.IsStrictlyGE a]
  [K.IsStrictlyLE b] {s : Finset ℤ} (hs : Finset.Icc a b ⊆ s) :
  ∑ n ∈ s, ↑n.negOnePow • TauCeti.ExactK0.of { obj := K.X n, property := ⋯ } =
    ∑ n ∈ s,
      ↑n.negOnePow • TauCeti.ExactK0.of { obj := HomologicalComplex.homology K n, property := ⋯ }

Sources

• Tau Ceti documentation: TauCeti.AbelianK0.eulerChar_eq_homologyEulerChar
• Source of TauCeti.AbelianK0.eulerChar_eq_homologyEulerChar in TauCeti/CategoryTheory/GrothendieckGroup/EulerCharacteristic.lean

LeanTauCeti.AbelianK0.eulerChar_eq_homologyEulerChar · TauCeti.AbelianK0.AdditiveInvariant.sum_negOnePow_obj_X_eq_sum_negOnePow_obj_homology · TauCeti.ExactK0.AdditiveInvariant.sum_negOnePow_obj_X_eq_sum_negOnePow_obj_homology · TauCeti.ExactK0.sum_negOnePow_of_X_eq_sum_negOnePow_of_homology

Uses 2 · Used by 1

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

Used byEuler–Poincaré for cubes

TheoremThe generating half of the resolution theorem#

If every object of C admits a finite P-resolution, then the classes of the objects satisfying P generate exact K₀.

TauCeti.ExactK0.closure_propClasses_eq_top.{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) [CategoryTheory.EssentiallySmall.{w, v, u} C]
  (h : ∀ (X : C), E.admitsFiniteResolution P X) :
  AddSubgroup.closure (TauCeti.ExactK0.propClasses E P) = ⊤

Lean

Formalized in Tau Ceti as TauCeti.ExactK0.closure_propClasses_eq_top.

Sources

• Tau Ceti documentation: TauCeti.ExactK0.closure_propClasses_eq_top
• Source of TauCeti.ExactK0.closure_propClasses_eq_top in TauCeti/CategoryTheory/GrothendieckGroup/Resolution.lean

LeanTauCeti.ExactK0.closure_propClasses_eq_top

DefinitionThe graded resolution theorem#

Let P be a class of E-projectives containing a zero object, closed under binary biproducts, and stable under the grading shift. Then the inclusion of P into the objects of finite P-dimension induces an isomorphism of graded Grothendieck groups as ℤ[q,q⁻¹]-modules. Its inverse sends the class of an object to its Euler class, by TauCeti.GradedExactStructure.laurentResolutionEquiv_symm_of.

TauCeti.GradedExactStructure.laurentResolutionEquiv.{w, v, u} {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C]
  (E : TauCeti.GradedExactStructure C) [CategoryTheory.LocallySmall.{w, v, u} C]
  {P : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P]
  [P.ContainsZero] [P.IsClosedUnderBinaryProducts]
  [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (E.admitsFiniteResolution P)]
  (hproj : P ≤ E.isProjective) (hshift : P.inverseImage E.shift.functor = P) :
  TauCeti.LaurentK0 (E.fullSubcategory P ⋯ hshift) ≃ₗ[LaurentPolynomial ℤ]
    TauCeti.LaurentK0 (E.fullSubcategory (E.admitsFiniteResolution P) ⋯ ⋯)

Lean

Formalized in Tau Ceti as TauCeti.GradedExactStructure.laurentResolutionEquiv.

Other forms

The graded resolution theorem for a resolving subcategory. Formalized in Tau Ceti as TauCeti.GradedExactStructure.IsResolving.laurentResolutionEquiv.

TauCeti.GradedExactStructure.IsResolving.laurentResolutionEquiv.{w, v, u} {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C]
  [CategoryTheory.EssentiallySmall.{w, v, u} C] (E : TauCeti.GradedExactStructure C)
  (P : CategoryTheory.ObjectProperty C) [E.IsResolving P]
  (hshift : P.inverseImage E.shift.functor = P) :
  TauCeti.LaurentK0 (E.fullSubcategory P ⋯ hshift) ≃ₗ[LaurentPolynomial ℤ] TauCeti.LaurentK0 E

Sources

• Tau Ceti documentation: TauCeti.GradedExactStructure.laurentResolutionEquiv
• Source of TauCeti.GradedExactStructure.laurentResolutionEquiv in TauCeti/CategoryTheory/GrothendieckGroup/Laurent/Resolution.lean

LeanTauCeti.GradedExactStructure.laurentResolutionEquiv · TauCeti.GradedExactStructure.IsResolving.laurentResolutionEquiv

Uses 4 · Used by 1

Statement usesThe resolution theorem · The resolution theorem for finite projective resolutions

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

Used byTauCeti.gradedCartanEquiv

DefinitionThe resolution theorem for finite projective resolutions#

When every object satisfying P is E-projective, the inclusion of the full subcategory on P into the full subcategory of objects admitting a finite P-resolution 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.resolutionEquiv_symm_of.

TauCeti.ExactStructure.resolutionEquiv.{w, v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.LocallySmall.{w, v, u} C]
  {E : TauCeti.ExactStructure C} {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [P.ContainsZero]
  [P.IsClosedUnderBinaryProducts] (hproj : P ≤ E.isProjective)
  [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (E.admitsFiniteResolution P)] :
  TauCeti.ExactK0 (TauCeti.ExactStructure.fullSubcategory P ⋯) ≃+
    TauCeti.ExactK0 (TauCeti.ExactStructure.fullSubcategory (E.admitsFiniteResolution P) ⋯)

Lean

Formalized in Tau Ceti as TauCeti.ExactStructure.resolutionEquiv.

Sources

• Tau Ceti documentation: TauCeti.ExactStructure.resolutionEquiv
• Source of TauCeti.ExactStructure.resolutionEquiv in TauCeti/CategoryTheory/GrothendieckGroup/ProjectiveResolution.lean

LeanTauCeti.ExactStructure.resolutionEquiv

Uses 3 · Used by 4

Proof usesThe dual Noether isomorphism · The Noether isomorphism for exact categories · Schanuel's lemma

Used byThe resolution theorem for modules · The resolution theorem for modules admitting finite resolutions by finitely generated projectives · TauCeti.gradedCartanEquiv · The graded resolution theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.