Descending Hom cocycles to the image

A map vanishing on the kernel of f : P₁ → P₀ descends uniquely to range f. This identifies Hom cocycles modulo coboundaries with the cokernel of restriction Hom(P₀,N) → Hom(range f,N). In a projective presentation this is the syzygy model of Ext¹, including presentations whose leftmost arrow is not injective.

The descent uses Mathlib's LinearMap.liftOfSurjective. No exactness, projectivity or finiteness assumption is needed.

noncomputable def LinearMap.rangeHomEquivCocycles {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.range →ₗ[A] N) ≃ₗ[k] ↥(lcomp k N f.ker.subtype).ker

Precomposition with the surjection onto range f identifies maps on the image with maps vanishing on ker f.

@[simp]

theorem LinearMap.rangeHomEquivCocycles_apply_val {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₀) (h : ↥f.range →ₗ[A] N) : ↑(f.rangeHomEquivCocycles h) = h ∘ₗ f.rangeRestrict

On a map defined on the image, the cocycle comparison is precomposition.

@[simp]

theorem LinearMap.rangeHomEquivCocycles_symm_apply_rangeRestrict {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₀) (h : ↥(lcomp k N f.ker.subtype).ker) (x : P₁) : (f.rangeHomEquivCocycles.symm h) (f.rangeRestrict x) = ↑h x

Descent evaluates at f x by evaluating the original cocycle at x.

noncomputable def LinearMap.homCocycleQuotientEquivRange {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.HomCocycleQuotient N ≃ₗ[k] (↥f.range →ₗ[A] N) ⧸ (lcomp k N f.range.subtype).range

Hom cocycles modulo coboundaries are maps on the image modulo maps extending to the presenting middle term.

@[simp]

theorem LinearMap.homCocycleQuotientEquivRange_symm_mk {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₀) (h : ↥f.range →ₗ[A] N) : f.homCocycleQuotientEquivRange.symm (Submodule.Quotient.mk h) = Submodule.Quotient.mk (f.rangeHomEquivCocycles h)

The inverse comparison pulls a map on the image back to its cocycle class.

@[simp]

theorem LinearMap.homCocycleQuotientEquivRange_mk {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₀) (h : ↥f.range →ₗ[A] N) : f.homCocycleQuotientEquivRange (Submodule.Quotient.mk (f.rangeHomEquivCocycles h)) = Submodule.Quotient.mk h

A cocycle obtained from a map on the image descends to that map's class.