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; precomposition acts contravariantly on the presenting object. A morphism killed by the presenting map defines a restriction out of the quotient. These operations need no 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.

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.

@[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.

def TauCeti.HomCokernel.precomp (R : Type t) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {X P Y W : C} (f : X ⟶ P) (e : W ⟶ X) : HomCokernel R f Y →ₗ[R] HomCokernel R (CategoryTheory.CategoryStruct.comp e f) Y

Precomposition by e on the cokernel of precomposition with f.

@[simp]

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

Precomposition sends the class of h to the class of e ≫ h.

@[simp]

theorem TauCeti.HomCokernel.precomp_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 W : C} (f : X ⟶ P) (e : W ⟶ X) (g : Y ⟶ Z) (x : HomCokernel R f Y) : (precomp R f e) ((map R f g) x) = (map R (CategoryTheory.CategoryStruct.comp e f) g) ((precomp R f e) x)

Precomposition commutes with postcomposition on Hom cokernels.

def TauCeti.HomCokernel.restrict (R : Type t) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {X P Y W : C} (f : X ⟶ P) (e : W ⟶ X) (h : CategoryTheory.CategoryStruct.comp e f = 0) : HomCokernel R f Y →ₗ[R] W ⟶ Y

Restriction of a Hom-cokernel class to a morphism annihilated by the presenting map.

@[simp]

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

Restriction evaluates a representative by precomposition.

@[simp]

theorem TauCeti.HomCokernel.restrict_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 W : C} (f : X ⟶ P) (e : W ⟶ X) (h : CategoryTheory.CategoryStruct.comp e f = 0) (g : Y ⟶ Z) (x : HomCokernel R f Y) : (restrict R f e h) ((map R f g) x) = CategoryTheory.CategoryStruct.comp ((restrict R f e h) x) g

Restriction commutes with postcomposition in the coefficient object.

theorem TauCeti.HomCokernel.precomp_injective (R : Type t) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {X P Y W : C} (f : X ⟶ P) (e : W ⟶ X) [CategoryTheory.Epi e] : Function.Injective ⇑(precomp R f e)

An epimorphism induces an injection on Hom cokernels by precomposition.