Hom cocycles modulo coboundaries

For an arrow f : P₁ → P₀, Hom cocycles with coefficients in N are the maps P₁ → N vanishing on ker f. Coboundaries are the maps obtained by precomposition with f. Postcomposition induces a covariant map on their quotient. The quotient map, induction principle and universal property are those of Submodule.

For a projective presentation, the cocycle condition distinguishes the quotient computing Ext¹ from the full Hom cokernel. Its scalar dual is the coefficient side of the Auslander–Reiten pairing. The construction itself needs neither projectivity nor an exactness or finiteness hypothesis.

References

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

@[reducible, inline]

abbrev LinearMap.HomCocycleQuotient {k : Type u_1} {A : Type u_2} {P₀ : Type u_3} {P₁ : Type u_4} [CommRing k] [Ring A] [Algebra k A] [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] (f : P₁ →ₗ[A] P₀) (N : Type u_8) [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] : Type (max u_4 u_8)

Maps vanishing on the kernel of f, modulo maps extending across f.

theorem LinearMap.homCocycleComp_mem {k : Type u_1} {A : Type u_2} {P₀ : Type u_3} {P₁ : Type u_4} {N : Type u_5} {N' : Type u_6} [CommRing k] [Ring A] [Algebra k A] [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] [AddCommGroup N'] [Module A N'] [Module k N'] [IsScalarTower k A N'] {f : P₁ →ₗ[A] P₀} (g : N →ₗ[A] N') {h : P₁ →ₗ[A] N} (hh : h ∈ (lcomp k N f.ker.subtype).ker) : g ∘ₗ h ∈ (lcomp k N' f.ker.subtype).ker

Postcomposition preserves the Hom cocycle condition.

def LinearMap.homCocycleQuotientMap {k : Type u_1} {A : Type u_2} {P₀ : Type u_3} {P₁ : Type u_4} {N : Type u_5} {N' : Type u_6} [CommRing k] [Ring A] [Algebra k A] [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] [AddCommGroup N'] [Module A N'] [Module k N'] [IsScalarTower k A N'] (f : P₁ →ₗ[A] P₀) (g : N →ₗ[A] N') : f.HomCocycleQuotient N →ₗ[k] f.HomCocycleQuotient N'

Postcomposition on Hom cocycles modulo coboundaries.

@[simp]

theorem LinearMap.homCocycleQuotientMap_mk {k : Type u_1} {A : Type u_2} {P₀ : Type u_3} {P₁ : Type u_4} {N : Type u_5} {N' : Type u_6} [CommRing k] [Ring A] [Algebra k A] [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] [AddCommGroup N'] [Module A N'] [Module k N'] [IsScalarTower k A N'] (f : P₁ →ₗ[A] P₀) (g : N →ₗ[A] N') (h : ↥(lcomp k N f.ker.subtype).ker) : (f.homCocycleQuotientMap g) (Submodule.Quotient.mk h) = Submodule.Quotient.mk ⟨g ∘ₗ ↑h, ⋯⟩

Postcomposition sends a cocycle class to the class of the composite.

@[simp]

theorem LinearMap.homCocycleQuotientMap_id {k : Type u_1} {A : Type u_2} {P₀ : Type u_3} {P₁ : Type u_4} {N : Type u_5} [CommRing k] [Ring A] [Algebra k A] [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] (f : P₁ →ₗ[A] P₀) : f.homCocycleQuotientMap id = id

Postcomposition with the identity preserves cocycle classes.

@[simp]

theorem LinearMap.homCocycleQuotientMap_comp {k : Type u_1} {A : Type u_2} {P₀ : Type u_3} {P₁ : Type u_4} {N : Type u_5} {N' : Type u_6} {N'' : Type u_7} [CommRing k] [Ring A] [Algebra k A] [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] [AddCommGroup N'] [Module A N'] [Module k N'] [IsScalarTower k A N'] [AddCommGroup N''] [Module A N''] [Module k N''] [IsScalarTower k A N''] (f : P₁ →ₗ[A] P₀) (g : N →ₗ[A] N') (h : N' →ₗ[A] N'') : f.homCocycleQuotientMap (h ∘ₗ g) = f.homCocycleQuotientMap h ∘ₗ f.homCocycleQuotientMap g

Postcomposition on cocycle classes respects composition.