NYLL
Module

Exists_linearEquiv_structureSheafH1_cechH1.lean

Nyll.AlgebraicCurves.Cohomology.Exists_linearEquiv_structureSheafH1_cechH1
13 declarations indexed from sourceView source ↗

Module documentation

Exists linear Equiv structure Sheaf H1 cech H1

Imports10
Imported by1

Declarations

theorem

kerMap_bijective_of_bijective

L54 ↗
AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech.TwoChartCech.kerMap_bijective_of_bijective
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech
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 TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
universe uR uK uC
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

L70 ↗
AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech.TwoChartCech.cokerMap_bijective_of_bijective
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech
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 TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
universe uR uK uC
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

L98 ↗
AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech.AlgebraicCurve.placesOf_inf
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech
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 Opposite TopologicalSpace
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K)) [IsIntegral C]
Lean source · full declaration
theorem placesOf_inf [IsSeparated c] [SmoothOfRelativeDimension 1 c] (U V : C.Opens) :
    letI := (baseToFunctionField c).toAlgebra
    placesOf c (U ⊓ V) = placesOf c U ∩ placesOf c V := by
  let := (baseToFunctionField c).toAlgebra
  apply Set.Subset.antisymm
  · exact fun v hv => ⟨placesOf_mono c inf_le_left hv, placesOf_mono c inf_le_right hv⟩
  · rintro v ⟨⟨x, hxU, hx, hvx⟩, ⟨y, hyV, -, hvy⟩⟩
    have hxy : x = y := eq_of_range_stalk_eq c x y (hvx.trans hvy.symm)
    subst hxy
    exact ⟨x, ⟨hxU, hyV⟩, hx, hvx⟩
theorem

germToFunctionField_algebraMap

L109 ↗
AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech.AlgebraicCurve.germToFunctionField_algebraMap
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech
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 Opposite TopologicalSpace
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K)) [IsIntegral C]
Lean source · statement
theorem germToFunctionField_algebraMap (U : C.Opens) [Nonempty U] (r : K) :
    (C.germToFunctionField U).hom ((Scheme.TwoAffineOpenCover.algebraOfHom c U).algebraMap r)
      = baseToFunctionField c r
theorem

germToFunctionField_map

L122 ↗
AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech.AlgebraicCurve.germToFunctionField_map
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech
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 Opposite TopologicalSpace
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K)) [IsIntegral C]
omit [IsIntegral C] in
Lean source · statement
theorem germToFunctionField_map [IrreducibleSpace C] {U V : C.Opens} [Nonempty U] [Nonempty V]
    (h : V ≤ U) (s : Γ(C, U)) :
    (C.germToFunctionField V).hom ((C.presheaf.map (homOfLE h).op).hom s)
      = (C.germToFunctionField U).hom s
def

germLinear

L131 ↗
AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech.AlgebraicCurve.germLinear
Documentation

The generic-point germ as a linear map from sections to the function field.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech
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 Opposite TopologicalSpace
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K)) [IsIntegral C]
Lean source · full declaration
def germLinear (U : C.Opens) [Nonempty U] :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
    letI := (baseToFunctionField c).toAlgebra
    Γ(C, U) →ₗ[K] C.functionField :=
  letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
  letI := (baseToFunctionField c).toAlgebra
  { toFun := (C.germToFunctionField U).hom
    map_add' := fun x y => map_add _ x y
    map_smul' := fun r s => by
      rw [Algebra.smul_def, map_mul, germToFunctionField_algebraMap, RingHom.id_apply,
        Algebra.smul_def]
      rfl }
theorem

germLinear_apply

L144 ↗
AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech.AlgebraicCurve.germLinear_apply
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech
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 Opposite TopologicalSpace
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K)) [IsIntegral C]
Lean source · statement
theorem germLinear_apply (U : C.Opens) [Nonempty U] (s : Γ(C, U)) :
    germLinear c U s = (C.germToFunctionField U).hom s
