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

Non-degeneracy of the residue pairing on Laurent-style finitely supported functions ℤ →₀ k: if f pairs to zero against every g, then f = 0.

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

Right-side non-degeneracy of the residue pairing: if g pairs to zero against every f, then g = 0.

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

The nonneg-supported lattice is self-orthogonal under the residue pairing: if f and g are both supported on ℕ ⊂ ℤ, the residue pairing vanishes.

theorem TateResidueOrthogonality.lattice_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

Characterization: f annihilates every nonneg-supported g under the residue pairing iff f itself is nonneg-supported.

structure TateResidueOrthogonality.IsArithmeticallyDiscrete (k : Type u_1) [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (W Λ : Submodule k V) : Prop

Λ is arithmetically discrete with respect to W iff Λ / (W ∩ Λ) is finite-dimensional over k.

• finiteDim : Module.Finite k (↥Λ ⧸ Submodule.comap Λ.subtype (W ⊓ Λ))

structure TateResidueOrthogonality.IsArithmeticallyCocompact (k : Type u_1) [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (W Λ : Submodule k V) : Prop

Λ is arithmetically cocompact with respect to W iff V / (W + Λ) is finite-dimensional over k.

• finiteDim : Module.Finite k (V ⧸ W ⊔ Λ)

theorem TateResidueOrthogonality.discrete_cocompact_dual (k : Type u_1) [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (W Λ : Submodule k V) : IsArithmeticallyDiscrete k W Λ → IsArithmeticallyCocompact k W Λ → IsArithmeticallyDiscrete k W.dualAnnihilator Λ.dualAnnihilator ∧ IsArithmeticallyCocompact k W.dualAnnihilator Λ.dualAnnihilator

Duality between discreteness and cocompactness: in the finite-dimensional setting, the annihilators of a discrete/cocompact pair are themselves a discrete/cocompact pair.

theorem TateResidueOrthogonality.annihilator_finiteDim (k : Type u_1) [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (W : Submodule k V) : FiniteDimensional k ↥W.dualAnnihilator

The annihilator of a subspace inside the dual of a finite-dimensional space is itself finite-dimensional.

theorem TateResidueOrthogonality.inclusion_to_equality_by_dimension {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (W₁ W₂ : Submodule k V) [FiniteDimensional k ↥W₂] (h_le : W₁ ≤ W₂) (h_dim : Module.finrank k ↥W₁ = Module.finrank k ↥W₂) : W₁ = W₂

An inclusion of subspaces becomes an equality once their dimensions agree and the larger one is finite-dimensional.

theorem TateResidueOrthogonality.annihilator_equality_from_inclusion_and_dim {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (V₁ : Submodule k V) (V₁' : Submodule k (Module.Dual k V)) [FiniteDimensional k ↥V₁.dualAnnihilator] (h_inc : V₁' ≤ V₁.dualAnnihilator) (h_dim : Module.finrank k ↥V₁' = Module.finrank k ↥V₁.dualAnnihilator) : V₁' = V₁.dualAnnihilator

Specialization of inclusion_to_equality_by_dimension to comparing a subspace of the dual to the annihilator of V₁.

theorem TateResidueOrthogonality.tate_orthogonality_complete {k : Type u_1} [Field k] (S : SerreDualityTate.TateDualitySetup k) [FiniteDimensional k S.V] (V₁' V₂' : Submodule k (Module.Dual k S.V)) (h_V1_eq : V₁' = S.V₁.dualAnnihilator) (h_V2_eq : V₂' = S.V₂.dualAnnihilator) : V₁' ⊓ V₂' = (S.V₁ ⊔ S.V₂).dualAnnihilator ∧ Module.finrank k ↥(V₁' ⊓ V₂') = Module.finrank k (S.V ⧸ S.V₁ ⊔ S.V₂)

Complete Tate orthogonality: under the annihilator identifications, the intersection V₁' ⊓ V₂' equals the annihilator of V₁ ⊔ V₂ and has the same dimension as the quotient V / (V₁ ⊔ V₂).

theorem TateResidueOrthogonality.tate_orthogonality_gives_serre_duality {k : Type u_1} [Field k] (S : SerreDualityTate.TateDualitySetup k) [FiniteDimensional k S.V] (V₁' V₂' : Submodule k (Module.Dual k S.V)) (h_V1_eq : V₁' = S.V₁.dualAnnihilator) (h_V2_eq : V₂' = S.V₂.dualAnnihilator) : Module.finrank k ↥(V₁' ⊓ V₂') = Module.finrank k S.cechH1

Tate orthogonality implies Serre duality at the level of dimensions: the intersection of dual annihilators matches H¹.

theorem TateResidueOrthogonality.tate_serre_duality_chain {k : Type u_1} [Field k] (S : SerreDualityTate.TateDualitySetup k) [FiniteDimensional k S.V] (C : CanonicalSheafCurves.SmoothCompleteCurve) (d h0_E h1_EK : ℤ) (hRR_E : h0_E - ↑(Module.finrank k S.cechH1) = C.χ (1, d)) (hRR_EK : ↑(Module.finrank k ↥S.dual.cechH0) - h1_EK = C.χ (1, C.degK - d)) : h0_E = h1_EK

Chain Tate self-duality together with Riemann–Roch on a smooth complete curve to recover Serre duality h⁰(E) = h¹(K - E).

theorem TateResidueOrthogonality.residue_pairing_separating {k : Type u_1} [Field k] (f : ℤ →₀ k) (hf : f ≠ 0) : ∃ (g : ℤ →₀ k), ∑ j ∈ f.support, f j * g (-1 - j) ≠ 0

Separation: any nonzero f admits a g against which the residue pairing is nonzero, i.e. residues separate Laurent-style sections (Lem 36, Tate residue orthogonality).

theorem TateResidueOrthogonality.residue_dual_basis {k : Type u_1} [Field k] (i : ℤ) : ∑ j ∈ (Finsupp.single i 1).support, (Finsupp.single i 1) j * (Finsupp.single (-1 - i) 1) (-1 - j) = 1

Dual basis: the indicator at i pairs with itself via the index -1 - i to give 1.

theorem TateResidueOrthogonality.residue_dual_basis_orthog {k : Type u_1} [Field k] (i j : ℤ) (hij : i ≠ j) : ∑ l ∈ (Finsupp.single i 1).support, (Finsupp.single i 1) l * (Finsupp.single (-1 - j) 1) (-1 - l) = 0

Orthogonality of distinct dual basis elements under the residue pairing.