NYLL
Module

OModulePresheaf_nonempty_sections_top_equiv_H0_ofModules.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_nonempty_sections_top_equiv_H0_ofModules
14 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf nonempty sections top equiv H0 of Modules

Imports8
Imported by4

Declarations

def

chain0

L44 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0.AC3Aux.chain0
Documentation

The constant zero-simplex at the given cover index.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
noncomputable section
namespace AC3Aux
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R)) (M :
  V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
def chain0 (i : K.ι) : K.Idx 0
theorem

idx0_eq

L46 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0.AC3Aux.idx0_eq
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
noncomputable section
namespace AC3Aux
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R)) (M :
  V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
theorem idx0_eq (t : K.Idx 0) : t = chain0 K (t.1 0)
theorem

U_le_inter_chain0

L52 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0.AC3Aux.U_le_inter_chain0
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
noncomputable section
namespace AC3Aux
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R)) (M :
  V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
theorem U_le_inter_chain0 (i : K.ι) : K.U i ≤ K.inter (chain0 K i)
theorem

inter_le_U

L55 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0.AC3Aux.inter_le_U
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
noncomputable section
namespace AC3Aux
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R)) (M :
  V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
theorem inter_le_U (t : K.Idx 0) : K.inter t ≤ K.U (t.1 0)
def

chain1

L58 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0.AC3Aux.chain1
Documentation

The ordered one-simplex associated to two increasing cover indices.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
noncomputable section
namespace AC3Aux
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R)) (M :
  V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
def chain1 {i j : K.ι} (h : i < j) : K.Idx 1
theorem

inf_le_inter_chain1

L61 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0.AC3Aux.inf_le_inter_chain1
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
noncomputable section
namespace AC3Aux
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R)) (M :
  V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
theorem inf_le_inter_chain1 {i j : K.ι} (h : i < j) : K.U i ⊓ K.U j ≤ K.inter (chain1 K h)
abbrev

F

L69 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0.AC3Aux.F
Documentation

The module presheaf of sections of the given sheaf of modules.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
noncomputable section
namespace AC3Aux
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R)) (M :
  V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
abbrev F : OModulePresheaf π
theorem

res_mem_H0

L71 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0.AC3Aux.res_mem_H0
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
noncomputable section
namespace AC3Aux
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R)) (M :
  V.Modules)
  (K : V.OrderedAffineCover)
Lean source · full declaration
theorem res_mem_H0 (x : (F π M).obj ⊤) : (fun s : K.Idx 0 => (F π M).res (le_top : K.inter s ≤ ⊤)
  x) ∈ (F π M).H0 K := by
  rw [LinearMap.mem_ker]
  funext s
  rw [OModulePresheaf.d_apply, Fin.sum_univ_two]
  simp only [Fin.val_zero, pow_zero, one_smul, Fin.val_one, pow_one, neg_smul,
    OModulePresheaf.res_res]
  exact add_neg_cancel _
def

toH0

L81 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0.AC3Aux.toH0
Documentation

The linear map sending a global section to its Čech zero-cocycle.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
noncomputable section
namespace AC3Aux
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R)) (M :
  V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
def toH0 : (F π M).obj ⊤ →ₗ[R] (F π M).H0 K
theorem

toH0_apply

L86 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0.AC3Aux.toH0_apply
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
noncomputable section
namespace AC3Aux
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R)) (M :
  V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
theorem toH0_apply (x : (F π M).obj ⊤) (s : K.Idx 0) : (toH0 π M K x : (F π M).cochain K 0) s = (F
  π M).res le_top x
def

shf

L90 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0.AC3Aux.shf
Documentation

The underlying sheaf of abelian groups of the given sheaf of modules.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
noncomputable section
namespace AC3Aux
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R)) (M :
  V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
def shf : TopCat.Sheaf Ab V.toTopCat
theorem

toH0_injective

L92 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0.AC3Aux.toH0_injective
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
noncomputable section
namespace AC3Aux
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R)) (M :
  V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
theorem toH0_injective : Function.Injective (toH0 π M K)
theorem

toH0_surjective

L103 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0.AC3Aux.toH0_surjective
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
noncomputable section
namespace AC3Aux
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R)) (M :
  V.Modules)
  (K : V.OrderedAffineCover)
Lean source · statement
theorem toH0_surjective : Function.Surjective (toH0 π M K)
theorem

nonempty_sections_top_equiv_H0_ofModules

L170 ↗
AlgebraicGeometry.OModulePresheaf.nonempty_sections_top_equiv_H0_ofModules
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.GlobalSectionsH0
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
open AC3Aux in
Lean source · full declaration
theorem _root_.AlgebraicGeometry.OModulePresheaf.nonempty_sections_top_equiv_H0_ofModules
    {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R))
    (M : V.Modules) (K : V.OrderedAffineCover) :
    letI := Scheme.TwoAffineOpenCover.moduleSectionsOfHom π M ⊤
    Nonempty (Γ(M, ⊤) ≃ₗ[R] (OModulePresheaf.ofModules π M).H0 K) := by
  exact ⟨LinearEquiv.ofBijective (toH0 π M K) ⟨toH0_injective π M K, toH0_surjective π M K⟩⟩

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