theorem

range_germ_eq_lSpaceOn

L147 ↗
AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech.AlgebraicCurve.range_germ_eq_lSpaceOn
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech
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 Opposite TopologicalSpace
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K)) [IsIntegral C]
Lean source · full declaration
theorem range_germ_eq_lSpaceOn (U : C.Opens) [Nonempty U]
    (hsec : letI := (baseToFunctionField c).toAlgebra
      (C.germToFunctionField U).hom.range = ⨅ v ∈ placesOf c U, v.toValuationSubring.toSubring) :
    letI := (baseToFunctionField c).toAlgebra
    Set.range (germLinear c U) = (lSpaceOn (placesOf c U) (0 : Divisor K C.functionField) : Set
      C.functionField) := by
  let := (baseToFunctionField c).toAlgebra
  ext f
  have h1 : f ∈ Set.range (germLinear c U) ↔ f ∈ (C.germToFunctionField U).hom.range := by
    simp only [Set.mem_range, RingHom.mem_range, germLinear_apply]
  rw [h1, hsec, SetLike.mem_coe, mem_lSpaceOn_iff]
  simp only [Subring.mem_iInf, Finsupp.coe_zero, Pi.zero_apply, WithZero.exp_zero]
  refine forall₂_congr fun v _ => ?_
  exact (Place.mem_iff_adicValuation_le_one v)
def

germEquiv

L163 ↗
AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech.AlgebraicCurve.germEquiv
Documentation

Identify sections with the zero-divisor valuation space using the given germ range.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech
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 Opposite TopologicalSpace
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K)) [IsIntegral C]
Lean source · full declaration
def germEquiv (U : C.Opens) [Nonempty U]
    (hsec : letI := (baseToFunctionField c).toAlgebra
      (C.germToFunctionField U).hom.range = ⨅ v ∈ placesOf c U, v.toValuationSubring.toSubring) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
    letI := (baseToFunctionField c).toAlgebra
    Γ(C, U) ≃ₗ[K] ↥(lSpaceOn (placesOf c U) (0 : Divisor K C.functionField)) :=
  letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
  letI := (baseToFunctionField c).toAlgebra
  LinearEquiv.ofBijective
    (LinearMap.codRestrict _ (germLinear c U) (fun s => by
      have : germLinear c U s ∈ Set.range (germLinear c U) := ⟨s, rfl⟩
      rw [range_germ_eq_lSpaceOn c U hsec] at this
      exact this))
    ⟨fun x y hxy => Scheme.germToFunctionField_injective C U (congrArg Subtype.val hxy),
     fun ⟨f, hf⟩ => by
      have : f ∈ Set.range (germLinear c U) := by rw [range_germ_eq_lSpaceOn c U hsec]; exact hf
      obtain ⟨s, rfl⟩ := this
      exact ⟨s, rfl⟩⟩
theorem

coe_germEquiv_apply

L182 ↗
AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech.AlgebraicCurve.coe_germEquiv_apply
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech
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 Opposite TopologicalSpace
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K)) [IsIntegral C]
Lean source · full declaration
theorem coe_germEquiv_apply (U : C.Opens) [Nonempty U]
    (hsec : letI := (baseToFunctionField c).toAlgebra
      (C.germToFunctionField U).hom.range = ⨅ v ∈ placesOf c U, v.toValuationSubring.toSubring)
    (s : Γ(C, U)) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom c U
    letI := (baseToFunctionField c).toAlgebra
    ((germEquiv c U hsec s : ↥(lSpaceOn (placesOf c U) (0 : Divisor K C.functionField))) :
      C.functionField)
      = (C.germToFunctionField U).hom s := rfl
theorem

germ_mem_lSpaceOn_inter

