NYLL
Module

Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero
12 declarations indexed from sourceView source ↗

Module documentation

Function-field sections of the unit module

The unit module embeds in the function field of a smooth integral curve. On each affine open, its image is the Riemann-Roch space for the zero divisor.

Imports9
Imported by4

Declarations

abbrev

OU

L66 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero.AlgebraicGeometry.Scheme.Modules.UnitFF.OU
Documentation

The structure sheaf viewed as the tensor unit of sheaves of modules on X.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero
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 _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace UnitFF
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open AlgebraicCurve TopologicalSpace Opposite
variable {K : Type u} [Field K] {X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of K)) [IsIntegral X]
Lean source · statement
abbrev OU (X : Scheme.{u}) : X.Modules
theorem

smul_eq

L68 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero.AlgebraicGeometry.Scheme.Modules.UnitFF.smul_eq
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero
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 _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace UnitFF
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open AlgebraicCurve TopologicalSpace Opposite
variable {K : Type u} [Field K] {X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of K)) [IsIntegral X]
omit [IsIntegral X] in
Lean source · full declaration
theorem smul_eq (U : X.Opens) (a : Γ(X, U)) (m : Γ(OU X, U)) :
    (show Γ(X, U) from a • m) = a * (show Γ(X, U) from m) := rfl
theorem

map_eq

L71 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero.AlgebraicGeometry.Scheme.Modules.UnitFF.map_eq
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero
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 _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace UnitFF
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open AlgebraicCurve TopologicalSpace Opposite
variable {K : Type u} [Field K] {X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of K)) [IsIntegral X]
omit [IsIntegral X] in
Lean source · full declaration
theorem map_eq {U V : X.Opens} (h : V ≤ U) (m : Γ(OU X, U)) :
    (show Γ(X, V) from (OU X).presheaf.map (homOfLE h).op m) = X.presheaf.map (homOfLE h).op
        (show Γ(X, U) from m) :=
  rfl
def

φ

L77 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero.AlgebraicGeometry.Scheme.Modules.UnitFF.φ
Documentation

The germ of a unit section in the function field, extended by zero on the empty open.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero
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 _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace UnitFF
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open AlgebraicCurve TopologicalSpace Opposite
variable {K : Type u} [Field K] {X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of K)) [IsIntegral X]
Lean source · statement
def φ (U : X.Opens) : Γ(OU X, U) →+ (X.functionField : Type u)
theorem

φ_apply

L86 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero.AlgebraicGeometry.Scheme.Modules.UnitFF.φ_apply
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero
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 _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace UnitFF
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open AlgebraicCurve TopologicalSpace Opposite
variable {K : Type u} [Field K] {X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of K)) [IsIntegral X]
Lean source · full declaration
theorem φ_apply (U : X.Opens) [h : Nonempty U] (m : Γ(OU X, U)) :
    φ U m = (X.germToFunctionField U).hom (show Γ(X, U) from m) := by
  simp only [φ, dite_eq_left h]
  rfl
theorem

φ_nat

L91 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero.AlgebraicGeometry.Scheme.Modules.UnitFF.φ_nat
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero
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 _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace UnitFF
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open AlgebraicCurve TopologicalSpace Opposite
variable {K : Type u} [Field K] {X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of K)) [IsIntegral X]
Lean source · statement
theorem φ_nat {U V : X.Opens} (h : V ≤ U) [Nonempty U] [Nonempty V] (m : Γ(OU X, U)) :
    φ V ((OU X).presheaf.map (homOfLE h).op m) = φ U m
theorem

φ_smul

L98 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero.AlgebraicGeometry.Scheme.Modules.UnitFF.φ_smul
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero
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 _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace UnitFF
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open AlgebraicCurve TopologicalSpace Opposite
variable {K : Type u} [Field K] {X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of K)) [IsIntegral X]
Lean source · statement
theorem φ_smul (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(OU X, U)) :
    φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m
theorem

φ_injective

