Module

Scheme_Modules_isZero_of_forall_exists_isZero_pullback_obj.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isZero_of_forall_exists_isZero_pullback_obj

2 declarations indexed from sourceView source ↗

Module documentation

Vanishing of modules detected by pullback

Detects a zero module from vanishing pullbacks on a family covering all points.

Imports4

Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Mathlib.Tactic.Choose

Imported by2

lemma

sections_eq_zero_of_isZero_pullback_ι

L49 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isZero_of_forall_exists_isZero_pullback_obj.AlgebraicGeometry.Scheme.Modules.sections_eq_zero_of_isZero_pullback_ι

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isZero_of_forall_exists_isZero_pullback_obj
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
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
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}

Lean source · statement

lemma sections_eq_zero_of_isZero_pullback_ι {M : X.Modules} (U : X.Opens)
    (hU : IsZero ((Scheme.Modules.pullback U.ι).obj M)) (W : X.Opens) (hWU : W ≤ U)
    (s : Γ(M, W)) : s = 0

theorem

isZero_of_forall_exists_isZero_pullback_obj

L73 ↗

AlgebraicGeometry.Scheme.Modules.isZero_of_forall_exists_isZero_pullback_obj