structure SerrePairingNondegenerate.SerrePairingData (k : Type u_1) [Field k] : Type (max (max u_1 (u_2 + 1)) (u_3 + 1))

Data for a Serre pairing: a Čech-style two-cover V₁, V₂ ⊆ K, a finite-dimensional "dual sections" space H0dual, and a residue pairing that vanishes on V₁ + V₂ and is right-separating.

• K : Type u_2
• K_acg : AddCommGroup self.K
• K_mod : Module k self.K
• V₁ : Submodule k self.K
• V₂ : Submodule k self.K
• H0dual : Type u_3
• H0dual_acg : AddCommGroup self.H0dual
• H0dual_mod : Module k self.H0dual
• H0dual_fd : FiniteDimensional k self.H0dual
• residuePairing : self.K →ₗ[k] self.H0dual →ₗ[k] k
• residue_vanishes_on_image (ω : self.H0dual) (f : self.K) : f ∈ self.V₁ ⊔ self.V₂ → (self.residuePairing f) ω = 0
• residue_separating (ω : self.H0dual) : (∀ (f : self.K), (self.residuePairing f) ω = 0) → ω = 0

structure SerrePairingNondegenerate.PerfectSerrePairingData (k : Type u_1) [Field k] extends SerrePairingNondegenerate.SerrePairingData k : Type (max (max u_1 (u_2 + 1)) (u_3 + 1))

Perfect Serre pairing data: a SerrePairingData with the additional left-separating axiom — if the pairing vanishes on all ω, then f ∈ V₁ + V₂.

• K : Type u_3
• K_acg : AddCommGroup self.K
• K_mod : Module k self.K
• V₁ : Submodule k self.K
• V₂ : Submodule k self.K
• H0dual : Type u_2
• H0dual_acg : AddCommGroup self.H0dual
• H0dual_mod : Module k self.H0dual
• H0dual_fd : FiniteDimensional k self.H0dual
• residuePairing : self.K →ₗ[k] self.H0dual →ₗ[k] k
• residue_vanishes_on_image (ω : self.H0dual) (f : self.K) : f ∈ self.V₁ ⊔ self.V₂ → (self.residuePairing f) ω = 0
• residue_separating (ω : self.H0dual) : (∀ (f : self.K), (self.residuePairing f) ω = 0) → ω = 0
• residue_separating_left (f : self.K) : (∀ (ω : self.H0dual), (self.residuePairing f) ω = 0) → f ∈ self.V₁ ⊔ self.V₂

def SerrePairingNondegenerate.SerrePairingData.H1 {k : Type u_1} [Field k] (D : SerrePairingData k) : Type u_2

Čech H¹ of a Serre pairing data: the quotient K / (V₁ + V₂).

@[implicit_reducible]

instance SerrePairingNondegenerate.instAddCommGroupH1 {k : Type u_1} [Field k] (D : SerrePairingData k) : AddCommGroup D.H1

H¹ of a Serre pairing data is an additive commutative group.

@[implicit_reducible]

instance SerrePairingNondegenerate.instModuleH1 {k : Type u_1} [Field k] (D : SerrePairingData k) : Module k D.H1

H¹ is a k-module.

def SerrePairingNondegenerate.SerrePairingData.serrePairing {k : Type u_1} [Field k] (D : SerrePairingData k) : D.H1 →ₗ[k] D.H0dual →ₗ[k] k

The Serre pairing H¹ × H0dual → k obtained by descending the residue pairing through the quotient K → K/(V₁ + V₂).

@[simp]

theorem SerrePairingNondegenerate.SerrePairingData.serrePairing_mk {k : Type u_1} [Field k] (D : SerrePairingData k) (f : D.K) : D.serrePairing (Submodule.Quotient.mk f) = D.residuePairing f

The Serre pairing on a representative [f] agrees with the residue pairing on f.

theorem SerrePairingNondegenerate.SerrePairingData.pairing_nondegenerate_right {k : Type u_1} [Field k] (D : SerrePairingData k) (ω : D.H0dual) (h : ∀ (ξ : D.H1), (D.serrePairing ξ) ω = 0) : ω = 0

Right non-degeneracy of the Serre pairing: if ω pairs to 0 with every class in H¹, then ω = 0.

theorem SerrePairingNondegenerate.PerfectSerrePairingData.pairing_nondegenerate_left {k : Type u_1} [Field k] (D : PerfectSerrePairingData k) (ξ : D.H1) (h : ∀ (ω : D.H0dual), (D.serrePairing ξ) ω = 0) : ξ = 0

Left non-degeneracy of a perfect Serre pairing: if ξ ∈ H¹ pairs to 0 with every ω, then ξ = 0.

theorem SerrePairingNondegenerate.PerfectSerrePairingData.pairing_perfect {k : Type u_1} [Field k] (D : PerfectSerrePairingData k) : (∀ (ω : D.H0dual), (∀ (ξ : D.H1), (D.serrePairing ξ) ω = 0) → ω = 0) ∧ ∀ (ξ : D.H1), (∀ (ω : D.H0dual), (D.serrePairing ξ) ω = 0) → ξ = 0

The Serre pairing is perfect (non-degenerate on both sides) for a perfect data.