L103 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero.AlgebraicGeometry.Scheme.Modules.UnitFF.φ_injective
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero
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 _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace UnitFF
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open AlgebraicCurve TopologicalSpace Opposite
variable {K : Type u} [Field K] {X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of K)) [IsIntegral X]
Lean source · statement
theorem φ_injective (U : X.Opens) [Nonempty U] : Function.Injective (φ (X := X) U)
theorem

range_φ

L108 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero.AlgebraicGeometry.Scheme.Modules.UnitFF.range_φ
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero
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 _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace UnitFF
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open AlgebraicCurve TopologicalSpace Opposite
variable {K : Type u} [Field K] {X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of K)) [IsIntegral X]
Lean source · full declaration
theorem range_φ [SmoothOfRelativeDimension 1 x] (U : X.Opens) (hU : IsAffineOpen U) [Nonempty U] :
    letI := (baseToFunctionField x).toAlgebra
    Set.range (φ (X := X) U) = (lSpaceOn (placesOf x U) (0 : Divisor K X.functionField) : Set
        X.functionField) := by
  let := (baseToFunctionField x).toAlgebra
  have hsec := range_algebraMap_functionField_eq_iInf_of_isAffineOpen x U hU
  ext f
  have h1 : f ∈ Set.range (φ (X := X) U) ↔ f ∈ (algebraMap Γ(X, U) X.functionField).range := by
    simp only [Set.mem_range, RingHom.mem_range]
    constructor
    · rintro ⟨m, rfl⟩
      exact ⟨show Γ(X, U) from m, by rw [φ_apply]; rfl⟩
    · rintro ⟨a, rfl⟩
      exact ⟨show Γ(OU X, U) from a, by rw [φ_apply]; rfl⟩
  rw [h1, hsec, SetLike.mem_coe, mem_lSpaceOn_iff]
  simp only [Subring.mem_iInf, Finsupp.coe_zero, Pi.zero_apply, WithZero.exp_zero]
  constructor
  · intro hf v hv
    exact (Place.mem_iff_adicValuation_le_one v).mp (hf v hv)
  · intro hf v hv
    exact (Place.mem_iff_adicValuation_le_one v).mpr (hf v hv)
instance

nativeUnitSectionsModule

L132 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero.nativeUnitSectionsModule
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero
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 _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
Lean source · statement
instance nativeUnitSectionsModule (X : Scheme.{u}) (U : X.Opens) :
    Module Γ(X, U) Γ((SheafOfModules.unit X.ringCatSheaf : X.Modules), U)
theorem

exists_unit_range_eq_lSpaceOn_zero'

L153 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero.AlgebraicGeometry.Scheme.Modules.exists_unit_range_eq_lSpaceOn_zero'
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero
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 _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
noncomputable local instance nativeUnitSectionsModule (X : Scheme.{u}) (U : X.Opens) :
    Module Γ(X, U) Γ((SheafOfModules.unit X.ringCatSheaf : X.Modules), U) :=
  ((SheafOfModules.unit X.ringCatSheaf : X.Modules).val.obj (Opposite.op U)).isModule