L192 ↗
AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech.AlgebraicCurve.germ_mem_lSpaceOn_inter
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech
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 Opposite TopologicalSpace
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K)) [IsIntegral C]
Lean source · full declaration
theorem germ_mem_lSpaceOn_inter [IsSeparated c] [SmoothOfRelativeDimension 1 c]
    (𝒱 : C.TwoAffineOpenCover) [Nonempty (𝒱.U0 ⊓ 𝒱.U1 : C.Opens)] (s : (𝒱.cover c).A01) :
    letI := (baseToFunctionField c).toAlgebra
    (C.germToFunctionField (𝒱.U0 ⊓ 𝒱.U1)).hom s ∈
      lSpaceOn (placesOf c 𝒱.U0 ∩ placesOf c 𝒱.U1) (0 : Divisor K C.functionField) := by
  let := (baseToFunctionField c).toAlgebra
  have hsec : (C.germToFunctionField (𝒱.U0 ⊓ 𝒱.U1)).hom.range
      = ⨅ v ∈ placesOf c (𝒱.U0 ⊓ 𝒱.U1), v.toValuationSubring.toSubring :=
    range_algebraMap_functionField_eq_iInf_of_isAffineOpen c (𝒱.U0 ⊓ 𝒱.U1) 𝒱.isAffineOpen_inf
  have h : (C.germToFunctionField (𝒱.U0 ⊓ 𝒱.U1)).hom s ∈ Set.range (germLinear c (𝒱.U0 ⊓ 𝒱.U1)) :=
    ⟨s, rfl⟩
  rw [range_germ_eq_lSpaceOn c (𝒱.U0 ⊓ 𝒱.U1) hsec, SetLike.mem_coe, placesOf_inf c 𝒱.U0 𝒱.U1] at h
  exact h
theorem

exists_linearEquiv_structureSheafH1_cechH1'

