Detecting monomorphisms and epimorphisms of polarizable Hodge structures

In the category of polarizable rational Hodge structures, a morphism is monic exactly when its rational map is injective, and epic exactly when its rational map is surjective. These criteria allow categorical subobjects to be identified with rational Hodge substructures, and hence allow orthogonal complements to be used to split categorical monomorphisms.

A morphism is an isomorphism exactly when its rational map is bijective. The category is balanced, and the rational realization preserves monomorphisms and epimorphisms and reflects isomorphisms.

References

Voisin, Hodge Theory and Complex Algebraic Geometry I, §7.1.2; Peters--Steenbrink, Mixed Hodge Structures, §2.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.mono_iff_injective {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (f : X ⟶ Y) : CategoryTheory.Mono f ↔ Function.Injective ⇑f.hom.toRatLinearMap

A morphism of polarizable rational Hodge structures is monic exactly when its rational map is injective.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.epi_iff_surjective {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ Function.Surjective ⇑f.hom.toRatLinearMap

A morphism of polarizable rational Hodge structures is epic exactly when its rational map is surjective.

instance TauCeti.Hodge.PolarizableHodgeStructureCat.instPreservesMonomorphismsModuleCatRatRational {n : ℤ} : rational.PreservesMonomorphisms

The rational realization preserves monomorphisms.

instance TauCeti.Hodge.PolarizableHodgeStructureCat.instPreservesEpimorphismsModuleCatRatRational {n : ℤ} : rational.PreservesEpimorphisms

The rational realization preserves epimorphisms.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.isIso_iff_bijective {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ Function.Bijective ⇑f.hom.toRatLinearMap

A morphism of polarizable rational Hodge structures is an isomorphism exactly when its rational map is bijective.

instance TauCeti.Hodge.PolarizableHodgeStructureCat.instReflectsIsomorphismsModuleCatRatRational {n : ℤ} : rational.ReflectsIsomorphisms

The rational realization reflects isomorphisms: a rationally invertible Hodge morphism has an inverse preserving the Hodge filtration.

instance TauCeti.Hodge.PolarizableHodgeStructureCat.instBalanced {n : ℤ} : CategoryTheory.Balanced (PolarizableHodgeStructureCat n)

A morphism of polarizable rational Hodge structures which is both monic and epic is an isomorphism.