Isomorphisms of mixed Hodge structures

A morphism in the category of mixed Hodge structures is an isomorphism exactly when its underlying rational map is bijective. This is Deligne's strictness: the inverse of a bijective morphism preserves both filtrations (TauCeti.Hodge.MixedHodgeStructure.Hom.invOfBijective), so the rational realization reflects isomorphisms.

Main declarations

• TauCeti.Hodge.MixedHodgeStructureCat.isIso_iff_bijective: isomorphisms are detected rationally.
• the instance ReflectsIsomorphisms TauCeti.Hodge.MixedHodgeStructureCat.rational: the rational realization reflects isomorphisms.

References

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

theorem TauCeti.Hodge.MixedHodgeStructureCat.isIso_of_bijective {X Y : MixedHodgeStructureCat} (f : X ⟶ Y) (hf : Function.Bijective ⇑f.toRatLinearMap) : CategoryTheory.IsIso f

A bijective morphism of mixed Hodge structures is an isomorphism. Its inverse is a morphism of mixed Hodge structures by strictness.

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

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

instance TauCeti.Hodge.MixedHodgeStructureCat.instReflectsIsomorphismsModuleCatRatRational : rational.ReflectsIsomorphisms

The rational realization reflects isomorphisms: a morphism of mixed Hodge structures whose rational map is invertible is itself invertible.