NYLL
Module

Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
53 declarations indexed from sourceView source ↗

Module documentation

Coefficient ideals and zero schemes of invertible-module sections

The coefficient ideal of a section lies in its zero-scheme ideal. Under a local trivialization, both ideals equal the principal ideal generated by the coefficient.

Imports6
Imported by21

Declarations

def

sAt

L50 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.sAt
Documentation

The section represented by the unit-module morphism on the image of an open subset.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
Lean source · statement
def sAt (V : (U : Scheme.{u}).Opens) : Γ(M, U.ι ''ᵁ V)
lemma

sAt_top

L53 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.sAt_top
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
Lean source · statement
lemma sAt_top : sAt s U ⊤ = restrictSection s U
lemma

unit_map_one

L55 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.unit_map_one
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
Lean source · statement
lemma unit_map_one {W W' : X.Opens} (i : W' ⟶ W) :
    (𝟙_ X.Modules).presheaf.map i.op (toUnitSection W 1) = toUnitSection W' 1
lemma

map_sAt

L59 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.map_sAt
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
Lean source · statement
lemma map_sAt {V V' : (U : Scheme.{u}).Opens} (i : V' ⟶ V) :
    M.presheaf.map (U.ι.opensFunctor.map i).op (sAt s U V) = sAt s U V'
lemma

restrict_smul

L67 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.restrict_smul
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
Lean source · statement
lemma restrict_smul (V : (U : Scheme.{u}).Opens) (r : Γ((U : Scheme.{u}), V))
    (m : Γ(M.restrict U.ι, V)) :
    r • m = (id r : Γ(X, U.ι ''ᵁ V)) • (id m : Γ(M, U.ι ''ᵁ V))
lemma

app_smul'

L75 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.app_smul'
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
Lean source · statement
lemma app_smul' {N : (U : Scheme.{u}).Modules} (φ : M.restrict U.ι ⟶ N) (V : (U : Scheme.{u}).Opens)
    (r : Γ(X, U.ι ''ᵁ V)) (m : Γ(M, U.ι ''ᵁ V)) :
    φ.app V (r • m) = (id r : Γ((U : Scheme.{u}), V)) • φ.app V m
def

coord

L85 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.coord
Documentation

The scalar coordinate of a section under a chosen morphism to the unit module.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
Lean source · statement
def coord (φ : M.restrict U.ι ⟶ 𝟙_ (U : Scheme.{u}).Modules) (V : (U : Scheme.{u}).Opens)
    (m : Γ(M, U.ι ''ᵁ V)) : Γ(X, U.ι ''ᵁ V)
def

cf

L91 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.cf
Documentation

The scalar coordinate of the distinguished section in the chosen local trivialization.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
Lean source · statement
def cf (φ : M.restrict U.ι ⟶ 𝟙_ (U : Scheme.{u}).Modules) (V : (U : Scheme.{u}).Opens) :
    Γ(X, U.ι ''ᵁ V)
lemma

cf_top

L95 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.cf_top
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
Lean source · statement
lemma cf_top (φ : M.restrict U.ι ⟶ 𝟙_ (U : Scheme.{u}).Modules) :
    U.topIso.hom.hom (cf s φ ⊤) = coeff s U φ
lemma

map_coord