L206 ↗
AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech.AlgebraicCurve.exists_linearEquiv_structureSheafH1_cechH1'
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech
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 Opposite TopologicalSpace
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K)) [IsIntegral C]
Lean source · full declaration
theorem exists_linearEquiv_structureSheafH1_cechH1' [IsSeparated c] [SmoothOfRelativeDimension 1 c]
    (𝒱 : C.TwoAffineOpenCover) (h0 : Nonempty 𝒱.U0) (h1 : Nonempty 𝒱.U1) :
    letI := (baseToFunctionField c).toAlgebra
    (∀ [Nonempty (𝒱.U0 ⊓ 𝒱.U1 : C.Opens)] (s : (𝒱.cover c).A01),
        (C.germToFunctionField (𝒱.U0 ⊓ 𝒱.U1)).hom s ∈
          lSpaceOn (placesOf c 𝒱.U0 ∩ placesOf c 𝒱.U1) (0 : Divisor K C.functionField)) ∧
      ∃ e : (𝒱.structureSheafSections c).H1 ≃ₗ[K]
          cechH1 (placesOf c 𝒱.U0) (placesOf c 𝒱.U1) (0 : Divisor K C.functionField),
        ∀ [Nonempty (𝒱.U0 ⊓ 𝒱.U1 : C.Opens)] (s : (𝒱.cover c).A01)
          (hs : (C.germToFunctionField (𝒱.U0 ⊓ 𝒱.U1)).hom s ∈
            lSpaceOn (placesOf c 𝒱.U0 ∩ placesOf c 𝒱.U1) (0 : Divisor K C.functionField)),
          e (Submodule.Quotient.mk s) =
            Submodule.Quotient.mk ⟨(C.germToFunctionField (𝒱.U0 ⊓ 𝒱.U1)).hom s, hs⟩ := by
  let := (baseToFunctionField c).toAlgebra
  have := h0
  have := h1
  have h01' : ((𝒱.U0 ⊓ 𝒱.U1 : C.Opens) : Set C).Nonempty :=
    nonempty_preirreducible_inter 𝒱.U0.isOpen 𝒱.U1.isOpen
      (Set.nonempty_coe_sort.mp h0) (Set.nonempty_coe_sort.mp h1)
  have h01 : Nonempty (𝒱.U0 ⊓ 𝒱.U1 : C.Opens) := h01'.to_subtype
  refine ⟨fun s => germ_mem_lSpaceOn_inter c 𝒱 s, ?_⟩
  have hS01 : placesOf c (𝒱.U0 ⊓ 𝒱.U1) = placesOf c 𝒱.U0 ∩ placesOf c 𝒱.U1 :=
    placesOf_inf c 𝒱.U0 𝒱.U1
  have hsec' : ∀ (U : C.Opens), IsAffineOpen U → ∀ [Nonempty U],
      (C.germToFunctionField U).hom.range = ⨅ v ∈ placesOf c U, v.toValuationSubring.toSubring :=
    fun U hU _ => range_algebraMap_functionField_eq_iInf_of_isAffineOpen c U hU
  let e0 := germEquiv c 𝒱.U0 (hsec' _ 𝒱.isAffineOpen_U0)
  let e1 := germEquiv c 𝒱.U1 (hsec' _ 𝒱.isAffineOpen_U1)
  let e01' := germEquiv c (𝒱.U0 ⊓ 𝒱.U1) (hsec' _ 𝒱.isAffineOpen_inf)
  have hL01 : lSpaceOn (placesOf c (𝒱.U0 ⊓ 𝒱.U1)) (0 : Divisor K C.functionField)
      = lSpaceOn (placesOf c 𝒱.U0 ∩ placesOf c 𝒱.U1) 0 := by rw [hS01]
  let e01 := e01'.trans (LinearEquiv.ofEq _ _ hL01)
  let := Scheme.TwoAffineOpenCover.algebraOfHom c 𝒱.U0
  let := Scheme.TwoAffineOpenCover.algebraOfHom c 𝒱.U1
  let := Scheme.TwoAffineOpenCover.algebraOfHom c (𝒱.U0 ⊓ 𝒱.U1)
  let ι0 : Γ(C, 𝒱.U0) × Γ(C, 𝒱.U1)
      →ₗ[K] ↥(lSpaceOn (placesOf c 𝒱.U0) (0 : Divisor K C.functionField))
        × ↥(lSpaceOn (placesOf c 𝒱.U1) (0 : Divisor K C.functionField)) :=
    LinearMap.prodMap e0.toLinearMap e1.toLinearMap
  let ι1 : Γ(C, 𝒱.U0 ⊓ 𝒱.U1)
      →ₗ[K] ↥(lSpaceOn (placesOf c 𝒱.U0 ∩ placesOf c 𝒱.U1) (0 : Divisor K C.functionField)) :=
    e01.toLinearMap
  have comm : cechDiff (placesOf c 𝒱.U0) (placesOf c 𝒱.U1) 0 ∘ₗ ι0
      = ι1 ∘ₗ (𝒱.structureSheafSections c).cechDiff := by
    apply LinearMap.ext
    intro p
    apply Subtype.ext
    have lhs : ((cechDiff (placesOf c 𝒱.U0) (placesOf c 𝒱.U1) 0 ∘ₗ ι0) p : C.functionField)
        = (C.germToFunctionField 𝒱.U1).hom p.2 - (C.germToFunctionField 𝒱.U0).hom p.1 := by
      rw [LinearMap.comp_apply, coe_cechDiff_apply]
      rfl
    have rhs : ((ι1 ∘ₗ (𝒱.structureSheafSections c).cechDiff) p : C.functionField)
        = (C.germToFunctionField (𝒱.U0 ⊓ 𝒱.U1)).hom ((𝒱.structureSheafSections c).cechDiff p) := rfl
    rw [lhs]
    refine Eq.trans ?_ rhs.symm
    erw [TwoChartCech.Sections.cechDiff_apply, TwoChartCech.Cover.lineBundle_r1_apply,
      TwoChartCech.Cover.lineBundle_r0_apply, Units.val_one, one_mul]
    change _ = (C.germToFunctionField (𝒱.U0 ⊓ 𝒱.U1)).hom
        (((C.presheaf.map (homOfLE inf_le_right).op).hom p.2 : Γ(C, 𝒱.U0 ⊓ 𝒱.U1))
          - (C.presheaf.map (homOfLE inf_le_left).op).hom p.1)
    rw [← germToFunctionField_map (C := C) (inf_le_right : 𝒱.U0 ⊓ 𝒱.U1 ≤ 𝒱.U1) p.2,
      ← germToFunctionField_map (C := C) (inf_le_left : 𝒱.U0 ⊓ 𝒱.U1 ≤ 𝒱.U0) p.1]
    exact (map_sub _ _ _).symm
  have hι0 : Function.Bijective ι0 :=
    ⟨fun x y hxy => Prod.ext (e0.injective (congrArg Prod.fst hxy)) (e1.injective (congrArg
      Prod.snd hxy)),
     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
  refine ⟨LinearEquiv.ofBijective _
      (TwoChartCech.cokerMap_bijective_of_bijective ((𝒱.structureSheafSections c).cechDiff)
        (cechDiff (placesOf c 𝒱.U0) (placesOf c 𝒱.U1) 0) ι0 ι1 comm hι0.2 hι1), ?_⟩
  intro _ s hs
  change Submodule.Quotient.mk (ι1 s) = Submodule.Quotient.mk _
  congr 1
theorem

exists_linearEquiv_structureSheafH1_cechH1

L286 ↗
AlgebraicCurve.exists_linearEquiv_structureSheafH1_cechH1
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech
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_.AlgebraicCurve
  _root_.AlgebraicCurves.Cohomology.Proofs.ExistsEquivStructureSheafH1Cech.AlgebraicCurve in
Lean source · full declaration
theorem _root_.AlgebraicCurve.exists_linearEquiv_structureSheafH1_cechH1 {K : Type u} [Field K] {C
  : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (CommRingCat.of K))
    [IsIntegral C] [IsSeparated c] [SmoothOfRelativeDimension 1 c]
    (h0 : Nonempty 𝒱.U0) (h1 : Nonempty 𝒱.U1) :
    letI := (AlgebraicCurve.baseToFunctionField c).toAlgebra
    (∀ [Nonempty (𝒱.U0 ⊓ 𝒱.U1 : C.Opens)] (s : (𝒱.cover c).A01),
        (C.germToFunctionField (𝒱.U0 ⊓ 𝒱.U1)).hom s ∈
          AlgebraicCurve.lSpaceOn (AlgebraicCurve.placesOf c 𝒱.U0 ∩ AlgebraicCurve.placesOf c 𝒱.U1)
            (0 : AlgebraicCurve.Divisor K C.functionField)) ∧
      ∃ e : (𝒱.structureSheafSections c).H1 ≃ₗ[K]
          AlgebraicCurve.cechH1 (AlgebraicCurve.placesOf c 𝒱.U0) (AlgebraicCurve.placesOf c 𝒱.U1)
            (0 : AlgebraicCurve.Divisor K C.functionField),
        ∀ [Nonempty (𝒱.U0 ⊓ 𝒱.U1 : C.Opens)] (s : (𝒱.cover c).A01)
          (hs : (C.germToFunctionField (𝒱.U0 ⊓ 𝒱.U1)).hom s ∈
            AlgebraicCurve.lSpaceOn (AlgebraicCurve.placesOf c 𝒱.U0 ∩ AlgebraicCurve.placesOf c
              𝒱.U1)
              (0 : AlgebraicCurve.Divisor K C.functionField)),
          e (Submodule.Quotient.mk s) =
            Submodule.Quotient.mk ⟨(C.germToFunctionField (𝒱.U0 ⊓ 𝒱.U1)).hom s, hs⟩ :=
  exists_linearEquiv_structureSheafH1_cechH1' c 𝒱 h0 h1

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