structure SerreDualityTate.TateDualitySetup (k : Type u_1) [Field k] : Type (max u_1 (u_2 + 1))

A Tate-style duality setup: a k-vector space V together with two subspaces V₁, V₂ which model a two-cover Čech setup.

• V : Type u_2
• instACG : AddCommGroup self.V
• instModule : Module k self.V
• V₁ : Submodule k self.V
• V₂ : Submodule k self.V

def SerreDualityTate.TateDualitySetup.cechH0 {k : Type u_1} [Field k] (S : TateDualitySetup k) : Submodule k S.V

The Čech H⁰ of the setup: the intersection V₁ ∩ V₂.

def SerreDualityTate.TateDualitySetup.cechH1 {k : Type u_1} [Field k] (S : TateDualitySetup k) : Type u_2

The Čech H¹ of the setup: the quotient V / (V₁ + V₂).

@[implicit_reducible]

instance SerreDualityTate.TateDualitySetup.cechH1.instACG {k : Type u_1} [Field k] (S : TateDualitySetup k) : AddCommGroup S.cechH1

cechH1 is an additive commutative group, inherited from the quotient.

@[implicit_reducible]

instance SerreDualityTate.TateDualitySetup.cechH1.instModule {k : Type u_1} [Field k] (S : TateDualitySetup k) : Module k S.cechH1

cechH1 is a k-module, inherited from the quotient.

theorem SerreDualityTate.TateDualitySetup.cechH0_eq_inf {k : Type u_1} [Field k] (S : TateDualitySetup k) : S.cechH0 = S.V₁ ⊓ S.V₂

Unfolds cechH0 as V₁ ∩ V₂.

def SerreDualityTate.TateDualitySetup.dual {k : Type u_1} [Field k] (S : TateDualitySetup k) : TateDualitySetup k

The dual Tate setup: V* with subspaces given by the annihilators of V₁ and V₂.

theorem SerreDualityTate.dual_H0_eq_annihilator_sup {k : Type u_1} [Field k] (S : TateDualitySetup k) : S.dual.cechH0 = (S.V₁ ⊔ S.V₂).dualAnnihilator

The dual cechH0 equals the annihilator of the sum V₁ + V₂: V₁⁰ ∩ V₂⁰ = (V₁ + V₂)⁰.

