theorem SerreDualityAnnihilator.annihilator_nonneg_reverse {k : Type u_1} [Field k] (f : ℤ →₀ k) : (∀ i < 0, f i = 0) → ∀ (g : ℤ →₀ k), (∀ i < 0, g i = 0) → ∑ j ∈ f.support, f j * g (-1 - j) = 0

If f : ℤ →₀ k is supported in nonnegative degrees, then it lies in the annihilator of any g supported in nonnegative degrees under the residue pairing (f, g) ↦ ∑ j f j · g (-1 - j).

theorem SerreDualityAnnihilator.annihilator_nonneg_iff {k : Type u_1} [Field k] (f : ℤ →₀ k) : (∀ (g : ℤ →₀ k), (∀ i < 0, g i = 0) → ∑ j ∈ f.support, f j * g (-1 - j) = 0) ↔ ∀ i < 0, f i = 0

Annihilator characterization: f annihilates every nonneg-supported g under the residue pairing if and only if f is itself nonneg-supported.

theorem SerreDualityAnnihilator.strictly_neg_annihilates_strictly_neg {k : Type u_1} [Field k] (f : ℤ →₀ k) (hf : ∀ (i : ℤ), 0 ≤ i → f i = 0) (g : ℤ →₀ k) : (∀ (i : ℤ), 0 ≤ i → g i = 0) → ∑ j ∈ g.support, g j * f (-1 - j) = 0

An f supported in strictly negative degrees annihilates every g supported in strictly negative degrees under the residue pairing.

theorem SerreDualityAnnihilator.annihilator_strictly_neg {k : Type u_1} [Field k] (f : ℤ →₀ k) : (∀ (g : ℤ →₀ k), (∀ (i : ℤ), 0 ≤ i → g i = 0) → ∑ j ∈ g.support, g j * f (-1 - j) = 0) → ∀ (i : ℤ), 0 ≤ i → f i = 0

Converse: if f annihilates every strictly-negative-supported g under the residue pairing, then f is supported in strictly negative degrees.

theorem SerreDualityAnnihilator.annihilator_strictly_neg_iff {k : Type u_1} [Field k] (f : ℤ →₀ k) : (∀ (g : ℤ →₀ k), (∀ (i : ℤ), 0 ≤ i → g i = 0) → ∑ j ∈ g.support, g j * f (-1 - j) = 0) ↔ ∀ (i : ℤ), 0 ≤ i → f i = 0

Biconditional version: the annihilator of the nonneg-supported subspace under the residue pairing is exactly the strictly-negative-supported subspace.

theorem SerreDualityAnnihilator.tate_duality_via_pairing {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : V ≃ₗ[k] Module.Dual k V) (W₁ W₂ : Submodule k V) : Module.finrank k ↥(Submodule.comap (↑B) W₁.dualAnnihilator ⊓ Submodule.comap (↑B) W₂.dualAnnihilator) = Module.finrank k (V ⧸ W₁ ⊔ W₂)

Tate-style duality: for a self-dual pairing B : V ≃ V*, the dimension of B⁻¹(W₁⁰) ∩ B⁻¹(W₂⁰) equals the codimension of W₁ + W₂ in V.

theorem SerreDualityAnnihilator.tate_duality_via_self_duality {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : V ≃ₗ[k] Module.Dual k V) (W₁ W₂ W₁' W₂' : Submodule k V) (h₁ : W₁' = Submodule.comap (↑B) W₁.dualAnnihilator) (h₂ : W₂' = Submodule.comap (↑B) W₂.dualAnnihilator) : Module.finrank k ↥(W₁' ⊓ W₂') = Module.finrank k (V ⧸ W₁ ⊔ W₂)

Restated form of tate_duality_via_pairing where the annihilator subspaces W₁' and W₂' are given as hypotheses.