L99 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.map_coord
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
Lean source · statement
lemma map_coord (φ : M.restrict U.ι ⟶ 𝟙_ (U : Scheme.{u}).Modules) {V V' : (U : Scheme.{u}).Opens}
    (i : V' ⟶ V) (m : Γ(M, U.ι ''ᵁ V)) :
    X.presheaf.map (U.ι.opensFunctor.map i).op (coord φ V m) =
      coord φ V' (M.presheaf.map (U.ι.opensFunctor.map i).op m)
lemma

map_cf

L110 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.map_cf
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
Lean source · statement
lemma map_cf (φ : M.restrict U.ι ⟶ 𝟙_ (U : Scheme.{u}).Modules) {V V' : (U : Scheme.{u}).Opens}
    (i : V' ⟶ V) : X.presheaf.map (U.ι.opensFunctor.map i).op (cf s φ V) = cf s φ V'
lemma

coord_smul

L116 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.coord_smul
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
Lean source · statement
lemma coord_smul (φ : M.restrict U.ι ⟶ 𝟙_ (U : Scheme.{u}).Modules) (V : (U : Scheme.{u}).Opens)
    (r : Γ(X, U.ι ''ᵁ V)) (m : Γ(M, U.ι ''ᵁ V)) :
    coord φ V (r • m) = r * coord φ V m
def

gen

L125 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.gen
Documentation

The local generator obtained by applying the inverse trivialization to the unit section.

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_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
Lean source · statement
def gen (τ : M.restrict U.ι ≅ 𝟙_ (U : Scheme.{u}).Modules) (V : (U : Scheme.{u}).Opens) :
    Γ(M, U.ι ''ᵁ V)
lemma

coord_smul_gen

L130 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.coord_smul_gen
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_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
Lean source · statement
lemma coord_smul_gen (τ : M.restrict U.ι ≅ 𝟙_ (U : Scheme.{u}).Modules) (V : (U : Scheme.{u}).Opens)
    (m : Γ(M, U.ι ''ᵁ V)) : coord τ.hom V m • gen τ V = m
lemma

cf_eq_mul

L144 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.cf_eq_mul
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
Lean source · statement
lemma cf_eq_mul (τ : M.restrict U.ι ≅ 𝟙_ (U : Scheme.{u}).Modules)
    (φ : M.restrict U.ι ⟶ 𝟙_ (U : Scheme.{u}).Modules) (V : (U : Scheme.{u}).Opens) :
    cf s φ V = cf s τ.hom V * coord φ V (gen τ V)
lemma

image_preimage_eq_of_le

L153 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.image_preimage_eq_of_le
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
Lean source · statement
lemma image_preimage_eq_of_le {W : X.Opens} (hW : W ≤ U) : U.ι ''ᵁ (U.ι ⁻¹ᵁ W) = W
def

resX

L158 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.resX
Documentation

Transport scalar sections from the image of a preimage open to the original open.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
Lean source · statement
def resX {W : X.Opens} (hW : W ≤ U) : Γ(X, U.ι ''ᵁ (U.ι ⁻¹ᵁ W)) ⟶ Γ(X, W)
def

resX'

L162 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.resX'
Documentation

Transport scalar sections from the original open to the image of its preimage.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
Lean source · statement
def resX' {W : X.Opens} (hW : W ≤ U) : Γ(X, W) ⟶ Γ(X, U.ι ''ᵁ (U.ι ⁻¹ᵁ W))
def

resM

L166 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.resM
Documentation

Transport module sections from the image of a preimage open to the original open.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
Lean source · statement
def resM {W : X.Opens} (hW : W ≤ U) : Γ(M, U.ι ''ᵁ (U.ι ⁻¹ᵁ W)) ⟶ Γ(M, W)
def

resM'

L170 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.resM'
Documentation

Transport module sections from the original open to the image of its preimage.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
Lean source · statement
def resM' {W : X.Opens} (hW : W ≤ U) : Γ(M, W) ⟶ Γ(M, U.ι ''ᵁ (U.ι ⁻¹ᵁ W))
lemma

resX_resX'

L174 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.resX_resX'
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
omit s in
Lean source · statement
lemma resX_resX' {W : X.Opens} (hW : W ≤ U) (r : Γ(X, W)) : resX hW (resX' hW r) = r
lemma

resX'_resX

L181 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.resX'_resX
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
omit s in
Lean source · statement
lemma resX'_resX {W : X.Opens} (hW : W ≤ U) (r : Γ(X, U.ι ''ᵁ (U.ι ⁻¹ᵁ W))) :
    resX' hW (resX hW r) = r
lemma

resM_resM'

L189 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.resM_resM'
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
omit s in
Lean source · statement
lemma resM_resM' {W : X.Opens} (hW : W ≤ U) (m : Γ(M, W)) : resM (M := M) hW (resM' hW m) = m
lemma

resM_smul

L196 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.resM_smul
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
omit s in
Lean source · statement
lemma resM_smul {W : X.Opens} (hW : W ≤ U) (r : Γ(X, U.ι ''ᵁ (U.ι ⁻¹ᵁ W)))
    (m : Γ(M, U.ι ''ᵁ (U.ι ⁻¹ᵁ W))) : resM (M := M) hW (r • m) = resX hW r • resM hW m
lemma

resM'_smul

L201 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.resM'_smul
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
omit s in
Lean source · statement
lemma resM'_smul {W : X.Opens} (hW : W ≤ U) (r : Γ(X, W)) (m : Γ(M, W)) :
    resM' (M := M) (U := U) hW (r • m) = resX' hW r • resM' hW m
lemma

resM'_sApp

L205 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.resM'_sApp
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
Lean source · statement
lemma resM'_sApp {W : X.Opens} (hW : W ≤ U) :
    resM' (U := U) hW (s.app W (toUnitSection W 1)) = sAt s U (U.ι ⁻¹ᵁ W)
def

cX

L214 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.cX
Documentation

The scalar coordinate of the distinguished section transported to the original open.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
Lean source · statement
def cX (φ : M.restrict U.ι ⟶ 𝟙_ (U : Scheme.{u}).Modules) {W : X.Opens} (hW : W ≤ U) : Γ(X, W)
def

tX

L218 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.tX
Documentation

The scalar coordinate map on sections of the original open subset.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
Lean source · statement
def tX (φ : M.restrict U.ι ⟶ 𝟙_ (U : Scheme.{u}).Modules) {W : X.Opens} (hW : W ≤ U)
    (m : Γ(M, W)) : Γ(X, W)
def

eX

L223 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.eX
Documentation

The generator of the chosen local trivialization transported to the original open.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
Lean source · statement
def eX (τ : M.restrict U.ι ≅ 𝟙_ (U : Scheme.{u}).Modules) {W : X.Opens} (hW : W ≤ U) : Γ(M, W)
lemma

tX_sApp

L226 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.tX_sApp
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
Lean source · statement
lemma tX_sApp (φ : M.restrict U.ι ⟶ 𝟙_ (U : Scheme.{u}).Modules) {W : X.Opens} (hW : W ≤ U) :
    tX φ hW (s.app W (toUnitSection W 1)) = cX s φ hW
lemma

tX_smul

L232 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.tX_smul
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
omit s in
Lean source · statement
lemma tX_smul (φ : M.restrict U.ι ⟶ 𝟙_ (U : Scheme.{u}).Modules) {W : X.Opens} (hW : W ≤ U)
    (r : Γ(X, W)) (m : Γ(M, W)) : tX φ hW (r • m) = r * tX φ hW m
lemma

tX_smul_eX

L238 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.tX_smul_eX
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
omit s in
Lean source · statement
lemma tX_smul_eX (τ : M.restrict U.ι ≅ 𝟙_ (U : Scheme.{u}).Modules) {W : X.Opens} (hW : W ≤ U)
    (m : Γ(M, W)) : tX τ.hom hW m • eX τ hW = m
lemma

cX_dvd

L244 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.cX_dvd
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
Lean source · statement
lemma cX_dvd (τ : M.restrict U.ι ≅ 𝟙_ (U : Scheme.{u}).Modules) {W : X.Opens} (hW : W ≤ U)
    (t : Γ(M, W) → Γ(X, W)) (ht : ∀ (r : Γ(X, W)) (m : Γ(M, W)), t (r • m) = r * t m) :
    cX s τ.hom hW ∣ t (s.app W (toUnitSection W 1))
lemma

map_cX

L251 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.map_cX
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
Lean source · statement
lemma map_cX (φ : M.restrict U.ι ⟶ 𝟙_ (U : Scheme.{u}).Modules) {W W' : X.Opens} (hW : W ≤ U)
    (h : W' ≤ W) : X.presheaf.map (homOfLE h).op (cX s φ hW) = cX s φ (h.trans hW)
lemma

cX_image

L260 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.cX_image
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
Lean source · statement
lemma cX_image (φ : M.restrict U.ι ⟶ 𝟙_ (U : Scheme.{u}).Modules) (V : (U : Scheme.{u}).Opens)
    (h : U.ι ''ᵁ V ≤ U) : cX s φ h = cf s φ V
theorem

mem_ideal_of_forall_exists_basicOpen

L269 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.mem_ideal_of_forall_exists_basicOpen
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
omit s in
Lean source · statement
theorem mem_ideal_of_forall_exists_basicOpen {Y : Scheme.{u}} (I : Y.IdealSheafData)
    (Ω : Y.affineOpens) (r : Γ(Y, Ω.1))
    (h : ∀ y ∈ Ω.1, ∃ g : Γ(Y, Ω.1), y ∈ Y.basicOpen g ∧
      Y.presheaf.map (homOfLE (Y.basicOpen_le g)).op r ∈ I.ideal (Y.affineBasicOpen g)) :
    r ∈ I.ideal Ω
theorem

ideal_eq_of_forall_exists_basicOpen

L294 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.ideal_eq_of_forall_exists_basicOpen
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
omit s in
Lean source · statement
theorem ideal_eq_of_forall_exists_basicOpen {Y : Scheme.{u}} (I₁ I₂ : Y.IdealSheafData)
    (Ω : Y.affineOpens)
    (h : ∀ y ∈ Ω.1, ∃ g : Γ(Y, Ω.1), y ∈ Y.basicOpen g ∧
      I₁.ideal (Y.affineBasicOpen g) = I₂.ideal (Y.affineBasicOpen g)) :
    I₁.ideal Ω = I₂.ideal Ω
def

Idx

L313 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.Idx
Documentation

The indices consisting of affine opens with a chosen trivialization of the invertible module.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
variable (M) in
Lean source · statement
def Idx : Type u
def

piece

L316 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.piece
Documentation

The local ideal sheaf generated by the coordinate of the distinguished section.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
variable (M) in
Lean source · full declaration
def piece (j : Idx M) : (j.1.1 : Scheme.{u}).IdealSheafData where
  ideal V := Ideal.span {(id (cf s j.2.hom V.1) : Γ((j.1.1 : Scheme.{u}), V.1))}
  map_ideal_basicOpen V f := by
    rw [Ideal.map_span, Set.image_singleton]
    exact congrArg (fun x => Ideal.span ({x} : Set Γ((j.1.1 : Scheme.{u}), _)))
      (map_cf s j.2.hom (homOfLE ((j.1.1 : Scheme.{u}).basicOpen_le f)))
lemma

ideal_piece

L323 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.ideal_piece
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
variable (M) in
Lean source · statement
lemma ideal_piece (j : Idx M) (V : (j.1.1 : Scheme.{u}).affineOpens) :
    (piece s j).ideal V = Ideal.span {(id (cf s j.2.hom V.1) : Γ((j.1.1 : Scheme.{u}), V.1))}
def

cover

L328 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.cover
Documentation

The open cover of all affine local trivializations of the invertible module.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
variable (M) in
Lean source · statement
def cover (hM : Scheme.Modules.IsInvertible M) : X.OpenCover
lemma

span_cX_eq

L333 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.span_cX_eq
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
variable (M) in
Lean source · statement
lemma span_cX_eq (j j' : Idx M) {W : X.Opens} (hj : W ≤ j.1.1) (hj' : W ≤ j'.1.1) :
    Ideal.span {cX s j.2.hom hj} = Ideal.span {cX s j'.2.hom hj'}
lemma

ideal_comap_piece

L343 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.ideal_comap_piece
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
variable (M) in
Lean source · statement
lemma ideal_comap_piece (j : Idx M) {V : Scheme.{u}} (a : V ⟶ (j.1.1 : Scheme.{u}))
    {W : X.Opens} (hW : W ≤ j.1.1) (hWa : IsAffineOpen W) (Ω : V.affineOpens)
    (hΩ : (Ω : V.Opens) ≤ (a ≫ j.1.1.ι) ⁻¹ᵁ W) :
    ((piece s j).comap a).ideal Ω =
      Ideal.span {((a ≫ j.1.1.ι).appLE W Ω hΩ).hom (cX s j.2.hom hW)}
lemma

comap_piece_eq

L360 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.comap_piece_eq
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
variable (M) in
Lean source · statement
lemma comap_piece_eq (j j' : Idx M) {V : Scheme.{u}} (a : V ⟶ (j.1.1 : Scheme.{u}))
    (b : V ⟶ (j'.1.1 : Scheme.{u})) (hab : a ≫ j.1.1.ι = b ≫ j'.1.1.ι) :
    (piece s j).comap a = (piece s j').comap b
lemma

coeff_eq_cX

L392 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.coeff_eq_cX
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
variable (M) in
Lean source · statement
lemma coeff_eq_cX (φ : M.restrict U.ι ⟶ 𝟙_ (U : Scheme.{u}).Modules) :
    coeff s U φ = cX s φ (le_refl U)
def

P

L402 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.P
Documentation

The ideal sheaf obtained by gluing the coordinate ideals on the trivializing cover.

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
variable (M) in
variable (hM : Scheme.Modules.IsInvertible M)
Lean source · statement
def P : X.IdealSheafData
lemma

P_comap

L406 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.P_comap
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
variable (M) in
variable (hM : Scheme.Modules.IsInvertible M)
Lean source · statement
lemma P_comap (j : Idx M) : (P s hM).comap j.1.1.ι = piece s j
lemma

ideal_P_self

L410 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.ideal_P_self
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
variable (M) in
variable (hM : Scheme.Modules.IsInvertible M)
Lean source · statement
lemma ideal_P_self (W : X.affineOpens) (τ : M.restrict W.1.ι ≅ 𝟙_ (W.1 : Scheme.{u}).Modules) :
    (P s hM).ideal W = Ideal.span {cX s τ.hom (le_refl _)}
lemma

ideal_P_of_le

L434 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.ideal_P_of_le
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
variable (M) in
variable (hM : Scheme.Modules.IsInvertible M)
Lean source · statement
lemma ideal_P_of_le (W : X.affineOpens) (τ : M.restrict W.1.ι ≅ 𝟙_ (W.1 : Scheme.{u}).Modules)
    (Ω : X.affineOpens) (h : (Ω : X.Opens) ≤ W.1) :
    (P s hM).ideal Ω = Ideal.span {cX s τ.hom h}
lemma

coeffIdeal_le_P

L441 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.coeffIdeal_le_P
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
variable (M) in
variable (hM : Scheme.Modules.IsInvertible M)
Lean source · statement
lemma coeffIdeal_le_P (V : X.affineOpens) : coeffIdeal s V.1 ≤ (P s hM).ideal V
lemma

P_le

L455 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.P_le
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
variable (M) in
variable (hM : Scheme.Modules.IsInvertible M)
Lean source · statement
lemma P_le (J : X.IdealSheafData) (hJ : ∀ U : X.affineOpens, coeffIdeal s U.1 ≤ J.ideal U) :
    P s hM ≤ J
theorem

zeroSchemeIdeal_eq_P

L477 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq.ZeroSchemeLoc.zeroSchemeIdeal_eq_P
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeLoc
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U} in
variable {U}
variable (M) in
variable (hM : Scheme.Modules.IsInvertible M)
Lean source · statement
theorem zeroSchemeIdeal_eq_P : zeroSchemeIdeal s = P s hM
theorem

coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq

L484 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
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_coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
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.coeffIdeal_le_and_ideal_zeroSchemeIdeal_eq
    {X : Scheme.{u}} {M : X.Modules} (hM : Scheme.Modules.IsInvertible M) (s : 𝟙_ X.Modules ⟶ M) :
    (∀ V : X.affineOpens,
        Scheme.Modules.coeffIdeal s V.1 ≤ (Scheme.Modules.zeroSchemeIdeal s).ideal V) ∧
    ∀ (U : X.affineOpens) (τ : M.restrict U.1.ι ≅ 𝟙_ (U.1 : Scheme.{u}).Modules),
      (Scheme.Modules.zeroSchemeIdeal s).ideal U = Ideal.span {Scheme.Modules.coeff s U.1 τ.hom} ∧
        (Scheme.Modules.zeroSchemeIdeal s).ideal U = Scheme.Modules.coeffIdeal s U.1

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