theorem SerreDualityTate.annihilator_inf_contains_sup {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (W₁ W₂ : Submodule k V) : W₁.dualAnnihilator ⊔ W₂.dualAnnihilator ≤ (W₁ ⊓ W₂).dualAnnihilator

The sum of annihilators is contained in the annihilator of the intersection: W₁⁰ + W₂⁰ ⊆ (W₁ ∩ W₂)⁰.

theorem SerreDualityTate.annihilator_inf_eq_sup_field {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (W₁ W₂ : Submodule k V) : (W₁ ⊓ W₂).dualAnnihilator = W₁.dualAnnihilator ⊔ W₂.dualAnnihilator

Over a field, the annihilator of the intersection equals the sum of annihilators: (W₁ ∩ W₂)⁰ = W₁⁰ + W₂⁰.

structure SerreDualityTate.TateVectorSpace (k : Type u_1) [Field k] : Type (max u_1 (u_2 + 1))

Tate vector space (Def 46, Lec 25): a k-vector space V with a topology admitting a neighborhood basis of 0 by mutually commensurable subspaces.

• V : Type u_2
• instACG : AddCommGroup self.V
• instModule : Module k self.V
• topology : TopologicalSpace self.V
• nhd_basis : Set (Submodule k self.V)
• is_nhd_basis (U : Submodule k self.V) : U ∈ self.nhd_basis → ↑U ∈ nhds 0
• commensurable (U₁ : Submodule k self.V) : U₁ ∈ self.nhd_basis → ∀ U₂ ∈ self.nhd_basis, Module.Finite k (↥U₁ ⧸ Submodule.comap U₁.subtype (U₁ ⊓ U₂)) ∧ Module.Finite k (↥U₂ ⧸ Submodule.comap U₂.subtype (U₁ ⊓ U₂))

def SerreDualityTate.Commensurable (k : Type u_1) [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (W₁ W₂ : Submodule k V) : Prop

Two subspaces W₁, W₂ are commensurable if each quotient Wᵢ / (W₁ ∩ W₂) is finite-dimensional.

def SerreDualityTate.shiftedSupported (k : Type u_1) [Field k] (i : ℤ) : Submodule k (ℤ →₀ k)

The subspace of Laurent polynomials supported in indices ≥ i.

def SerreDualityTate.laurentTopology (k : Type u_1) [Field k] : TopologicalSpace (ℤ →₀ k)

The Laurent topology on ℤ →₀ k generated by translates of the shiftedSupported subspaces — a basic case of a Tate vector space topology.

noncomputable def SerreDualityTate.tateVS_kLaurent (k : Type u_1) [Field k] : TateVectorSpace k

The Tate vector space structure on ℤ →₀ k with the Laurent topology and neighborhood basis given by shiftedSupported.

theorem SerreDualityTate.residue_annihilator_property {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (V₁ V₁' : Submodule k V) (φ : V →ₗ[k] Module.Dual k V) (h_zero : ∀ v ∈ V₁, ∀ w ∈ V₁', (φ w) v = 0) : V₁' ≤ Submodule.comap φ V₁.dualAnnihilator

Residue pairing vanishing implies annihilator inclusion: if φ(w)(v) = 0 for all v ∈ V₁, w ∈ V₁', then V₁' ⊆ φ⁻¹(V₁⁰).

theorem SerreDualityTate.lattice_annihilator_nonneg {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

If f annihilates every nonneg-supported g under the residue pairing, then f itself is nonneg-supported.

theorem SerreDualityTate.tate_H0_eq_intersection {k : Type u_1} [Field k] (S : TateDualitySetup k) : S.cechH0 = S.V₁ ⊓ S.V₂

cechH0 is by definition the intersection V₁ ∩ V₂.

theorem SerreDualityTate.tate_H0_dual_eq {k : Type u_1} [Field k] (S : TateDualitySetup k) : S.dual.cechH0 = (S.V₁ ⊔ S.V₂).dualAnnihilator

The dual cechH0 equals the annihilator of V₁ + V₂.

theorem SerreDualityTate.tate_duality_core {k : Type u_1} [Field k] (S : TateDualitySetup k) [FiniteDimensional k S.V] : Module.finrank k ↥S.dual.cechH0 = Module.finrank k S.cechH1

Core Tate-style duality: in finite dimension, dim H⁰(S.dual) = dim H¹(S), i.e. dim (V₁ + V₂)⁰ = dim (V / (V₁ + V₂)).

theorem SerreDualityTate.residue_characterization_exact (k : Type u_1) [Field k] (n : ℤ) (a : k) : (SerreDualityCurves.residueMap k) (Finsupp.single (n - 1) (↑n * a)) = 0

The residue of an exact differential d(a · z^n) vanishes.

theorem SerreDualityTate.residue_of_dt_over_t (k : Type u_1) [Field k] : (SerreDualityCurves.residueMap k) (Finsupp.single (-1) 1) = 1

The residue of dt / t (concentrated at index -1) equals 1.

theorem SerreDualityTate.residue_pairing_shift (k : Type u_1) [Field k] (i : ℤ) (a : k) (g : ℤ →₀ k) : SerreDualityCurves.residuePairing k (Finsupp.single i a) g = a * g (SerreDualityP1.residueShift i)

The residue pairing of a · z^i with g equals a · g(-1 - i).

theorem SerreDualityTate.serre_duality_from_tate_both {k : Type u_2} [Field k] (S : TateDualitySetup k) [FiniteDimensional k S.V] (C : CanonicalSheafCurves.SmoothCompleteCurve) (d h0_E h1_E h0_EK h1_EK : ℤ) (hRR_E : h0_E - h1_E = C.χ (1, d)) (hRR_EK : h0_EK - h1_EK = C.χ (1, C.degK - d)) (h_h0_EK : h0_EK = ↑(Module.finrank k ↥S.dual.cechH0)) (h_h1_E : h1_E = ↑(Module.finrank k S.cechH1)) : h0_EK = h1_E ∧ h0_E = h1_EK

Combining the Tate-style core duality with Riemann–Roch on a smooth complete curve yields both Serre-duality identities h⁰(E∨⊗K) = h¹(E) and h⁰(E) = h¹(E∨⊗K).

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

Rank-1 Euler-characteristic identity from Serre duality: χ(E) + χ(E∨⊗K) = 0.

theorem SerreDualityTate.euler_char_dual_pair_rank_r (C : CanonicalSheafCurves.SmoothCompleteCurve) (r d : ℤ) : C.χ (r, d) + C.χ (r, r * C.degK - d) = 0

Rank-r Euler-characteristic identity from Serre duality.

noncomputable def SerreDualityTate.cechSetup_P1 (k : Type) [Field k] (n : ℤ) : TateDualitySetup k

The Čech setup on ℙ¹ for O(n): V = (ℤ →₀ k) with the two cover-pieces realized as NonNeg and AtMost n subspaces.

theorem SerreDualityTate.cechSetup_P1_H0 (k : Type) [Field k] (n : ℤ) : (cechSetup_P1 k n).cechH0 = CohomologyP1.NonNeg k ⊓ CohomologyP1.AtMost k n

The Čech H⁰ of the ℙ¹ setup is NonNeg ∩ AtMost n.

theorem SerreDualityTate.serre_duality_P1_from_tate (k : Type) [Field k] (n : ℤ) (hn : n < -1) : Nonempty (((ℤ →₀ k) ⧸ CohomologyP1.NonNeg k ⊔ CohomologyP1.AtMost k n) ≃ₗ[k] ↥(CohomologyP1.CechH0 k (-2 - n)))

Serre duality on ℙ¹ derived from the Tate setup (existence form): for n < -1, H¹(O(n)) ≃ H⁰(O(-2 - n)).

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

Dimension form of Serre duality on ℙ¹.

theorem SerreDualityTate.sum_of_residues_zero (k : Type u_1) [Field k] {n : ℕ} (c a : Fin n → k) (hdist : Function.Injective a) : ∑ i : Fin n, ResidueSum.residuePartialFrac c a i + ResidueSum.residueAtInfPartialFrac c a = 0

Sum of residues theorem on ℙ¹: the sum of finite-place residues of a partial fraction plus the residue at infinity vanishes.

theorem SerreDualityTate.residue_implies_annihilator_inclusion (k : Type u_1) [Field k] (S : TateDualitySetup k) (V₁' : Submodule k (Module.Dual k S.V)) (h_residue : ∀ f ∈ S.V₁, ∀ φ ∈ V₁', φ f = 0) : V₁' ≤ S.V₁.dualAnnihilator

Vanishing of the residue pairing on V₁ × V₁' implies V₁' ⊆ V₁⁰.

theorem SerreDualityTate.annihilator_equality_gives_duality (k : Type u_1) [Field k] (S : TateDualitySetup k) (V₁' : Submodule k (Module.Dual k S.V)) (h_eq : V₁' = S.V₁.dualAnnihilator) (V₂' : Submodule k (Module.Dual k S.V)) (h_eq₂ : V₂' = S.V₂.dualAnnihilator) : V₁' ⊓ V₂' = (S.V₁ ⊔ S.V₂).dualAnnihilator

If V₁' = V₁⁰ and V₂' = V₂⁰, then V₁' ∩ V₂' = (V₁ + V₂)⁰.

theorem SerreDualityTate.serre_duality_full (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : ℤ) : C.χ (1, d) + C.χ (1, C.degK - d) = 0 ∧ C.χ (1, d) = d + 1 - C.g

Full Serre duality + Riemann–Roch package on a smooth complete curve.

theorem SerreDualityTate.genus_equality (C : CanonicalSheafCurves.SmoothCompleteCurve) : C.χ (1, 0) + C.χ (1, C.degK) = 0

Serre duality applied to O ↔ K: χ(O) + χ(K) = 0.

theorem SerreDualityTate.riemann_roch_serre (C : CanonicalSheafCurves.SmoothCompleteCurve) (d h0_D h0_KD : ℤ) (hRR : h0_D - h0_KD = C.χ (1, d)) : h0_D - h0_KD = d + 1 - C.g

Riemann–Roch in Serre form: h⁰(D) − h⁰(K - D) = d + 1 − g.

theorem SerreDualityTate.deg_canonical (C : CanonicalSheafCurves.SmoothCompleteCurve) : C.degK = 2 * C.g - 2

The degree of the canonical divisor: deg K_C = 2g − 2.

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

Serre duality on ℙ¹ at the dimension level (verification).

theorem SerreDualityTate.P1_riemann_roch (k : Type) [Field k] (n : ℤ) : ↑(RiemannRoch.dimH0 k n) - ↑(RiemannRoch.dimH1 k n) = n + 1

Riemann–Roch on ℙ¹: h⁰(O(n)) − h¹(O(n)) = n + 1.

theorem SerreDualityTate.P1_serre_duality_equiv (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))

Equivalent dimensional form of Serre duality on ℙ¹, for n < -1.