Module

Cover_LaurentChart_residue_r0.lean

Nyll.AlgebraicCurves.Cohomology.Cech.Cover_LaurentChart_residue_r0

1 declaration indexed from sourceView source ↗

Module documentation

Compatibility of Laurent-chart residues with restriction from the first chart.

Imports3

Mathlib.RingTheory.Kaehler.Basic
Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCechLaurentChart
Nyll.AlgebraicCurves.Geometry.Schemes.TwoAffineOpenCoverKaehler

Imported by1

Nyll.AlgebraicCurves.Cohomology.Cech.All

theorem

residue_r0

L28 ↗

TwoChartCech.Cover.LaurentChart.residue_r0

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.Cover_LaurentChart_residue_r0
universe u v

Lean source · statement

theorem _root_.TwoChartCech.Cover.LaurentChart.residue_r0 {R : Type u} [CommRing R] {𝒰 :
  TwoChartCech.Cover.{u, v} R}
    (Λ : 𝒰.LaurentChart) (h : Λ.IsRegular 𝒰.ρ0) (ω : Ω[𝒰.A0⁄R]) : Λ.residue (𝒰.kaehler.r0 ω) = 0

Module documentation

Declarations

residue_r0