Epimorphisms of differences of restrictions for presheaves of abelian groups

Let P be a presheaf of abelian groups on a meet-semilattice X with a greatest element, and let U and V be elements of X. The difference of restrictions P(U) ⊞ P(V) ⟶ P(U ⨯ V) (the second map of the Mayer-Vietoris sequence) is an epimorphism of abelian groups exactly when every element of P(U ⊓ V) is the difference of the restrictions of an element of P(U) and an element of P(V). The categorical product U ⨯ V is the meet U ⊓ V (CategoryTheory.Limits.CompleteLattice.prod_eq_inf), and epimorphisms in AddCommGrpCat are the surjections (AddCommGrpCat.epi_iff_surjective).

Main results

• CategoryTheory.Functor.epi_biprod_desc_map_prod_fst_neg_map_prod_snd_iff_surjective: the difference of restrictions P(U) ⊞ P(V) ⟶ P(U ⨯ V) is an epimorphism if and only if the difference of restrictions P(U) × P(V) → P(U ⊓ V) is surjective.

theorem CategoryTheory.Functor.epi_biprod_desc_map_prod_fst_neg_map_prod_snd_iff_surjective {X : Type u} [SemilatticeInf X] [OrderTop X] (P : Functor Xᵒᵖ AddCommGrpCat) (U V : X) : Epi (Limits.biprod.desc (P.map Limits.prod.fst.op) (-P.map Limits.prod.snd.op)) ↔ Function.Surjective fun (x : ↑(P.obj (Opposite.op U)) × ↑(P.obj (Opposite.op V))) => (ConcreteCategory.hom (P.map (homOfLE ⋯).op)) x.1 - (ConcreteCategory.hom (P.map (homOfLE ⋯).op)) x.2

Surjectivity of a difference of restrictions. For a presheaf P of abelian groups on a meet-semilattice with a greatest element, the map P(U) ⊞ P(V) ⟶ P(U ⨯ V) sending (s, t) to the difference of the restrictions of s and t is an epimorphism exactly when the difference of restrictions P(U) × P(V) → P(U ⊓ V) is surjective.