NYLL
Module

Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn.lean

Nyll.AlgebraicCurves.Cohomology.Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn
8 declarations indexed from sourceView source ↗

Module documentation

Identify sheaf Cech cohomology with divisor-section cohomology from chartwise range identifications.

Imports8
Imported by3

Declarations

theorem

kerMap_bijective_of_bijective'

L47 ↗
AlgebraicCurves.Cohomology.Proofs.Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn.TwoChartCech.kerMap_bijective_of_bijective'
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs
namespace Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
universe uR uK
variable {R : Type uR} [CommRing R]
variable {K0 K1 : Type uK} [AddCommGroup K0] [Module R K0] [AddCommGroup K1] [Module R K1]
variable {C0 C1 : Type uK} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
Lean source · statement
theorem kerMap_bijective_of_bijective' (dK : K0 →ₗ[R] K1) (d : C0 →ₗ[R] C1) (ι0 : K0 →ₗ[R] C0)
    (ι1 : K1 →ₗ[R] C1) (comm : d ∘ₗ ι0 = ι1 ∘ₗ dK) (h0 : Function.Bijective ι0)
    (h1 : Function.Injective ι1) : Function.Bijective (kerMap dK d ι0 ι1 comm)
theorem

cokerMap_bijective_of_bijective'

L63 ↗
AlgebraicCurves.Cohomology.Proofs.Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn.TwoChartCech.cokerMap_bijective_of_bijective'
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs
namespace Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
universe uR uK
variable {R : Type uR} [CommRing R]
variable {K0 K1 : Type uK} [AddCommGroup K0] [Module R K0] [AddCommGroup K1] [Module R K1]
variable {C0 C1 : Type uK} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
Lean source · statement
theorem cokerMap_bijective_of_bijective' (dK : K0 →ₗ[R] K1) (d : C0 →ₗ[R] C1) (ι0 : K0 →ₗ[R] C0)
    (ι1 : K1 →ₗ[R] C1) (comm : d ∘ₗ ι0 = ι1 ∘ₗ dK) (h0 : Function.Surjective ι0)
    (h1 : Function.Bijective ι1) : Function.Bijective (cokerMap dK d ι0 ι1 comm)
theorem

placesOf_inf'

L91 ↗
AlgebraicCurves.Cohomology.Proofs.Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn.AlgebraicCurve.placesOf_inf'
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs
namespace Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
variable {K : Type u} [Field K] {X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of K)) [IsIntegral X]
Lean source · full declaration
theorem placesOf_inf' [IsSeparated x] [SmoothOfRelativeDimension 1 x] (U V : X.Opens) :
    let := (baseToFunctionField x).toAlgebra
    placesOf x (U ⊓ V) = placesOf x U ∩ placesOf x V := by
  let := (baseToFunctionField x).toAlgebra
  apply Set.Subset.antisymm
  · exact fun v hv => ⟨placesOf_mono x inf_le_left hv, placesOf_mono x inf_le_right hv⟩
  · rintro v ⟨⟨y, hyU, hy, hvy⟩, ⟨z, hzV, -, hvz⟩⟩
    have hyz : y = z := eq_of_range_stalk_eq x y z (hvy.trans hvz.symm)
    subst hyz
    exact ⟨y, ⟨hyU, hzV⟩, hy, hvy⟩
theorem

germToFunctionField_algebraMap'

L102 ↗
AlgebraicCurves.Cohomology.Proofs.Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn.AlgebraicCurve.germToFunctionField_algebraMap'
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs
namespace Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
variable {K : Type u} [Field K] {X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of K)) [IsIntegral X]
Lean source · statement
theorem germToFunctionField_algebraMap' (U : X.Opens) [Nonempty U] (r : K) :
    (X.germToFunctionField U).hom ((Scheme.TwoAffineOpenCover.algebraOfHom x U).algebraMap r)
      = baseToFunctionField x r
def

sectionsEquivLSpaceOn

L119 ↗
AlgebraicCurves.Cohomology.Proofs.Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn.AlgebraicCurve.sectionsEquivLSpaceOn
Documentation

