Kernels and cokernels of mixed Hodge structures

The category of mixed Hodge structures has kernels and cokernels, and both are computed on the underlying rational vector spaces; rational realization preserves both constructions. The kernel of a morphism f is the mixed Hodge structure induced on its rational kernel, and its cokernel is the quotient of the target by its rational image. Both constructions are available because the kernel and the image are sub-mixed Hodge structures: this is where the Deligne bigrading, through the functoriality of its pieces, enters the categorical structure.

Consequently a morphism of mixed Hodge structures is a monomorphism exactly when its rational map is injective, and an epimorphism exactly when its rational map is surjective.

Main declarations

• TauCeti.Hodge.MixedHodgeStructureCat.kernelCone: the kernel fork given by the inclusion of the induced structure on the rational kernel.
• TauCeti.Hodge.MixedHodgeStructureCat.kernelIsLimit: this fork is a limit.
• TauCeti.Hodge.MixedHodgeStructureCat.cokernelCocone: the cokernel cofork given by the projection onto the quotient by the rational image.
• TauCeti.Hodge.MixedHodgeStructureCat.cokernelIsColimit: this cofork is a colimit.
• TauCeti.Hodge.MixedHodgeStructureCat.mono_iff_injective, TauCeti.Hodge.MixedHodgeStructureCat.epi_iff_surjective: monomorphisms and epimorphisms are detected on rational maps.

References

Deligne, Théorie de Hodge II, §2.3; Peters–Steenbrink, Mixed Hodge Structures, Chapter 3.

The kernel and cokernel constructions adapt the corresponding formalization in Mathlib.Algebra.Category.ModuleCat.Kernels, by Markus Himmel.

noncomputable def TauCeti.Hodge.MixedHodgeStructureCat.kernelCone {X Y : MixedHodgeStructureCat} (f : X ⟶ Y) : CategoryTheory.Limits.KernelFork f

The kernel fork of a morphism of mixed Hodge structures: the inclusion of the mixed Hodge structure induced on the kernel of its rational map.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructureCat.kernelCone_pt {X Y : MixedHodgeStructureCat} (f : X ⟶ Y) : (kernelCone f).pt = of ⋯ ⋯ ⋯.hodgeStructure

The point of the kernel fork is the structure induced on the rational kernel.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructureCat.kernelCone_ι {X Y : MixedHodgeStructureCat} (f : X ⟶ Y) : CategoryTheory.Limits.Fork.ι (kernelCone f) = ⋯.inclusion

The kernel inclusion is the inclusion of the structure induced on the rational kernel.

noncomputable def TauCeti.Hodge.MixedHodgeStructureCat.kernelIsLimit {X Y : MixedHodgeStructureCat} (f : X ⟶ Y) : CategoryTheory.Limits.IsLimit (kernelCone f)

The inclusion of the induced structure on the rational kernel is a kernel.

noncomputable def TauCeti.Hodge.MixedHodgeStructureCat.cokernelCocone {X Y : MixedHodgeStructureCat} (f : X ⟶ Y) : CategoryTheory.Limits.CokernelCofork f

The cokernel cofork of a morphism of mixed Hodge structures: the projection onto the quotient of the target by the image of its rational map.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructureCat.cokernelCocone_pt {X Y : MixedHodgeStructureCat} (f : X ⟶ Y) : (cokernelCocone f).pt = of ⋯ ⋯ ⋯.quotient

The point of the cokernel cofork is the quotient by the rational image.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructureCat.cokernelCocone_π {X Y : MixedHodgeStructureCat} (f : X ⟶ Y) : CategoryTheory.Limits.Cofork.π (cokernelCocone f) = ⋯.projection

The cokernel projection is the projection onto the quotient by the rational image.

noncomputable def TauCeti.Hodge.MixedHodgeStructureCat.cokernelIsColimit {X Y : MixedHodgeStructureCat} (f : X ⟶ Y) : CategoryTheory.Limits.IsColimit (cokernelCocone f)

The projection onto the quotient by the rational image is a cokernel.

instance TauCeti.Hodge.MixedHodgeStructureCat.instHasKernels : CategoryTheory.Limits.HasKernels MixedHodgeStructureCat

The category of mixed Hodge structures has kernels.

instance TauCeti.Hodge.MixedHodgeStructureCat.instHasCokernels : CategoryTheory.Limits.HasCokernels MixedHodgeStructureCat

The category of mixed Hodge structures has cokernels.

instance TauCeti.Hodge.MixedHodgeStructureCat.rational_preservesKernel {X Y : MixedHodgeStructureCat} (f : X ⟶ Y) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) rational

Rational realization preserves kernels of mixed Hodge morphisms.

instance TauCeti.Hodge.MixedHodgeStructureCat.rational_preservesCokernel {X Y : MixedHodgeStructureCat} (f : X ⟶ Y) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) rational

Rational realization preserves cokernels of mixed Hodge morphisms.

theorem TauCeti.Hodge.MixedHodgeStructureCat.mono_iff_injective {X Y : MixedHodgeStructureCat} {f : X ⟶ Y} : CategoryTheory.Mono f ↔ Function.Injective ⇑f.toRatLinearMap

A morphism of mixed Hodge structures is a monomorphism if and only if its rational map is injective.

theorem TauCeti.Hodge.MixedHodgeStructureCat.epi_iff_surjective {X Y : MixedHodgeStructureCat} {f : X ⟶ Y} : CategoryTheory.Epi f ↔ Function.Surjective ⇑f.toRatLinearMap

A morphism of mixed Hodge structures is an epimorphism if and only if its rational map is surjective.