Naturality of the Ext-Euler characteristic under exact functors #

Let F : C ⥤ D be an exact k-linear functor between k-linear abelian categories. It induces k-linear maps Extⁿ(X, Y) → Extⁿ(F X, F Y) (Mathlib's CategoryTheory.Functor.mapExtAddHom and CategoryTheory.Functor.mapExtLinearMap). This file proves that the finiteness data behind the Ext-Euler characteristic, and the characteristic itself, are carried along F whenever these maps are bijective:

χ(F X, F Y) = χ(X, Y).

The two finiteness conditions travel in opposite directions under the weaker one-sided hypotheses: injectivity of the maps on Ext reflects Ext-finiteness and vanishing from D back to C, while surjectivity carries them from C to D.

At the level of Grothendieck groups, if F carries the extension-closed properties P and Q of C into extension-closed properties P' and Q' of D, it restricts to conflation-exact functors between the full subcategories and so induces maps of exact K₀. When F is bijective on the Ext groups of every pair in P × Q, these maps intertwine the two Ext-Euler pairings (TauCeti.extEulerPairing_map_map).

Mathlib supplies the bijectivity hypothesis for a fully faithful exact functor out of a category with enough projectives which preserves projective objects (CategoryTheory.Functor.mapExt_bijective_of_preservesProjectiveObjects), and dually with enough injectives (CategoryTheory.Functor.mapExt_bijective_of_preservesInjectiveObjects). For the forward functor of an additive equivalence it is CategoryTheory.Equivalence.extAddEquiv, whose underlying map is Ext.mapExactFunctor by CategoryTheory.Equivalence.extAddEquiv_apply.

Main results #

TauCeti.IsEulerAdmissible.map and TauCeti.IsEulerAdmissible.of_map: Euler-admissibility is carried along F, respectively reflected by it, under surjectivity, respectively injectivity, of the maps on Ext; TauCeti.IsEulerAdmissibleOn.of_map is the version for object properties.
TauCeti.extEuler_map: χ(F X, F Y) = χ(X, Y) when F is bijective on Ext.
TauCeti.extEulerPairing_map_map: the induced maps of exact K₀ intertwine the Ext-Euler pairings.

References #

Charles A. Weibel, An Introduction to Homological Algebra, Cambridge Studies in Advanced Mathematics 38, Cambridge University Press (1994), Sections 2.4--2.7, for Ext.

Transporting the finiteness conditions #

source

theorem TauCeti.IsExtFinite.of_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {X Y : C} (h : IsExtFinite k (F.obj X) (F.obj Y)) (hF : ∀ (n : ℕ), Function.Injective ⇑(F.mapExtAddHom X Y n)) :

IsExtFinite k X Y

Ext-finiteness is reflected by an exact functor which is injective on Ext.

source

theorem TauCeti.IsExtFinite.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {X Y : C} (h : IsExtFinite k X Y) (hF : ∀ (n : ℕ), Function.Surjective ⇑(F.mapExtAddHom X Y n)) :

IsExtFinite k (F.obj X) (F.obj Y)

Ext-finiteness is carried along an exact functor which is surjective on Ext.

source

theorem TauCeti.IsExtBoundedBy.of_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {X Y : C} {N : ℕ} (h : IsExtBoundedBy (F.obj X) (F.obj Y) N) (hF : ∀ ⦃n : ℕ⦄, N ≤ n → Function.Injective ⇑(F.mapExtAddHom X Y n)) :

IsExtBoundedBy X Y N

A vanishing bound is reflected by an exact functor which is injective on Ext from that degree on.

source

theorem TauCeti.IsExtBoundedBy.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {X Y : C} {N : ℕ} (h : IsExtBoundedBy X Y N) (hF : ∀ ⦃n : ℕ⦄, N ≤ n → Function.Surjective ⇑(F.mapExtAddHom X Y n)) :

IsExtBoundedBy (F.obj X) (F.obj Y) N

A vanishing bound is carried along an exact functor which is surjective on Ext from that degree on.

source

theorem TauCeti.IsExtBounded.of_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {X Y : C} (h : IsExtBounded (F.obj X) (F.obj Y)) (hF : ∀ᶠ (n : ℕ) in Filter.atTop , Function.Injective ⇑(F.mapExtAddHom X Y n)) :

IsExtBounded X Y

Eventual Ext-vanishing is reflected by an exact functor which is injective on Ext in all large degrees.

source

theorem TauCeti.IsExtBounded.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {X Y : C} (h : IsExtBounded X Y) (hF : ∀ᶠ (n : ℕ) in Filter.atTop , Function.Surjective ⇑(F.mapExtAddHom X Y n)) :

IsExtBounded (F.obj X) (F.obj Y)

Eventual Ext-vanishing is carried along an exact functor which is surjective on Ext in all large degrees.

source

theorem TauCeti.IsEulerAdmissible.of_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {X Y : C} (h : IsEulerAdmissible k (F.obj X) (F.obj Y)) (hF : ∀ (n : ℕ), Function.Injective ⇑(F.mapExtAddHom X Y n)) :

IsEulerAdmissible k X Y

Euler-admissibility is reflected by an exact functor which is injective on Ext.

source

theorem TauCeti.IsEulerAdmissible.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {X Y : C} (h : IsEulerAdmissible k X Y) (hF : ∀ (n : ℕ), Function.Surjective ⇑(F.mapExtAddHom X Y n)) :

IsEulerAdmissible k (F.obj X) (F.obj Y)

Euler-admissibility is carried along an exact functor which is surjective on Ext.

source

theorem TauCeti.IsEulerAdmissibleOn.of_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {P Q : CategoryTheory.ObjectProperty C} {P' Q' : CategoryTheory.ObjectProperty D} (h : IsEulerAdmissibleOn k P' Q') (hFP : ∀ ⦃X : C⦄, P X → P' (F.obj X)) (hFQ : ∀ ⦃Y : C⦄, Q Y → Q' (F.obj Y)) (hF : ∀ ⦃X Y : C⦄, P X → Q Y → ∀ (n : ℕ), Function.Injective ⇑(F.mapExtAddHom X Y n)) :

IsEulerAdmissibleOn k P Q

Euler-admissibility on a pair of object properties is reflected by an exact functor carrying them into Euler-admissible properties and injective on the Ext groups between them.