Transport and exactness lemmas for Ext groups

This file collects general Ext API that Mathlib does not state in this form:

• the transport of Extⁿ(X, Y) along isomorphisms X ≅ X' and Y ≅ Y', additively as TauCeti.extAddEquivOfIso and R-linearly as TauCeti.extLinearEquivOfIso;
• the vanishing of Extⁿ(X, Y) when either of the two objects is a zero object;
• short exact cokernel sequences, the cokernel sequence of the chosen embedding into an injective object, and a dimension-shift criterion for vanishing of the next Ext group;
• Mathlib's long exact Ext sequences of a short exact sequence S, repackaged as Function.Exact statements about the composition maps: TauCeti.exact_postcomp and TauCeti.exact_precomp for CategoryTheory.Abelian.Ext.postcomp and CategoryTheory.Abelian.Ext.precomp, and TauCeti.exact_postcompOfLinear and TauCeti.exact_precompOfLinear for their R-linear forms; TauCeti.exact_precomp₃ and TauCeti.exact_precompOfLinear₃ are the same repackaging one step further along the contravariant sequence, where the incoming map is precomposition with the extension class.

The exactness statements are CategoryTheory.Abelian.Ext.covariant_sequence_exact₂ and CategoryTheory.Abelian.Ext.contravariant_sequence_exact₂ with the vanishing of the composite supplied, which is what makes them usable with the Function.Exact API.

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 and its long exact sequences.

Transport along isomorphisms

noncomputable def TauCeti.extAddEquivOfIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X X' Y Y' : C} (e : X ≅ X') (f : Y ≅ Y') (n : ℕ) : CategoryTheory.Abelian.Ext X Y n ≃+ CategoryTheory.Abelian.Ext X' Y' n

Isomorphisms e : X ≅ X' and f : Y ≅ Y' induce an isomorphism Extⁿ(X, Y) ≃ Extⁿ(X', Y'), by composing with e.inv on the left and with f.hom on the right. This is the action of an isomorphism through CategoryTheory.Abelian.extFunctor, spelled out so that TauCeti.extLinearEquivOfIso can refine it to an R-linear equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.extAddEquivOfIso_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X X' Y Y' : C} (e : X ≅ X') (f : Y ≅ Y') (n : ℕ) (x : CategoryTheory.Abelian.Ext X Y n) : (extAddEquivOfIso e f n) x = (CategoryTheory.Abelian.Ext.mk₀ e.inv).comp (x.comp (CategoryTheory.Abelian.Ext.mk₀ f.hom) ⋯) ⋯

TauCeti.extAddEquivOfIso composes with e.inv and f.hom.

noncomputable def TauCeti.extLinearEquivOfIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X X' Y Y' : C} (R : Type t) [Ring R] [CategoryTheory.Linear R C] (e : X ≅ X') (f : Y ≅ Y') (n : ℕ) : CategoryTheory.Abelian.Ext X Y n ≃ₗ[R] CategoryTheory.Abelian.Ext X' Y' n

The R-linear refinement of TauCeti.extAddEquivOfIso: in an R-linear abelian category, isomorphisms X ≅ X' and Y ≅ Y' identify Extⁿ(X, Y) and Extⁿ(X', Y') as R-modules.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.extLinearEquivOfIso_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X X' Y Y' : C} (R : Type t) [Ring R] [CategoryTheory.Linear R C] (e : X ≅ X') (f : Y ≅ Y') (n : ℕ) (x : CategoryTheory.Abelian.Ext X Y n) : (extLinearEquivOfIso R e f n) x = (CategoryTheory.Abelian.Ext.mk₀ e.inv).comp (x.comp (CategoryTheory.Abelian.Ext.mk₀ f.hom) ⋯) ⋯

TauCeti.extLinearEquivOfIso composes with e.inv and f.hom.

Vanishing against a zero object

theorem TauCeti.subsingleton_ext_of_isZero_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X : C} (hX : CategoryTheory.Limits.IsZero X) (Y : C) (n : ℕ) : Subsingleton (CategoryTheory.Abelian.Ext X Y n)

There is no Ext out of a zero object, in any degree.

theorem TauCeti.subsingleton_ext_of_isZero_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {Y : C} (X : C) (hY : CategoryTheory.Limits.IsZero Y) (n : ℕ) : Subsingleton (CategoryTheory.Abelian.Ext X Y n)

There is no Ext into a zero object, in any degree.

Dimension shifting along an injective embedding

instance TauCeti.injective_cokernelSequence_X₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Injective Y] : CategoryTheory.Injective (CategoryTheory.ShortComplex.cokernelSequence f).X₂

The middle object in a cokernel sequence is injective when the target of its first map is.

theorem TauCeti.subsingleton_ext_succ_of_comp_extClass_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) [CategoryTheory.Injective S.X₂] (X : C) (n : ℕ) (hzero : ∀ (x₃ : CategoryTheory.Abelian.Ext X S.X₃ n), x₃.comp hS.extClass ⋯ = 0) : Subsingleton (CategoryTheory.Abelian.Ext X S.X₁ (n + 1))

A dimension-shift criterion along a short exact sequence with injective middle term: if composition with its extension class vanishes, then the next Ext group is subsingleton.

@[reducible, inline]

