Hom cocycles compute Ext¹

For f : P₁ → P₀ with P₀ projective, maps P₁ → N killing ker f, modulo maps extending across f, compute Ext¹(P₀ / range f,N). No injectivity of f, projectivity of P₁, or minimality is required.

The comparison descends cocycles to range f, then applies TauCeti.homCokernelEquivExt to the short exact sequence 0 → range f → P₀ → P₀ / range f → 0. This connects the cocycle form of the Auslander–Reiten pairing to the usual extension group. Precomposition by a square of presentations agrees with pullback along its induced cokernel map; postcomposition agrees with pushforward in the coefficients.

References

• M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), Section IV.2.

noncomputable def LinearMap.homCocycleQuotientEquivExt {k : Type u} {A : Type v} [CommRing k] [Ring A] [Algebra k A] {P₀ P₁ : Type (max u v w)} [AddCommGroup P₀] [Module A P₀] [Module.Projective A P₀] [AddCommGroup P₁] [Module A P₁] (f : P₁ →ₗ[A] P₀) (N : ModuleCat A) : f.HomCocycleQuotient ↑N ≃ₗ[k] CategoryTheory.Abelian.Ext (↧(P₀ ⧸ f.range)) N 1

Hom cocycles modulo coboundaries compute the first extension group of the cokernel of f, provided its middle term is projective.

@[simp]

theorem LinearMap.homCocycleQuotientEquivExt_mk {k : Type u} {A : Type v} [CommRing k] [Ring A] [Algebra k A] {P₀ P₁ : Type (max u v w)} [AddCommGroup P₀] [Module A P₀] [Module.Projective A P₀] [AddCommGroup P₁] [Module A P₁] (f : P₁ →ₗ[A] P₀) (N : ModuleCat A) (h : ↥f.range →ₗ[A] ↑N) : (f.homCocycleQuotientEquivExt N) (Submodule.Quotient.mk (f.rangeHomEquivCocycles h)) = ⋯.extClass.comp (CategoryTheory.Abelian.Ext.mk₀ (ModuleCat.ofHom h)) ⋯

A map on the image represents the pushout of the image short exact sequence.

@[simp]

theorem LinearMap.homCocycleQuotientEquivExt_symm_comp_mk₀ {k : Type u} {A : Type v} [CommRing k] [Ring A] [Algebra k A] {P₀ P₁ : Type (max u v w)} [AddCommGroup P₀] [Module A P₀] [Module.Projective A P₀] [AddCommGroup P₁] [Module A P₁] (f : P₁ →ₗ[A] P₀) (N : ModuleCat A) (h : ↥f.range →ₗ[A] ↑N) : (f.homCocycleQuotientEquivExt N).symm (⋯.extClass.comp (CategoryTheory.Abelian.Ext.mk₀ (ModuleCat.ofHom h)) ⋯) = Submodule.Quotient.mk (f.rangeHomEquivCocycles h)

The inverse comparison represents a pushout extension by its Hom cocycle.

@[simp]

theorem LinearMap.homCocycleQuotientEquivExt_naturality {k : Type u} {A : Type v} [CommRing k] [Ring A] [Algebra k A] {P₀ P₁ : Type (max u v w)} [AddCommGroup P₀] [Module A P₀] [Module.Projective A P₀] [AddCommGroup P₁] [Module A P₁] (f : P₁ →ₗ[A] P₀) {N N' : ModuleCat A} (g : N ⟶ N') (x : f.HomCocycleQuotient ↑N) : (f.homCocycleQuotientEquivExt N') ((f.homCocycleQuotientMap (ModuleCat.Hom.hom g)) x) = ((f.homCocycleQuotientEquivExt N) x).comp (CategoryTheory.Abelian.Ext.mk₀ g) ⋯

Postcomposition on cocycle classes agrees with pushforward on extension classes.

theorem LinearMap.homCocycleQuotientEquivExt_precomp {k : Type u} {A : Type v} [CommRing k] [Ring A] [Algebra k A] {P₀ P₁ : Type (max u v w)} [AddCommGroup P₀] [Module A P₀] [Module.Projective A P₀] [AddCommGroup P₁] [Module A P₁] {Q₀ Q₁ : Type (max u v w)} [AddCommGroup Q₀] [Module A Q₀] [Module.Projective A Q₀] [AddCommGroup Q₁] [Module A Q₁] {p : P₁ →ₗ[A] P₀} {q : Q₁ →ₗ[A] Q₀} (f₀ : P₀ →ₗ[A] Q₀) (f₁ : P₁ →ₗ[A] Q₁) (hf : f₀ ∘ₗ p = q ∘ₗ f₁) (g : P₀ ⧸ p.range →ₗ[A] Q₀ ⧸ q.range) (hg : g ∘ₗ p.range.mkQ = q.range.mkQ ∘ₗ f₀) (N : ModuleCat A) (x : q.HomCocycleQuotient ↑N) : (p.homCocycleQuotientEquivExt N) ((homCocycleQuotientPrecomp f₀ f₁ hf) x) = (CategoryTheory.Abelian.Ext.mk₀ (ModuleCat.ofHom g)).comp ((q.homCocycleQuotientEquivExt N) x) ⋯

Precomposition by a presentation square computes pullback of extension classes along its induced cokernel map.

theorem LinearMap.finiteDimensional_ext_cokernel {A : Type v} [Ring A] {P₀ P₁ : Type (max u v w)} [AddCommGroup P₀] [Module A P₀] [Module.Projective A P₀] [AddCommGroup P₁] [Module A P₁] {K : Type u} [Field K] [Algebra K A] [Module K P₁] [IsScalarTower K A P₁] [Module.Finite K P₁] (f : P₁ →ₗ[A] P₀) (N : ModuleCat A) [Module.Finite K ↑N] : Module.Finite K (CategoryTheory.Abelian.Ext (↧(P₀ ⧸ f.range)) N 1)

The first extension group of a cokernel is finite-dimensional when its presenting source and the coefficient module are finite-dimensional. The presenting arrow need not be injective, and its source need not be projective.