Coimages and images of mixed Hodge morphisms

The canonical map from the coimage of a mixed Hodge morphism to its image is an isomorphism. Thus the quotient by the kernel agrees, as a mixed Hodge structure, with the image carrying the induced filtrations. This is the first isomorphism theorem for mixed Hodge structures, and supplies the coimage–image condition in the characterization of an abelian category.

Rational realization preserves kernels and cokernels and reflects isomorphisms by strictness. Mathlib's CategoryTheory.Abelian.PreservesCoimageImageComparison.iso therefore reduces the comparison to the first isomorphism theorem for rational vector spaces.

References

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

instance TauCeti.Hodge.MixedHodgeStructureCat.isIso_coimageImageComparison {X Y : MixedHodgeStructureCat} (f : X ⟶ Y) : CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)

The canonical coimage-to-image map of a mixed Hodge morphism is an isomorphism.