def IsCommensurable {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₂ of V are commensurable iff their quotients by their intersection are both finite-dimensional.

theorem IsCommensurable.refl {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (W : Submodule k V) : IsCommensurable W W

Commensurability is reflexive: every subspace is commensurable with itself.

theorem IsCommensurable.symm {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] {W₁ W₂ : Submodule k V} (h : IsCommensurable W₁ W₂) : IsCommensurable W₂ W₁

Commensurability is symmetric in its two arguments.

class IsTateVectorSpace (k : Type u_3) [Field k] (V : Type u_4) [AddCommGroup V] [Module k V] [TopologicalSpace V] : Prop

A Tate vector space over k (Def 46, Lec 25): a topological k-vector space whose neighborhood basis of zero consists of pairwise commensurable linear subspaces.

• exists_nhds_basis : ∃ (ι : Type u_5) (W : ι → Submodule k V), ((nhds 0).HasBasis (fun (x : ι) => True) fun (i : ι) => ↑(W i)) ∧ ∀ (i j : ι), IsCommensurable (W i) (W j)

structure TateCechInfra.CechSheafData (k : Type u_1) [Field k] : Type (max u_1 (v + 1))

Packaging the data needed to apply Tate self-duality machinery to a Čech cohomology setup on a smooth complete curve, recording the Riemann–Roch identities for both E and the dualized line bundle K - E.

• setup : SerreDualityTate.TateDualitySetup k
• instFD : FiniteDimensional k self.setup.V
• curve : CanonicalSheafCurves.SmoothCompleteCurve
• deg : ℤ
• h0_E : ℤ
• h1_EK : ℤ
• hRR_E : self.h0_E - ↑(Module.finrank k self.setup.cechH1) = self.curve.χ (1, self.deg)
• hRR_EK : ↑(Module.finrank k ↥self.setup.dual.cechH0) - self.h1_EK = self.curve.χ (1, self.curve.degK - self.deg)

noncomputable def TateCechInfra.CechSheafData.h1_E {k : Type u_1} [Field k] (D : CechSheafData k) : ℤ

The dimension of H¹(E) as an integer, extracted from the Čech data.

noncomputable def TateCechInfra.CechSheafData.h0_EK {k : Type u_1} [Field k] (D : CechSheafData k) : ℤ

The dimension of H⁰(K - E) as an integer, extracted from the Čech data.

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

Unconditional Serre duality from Tate self-duality: h⁰(K - E) = h¹(E).

theorem TateCechInfra.serre_duality_h0_eq_h1 {k : Type u_1} [Field k] (D : CechSheafData k) : D.h0_E = D.h1_EK

Combining Tate duality with Riemann–Roch gives h⁰(E) = h¹(K - E).

theorem TateCechInfra.serre_duality_both {k : Type u_1} [Field k] (D : CechSheafData k) : D.h0_EK = D.h1_E ∧ D.h0_E = D.h1_EK

Both halves of Serre duality packaged together.

theorem TateCechInfra.cech_data_feeds_tate {k : Type u_1} [Field k] (D : CechSheafData k) : D.h0_EK = D.h1_E ∧ D.h0_E = D.h1_EK

Adapter feeding the Čech data into the generic Tate-duality result.

theorem TateCechInfra.serre_duality_full_chain {k : Type u_1} [Field k] (D : CechSheafData k) : D.h0_EK = D.h1_E ∧ D.h0_E = D.h1_EK ∧ D.curve.χ (1, D.deg) + D.curve.χ (1, D.curve.degK - D.deg) = 0

Full chain: Tate self-duality combined with the Euler characteristic identity yields both Serre duality isomorphisms together with the genus constraint χ(E) + χ(K - E) = 0.

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

If the residue pairing vanishes on S.V₁ × V₁', then V₁' is contained in the annihilator of S.V₁.

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

If both Vᵢ' equal the annihilators of S.Vᵢ, then their intersection equals the annihilator of S.V₁ ⊔ S.V₂.

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

Core Tate dimension identity: the dual cohomology has the same dimension as the original Čech H¹.

theorem TateCechInfra.annihilator_quotient_dimension {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₂).dualAnnihilator = Module.finrank k (V ⧸ W₁ ⊔ W₂)

In a finite-dimensional space, the annihilator of a sum has the same dimension as the quotient by that sum.

theorem TateCechInfra.self_pairing_tate_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₂ : Submodule k V) : Module.finrank k ↥(Submodule.comap (↑B) W₁.dualAnnihilator ⊓ Submodule.comap (↑B) W₂.dualAnnihilator) = Module.finrank k (V ⧸ W₁ ⊔ W₂)

Tate duality via a self-pairing isomorphism V ≃ V*: the dimension of the intersection of annihilators pulled back through B matches the quotient dimension.

theorem TateCechInfra.genus_equality_from_serre (C : CanonicalSheafCurves.SmoothCompleteCurve) : C.χ (1, 0) + C.χ (1, C.degK) = 0

Genus equality χ(O) + χ(K) = 0 deduced from Serre duality on a smooth complete curve.

theorem TateCechInfra.canonical_degree (C : CanonicalSheafCurves.SmoothCompleteCurve) : C.degK = 2 * C.g - 2

The canonical divisor has degree 2g - 2, computed from Serre duality.

theorem TateCechInfra.serre_duality_direction_transfer (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)) (hSD_one : h0_E = h1_EK) : h1_E = h0_EK

Transfer one direction of Serre duality to the other via the Euler characteristic identity.