AlgebraicCurve.nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf
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
universe u
open CategoryTheory AlgebraicGeometry
open AlgebraicCurve inLean source · full declaration
theorem _root_.AlgebraicCurve.nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf
{K : Type u} [Field K] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (x : X ⟶ Spec
(CommRingCat.of K))
[IsIntegral X] [IsSeparated x] [QuasiCompact x] [SmoothOfRelativeDimension 1 x]
(h0 : Nonempty 𝒱.U0) (h1 : Nonempty 𝒱.U1)
(M : X.Modules) (hM : Scheme.Modules.IsInvertible M) :
letI := (AlgebraicCurve.baseToFunctionField x).toAlgebra
∃ D : AlgebraicCurve.Divisor K X.functionField,
Nonempty ((𝒱.sectionsOf x M).H0 ≃ₗ[K]
↥(AlgebraicCurve.cechH0 (AlgebraicCurve.placesOf x 𝒱.U0) (AlgebraicCurve.placesOf x 𝒱.U1)
D)) ∧
Nonempty ((𝒱.sectionsOf x M).H1 ≃ₗ[K]
AlgebraicCurve.cechH1 (AlgebraicCurve.placesOf x 𝒱.U0) (AlgebraicCurve.placesOf x 𝒱.U1) D)
:= by
let := (AlgebraicCurve.baseToFunctionField x).toAlgebra
obtain ⟨D, φ, hnat, hsmul, hinj, hrange, -⟩ :=
Scheme.Modules.IsInvertible.exists_divisor_range_eq_lSpaceOn x M hM
exact ⟨D, nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn 𝒱 x h0 h1 M D φ
hnat
(fun U _ a m => hsmul U a m) hinj hrange⟩