AlgebraicCurve.serrePairing_traceAlong_eq_serrePairing_traceAlong_pullbackAlong_of_cechH1ToH1_eq
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
section PublicStatement
open _root_.KaehlerDifferential
open _root_.AlgebraicCurve
open _root_.AlgebraicCurves.Cohomology.Proofs.SerrePairingTraceCompatibility
namespace AlgebraicCurveLean source · statement
theorem serrePairing_traceAlong_eq_serrePairing_traceAlong_pullbackAlong_of_cechH1ToH1_eq
{K : Type*} {F : Type*} {F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
[HasCanonicalLocalResidueKStar K F] [HasCanonicalLocalResidueKStar K F']
[∀ v : Place K F, v.DCoordGenerates] [∀ w : Place K F', w.DCoordGenerates]
[Nontrivial Ω[F⁄K]] [Nontrivial Ω[F'⁄K]] [IsCurveOver K F']
[HasCanonicalDivisor (K := K) (F := F)] [HasCanonicalDivisor (K := K) (F := F')]
[HasPrincipalDivisors K F]
(hRT : ResidueTheorem K F) (hRT' : ResidueTheorem K F')
(φα φβ : F →ₐ[K] F') (hφα : φα.toRingHom.IsIntegral) (hφβ : φβ.toRingHom.IsIntegral)
(htrα : TraceIntegralAlong φα hφα) (hsepβ : SeparableAlong K φβ)
(hfibα : FibreResidueIdentityAlong φα hφα) (hfibβ : FibreResidueIdentityAlong φβ hφβ)
{S₀ S₁ T₀ T₁ : Set (Place K F)} (hS : S₀ ∪ S₁ = Set.univ) (hT : T₀ ∪ T₁ = Set.univ)
(ω : ↥(regularDifferentials K F))
(hωα : Differential.pullbackAlong φα (ω : Ω[F⁄K]) ∈ regularDifferentials K F')
(hωβα : Differential.traceAlong φβ (Differential.pullbackAlong φα (ω : Ω[F⁄K])) ∈
regularDifferentials K F)
(y : cechH1 T₀ T₁ (0 : Divisor K F))
(x' : cechH1 ((Place.restrictAlong φα hφα) ⁻¹' S₀) ((Place.restrictAlong φα hφα) ⁻¹' S₁) (0 :
Divisor K F'))
(hx' : cechH1ToH1 (preimage_restrictAlong_union_eq_univ φα hφα hS) 0 x' =
cechH1ToH1 (preimage_restrictAlong_union_eq_univ φβ hφβ hT) 0 (cechH1.pullbackAlong φβ hφβ
T₀ T₁ y)) :
serrePairing hRT hS ω (cechH1.traceAlong φα hφα htrα S₀ S₁ x')
= serrePairing hRT hT
⟨Differential.traceAlong φβ (Differential.pullbackAlong φα (ω : Ω[F⁄K])), hωβα⟩ y