NYLL
Module

Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support
9 declarations indexed from sourceView source ↗

Module documentation

Vanishing of a pulled-back section at a field-valued point

An invertible-module section vanishes after pullback to a field-valued point exactly when that point lies in the support of the zero-scheme ideal of the section.

Imports3
Imported by7

Declarations

abbrev

sVal

L54 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support.AlgebraicGeometry.Scheme.Modules.PointVanishing.sVal
Documentation

The local section obtained by evaluating a unit-module morphism on the scalar one.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
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
namespace PointVanishing
variable {X : Scheme.{u}} {N : X.Modules}
Lean source · statement
abbrev sVal (t : 𝟙_ X.Modules ⟶ N) (W : X.Opens) : Γ(N, W)
lemma

map_sVal

L56 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support.AlgebraicGeometry.Scheme.Modules.PointVanishing.map_sVal
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
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
namespace PointVanishing
variable {X : Scheme.{u}} {N : X.Modules}
Lean source · statement
lemma map_sVal (t : 𝟙_ X.Modules ⟶ N) {W V : X.Opens} (i : V ⟶ W) :
    N.presheaf.map i.op (sVal t W) = sVal t V
lemma

eq_smul_one

L64 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support.AlgebraicGeometry.Scheme.Modules.PointVanishing.eq_smul_one
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
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
namespace PointVanishing
variable {X : Scheme.{u}} {N : X.Modules}
Lean source · statement
lemma eq_smul_one (W : X.Opens) (x : Γ(𝟙_ X.Modules, W)) :
    x = ofUnitSection W x • toUnitSection W 1
lemma

eq_zero_iff_sVal_eq_zero

L68 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support.AlgebraicGeometry.Scheme.Modules.PointVanishing.eq_zero_iff_sVal_eq_zero
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
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
namespace PointVanishing
variable {X : Scheme.{u}} {N : X.Modules}
Lean source · statement
lemma eq_zero_iff_sVal_eq_zero (t : 𝟙_ X.Modules ⟶ N) (W₀ : X.Opens) (hW₀ : W₀ = ⊤) :
    t = 0 ↔ sVal t W₀ = 0
lemma

coeff_eq_zero_iff

L82 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support.AlgebraicGeometry.Scheme.Modules.PointVanishing.coeff_eq_zero_iff
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
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
namespace PointVanishing
variable {X : Scheme.{u}} {N : X.Modules}
Lean source · statement
lemma coeff_eq_zero_iff (t : 𝟙_ X.Modules ⟶ N) (U : X.Opens)
    (τ : N.restrict U.ι ≅ 𝟙_ (U : Scheme.{u}).Modules) :
    coeff t U τ.hom = 0 ↔ restrictSection t U = 0
lemma

closedPoint_mem_zeroLocus_span_singleton_iff

L105 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support.AlgebraicGeometry.Scheme.Modules.PointVanishing.closedPoint_mem_zeroLocus_span_singleton_iff
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
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
namespace PointVanishing
variable {X : Scheme.{u}} {N : X.Modules}
variable {k : Type u} [Field k]
Lean source · statement
lemma closedPoint_mem_zeroLocus_span_singleton_iff (c : Γ(Spec (CommRingCat.of k), ⊤)) :
    IsLocalRing.closedPoint k ∈ (Spec (CommRingCat.of k)).zeroLocus (U := ⊤)
        ((Ideal.span {c} : Ideal Γ(Spec (CommRingCat.of k), ⊤)) : Set Γ(Spec (CommRingCat.of k),
            ⊤)) ↔
      c = 0
lemma

eq_zero_iff_closedPoint_mem_support

L129 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support.AlgebraicGeometry.Scheme.Modules.PointVanishing.eq_zero_iff_closedPoint_mem_support
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
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
namespace PointVanishing
variable {X : Scheme.{u}} {N : X.Modules}
variable {k : Type u} [Field k]
Lean source · statement
lemma eq_zero_iff_closedPoint_mem_support {N : (Spec (CommRingCat.of k)).Modules}
    (hN : Scheme.Modules.IsInvertible N) (t : 𝟙_ _ ⟶ N) :
    t = 0 ↔ IsLocalRing.closedPoint k ∈ (zeroSchemeIdeal t).support
theorem

pullbackSection_eq_zero_iff_mem_support

L149 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support.AlgebraicGeometry.Scheme.Modules.PointVanishing.pullbackSection_eq_zero_iff_mem_support
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
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
namespace PointVanishing
variable {X : Scheme.{u}} {N : X.Modules}
variable {k : Type u} [Field k]
Lean source · statement
theorem pullbackSection_eq_zero_iff_mem_support {M : X.Modules} (hM : Scheme.Modules.IsInvertible M)
    (s : 𝟙_ X.Modules ⟶ M) (z : Spec (CommRingCat.of k) ⟶ X) :
    pullbackSection z s = 0 ↔
      z.base (IsLocalRing.closedPoint k) ∈ (zeroSchemeIdeal s).support
theorem

pullbackSection_eq_zero_iff_mem_support

L166 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.pullbackSection_eq_zero_iff_mem_support
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_pullbackSection_eq_zero_iff_mem_support
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.pullbackSection_eq_zero_iff_mem_support
    {k : Type u} [Field k] {X : Scheme.{u}} {M : X.Modules} (hM : Scheme.Modules.IsInvertible M)
    (s : 𝟙_ X.Modules ⟶ M) (z : Spec (CommRingCat.of k) ⟶ X) :
    Scheme.Modules.pullbackSection z s = 0 ↔
      z.base (IsLocalRing.closedPoint k) ∈ (Scheme.Modules.zeroSchemeIdeal s).support

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