Documentation

TauCeti.Algebra.Homology.EulerCharacteristic.ExtEuler.Resolution

The Ext-Euler characteristic from a finite projective resolution #

Let C be a k-linear abelian category. A finite projective resolution

0 ⟶ Pₙ ⟶ ⋯ ⟶ P₁ ⟶ P₀ ⟶ X ⟶ 0

computes the Ext-Euler characteristic against Y as the alternating Hom dimension

χ(X, Y) = ∑ i, (-1)ⁱ dimₖ Hom(Pᵢ, Y).

The hypotheses are conditions on the object property P along which the resolution is taken: every object satisfying P is projective and has a finite-dimensional Hom space into Y. Projectivity makes the higher Ext groups of the resolving terms vanish, and bounds the projective dimension of X by the length of the resolution. The long exact Ext sequence then proves, from the far end of the resolution towards X, both that (X, Y) is Euler-admissible and that the displayed formula holds.

Main definitions #

Main results #

References #

Alternating Hom dimension of a finite resolution #

source
noncomputable def TauCeti.ExactStructure.FiniteResolution.homEuler {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} (k : Type t) [Field k] [CategoryTheory.Linear k C] (Y : C) {X : C} (r : E.FiniteResolution P X) :
ℤ

The alternating Hom dimension of a finite resolution against Y: dim Hom(P₀,Y) - dim Hom(P₁,Y) + ⋯ + (-1)ⁿ dim Hom(Pₙ,Y).

As with TauCeti.truncatedExtEuler, this definition is total: Module.finrank has its usual zero fallback when a Hom space is not finite-dimensional. The theorems below assume Hom-finiteness, so every summand there is an actual dimension.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.ExactStructure.FiniteResolution.homEuler_base {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X Y : C} (hX : P X) :
    homEuler k Y (base hX) = ↑(Module.finrank k (X ⟶ Y))

    A length-zero resolution has Hom-Euler characteristic equal to its Hom dimension.

    source
    @[simp]
    theorem TauCeti.ExactStructure.FiniteResolution.homEuler_step {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X Y K Q : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) :
    homEuler k Y (step hQ i p zero hp r) = ↑(Module.finrank k (Q ⟶ Y)) - homEuler k Y r

    Prepending a resolving term subtracts the Hom-Euler characteristic of the remaining resolution from the Hom dimension of that term.

    Euler-admissibility along a projective resolution #

    source
    theorem TauCeti.ExactStructure.FiniteResolution.hasProjectiveDimensionLT {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CategoryTheory.ObjectProperty C} {X : C} (r : (abelian C).FiniteResolution P X) (hproj : P ≤ (abelian C).isProjective) :
    CategoryTheory.HasProjectiveDimensionLT X (r.length + 1)

    A finite resolution by projectives bounds the projective dimension of the resolved object by its length: the resolving terms have projective dimension < 1, and each conflation of the chain raises the bound by one through CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃.

    source
    theorem TauCeti.ExactStructure.FiniteResolution.isExtBoundedBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {P : CategoryTheory.ObjectProperty C} {X Y : C} (r : (abelian C).FiniteResolution P X) (hproj : P ≤ (abelian C).isProjective) :
    IsExtBoundedBy X Y (r.length + 1)

    The Ext groups out of an object with a finite projective resolution vanish from degree r.length + 1 on. Only projectivity of the P-objects is used; no Hom-finiteness is needed.

    source
    theorem TauCeti.ExactStructure.FiniteResolution.isExtFinite {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {P : CategoryTheory.ObjectProperty C} {X Y : C} (r : (abelian C).FiniteResolution P X) (hfinite : ∀ (Z : C), P Z → IsExtFinite k Z Y) :
    IsExtFinite k X Y

    Ext-finiteness propagates along a finite resolution: if every P-object has finite-dimensional Ext groups into Y, then so does the resolved object. Projectivity plays no role here; the projective case is the one used by TauCeti.ExactStructure.FiniteResolution.isEulerAdmissible.

    source
    theorem TauCeti.ExactStructure.FiniteResolution.isEulerAdmissible {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {P : CategoryTheory.ObjectProperty C} {X Y : C} (r : (abelian C).FiniteResolution P X) (hproj : P ≤ (abelian C).isProjective) (hHom : ∀ (Z : C), P Z → FiniteDimensional k (Z ⟶ Y)) :
    IsEulerAdmissible k X Y

    A finite resolution along an object property whose objects are projective and have finite-dimensional Hom spaces into Y makes the resolved pair (X,Y) Euler-admissible.

    source
    theorem TauCeti.ExactStructure.FiniteResolution.extEuler_eq_homEuler {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {P : CategoryTheory.ObjectProperty C} {X Y : C} (r : (abelian C).FiniteResolution P X) (hproj : P ≤ (abelian C).isProjective) (hHom : ∀ (Z : C), P Z → FiniteDimensional k (Z ⟶ Y)) :
    extEuler k ⋯ = homEuler k Y r

    Finite-projective-resolution formula for the Ext-Euler characteristic. The value of χ(X,Y) is the alternating sum of the dimensions of Hom(Pᵢ,Y) along any finite P-resolution of X, provided the P-objects are projective and those Hom spaces are finite-dimensional.

    source
    theorem TauCeti.ExactStructure.FiniteResolution.homEuler_eq_homEuler {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {P : CategoryTheory.ObjectProperty C} {X Y : C} {P' : CategoryTheory.ObjectProperty C} (r : (abelian C).FiniteResolution P X) (s : (abelian C).FiniteResolution P' X) (hproj : P ≤ (abelian C).isProjective) (hHom : ∀ (Z : C), P Z → FiniteDimensional k (Z ⟶ Y)) (hproj' : P' ≤ (abelian C).isProjective) (hHom' : ∀ (Z : C), P' Z → FiniteDimensional k (Z ⟶ Y)) :
    homEuler k Y r = homEuler k Y s

    The alternating Hom dimension is the same along any two finite resolutions of X taken along object properties whose objects are projective and have finite-dimensional Hom spaces into Y.