NYLL
Module

SmoothProperCurve_FiniteMapData_finite_H0_H1_sectionsOf.lean

Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_FiniteMapData_finite_H0_H1_sectionsOf
7 declarations indexed from sourceView source ↗

Module documentation

Finite cohomology from finite-map data on a curve

Finite-map data on a smooth proper curve gives finite zeroth and first two-chart cohomology for a module that is locally trivial.

Imports8
Imported by5

Declarations

abbrev

rO

L62 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_finite_H0_H1_sectionsOf.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.SectionsOfFinite.rO
Documentation

Restriction in the structure sheaf between the specified open subsets.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_sectionsOf
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
namespace SectionsOfFinite
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : FiniteMapData c ε) (M : C.Modules)
  (htriv : ∀ x : C, ∃ (V : C.Opens), x ∈ V ∧
    Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
open AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
abbrev rO {W₁ W₂ : C.Opens} (h : W₂ ≤ W₁) : Γ(C, W₁) → Γ(C, W₂)
theorem

VU_eq_basicOpen_g

L65 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_finite_H0_H1_sectionsOf.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.SectionsOfFinite.VU_eq_basicOpen_g
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_sectionsOf
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
namespace SectionsOfFinite
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : FiniteMapData c ε) (M : C.Modules)
  (htriv : ∀ x : C, ∃ (V : C.Opens), x ∈ V ∧
    Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
open AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
theorem VU_eq_basicOpen_g : 𝔉.V ⊓ 𝔉.U = C.basicOpen 𝔉.g
theorem

VU_eq_basicOpen_f

L66 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_finite_H0_H1_sectionsOf.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.SectionsOfFinite.VU_eq_basicOpen_f
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_sectionsOf
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
namespace SectionsOfFinite
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : FiniteMapData c ε) (M : C.Modules)
  (htriv : ∀ x : C, ∃ (V : C.Opens), x ∈ V ∧
    Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
open AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
theorem VU_eq_basicOpen_f : 𝔉.V ⊓ 𝔉.U = C.basicOpen 𝔉.f
theorem

loc_transport

L68 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_finite_H0_H1_sectionsOf.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.SectionsOfFinite.loc_transport
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_sectionsOf
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
namespace SectionsOfFinite
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : FiniteMapData c ε) (M : C.Modules)
  (htriv : ∀ x : C, ∃ (V : C.Opens), x ∈ V ∧
    Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
open AlgebraicGeometry.Scheme.TwoAffineOpenCover
include htriv in
Lean source · statement
theorem loc_transport {W₁ W₂ : C.Opens} (hW₁ : IsAffineOpen W₁) (h : Γ(C, W₁)) (hW₂ : W₂ =
    C.basicOpen h)
    (hle : W₂ ≤ W₁) :
    (∀ x : Γ(M, W₂), ∃ (n : ℕ) (y : Γ(M, W₁)), M.presheaf.map (homOfLE hle).op y = rO hle h ^ n
        • x) ∧
    (∀ y : Γ(M, W₁), M.presheaf.map (homOfLE hle).op y = 0 → ∃ n : ℕ, (h ^ n : Γ(C, W₁)) • y =
        0)
theorem

finite_adjoin_of_aeval_finite

L82 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_finite_H0_H1_sectionsOf.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.SectionsOfFinite.finite_adjoin_of_aeval_finite
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_sectionsOf
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
namespace SectionsOfFinite
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : FiniteMapData c ε) (M : C.Modules)
  (htriv : ∀ x : C, ∃ (V : C.Opens), x ∈ V ∧
    Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
open AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
theorem finite_adjoin_of_aeval_finite {A : Type u} [CommRing A] [Algebra R A] (f : A)
    (hf : (Polynomial.aeval f : Polynomial R →ₐ[R] A).toRingHom.Finite) :
    Module.Finite (Algebra.adjoin R ({f} : Set A)) A
theorem

finite_H0_H1_sectionsOf'

L107 ↗
AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_finite_H0_H1_sectionsOf.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.finite_H0_H1_sectionsOf'
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_sectionsOf
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open SectionsOfFinite AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
theorem finite_H0_H1_sectionsOf'
    {R : Type u} [CommRing R] [IsNoetherianRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
    {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : SmoothProperCurve.FiniteMapData c ε)
    (M : C.Modules)
    (htriv : ∀ x : C, ∃ (V : C.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit
          V.toScheme.ringCatSheaf)) :
    Module.Finite R (𝔉.twoAffineOpenCover.sectionsOf c M).H0 ∧
      Module.Finite R (𝔉.twoAffineOpenCover.sectionsOf c M).H1
theorem

finite_H0_H1_sectionsOf

L173 ↗
AlgebraicGeometry.SmoothProperCurve.FiniteMapData.finite_H0_H1_sectionsOf
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_sectionsOf
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
Lean source · statement
theorem _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.finite_H0_H1_sectionsOf
    {R : Type u} [CommRing R] [IsNoetherianRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
    {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : SmoothProperCurve.FiniteMapData c ε)
    (M : C.Modules)
    (htriv : ∀ x : C, ∃ (V : C.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit
          V.toScheme.ringCatSheaf)) :
    Module.Finite R (𝔉.twoAffineOpenCover.sectionsOf c M).H0 ∧
      Module.Finite R (𝔉.twoAffineOpenCover.sectionsOf c M).H1

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