The abelian category of mixed Hodge structures

Mixed Hodge structures form an abelian category. The finite products supplied by Mixed.Prod, together with the existing kernels, cokernels and invertible coimage–image comparisons, give the abelian structure by CategoryTheory.Abelian.ofCoimageImageComparisonIsIso.

References

Deligne, Théorie de Hodge II, 2.3.5; Peters–Steenbrink, Mixed Hodge Structures, Ch. 3.

@[instance_reducible]

noncomputable instance TauCeti.Hodge.MixedHodgeStructureCat.abelian : CategoryTheory.Abelian MixedHodgeStructureCat

Mixed Hodge structures, with rational Hodge morphisms, form an abelian category.