with_weak_namespace _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
with_weak_namespace Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero
open scoped AlgebraicGeometry in
with_weak_namespace AlgebraicGeometry
open scoped Scheme in
with_weak_namespace Scheme
open scoped Modules in
with_weak_namespace _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
with_weak_namespace Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero
open AlgebraicGeometry.Scheme.Modules.UnitFF in
Lean source · full declaration
theorem AlgebraicGeometry.Scheme.Modules.exists_unit_range_eq_lSpaceOn_zero'
    {K : Type u} [Field K] {X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of K))
    [IsIntegral X] [SmoothOfRelativeDimension 1 x] :
    letI := (AlgebraicCurve.baseToFunctionField x).toAlgebra
    ∃ φ : ∀ U : X.Opens, Γ((SheafOfModules.unit X.ringCatSheaf : X.Modules), U) →+
        (X.functionField : Type u),
      (∀ (U : X.Opens) [Nonempty U] (m : Γ((SheafOfModules.unit X.ringCatSheaf : X.Modules), U)),
          φ U m = (X.germToFunctionField U).hom (show Γ(X, U) from m)) ∧
      (∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
          ∀ m : Γ((SheafOfModules.unit X.ringCatSheaf : X.Modules), U),
            φ V ((Scheme.Modules.presheaf (SheafOfModules.unit X.ringCatSheaf : X.Modules)).map
                (homOfLE h).op m)
              = φ U m) ∧
      (∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ((SheafOfModules.unit X.ringCatSheaf :
          X.Modules), U)),
          φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m) ∧
      (∀ U : X.Opens, Nonempty U → Function.Injective (φ U)) ∧
      (∀ U : X.Opens, IsAffineOpen U → Nonempty U →
          Set.range (φ U) = (AlgebraicCurve.lSpaceOn (AlgebraicCurve.placesOf x U)
            (0 : AlgebraicCurve.Divisor K X.functionField) : Set X.functionField)) := by
  let := (AlgebraicCurve.baseToFunctionField x).toAlgebra
  refine ⟨fun U => φ U, fun U _ m => φ_apply U m, ?_, fun U _ a m => φ_smul U a m,
    fun U hU => by
      have := hU
      exact φ_injective U, fun U hU hne => by
      have := hne
      exact range_φ x U hU⟩
  intro U V h hV m
  have := hV
  have : Nonempty U := let ⟨⟨z, hz⟩⟩ := hV; ⟨⟨z, h hz⟩⟩
  exact φ_nat h m
theorem

exists_unit_range_eq_lSpaceOn_zero

L186 ↗
AlgebraicGeometry.Scheme.Modules.exists_unit_range_eq_lSpaceOn_zero
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unit_range_eq_lSpaceOn_zero
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 _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
noncomputable local instance nativeUnitSectionsModule (X : Scheme.{u}) (U : X.Opens) :
    Module Γ(X, U) Γ((SheafOfModules.unit X.ringCatSheaf : X.Modules), U) :=
  ((SheafOfModules.unit X.ringCatSheaf : X.Modules).val.obj (Opposite.op U)).isModule
open AlgebraicGeometry.Scheme.Modules.UnitFF in
Lean source · full declaration
theorem _root_.AlgebraicGeometry.Scheme.Modules.exists_unit_range_eq_lSpaceOn_zero
    {K : Type u} [Field K] {X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of K))
    [IsIntegral X] [SmoothOfRelativeDimension 1 x] :
    letI := (AlgebraicCurve.baseToFunctionField x).toAlgebra
    ∃ φ : ∀ U : X.Opens, Γ((SheafOfModules.unit X.ringCatSheaf : X.Modules), U) →+
        (X.functionField : Type u),
      (∀ (U : X.Opens) [Nonempty U] (m : Γ((SheafOfModules.unit X.ringCatSheaf : X.Modules), U)),
          φ U m = (X.germToFunctionField U).hom (show Γ(X, U) from m)) ∧
      (∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
          ∀ m : Γ((SheafOfModules.unit X.ringCatSheaf : X.Modules), U),
            φ V ((Scheme.Modules.presheaf (SheafOfModules.unit X.ringCatSheaf : X.Modules)).map
                (homOfLE h).op m)
              = φ U m) ∧
      (∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ((SheafOfModules.unit X.ringCatSheaf :
          X.Modules), U)),
          φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m) ∧
      (∀ U : X.Opens, Nonempty U → Function.Injective (φ U)) ∧
      (∀ U : X.Opens, IsAffineOpen U → Nonempty U →
          Set.range (φ U) = (AlgebraicCurve.lSpaceOn (AlgebraicCurve.placesOf x U)
            (0 : AlgebraicCurve.Divisor K X.functionField) : Set X.functionField)) :=
  AlgebraicGeometry.Scheme.Modules.exists_unit_range_eq_lSpaceOn_zero' x

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