Documentation

TauCeti.Algebra.Homology.EulerCharacteristic.ExtEuler.Descent

Additivity and descent of the Ext-Euler characteristic #

This file proves that the Ext-Euler characteristic is additive along a short exact sequence in either variable. The proof cuts the long exact Ext sequence off at a common vanishing bound; the correction term at a truncation is the rank of the next boundary map, and it vanishes at the chosen bound.

For extension-closed object properties P and Q, an Euler-admissibility hypothesis on every pair in P × Q then gives a biadditive pairing between the exact Grothendieck groups of the two full subcategories.

Main results #

References #

Additivity on short exact sequences #

source
theorem TauCeti.extEuler_shortExact₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (X : C) (h₁ : IsEulerAdmissible k X S.X₁) (h₂ : IsEulerAdmissible k X S.X₂) (h₃ : IsEulerAdmissible k X S.X₃) :
extEuler k h₂ = extEuler k h₁ + extEuler k h₃

The Ext-Euler characteristic is additive on a short exact sequence in its second variable.

source
theorem TauCeti.extEuler_shortExact₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) (h₁ : IsEulerAdmissible k S.X₁ Y) (h₂ : IsEulerAdmissible k S.X₂ Y) (h₃ : IsEulerAdmissible k S.X₃ Y) :
extEuler k h₂ = extEuler k h₁ + extEuler k h₃

The Ext-Euler characteristic is additive on a short exact sequence in its first variable.

Descent to exact Grothendieck groups #

source
noncomputable def TauCeti.extEulerRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) (X : P.FullSubcategory) :
ExactK0 (ExactStructure.fullSubcategory Q hQ) →+ ℤ

For a fixed object in P, the Ext-Euler characteristic descends in the second variable to the exact K₀ of the extension-closed full subcategory on Q.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.extEulerRight_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) (X : P.FullSubcategory) (Y : Q.FullSubcategory) :
    (extEulerRight hQ h X) (ExactK0.of Y) = extEuler k ⋯
    source
    noncomputable def TauCeti.extEulerPairing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) :
    ExactK0 (ExactStructure.fullSubcategory P hP) →+ ExactK0 (ExactStructure.fullSubcategory Q hQ) →+ ℤ

    The Ext-Euler pairing on Grothendieck groups. If P and Q are extension-closed additive object properties and every pair in P × Q is Euler-admissible, the object-level Ext-Euler characteristic descends to a map additive in both variables on their exact K₀ groups. The two groups are kept distinct: the pairing need not be symmetric.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.extEulerPairing_of_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) (X : P.FullSubcategory) (Y : Q.FullSubcategory) :
      ((extEulerPairing hP hQ h) (ExactK0.of X)) (ExactK0.of Y) = extEuler k ⋯

      The descended pairing evaluates on object classes as the original Ext-Euler characteristic.

      source
      theorem TauCeti.extEulerPairing_unique {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) (b : ExactK0 (ExactStructure.fullSubcategory P hP) →+ ExactK0 (ExactStructure.fullSubcategory Q hQ) →+ ℤ) (hb : ∀ (X : P.FullSubcategory) (Y : Q.FullSubcategory), (b (ExactK0.of X)) (ExactK0.of Y) = extEuler k ⋯) :
      b = extEulerPairing hP hQ h

      The Ext-Euler pairing is the unique biadditive map with the prescribed values on pairs of object classes.