NYLL
Module

OModulePresheaf_flat_cochain_ofModules_of_locallyTrivial.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_flat_cochain_ofModules_of_locallyTrivial
2 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf flat cochain of Modules of locally Trivial

Imports5
Imported by7

Declarations

theorem

isAffineOpen_inter

L34 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.FlatCochains.CechFlatSol.isAffineOpen_inter
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.FlatCochains
universe u
section cechflat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
namespace CechFlatSol
Lean source · statement
theorem isAffineOpen_inter {V : Scheme.{u}} [V.IsSeparated] (K : V.OrderedAffineCover) :
    ∀ (n : ℕ) (s : K.Idx n), IsAffineOpen (K.inter s)
theorem

flat_cochain_ofModules_of_locallyTrivial

L62 ↗
AlgebraicGeometry.OModulePresheaf.flat_cochain_ofModules_of_locallyTrivial
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.FlatCochains
universe u
section cechflat
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.flat_cochain_ofModules_of_locallyTrivial
    {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [Flat π] [IsSeparated π] (M
      : V.Modules)
    (htriv : ∀ x : V, ∃ (U : V.Opens), x ∈ U ∧
      Nonempty ((Scheme.Modules.pullback U.ι).obj M ≅ SheafOfModules.unit U.toScheme.ringCatSheaf))
    (K : V.OrderedAffineCover) (i : ℕ) :
    Module.Flat R ((OModulePresheaf.ofModules π M).cochain K i)

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