theorem SerreDualityAnnihilator.tate_euler_char_self_dual {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (W₁ W₂ : Submodule k V) : ↑(Module.finrank k ↥(W₁ ⊓ W₂)) - ↑(Module.finrank k (V ⧸ W₁ ⊔ W₂)) = ↑(Module.finrank k ↥W₁) + ↑(Module.finrank k ↥W₂) - ↑(Module.finrank k V)

Euler-characteristic identity: for any two subspaces of a finite-dimensional V, dim(W₁ ∩ W₂) - dim(V/(W₁ + W₂)) = dim W₁ + dim W₂ - dim V.

theorem SerreDualityAnnihilator.tate_duality_symmetric {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : V ≃ₗ[k] Module.Dual k V) (W₁ W₂ W₁' W₂' : Submodule k V) (h₁ : W₁' = Submodule.comap (↑B) W₁.dualAnnihilator) (h₂ : W₂' = Submodule.comap (↑B) W₂.dualAnnihilator) : ↑(Module.finrank k ↥(W₁ ⊓ W₂)) + ↑(Module.finrank k ↥(W₁' ⊓ W₂')) = ↑(Module.finrank k ↥W₁) + ↑(Module.finrank k ↥W₂) - ↑(Module.finrank k V) + 2 * ↑(Module.finrank k (V ⧸ W₁ ⊔ W₂))

Symmetric form combining Tate duality and the Euler identity, relating dim(W₁ ∩ W₂) + dim(W₁' ∩ W₂') to the dimensions of W₁, W₂, V, and the codimension of W₁ + W₂.

theorem SerreDualityAnnihilator.shift_realizes_tate_duality (k : Type) [Field k] (n : ℤ) (hn : n < -1) : Module.finrank k ((ℤ →₀ k) ⧸ CohomologyP1.NonNeg k ⊔ CohomologyP1.AtMost k n) = Module.finrank k ↥(CohomologyP1.CechH0 k (-2 - n))

For n < -1, the Čech H¹(O(n)) on ℙ¹ realizes Tate-style duality: its dimension equals dim H⁰(O(-2 - n)).

theorem SerreDualityAnnihilator.serre_duality_P1_both_directions (k : Type) [Field k] (n : ℤ) : RiemannRoch.dimH1 k n = RiemannRoch.dimH0 k (-2 - n) ∧ RiemannRoch.dimH0 k n = RiemannRoch.dimH1 k (-2 - n)

Both directions of Serre duality on ℙ¹: dim H¹(O(n)) = dim H⁰(O(-2-n)) and dim H⁰(O(n)) = dim H¹(O(-2-n)).

theorem SerreDualityAnnihilator.serre_duality_chain_P1 (k : Type) [Field k] (n : ℤ) : RiemannRoch.dimH1 k n = RiemannRoch.dimH0 k (-2 - n) ∧ RiemannRoch.dimH0 k n = RiemannRoch.dimH1 k (-2 - n) ∧ ↑(RiemannRoch.dimH0 k n) - ↑(RiemannRoch.dimH1 k n) = n + 1

Bundles Serre duality on ℙ¹ (both directions) together with the Riemann–Roch formula χ(O(n)) = n + 1.

theorem SerreDualityAnnihilator.serre_duality_general_strategy (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : ℤ) : C.χ (1, d) + C.χ (1, C.degK - d) = 0

For a smooth complete curve C and degree d, the sum χ(O(d)) + χ(O(K - d)) = 0, the Euler-characteristic shadow of Serre duality.

theorem SerreDualityAnnihilator.abstract_matches_P1 (k : Type) [Field k] (n : ℤ) : RiemannRoch.dimH0 k (-2 - n) = RiemannRoch.dimH1 k n

The abstract Serre duality matches the explicit ℙ¹ computation: dim H⁰(O(-2-n)) = dim H¹(O(n)).

theorem SerreDualityAnnihilator.tate_applied_to_P1 (k : Type) [Field k] (n : ℤ) (hn : n < -1) : Module.finrank k (SerreDualityTate.cechSetup_P1 k n).cechH1 = Module.finrank k ↥(CohomologyP1.CechH0 k (-2 - n))

The Tate-vector-space duality applied to the ℙ¹ Čech setup yields the equality of H¹(O(n)) and H⁰(O(-2 - n)) dimensions, for n < -1.