theorem SerreDualityUnconditional.serre_duality_numerical_unconditional {k : Type u_1} [Field k] (D : TateCechInfra.CechSheafData k) : D.h1_E = D.h0_EK

Numerical Serre duality, unconditional form: for any Čech sheaf data D, h¹(E) = h⁰(E∨ ⊗ K).

theorem SerreDualityUnconditional.genus_arithmetic_eq_geometric_unconditional {k : Type u_1} [Field k] (D : TateCechInfra.CechSheafData k) (ga gm : ℤ) (_hh0_O : D.h0_E = 1) (hga : ga = D.h1_E) (hgm : gm = D.h0_EK) : ga = gm

Arithmetic genus equals geometric genus from the unconditional Serre duality.

theorem SerreDualityUnconditional.serre_duality_both_directions_unconditional {k : Type u_1} [Field k] (D : TateCechInfra.CechSheafData k) : D.h1_E = D.h0_EK

Unconditional Serre duality in both directions (here h¹(E) = h⁰(E∨ ⊗ K)).