Computing Ext¹ from a projective presentation

For a short exact sequence S : 0 → P₁ → P₀ → M → 0 with P₀ projective, homCokernelEquivExt identifies the explicit quotient Hom(P₁, Y) / im(Hom(P₀, Y)) with Ext¹(M, Y). The quotient is defined independently of derived categories in TauCeti.CategoryTheory.Linear.HomCokernel. The comparison is natural in Y and identifies the quotients obtained from any two projective presentations of M. No projectivity of P₁ is needed to compute degree one.

Mathlib's extension class defines the connecting morphism in the contravariant long exact Ext sequence. For a projective middle term, this morphism is surjective with kernel the maps extending to that term, giving the quotient identification.

References

• Charles A. Weibel, An Introduction to Homological Algebra, Sections 2.4--2.7.

noncomputable def TauCeti.homBoundary {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (R : Type t) [Ring R] [CategoryTheory.Linear R C] (hS : S.ShortExact) (Y : C) : (S.X₁ ⟶ Y) →ₗ[R] CategoryTheory.Abelian.Ext S.X₃ Y 1

The connecting map Hom(S.X₁, Y) → Ext¹(S.X₃, Y) of a short exact sequence.

Equations

• TauCeti.homBoundary R hS Y = { toFun := fun (f : S.X₁ ⟶ Y) => hS.extClass.comp (CategoryTheory.Abelian.Ext.mk₀ f) TauCeti.homBoundary._proof_1✝, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.homBoundary_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (R : Type t) [Ring R] [CategoryTheory.Linear R C] (hS : S.ShortExact) (Y : C) (f : S.X₁ ⟶ Y) : (homBoundary R hS Y) f = hS.extClass.comp (CategoryTheory.Abelian.Ext.mk₀ f) ⋯

The Hom connecting map pushes the extension class forward along its argument.

theorem TauCeti.ker_homBoundary {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (R : Type t) [Ring R] [CategoryTheory.Linear R C] (hS : S.ShortExact) (Y : C) : (homBoundary R hS Y).ker = (CategoryTheory.Linear.leftComp R Y S.f).range

The kernel of the connecting map consists exactly of maps extending to S.X₂.

theorem TauCeti.homBoundary_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (R : Type t) [Ring R] [CategoryTheory.Linear R C] (hS : S.ShortExact) (Y : C) [CategoryTheory.Projective S.X₂] : Function.Surjective ⇑(homBoundary R hS Y)

If the middle term is projective, every extension class is a Hom boundary.

noncomputable def TauCeti.homCokernelEquivExt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (R : Type t) [Ring R] [CategoryTheory.Linear R C] (hS : S.ShortExact) (Y : C) [CategoryTheory.Projective S.X₂] : HomCokernel R S.f Y ≃ₗ[R] CategoryTheory.Abelian.Ext S.X₃ Y 1

The Hom cokernel of a projective presentation computes Ext¹ as an R-module.

Equations

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

@[simp]

theorem TauCeti.homCokernelEquivExt_mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (R : Type t) [Ring R] [CategoryTheory.Linear R C] (hS : S.ShortExact) (Y : C) [CategoryTheory.Projective S.X₂] (f : S.X₁ ⟶ Y) : (homCokernelEquivExt R hS Y) (Submodule.Quotient.mk f) = hS.extClass.comp (CategoryTheory.Abelian.Ext.mk₀ f) ⋯

The comparison sends the class of a map to the corresponding pushout extension class.

@[simp]

theorem TauCeti.homCokernelEquivExt_symm_comp_mk₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (R : Type t) [Ring R] [CategoryTheory.Linear R C] (hS : S.ShortExact) (Y : C) [CategoryTheory.Projective S.X₂] (f : S.X₁ ⟶ Y) : (homCokernelEquivExt R hS Y).symm (hS.extClass.comp (CategoryTheory.Abelian.Ext.mk₀ f) ⋯) = Submodule.Quotient.mk f

Under the inverse comparison, a pushout extension is represented by its defining map.

@[simp]

theorem TauCeti.homCokernelEquivExt_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (R : Type t) [Ring R] [CategoryTheory.Linear R C] (hS : S.ShortExact) {Y : C} [CategoryTheory.Projective S.X₂] {Z : C} (g : Y ⟶ Z) (x : HomCokernel R S.f Y) : (homCokernelEquivExt R hS Z) ((HomCokernel.map R S.f g) x) = ((homCokernelEquivExt R hS Y) x).comp (CategoryTheory.Abelian.Ext.mk₀ g) ⋯

The Hom-cokernel computation of Ext¹ is natural in the target object.

noncomputable def TauCeti.homCokernelEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S T : CategoryTheory.ShortComplex C} (R : Type t) [Ring R] [CategoryTheory.Linear R C] (hS : S.ShortExact) (Y : C) (hT : T.ShortExact) [CategoryTheory.Projective S.X₂] [CategoryTheory.Projective T.X₂] (e : S.X₃ ≅ T.X₃) : HomCokernel R S.f Y ≃ₗ[R] HomCokernel R T.f Y

Projective presentations of isomorphic objects give canonically equivalent Hom cokernels. The comparison identifies the extension classes represented in the two presentations.

Equations

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

@[simp]

theorem TauCeti.homCokernelEquivExt_homCokernelEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S T : CategoryTheory.ShortComplex C} (R : Type t) [Ring R] [CategoryTheory.Linear R C] (hS : S.ShortExact) (Y : C) (hT : T.ShortExact) [CategoryTheory.Projective S.X₂] [CategoryTheory.Projective T.X₂] (e : S.X₃ ≅ T.X₃) (x : HomCokernel R S.f Y) : (homCokernelEquivExt R hT Y) ((homCokernelEquiv R hS Y hT e) x) = (CategoryTheory.Abelian.Ext.mk₀ e.inv).comp ((homCokernelEquivExt R hS Y) x) ⋯

Comparing presentations preserves their extension classes, after transport along e.

@[simp]

theorem TauCeti.homCokernelEquiv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S T : CategoryTheory.ShortComplex C} (R : Type t) [Ring R] [CategoryTheory.Linear R C] (hS : S.ShortExact) {Y : C} (hT : T.ShortExact) [CategoryTheory.Projective S.X₂] [CategoryTheory.Projective T.X₂] (e : S.X₃ ≅ T.X₃) {Z : C} (g : Y ⟶ Z) (x : HomCokernel R S.f Y) : (homCokernelEquiv R hS Z hT e) ((HomCokernel.map R S.f g) x) = (HomCokernel.map R T.f g) ((homCokernelEquiv R hS Y hT e) x)

