Module

Scheme_Modules_IsInvertible_eq_zero_of_pullback_map_eq_zero_of_isReduced.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_eq_zero_of_pullback_map_eq_zero_of_isReduced

3 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Is Invertible eq zero of pullback map eq zero of is Reduced

Imports11

Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
Mathlib.AlgebraicGeometry.Properties
Mathlib.AlgebraicGeometry.Restrict
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.Topology.Sheaves.Stalks
Mathlib.CategoryTheory.Adjunction.Basic
Mathlib.CategoryTheory.Adjunction.Additive
Mathlib.Tactic.Ext
Nyll.AlgebraicCurves.Geometry.Picard.Functor
Nyll.AlgebraicCurves.Geometry.Schemes.IsClosedImmersion_app_injective_and_exists_of_app_pullback_eq_of_isReduced

Imported by1

Nyll.AlgebraicCurves.Geometry.Sheaves.All

theorem

app_apply_eq_zero_of_pullback_map_eq_zero

L59 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_eq_zero_of_pullback_map_eq_zero_of_isReduced.AlgebraicGeometry.Vanish2.app_apply_eq_zero_of_pullback_map_eq_zero

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_eq_zero_of_pullback_map_eq_zero_of_isReduced
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Vanish2
open _root_.AlgebraicGeometry

Lean source · statement

theorem app_apply_eq_zero_of_pullback_map_eq_zero {Z V : Scheme.{u}} (g : Z ⟶ V) {A : V.Modules}
    (τ : A ⟶ (SheafOfModules.unit V.ringCatSheaf : V.Modules))
    (h : (Scheme.Modules.pullback g).map τ = 0)
    (W : V.Opens) (a : Γ(A, W)) : g.app W (τ.app W a) = 0

theorem

pullback_morphismRestrict_map_restrictFunctor_map_eq_zero

L103 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_eq_zero_of_pullback_map_eq_zero_of_isReduced.AlgebraicGeometry.Scheme.Modules.pullback_morphismRestrict_map_restrictFunctor_map_eq_zero

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_eq_zero_of_pullback_map_eq_zero_of_isReduced
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open scoped _root_.AlgebraicGeometry in
open scoped _root_.AlgebraicGeometry.Scheme in
open scoped _root_.AlgebraicGeometry.Scheme.Modules in

Lean source · statement

theorem AlgebraicGeometry.Scheme.Modules.pullback_morphismRestrict_map_restrictFunctor_map_eq_zero
    {X Y : Scheme.{u}} (i : Y ⟶ X) (V : X.Opens) {A B : X.Modules} (σ : A ⟶ B)
    (h : (Scheme.Modules.pullback i).map σ = 0) :
    (Scheme.Modules.pullback (i ∣_ V)).map ((Scheme.Modules.restrictFunctor V.ι).map σ) = 0

theorem

eq_zero_of_pullback_map_eq_zero_of_isReduced

L126 ↗

AlgebraicGeometry.Scheme.Modules.IsInvertible.eq_zero_of_pullback_map_eq_zero_of_isReduced

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_eq_zero_of_pullback_map_eq_zero_of_isReduced
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Vanish2 in

Lean source · statement

theorem
  _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.eq_zero_of_pullback_map_eq_zero_of_isReduced
    {X Y₁ Y₂ : Scheme.{u}} [IsReduced X] (i₁ : Y₁ ⟶ X) (i₂ : Y₂ ⟶ X)
    [IsClosedImmersion i₁] [IsClosedImmersion i₂]
    (hcover : Set.range i₁.base ∪ Set.range i₂.base = Set.univ)
    {L : X.Modules} (hL : Scheme.Modules.IsInvertible L)
    (σ : Scheme.Modules.Hom (SheafOfModules.unit X.ringCatSheaf) L)
    (h₁ : (Scheme.Modules.pullback i₁).map σ = 0) (h₂ : (Scheme.Modules.pullback i₂).map σ = 0) :
    σ = (HasZeroMorphisms.zero (C := X.Modules) (SheafOfModules.unit X.ringCatSheaf) L).zero

Module documentation

Scheme Modules Is Invertible eq zero of pullback map eq zero of is Reduced

Declarations

app_apply_eq_zero_of_pullback_map_eq_zero

pullback_morphismRestrict_map_restrictFunctor_map_eq_zero

eq_zero_of_pullback_map_eq_zero_of_isReduced