TwoChartCech.Cover.sum_residue_eq_zero_of_residueTheorem
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.Cover_sum_residue_eq_zero_of_residueTheorem
universe u wLean source · statement
theorem _root_.TwoChartCech.Cover.sum_residue_eq_zero_of_residueTheorem
{k : Type u} [Field k] {F : Type u} [Field F] [Algebra k F]
[AlgebraicCurve.HasCanonicalLocalResidueKStar k F]
[∀ v : AlgebraicCurve.Place k F, v.DCoordGenerates] [Nontrivial Ω[F⁄k]]
[AlgebraicCurve.HasCanonicalDivisor (K := k) (F := F)] [AlgebraicCurve.HasPrincipalDivisors k F]
(hRT : AlgebraicCurve.ResidueTheorem k F)
(𝒰 : TwoChartCech.Cover.{u, u} k) {ι : Type w} [Fintype ι] (Λ : ι → 𝒰.LaurentChart)
(Φ : Ω[𝒰.A01⁄k] →ₗ[k] Ω[F⁄k]) (p : ι ↪ AlgebraicCurve.Place k F)
(hres : ∀ (i : ι) (η : Ω[𝒰.A01⁄k]),
(Λ i).residue η = AlgebraicCurve.kaehlerResidueTerm (Φ η) (AlgebraicCurve.diagonalHom k F
1) (p i))
(η : Ω[𝒰.A01⁄k])
(hreg : ∀ v : AlgebraicCurve.Place k F, v ∉ Set.range p →
AlgebraicCurve.kaehlerResidueTerm (Φ η) (AlgebraicCurve.diagonalHom k F 1) v = 0) :
∑ i, (Λ i).residue η = 0