Cokernels of precomposition on Hom spaces

For a morphism f : X ⟶ P in a linear category, HomCokernel R f Y is Hom(X, Y) modulo the maps extending across f. In a projective presentation 0 → X → P → M → 0, this quotient computes Ext¹(M, Y).

The quotient uses Mathlib's submodule quotient, so its quotient map, induction principle and universal property are those of Submodule. Postcomposition gives its covariant action on Y, without any abelian or projectivity hypothesis.

@[reducible, inline]

abbrev TauCeti.HomCokernel (R : Type t) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {X P : C} (f : X ⟶ P) (Y : C) : Type v

The cokernel of Hom(P, Y) → Hom(X, Y) given by precomposition with f. It is defined directly as a submodule quotient.

Equations

• TauCeti.HomCokernel R f Y = ((X ⟶ Y) ⧸ (CategoryTheory.Linear.leftComp R Y f).range)

theorem TauCeti.homCokernel_mk_eq_zero_iff (R : Type t) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {X P Y : C} (f : X ⟶ P) (g : X ⟶ Y) : Submodule.Quotient.mk g = 0 ↔ ∃ (h : P ⟶ Y), CategoryTheory.CategoryStruct.comp f h = g

A map represents zero in the Hom cokernel exactly when it extends across f.

def TauCeti.HomCokernel.map (R : Type t) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {X P Y Z : C} (f : X ⟶ P) (g : Y ⟶ Z) : HomCokernel R f Y →ₗ[R] HomCokernel R f Z

Postcomposition on the cokernel of precomposition with f.

Equations

• TauCeti.HomCokernel.map R f g = (CategoryTheory.Linear.leftComp R Y f).range.mapQ (CategoryTheory.Linear.leftComp R Z f).range (CategoryTheory.Linear.rightComp R X g) ⋯

@[simp]

theorem TauCeti.HomCokernel.map_mk (R : Type t) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {X P Y Z : C} (f : X ⟶ P) (g : Y ⟶ Z) (h : X ⟶ Y) : (map R f g) (Submodule.Quotient.mk h) = Submodule.Quotient.mk (CategoryTheory.CategoryStruct.comp h g)

Postcomposition sends the class of h to the class of h ≫ g.

@[simp]

theorem TauCeti.HomCokernel.map_id (R : Type t) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {X P Y : C} (f : X ⟶ P) : map R f (CategoryTheory.CategoryStruct.id Y) = LinearMap.id

Postcomposition with an identity acts as the identity.

@[simp]

theorem TauCeti.HomCokernel.map_comp (R : Type t) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {X P Y Z W : C} (f : X ⟶ P) (g : Y ⟶ Z) (h : Z ⟶ W) : map R f (CategoryTheory.CategoryStruct.comp g h) = map R f h ∘ₗ map R f g

Postcomposition respects composition of morphisms.