noncomputable abbrev TauCeti.injectiveCokernelSequence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (Y : C) : CategoryTheory.ShortComplex C

The cokernel sequence of the chosen embedding of an object into an injective object.

Equations

• TauCeti.injectiveCokernelSequence Y = CategoryTheory.ShortComplex.cokernelSequence (CategoryTheory.Injective.ι Y)

theorem TauCeti.injectiveCokernelSequence_shortExact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (Y : C) : (injectiveCokernelSequence Y).ShortExact

The cokernel sequence of the chosen embedding into an injective object is short exact.

theorem TauCeti.subsingleton_ext_succ_of_injectiveCokernelSequence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] [CategoryTheory.EnoughInjectives C] (X Y : C) (n : ℕ) (hzero : ∀ (x₃ : CategoryTheory.Abelian.Ext X (injectiveCokernelSequence Y).X₃ n), x₃.comp ⋯.extClass ⋯ = 0) : Subsingleton (CategoryTheory.Abelian.Ext X Y (n + 1))

The dimension-shift criterion specialised to the chosen embedding into an injective object.

The long exact sequences as Function.Exact statements

theorem TauCeti.exact_postcomp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (X : C) (n : ℕ) : Function.Exact ⇑((CategoryTheory.Abelian.Ext.mk₀ S.f).postcomp X ⋯) ⇑((CategoryTheory.Abelian.Ext.mk₀ S.g).postcomp X ⋯)

Exactness of Extⁿ(X, S.X₁) → Extⁿ(X, S.X₂) → Extⁿ(X, S.X₃) at the middle term, for a short exact sequence S. This is CategoryTheory.Abelian.Ext.covariant_sequence_exact₂ packaged as a Function.Exact statement about the postcomposition maps.

theorem TauCeti.exact_precomp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) (n : ℕ) : Function.Exact ⇑((CategoryTheory.Abelian.Ext.mk₀ S.g).precomp Y ⋯) ⇑((CategoryTheory.Abelian.Ext.mk₀ S.f).precomp Y ⋯)

Exactness of Extⁿ(S.X₃, Y) → Extⁿ(S.X₂, Y) → Extⁿ(S.X₁, Y) at the middle term, for a short exact sequence S. This is CategoryTheory.Abelian.Ext.contravariant_sequence_exact₂ packaged as a Function.Exact statement about the precomposition maps.

@[simp]

theorem TauCeti.coe_postcompOfLinear {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (R : Type t) [CommRing R] [CategoryTheory.Linear R C] {Y Z : C} {n a b : ℕ} (beta : CategoryTheory.Abelian.Ext Y Z n) (X : C) (h : a + n = b) : ⇑(beta.postcompOfLinear R X h) = ⇑(beta.postcomp X h)

The linear postcomposition map has CategoryTheory.Abelian.Ext.postcomp as its underlying function.

@[simp]

theorem TauCeti.coe_precompOfLinear {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (R : Type t) [CommRing R] [CategoryTheory.Linear R C] {X Y : C} {n a b : ℕ} (alpha : CategoryTheory.Abelian.Ext X Y n) (Z : C) (h : n + a = b) : ⇑(alpha.precompOfLinear R Z h) = ⇑(alpha.precomp Z h)

The linear precomposition map has CategoryTheory.Abelian.Ext.precomp as its underlying function.

theorem TauCeti.exact_postcompOfLinear {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (R : Type t) [CommRing R] [CategoryTheory.Linear R C] (hS : S.ShortExact) (X : C) (n : ℕ) : Function.Exact ⇑((CategoryTheory.Abelian.Ext.mk₀ S.f).postcompOfLinear R X ⋯) ⇑((CategoryTheory.Abelian.Ext.mk₀ S.g).postcompOfLinear R X ⋯)

The R-linear form of TauCeti.exact_postcomp.

theorem TauCeti.exact_precompOfLinear {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (R : Type t) [CommRing R] [CategoryTheory.Linear R C] (hS : S.ShortExact) (Y : C) (n : ℕ) : Function.Exact ⇑((CategoryTheory.Abelian.Ext.mk₀ S.g).precompOfLinear R Y ⋯) ⇑((CategoryTheory.Abelian.Ext.mk₀ S.f).precompOfLinear R Y ⋯)

The R-linear form of TauCeti.exact_precomp.

theorem TauCeti.exact_precomp₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) : Function.Exact ⇑(hS.extClass.precomp Y h) ⇑((CategoryTheory.Abelian.Ext.mk₀ S.g).precomp Y ⋯)

Exactness of Extⁿ⁰(S.X₁, Y) → Extⁿ¹(S.X₃, Y) → Extⁿ¹(S.X₂, Y) at the middle term, for a short exact sequence S and n₁ = 1 + n₀. The first map is precomposition with the extension class of S. This is CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃' with its AddCommGrpCat wrapper removed.

theorem TauCeti.exact_precompOfLinear₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (R : Type t) [CommRing R] [CategoryTheory.Linear R C] (hS : S.ShortExact) (Y : C) (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) : Function.Exact ⇑(hS.extClass.precompOfLinear R Y h) ⇑((CategoryTheory.Abelian.Ext.mk₀ S.g).precompOfLinear R Y ⋯)

The R-linear form of TauCeti.exact_precomp₃.