The linear equivalence from module sections to the divisor space specified by the injective section map and its range.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs
namespace Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
variable {K : Type u} [Field K] {X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of K)) [IsIntegral X]
Lean source · full declaration
def sectionsEquivLSpaceOn (M : X.Modules) (U : X.Opens) [Nonempty U]
    (D : letI := (baseToFunctionField x).toAlgebra; Divisor K X.functionField)
    (φ : Γ(M, U) →+ (X.functionField : Type u))
    (hsmul : ∀ (a : Γ(X, U)) (m : Γ(M, U)), φ (a • m) = algebraMap Γ(X, U) X.functionField a * φ m)
    (hinj : Function.Injective φ)
    (hrange : letI := (baseToFunctionField x).toAlgebra
      Set.range φ = (lSpaceOn (placesOf x U) D : Set X.functionField)) :
    letI := Scheme.TwoAffineOpenCover.moduleSectionsOfHom x M U
    letI := (baseToFunctionField x).toAlgebra
    Γ(M, U) ≃ₗ[K] ↥(lSpaceOn (placesOf x U) D) :=
  letI := Scheme.TwoAffineOpenCover.algebraOfHom x U
  letI := Scheme.TwoAffineOpenCover.moduleSectionsOfHom x M U
  letI := (baseToFunctionField x).toAlgebra
  LinearEquiv.ofBijective
    ({ toFun := fun m => ⟨φ m, by
          have : φ m ∈ Set.range φ := ⟨m, rfl⟩
          rw [hrange] at this
          exact this⟩
       map_add' := fun m m' => Subtype.ext (map_add φ m m')
       map_smul' := fun r m => Subtype.ext (by
          change φ (((Scheme.TwoAffineOpenCover.algebraOfHom x U).algebraMap r) • m) = r • φ m
          rw [hsmul, Algebra.smul_def]
          exact congrArg (· * φ m) (germToFunctionField_algebraMap' x U r)) }
      : Γ(M, U) →ₗ[K] ↥(lSpaceOn (placesOf x U) D))
    ⟨fun m m' h => hinj (congrArg Subtype.val h),
     fun ⟨f, hf⟩ => by
      have : f ∈ Set.range φ := by rw [hrange]; exact hf
      obtain ⟨m, rfl⟩ := this
      exact ⟨m, rfl⟩⟩
theorem

coe_sectionsEquivLSpaceOn_apply

L149 ↗
AlgebraicCurves.Cohomology.Proofs.Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn.AlgebraicCurve.coe_sectionsEquivLSpaceOn_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs
namespace Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
variable {K : Type u} [Field K] {X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of K)) [IsIntegral X]
Lean source · full declaration
theorem coe_sectionsEquivLSpaceOn_apply (M : X.Modules) (U : X.Opens) [Nonempty U]
    (D : letI := (baseToFunctionField x).toAlgebra; Divisor K X.functionField)
    (φ : Γ(M, U) →+ (X.functionField : Type u))
    (hsmul : ∀ (a : Γ(X, U)) (m : Γ(M, U)), φ (a • m) = algebraMap Γ(X, U) X.functionField a * φ m)
    (hinj : Function.Injective φ)
    (hrange : letI := (baseToFunctionField x).toAlgebra
      Set.range φ = (lSpaceOn (placesOf x U) D : Set X.functionField)) (m : Γ(M, U)) :
    letI := Scheme.TwoAffineOpenCover.moduleSectionsOfHom x M U
    letI := (baseToFunctionField x).toAlgebra
    ((sectionsEquivLSpaceOn x M U D φ hsmul hinj hrange m : ↥(lSpaceOn (placesOf x U) D)) :
      X.functionField)
      = φ m := rfl
theorem

nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq

L162 ↗
AlgebraicCurves.Cohomology.Proofs.Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn.AlgebraicCurve.nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs
namespace Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
variable {K : Type u} [Field K] {X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of K)) [IsIntegral X]
Lean source · full declaration
theorem nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq
    (𝒱 : X.TwoAffineOpenCover) [IsSeparated x] [SmoothOfRelativeDimension 1 x]
    (h0 : Nonempty 𝒱.U0) (h1 : Nonempty 𝒱.U1) (M : X.Modules)
    (D : letI := (baseToFunctionField x).toAlgebra; Divisor K X.functionField)
    (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
    (hnat : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
      ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m)
    (hsmul : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
      φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
    (hinj : ∀ U : X.Opens, Nonempty U → Function.Injective (φ U))
    (hrange : letI := (baseToFunctionField x).toAlgebra
      ∀ U : X.Opens, IsAffineOpen U → Nonempty U →
        Set.range (φ U) = (lSpaceOn (placesOf x U) D : Set X.functionField)) :
    letI := (baseToFunctionField x).toAlgebra
    Nonempty ((𝒱.sectionsOf x M).H0 ≃ₗ[K] ↥(cechH0 (placesOf x 𝒱.U0) (placesOf x 𝒱.U1) D)) ∧
      Nonempty ((𝒱.sectionsOf x M).H1 ≃ₗ[K] cechH1 (placesOf x 𝒱.U0) (placesOf x 𝒱.U1) D) := by
  let := (baseToFunctionField x).toAlgebra
  have := h0
  have := h1
  have h01 : Nonempty (𝒱.U0 ⊓ 𝒱.U1 : X.Opens) := by
    obtain ⟨⟨u, hu⟩⟩ := h0
    obtain ⟨⟨w, hw⟩⟩ := h1
    obtain ⟨z, hz⟩ := nonempty_preirreducible_inter 𝒱.U0.isOpen 𝒱.U1.isOpen ⟨u, hu⟩ ⟨w, hw⟩
    exact ⟨⟨z, hz⟩⟩
  have hS01 : placesOf x (𝒱.U0 ⊓ 𝒱.U1) = placesOf x 𝒱.U0 ∩ placesOf x 𝒱.U1 := placesOf_inf' x 𝒱.U0
    𝒱.U1
  let := Scheme.TwoAffineOpenCover.algebraOfHom x 𝒱.U0
  let := Scheme.TwoAffineOpenCover.algebraOfHom x 𝒱.U1
  let := Scheme.TwoAffineOpenCover.algebraOfHom x (𝒱.U0 ⊓ 𝒱.U1)
  let : Module K Γ(M, 𝒱.U0) := Scheme.TwoAffineOpenCover.moduleSectionsOfHom x M 𝒱.U0
  let : Module K Γ(M, 𝒱.U1) := Scheme.TwoAffineOpenCover.moduleSectionsOfHom x M 𝒱.U1
  let : Module K Γ(M, 𝒱.U0 ⊓ 𝒱.U1) := Scheme.TwoAffineOpenCover.moduleSectionsOfHom x M (𝒱.U0 ⊓
    𝒱.U1)
  let e0 := sectionsEquivLSpaceOn x M 𝒱.U0 D (φ 𝒱.U0) (fun a m => hsmul 𝒱.U0 a m) (hinj _ h0)
    (hrange _ 𝒱.isAffineOpen_U0 h0)
  let e1 := sectionsEquivLSpaceOn x M 𝒱.U1 D (φ 𝒱.U1) (fun a m => hsmul 𝒱.U1 a m) (hinj _ h1)
    (hrange _ 𝒱.isAffineOpen_U1 h1)
  let e01' := sectionsEquivLSpaceOn x M (𝒱.U0 ⊓ 𝒱.U1) D (φ (𝒱.U0 ⊓ 𝒱.U1)) (fun a m => hsmul _ a m)
    (hinj _ h01) (hrange _ 𝒱.isAffineOpen_inf h01)
  let e01 := e01'.trans (LinearEquiv.ofEq _ _ (by rw [hS01]))
  let ι0 : (𝒱.sectionsOf x M).M0 × (𝒱.sectionsOf x M).M1
      →ₗ[K] ↥(lSpaceOn (placesOf x 𝒱.U0) D) × ↥(lSpaceOn (placesOf x 𝒱.U1) D) :=
    LinearMap.prodMap e0.toLinearMap e1.toLinearMap
  let ι1 : (𝒱.sectionsOf x M).M01 →ₗ[K] ↥(lSpaceOn (placesOf x 𝒱.U0 ∩ placesOf x 𝒱.U1) D) :=
    e01.toLinearMap
  have comm : cechDiff (placesOf x 𝒱.U0) (placesOf x 𝒱.U1) D ∘ₗ ι0 = ι1 ∘ₗ (𝒱.sectionsOf x
    M).cechDiff := by
    apply LinearMap.ext
    intro p
    apply Subtype.ext
    have lhs : ((cechDiff (placesOf x 𝒱.U0) (placesOf x 𝒱.U1) D ∘ₗ ι0) p : X.functionField)
        = φ 𝒱.U1 p.2 - φ 𝒱.U0 p.1 := by
      rw [LinearMap.comp_apply, coe_cechDiff_apply]
      rfl
    have rhs : ((ι1 ∘ₗ (𝒱.sectionsOf x M).cechDiff) p : X.functionField)
        = φ (𝒱.U0 ⊓ 𝒱.U1) ((𝒱.sectionsOf x M).cechDiff p) := rfl
    rw [lhs, rhs, TwoChartCech.Sections.cechDiff_apply]
    have e2 : φ (𝒱.U0 ⊓ 𝒱.U1) ((𝒱.sectionsOf x M).r1 p.2) = φ 𝒱.U1 p.2 := by
      erw [Scheme.TwoAffineOpenCover.sectionsOf_r1_apply]
      exact hnat 𝒱.U1 (𝒱.U0 ⊓ 𝒱.U1) inf_le_right h01 p.2
    have e1 : φ (𝒱.U0 ⊓ 𝒱.U1) ((𝒱.sectionsOf x M).r0 p.1) = φ 𝒱.U0 p.1 := by
      erw [Scheme.TwoAffineOpenCover.sectionsOf_r0_apply]
      exact hnat 𝒱.U0 (𝒱.U0 ⊓ 𝒱.U1) inf_le_left h01 p.1
    have e3 : φ (𝒱.U0 ⊓ 𝒱.U1) ((𝒱.sectionsOf x M).r1 p.2 - (𝒱.sectionsOf x M).r0 p.1)
        = φ (𝒱.U0 ⊓ 𝒱.U1) ((𝒱.sectionsOf x M).r1 p.2) - φ (𝒱.U0 ⊓ 𝒱.U1) ((𝒱.sectionsOf x M).r0
          p.1) :=
      map_sub (φ (𝒱.U0 ⊓ 𝒱.U1)) _ _
    rw [e3, e2, e1]
  have hι0 : Function.Bijective ι0 :=
    ⟨fun a b hab => Prod.ext (e0.injective (congrArg Prod.fst hab)) (e1.injective (congrArg
      Prod.snd hab)),
     fun q => ⟨(e0.symm q.1, e1.symm q.2), Prod.ext (e0.apply_symm_apply q.1) (e1.apply_symm_apply
       q.2)⟩⟩
  have hι1 : Function.Bijective ι1 := e01.bijective
  exact ⟨⟨LinearEquiv.ofBijective _
      (TwoChartCech.kerMap_bijective_of_bijective' ((𝒱.sectionsOf x M).cechDiff)
        (cechDiff (placesOf x 𝒱.U0) (placesOf x 𝒱.U1) D) ι0 ι1 comm hι0 hι1.1)⟩,
    ⟨LinearEquiv.ofBijective _
      (TwoChartCech.cokerMap_bijective_of_bijective' ((𝒱.sectionsOf x M).cechDiff)
        (cechDiff (placesOf x 𝒱.U0) (placesOf x 𝒱.U1) D) ι0 ι1 comm hι0.2 hι1)⟩⟩
theorem

nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn

L248 ↗
AlgebraicCurve.nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs
namespace Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
open _root_.AlgebraicCurves.Cohomology.Proofs in
open _root_.AlgebraicCurve
  Nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn.AlgebraicCurve in
Lean source · full declaration
theorem _root_.AlgebraicCurve.nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq_lSpaceOn
    {K : Type u} [Field K] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (x : X ⟶ Spec
      (CommRingCat.of K))
    [IsIntegral X] [IsSeparated x] [SmoothOfRelativeDimension 1 x]
    (h0 : Nonempty 𝒱.U0) (h1 : Nonempty 𝒱.U1) (M : X.Modules)
    (D : letI := (AlgebraicCurve.baseToFunctionField x).toAlgebra
      AlgebraicCurve.Divisor K X.functionField)
    (φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u))
    (hnat : ∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
      ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m)
    (hsmul : ∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
      φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m)
    (hinj : ∀ U : X.Opens, Nonempty U → Function.Injective (φ U))
    (hrange : letI := (AlgebraicCurve.baseToFunctionField x).toAlgebra
      ∀ U : X.Opens, IsAffineOpen U → Nonempty U →
        Set.range (φ U) = (AlgebraicCurve.lSpaceOn (AlgebraicCurve.placesOf x U) D : Set
          X.functionField)) :
    letI := (AlgebraicCurve.baseToFunctionField x).toAlgebra
    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)
          :=
  nonempty_linearEquiv_cechH0_and_cechH1_sectionsOf_of_range_eq x 𝒱 h0 h1 M D φ hnat
    (fun U _ a m => hsmul U a m) hinj hrange

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.