Module

Finite_H0_H1_structureSheaf_of_smoothProperCurve.lean

Nyll.AlgebraicCurves.Cohomology.Finite_H0_H1_structureSheaf_of_smoothProperCurve

4 declarations indexed from sourceView source ↗

Module documentation

Finiteness of structure-sheaf cohomology of a smooth proper integral curve.

Imports14

Imported by2

theorem

nonempty_of_sup_eq_top

AlgebraicCurves.Cohomology.Proofs.Finite_H0_H1_structureSheaf_of_smoothProperCurve.AlgebraicCurve.nonempty_of_sup_eq_top

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.Finite_H0_H1_structureSheaf_of_smoothProperCurve
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open CategoryTheory AlgebraicGeometry TopologicalSpace

Lean source · statement

theorem nonempty_of_sup_eq_top {C : Scheme.{u}} (U V : C.Opens) (hUV : U ⊔ V = ⊤) (hV : V ≠ ⊤) :
    Nonempty U

theorem

ne_top_of_isAffineOpen

AlgebraicCurves.Cohomology.Proofs.Finite_H0_H1_structureSheaf_of_smoothProperCurve.AlgebraicCurve.ne_top_of_isAffineOpen

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.Finite_H0_H1_structureSheaf_of_smoothProperCurve
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open CategoryTheory AlgebraicGeometry TopologicalSpace

Lean source · statement

theorem ne_top_of_isAffineOpen {C : Scheme.{u}} (hC : ¬ IsAffine C) {U : C.Opens}
    (hU : IsAffineOpen U) : U ≠ ⊤

theorem

finite_H0_H1_structureSheaf_of_smoothProperCurve'

AlgebraicCurves.Cohomology.Proofs.Finite_H0_H1_structureSheaf_of_smoothProperCurve.AlgebraicCurve.finite_H0_H1_structureSheaf_of_smoothProperCurve'

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.Finite_H0_H1_structureSheaf_of_smoothProperCurve
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open CategoryTheory AlgebraicGeometry
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open CategoryTheory AlgebraicGeometry TopologicalSpace

Lean source · full declaration

theorem finite_H0_H1_structureSheaf_of_smoothProperCurve' {K : Type u} [Field K] {C : Scheme.{u}}
    (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (CommRingCat.of K))
    [IsIntegral C] [IsProper c] [SmoothOfRelativeDimension 1 c]
    (hcurve : letI := (AlgebraicCurve.baseToFunctionField c).toAlgebra
      AlgebraicCurve.IsCurveOver K C.functionField)
    (hL0 : letI := (AlgebraicCurve.baseToFunctionField c).toAlgebra
      FiniteDimensional K ↥(AlgebraicCurve.LSpace (0 : AlgebraicCurve.Divisor K C.functionField)))
    (hreach : letI := (AlgebraicCurve.baseToFunctionField c).toAlgebra
      ∃ (γ : ℤ) (D₀ : AlgebraicCurve.Divisor K C.functionField),
        AlgebraicCurve.RiemannGenusReachedAt γ D₀) :
    letI := (AlgebraicCurve.baseToFunctionField c).toAlgebra
    Module.Finite K (𝒱.structureSheafSections c).H0 ∧ Module.Finite K (𝒱.structureSheafSections
      c).H1 ∧
      Module.finrank K (𝒱.structureSheafSections c).H0
        = AlgebraicCurve.ell (0 : AlgebraicCurve.Divisor K C.functionField) ∧
      Module.finrank K (𝒱.structureSheafSections c).H1 = AlgebraicCurve.genusFF K C.functionField
        := by
  let := (AlgebraicCurve.baseToFunctionField c).toAlgebra
  have := hcurve
  have := hL0
  obtain ⟨γ, D₀, hγ⟩ := hreach
  have hNA := not_isAffine_of_isProper_of_smoothOfRelativeDimension_one c
  have hne0 : 𝒱.U0 ≠ ⊤ := ne_top_of_isAffineOpen hNA 𝒱.isAffineOpen_U0
  have hne1 : 𝒱.U1 ≠ ⊤ := ne_top_of_isAffineOpen hNA 𝒱.isAffineOpen_U1
  have h0 : Nonempty 𝒱.U0 := nonempty_of_sup_eq_top 𝒱.U0 𝒱.U1 𝒱.sup_eq_top hne1
  have h1 : Nonempty 𝒱.U1 := nonempty_of_sup_eq_top 𝒱.U1 𝒱.U0 (sup_comm 𝒱.U1 𝒱.U0 ▸ 𝒱.sup_eq_top)
    hne0
  obtain ⟨⟨e0⟩, ⟨e1⟩⟩ := nonempty_linearEquiv_cechH0_and_cechH1 𝒱 c h0 h1
  obtain ⟨hcov, hS0, hS1⟩ :=
    placesOf_union_eq_univ_of_sup_eq_top c 𝒱.U0 𝒱.U1 𝒱.sup_eq_top hne0 hne1
  obtain ⟨hfin0, hfin1, hrk0, hrk1, -, -⟩ :=
    cechRiemannRoch_of_genusReached hγ hcov hS0 hS1 (0 : Divisor K C.functionField)
  refine ⟨Module.Finite.equiv e0.symm, Module.Finite.equiv e1.symm, ?_, ?_⟩
  · rw [e0.finrank_eq, hrk0]
  · rw [e1.finrank_eq, hrk1, indexOfSpecialty_eq_finrank_H1]
    rfl

theorem

finite_H0_H1_structureSheaf_of_smoothProperCurve

AlgebraicCurve.finite_H0_H1_structureSheaf_of_smoothProperCurve

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.Finite_H0_H1_structureSheaf_of_smoothProperCurve
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open CategoryTheory AlgebraicGeometry
universe u
open _root_.AlgebraicCurves.Cohomology.Proofs in
open _root_.AlgebraicCurve Finite_H0_H1_structureSheaf_of_smoothProperCurve.AlgebraicCurve in

Lean source · full declaration

theorem _root_.AlgebraicCurve.finite_H0_H1_structureSheaf_of_smoothProperCurve {K : Type u} [Field
    K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (CommRingCat.of K))
    [IsIntegral C] [IsProper c] [SmoothOfRelativeDimension 1 c]
    (hcurve : letI := (AlgebraicCurve.baseToFunctionField c).toAlgebra
      AlgebraicCurve.IsCurveOver K C.functionField)
    (hL0 : letI := (AlgebraicCurve.baseToFunctionField c).toAlgebra
      FiniteDimensional K ↥(AlgebraicCurve.LSpace (0 : AlgebraicCurve.Divisor K C.functionField)))
    (hreach : letI := (AlgebraicCurve.baseToFunctionField c).toAlgebra
      ∃ (γ : ℤ) (D₀ : AlgebraicCurve.Divisor K C.functionField),
        AlgebraicCurve.RiemannGenusReachedAt γ D₀) :
    letI := (AlgebraicCurve.baseToFunctionField c).toAlgebra
    Module.Finite K (𝒱.structureSheafSections c).H0 ∧ Module.Finite K (𝒱.structureSheafSections
      c).H1 ∧
      Module.finrank K (𝒱.structureSheafSections c).H0
        = AlgebraicCurve.ell (0 : AlgebraicCurve.Divisor K C.functionField) ∧
      Module.finrank K (𝒱.structureSheafSections c).H1 = AlgebraicCurve.genusFF K C.functionField :=
  finite_H0_H1_structureSheaf_of_smoothProperCurve' 𝒱 c hcurve hL0 hreach