NYLL
Module

Scheme_Modules_isIso_fromTildeGamma_of_locallyTrivial.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_fromTildeGamma_of_locallyTrivial
1 declaration indexed from sourceView source ↗

Module documentation

Affine comparison for locally trivial modules

Proves that the global-sections comparison is an isomorphism for locally trivial modules.

The tilde comparison is an isomorphism for locally trivial modules.

Imports3
Imported by7

Declarations

theorem

isIso_fromTildeGamma_of_locallyTrivial

L35 ↗
AlgebraicGeometry.Scheme.Modules.isIso_fromTildeGamma_of_locallyTrivial
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_of_locallyTrivial
universe u
open CategoryTheory AlgebraicGeometry
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.isIso_fromTildeGamma_of_locallyTrivial
    {R : CommRingCat.{u}} (M : (Spec (.of R)).Modules)
    (htriv : ∀ x : Spec (.of R), ∃ (V : (Spec (.of R)).Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit
        V.toScheme.ringCatSheaf)) :
    IsIso M.fromTildeΓ

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