Presentation comparisons are natural in the target object.

@[simp]

theorem TauCeti.homCokernelEquiv_refl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (R : Type t) [Ring R] [CategoryTheory.Linear R C] (hS : S.ShortExact) (Y : C) [CategoryTheory.Projective S.X₂] : homCokernelEquiv R hS Y hS (CategoryTheory.Iso.refl S.X₃) = LinearEquiv.refl R (HomCokernel R S.f Y)

Comparing a presentation with itself induces the identity on its Hom cokernel.

@[simp]

theorem TauCeti.homCokernelEquiv_symm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S T : CategoryTheory.ShortComplex C} (R : Type t) [Ring R] [CategoryTheory.Linear R C] (hS : S.ShortExact) (Y : C) (hT : T.ShortExact) [CategoryTheory.Projective S.X₂] [CategoryTheory.Projective T.X₂] (e : S.X₃ ≅ T.X₃) : (homCokernelEquiv R hS Y hT e).symm = homCokernelEquiv R hT Y hS e.symm

Reversing the isomorphism of resolved objects reverses the presentation comparison.

@[simp]

theorem TauCeti.homCokernelEquiv_trans {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S T : CategoryTheory.ShortComplex C} (R : Type t) [Ring R] [CategoryTheory.Linear R C] (hS : S.ShortExact) (Y : C) {U : CategoryTheory.ShortComplex C} (hT : T.ShortExact) (hU : U.ShortExact) [CategoryTheory.Projective S.X₂] [CategoryTheory.Projective T.X₂] [CategoryTheory.Projective U.X₂] (e : S.X₃ ≅ T.X₃) (f : T.X₃ ≅ U.X₃) : homCokernelEquiv R hS Y hT e ≪≫ₗ homCokernelEquiv R hT Y hU f = homCokernelEquiv R hS Y hU (e ≪≫ f)

Presentation comparisons compose according to the isomorphisms of resolved objects.