NYLL
Module

Scheme_Modules_IsInvertible_genericPoint_notMem_support_zeroSchemeIdeal.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_genericPoint_notMem_support_zeroSchemeIdeal
6 declarations indexed from sourceView source ↗

Module documentation

A nonzero line-bundle section does not vanish at the generic point

For an invertible module on an integral scheme, the generic point lies outside the support of the zero-scheme ideal of a nonzero section.

Imports2
Imported by3

Declarations

theorem

map_app_unit

L41 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_genericPoint_notMem_support_zeroSchemeIdeal.S3ZD.map_app_unit
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_genericPoint_notMem_support_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace S3ZD
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem map_app_unit (φ : 𝟙_ X.Modules ⟶ M) {U V : X.Opens} (i : U ⟶ V)
    (m : Γ(𝟙_ X.Modules, V)) :
    M.presheaf.map i.op (φ.app V m) = φ.app U ((𝟙_ X.Modules).presheaf.map i.op m)
theorem

map_toUnitSection_one

L49 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_genericPoint_notMem_support_zeroSchemeIdeal.S3ZD.map_toUnitSection_one
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_genericPoint_notMem_support_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace S3ZD
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem map_toUnitSection_one {U V : X.Opens} (i : U ⟶ V) :
    (𝟙_ X.Modules).presheaf.map i.op (Scheme.Modules.toUnitSection V 1) =
      Scheme.Modules.toUnitSection U 1
theorem

eq_smul_toUnitSection_one

L56 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_genericPoint_notMem_support_zeroSchemeIdeal.S3ZD.eq_smul_toUnitSection_one
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_genericPoint_notMem_support_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace S3ZD
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem eq_smul_toUnitSection_one {U : X.Opens} (m : Γ(𝟙_ X.Modules, U)) :
    m = Scheme.Modules.ofUnitSection U m • Scheme.Modules.toUnitSection U 1
theorem

eq_zero_of_forall_app_one

L61 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_genericPoint_notMem_support_zeroSchemeIdeal.S3ZD.eq_zero_of_forall_app_one
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_genericPoint_notMem_support_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace S3ZD
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem eq_zero_of_forall_app_one (φ : 𝟙_ X.Modules ⟶ M)
    (h : ∀ U : X.Opens, φ.app U (Scheme.Modules.toUnitSection U 1) = 0) : φ = 0
theorem

restrictSection_eq_zero

L70 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_genericPoint_notMem_support_zeroSchemeIdeal.S3ZD.restrictSection_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_genericPoint_notMem_support_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace S3ZD
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem restrictSection_eq_zero (hM : Scheme.Modules.IsInvertible M) (s : 𝟙_ X.Modules ⟶ M)
    (U : X.affineOpens) (τ : M.restrict U.1.ι ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
    (hU : (Scheme.Modules.zeroSchemeIdeal s).ideal U = ⊥) :
    Scheme.Modules.restrictSection s U.1 = 0
theorem

genericPoint_notMem_support_zeroSchemeIdeal

L97 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.genericPoint_notMem_support_zeroSchemeIdeal
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_genericPoint_notMem_support_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
open S3ZD in
Lean source · statement
theorem
  _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.genericPoint_notMem_support_zeroSchemeIdeal
    {X : Scheme.{u}} [IsIntegral X] {M : X.Modules} (hM : Scheme.Modules.IsInvertible M)
    (s : 𝟙_ X.Modules ⟶ M) (hs : s ≠ 0) :
    genericPoint X ∉ (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.