Ext groups are invariant under an additive equivalence

Mathlib's CategoryTheory.Adjunction.extEquiv promotes an adjunction F ⊣ G between exact functors to an additive equivalence Extⁿ(F X, Y) ≃+ Extⁿ(X, G Y). For an equivalence e this specialises, along CategoryTheory.Equivalence.toAdjunction and the transport of the target along the unit isomorphism from TauCeti.extAddEquivOfIso, to the invariance of Ext under e, which Mathlib does not state in this form. (CategoryTheory.Abelian.Ext.mapExactFunctor is shown bijective only under a projective- or injective-object hypothesis.)

Main definitions

• CategoryTheory.Equivalence.extAddEquiv: Extⁿ(X, Y) ≃+ Extⁿ(e X, e Y) for an additive equivalence e.
• TauCeti.extLinearEquivOfEquivalence: its R-linear refinement for an R-linear equivalence of R-linear abelian categories. R-linearity of e is genuinely needed for the linear statement: an additive isomorphism of k-vector spaces need not preserve dimension.

noncomputable def CategoryTheory.Equivalence.extAddEquiv {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] [HasExt C] [HasExt D] (e : C ≌ D) [e.functor.Additive] (X Y : C) (n : ℕ) : Abelian.Ext X Y n ≃+ Abelian.Ext (e.functor.obj X) (e.functor.obj Y) n

Ext groups are invariant under an additive equivalence. The equivalence e carries Extⁿ(X, Y) isomorphically onto Extⁿ(e X, e Y). This is CategoryTheory.Adjunction.extEquiv for the adjunction e.functor ⊣ e.inverse, with the target transported along the unit isomorphism.

Equations

• e.extAddEquiv X Y n = (TauCeti.extAddEquivOfIso (CategoryTheory.Iso.refl X) (e.unitIso.app Y) n).trans e.toAdjunction.extEquiv.symm

@[simp]

theorem CategoryTheory.Equivalence.extAddEquiv_apply {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] [HasExt C] [HasExt D] (e : C ≌ D) [e.functor.Additive] {X Y : C} {n : ℕ} (α : Abelian.Ext X Y n) : (e.extAddEquiv X Y n) α = Abelian.Ext.mapExactFunctor e.functor α

noncomputable def TauCeti.extLinearEquivOfEquivalence {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] (R : Type t) [Ring R] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear R e.functor] (X Y : C) (n : ℕ) : CategoryTheory.Abelian.Ext X Y n ≃ₗ[R] CategoryTheory.Abelian.Ext (e.functor.obj X) (e.functor.obj Y) n

The R-linear refinement of CategoryTheory.Equivalence.extAddEquiv. For an R-linear equivalence of R-linear abelian categories, Extⁿ(X, Y) and Extⁿ(e X, e Y) are isomorphic as R-modules.

Equations

• TauCeti.extLinearEquivOfEquivalence R e X Y n = { toFun := (e.extAddEquiv X Y n).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (e.extAddEquiv X Y n).invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.extLinearEquivOfEquivalence_apply {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] (R : Type t) [Ring R] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (e : C ≌ D) [e.functor.Additive] [CategoryTheory.Functor.Linear R e.functor] {X Y : C} {n : ℕ} (α : CategoryTheory.Abelian.Ext X Y n) : (extLinearEquivOfEquivalence R e X Y n) α = CategoryTheory.Abelian.Ext.mapExactFunctor e.functor α