NYLL
Module

Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
60 declarations indexed from sourceView source ↗

Module documentation

Pullback of the zero scheme of a section

The zero-scheme ideal of a section of an invertible module pulls back to the zero-scheme ideal of the pulled-back section.

Imports6
Imported by20

Declarations

def

sAt

L49 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.sAt
Documentation

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

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L52 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.sAt_top
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L54 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.unit_map_one
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L58 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.map_sAt
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L66 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.restrict_smul
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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'

L74 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.app_smul'
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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_comap_zeroSchemeIdeal.ZeroSchemeLoc.coord
Documentation

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

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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_comap_zeroSchemeIdeal.ZeroSchemeLoc.cf
Documentation

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

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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_comap_zeroSchemeIdeal.ZeroSchemeLoc.cf_top
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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_comap_zeroSchemeIdeal.ZeroSchemeLoc.map_coord
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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_comap_zeroSchemeIdeal.ZeroSchemeLoc.map_cf
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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_comap_zeroSchemeIdeal.ZeroSchemeLoc.coord_smul
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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_comap_zeroSchemeIdeal.ZeroSchemeLoc.gen
Documentation

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

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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_comap_zeroSchemeIdeal.ZeroSchemeLoc.coord_smul_gen
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L145 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.cf_eq_mul
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L154 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.image_preimage_eq_of_le
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L159 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.resX
Documentation

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

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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'

L163 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.resX'
Documentation

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

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L167 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.resM
Documentation

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

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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'

L171 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.resM'
Documentation

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

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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'

L175 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.resX_resX'
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L182 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.resX'_resX
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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'

L190 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.resM_resM'
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L197 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.resM_smul
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L202 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.resM'_smul
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L206 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.resM'_sApp
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L215 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.cX
Documentation

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

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L219 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.tX
Documentation

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

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L224 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.eX
Documentation

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

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L227 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.tX_sApp
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L233 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.tX_smul
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L239 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.tX_smul_eX
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L245 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.cX_dvd
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L252 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.map_cX
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L261 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.cX_image
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L270 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.mem_ideal_of_forall_exists_basicOpen
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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

L295 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.ideal_eq_of_forall_exists_basicOpen
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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 Ω
lemma

coeff_eq_cX

L312 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeLoc.coeff_eq_cX
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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 coeff_eq_cX (φ : M.restrict U.ι ⟶ 𝟙_ (U : Scheme.{u}).Modules) :
    coeff s U φ = cX s φ (le_refl U)
abbrev

unitApp

L333 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.PullSections.unitApp
Documentation

The component of the original pullback-pushforward adjunction unit.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace PullSections
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X X' : Scheme.{u}} (F : X' ⟶ X)
Lean source · statement
abbrev unitApp (N : X.Modules) :
    N ⟶ (Scheme.Modules.pushforward F).obj ((Scheme.Modules.pullback F).obj N)
def

pullSec

L338 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.PullSections.pullSec
Documentation

The pullback of a local section obtained by evaluating the adjunction unit.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace PullSections
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X X' : Scheme.{u}} (F : X' ⟶ X)
Lean source · statement
def pullSec (N : X.Modules) (U : X.Opens) (m : Γ(N, U)) :
    Γ((Scheme.Modules.pullback F).obj N, F ⁻¹ᵁ U)
lemma

map_pullSec

L343 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.PullSections.map_pullSec
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace PullSections
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X X' : Scheme.{u}} (F : X' ⟶ X)
variable {F} in
Lean source · statement
lemma map_pullSec {N N' : X.Modules} (g : N ⟶ N') (U : X.Opens) (m : Γ(N, U)) :
    ((Scheme.Modules.pullback F).map g).app (F ⁻¹ᵁ U) (pullSec F N U m) =
      pullSec F N' U (g.app U m)
lemma

pullSec_map

L355 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.PullSections.pullSec_map
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace PullSections
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X X' : Scheme.{u}} (F : X' ⟶ X)
variable {F} in
Lean source · statement
lemma pullSec_map (N : X.Modules) {U V : X.Opens} (i : V ⟶ U) (m : Γ(N, U)) :
    ((Scheme.Modules.pullback F).obj N).presheaf.map
        ((TopologicalSpace.Opens.map F.base).map i).op (pullSec F N U m) =
      pullSec F N V (N.presheaf.map i.op m)
lemma

pullSec_smul

L363 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.PullSections.pullSec_smul
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace PullSections
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X X' : Scheme.{u}} (F : X' ⟶ X)
variable {F} in
Lean source · statement
lemma pullSec_smul (N : X.Modules) (U : X.Opens) (r : Γ(X, U)) (m : Γ(N, U)) :
    pullSec F N U (r • m) = F.app U r • pullSec F N U m
lemma

pullbackUnitIso_hom_pullSec

L367 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.PullSections.pullbackUnitIso_hom_pullSec
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace PullSections
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X X' : Scheme.{u}} (F : X' ⟶ X)
variable {F} in
Lean source · statement
lemma pullbackUnitIso_hom_pullSec (U : X.Opens) (r : Γ(X, U)) :
    (Scheme.Modules.pullbackUnitIso F).hom.app (F ⁻¹ᵁ U)
        (pullSec F (𝟙_ X.Modules) U (toUnitSection U r)) =
      toUnitSection (F ⁻¹ᵁ U) (F.app U r)
lemma

restrictFunctorIsoPullback_hom_app_apply

L388 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.PullSections.restrictFunctorIsoPullback_hom_app_apply
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace PullSections
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X X' : Scheme.{u}} (F : X' ⟶ X)
variable {F} in
Lean source · statement
lemma restrictFunctorIsoPullback_hom_app_apply {Y : Scheme.{u}} (j : Y ⟶ X) [IsOpenImmersion j]
    (N : X.Modules) (U : X.Opens) (m : Γ(N, U)) :
    ((restrictFunctorIsoPullback j).hom.app N).app (j ⁻¹ᵁ U)
        (N.presheaf.map (homOfLE (j.image_preimage_le U)).op m) = pullSec j N U m
lemma

restrictFunctorIsoPullback_inv_app_pullSec

L400 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.PullSections.restrictFunctorIsoPullback_inv_app_pullSec
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace PullSections
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X X' : Scheme.{u}} (F : X' ⟶ X)
variable {F} in
Lean source · statement
lemma restrictFunctorIsoPullback_inv_app_pullSec {Y : Scheme.{u}} (j : Y ⟶ X) [IsOpenImmersion j]
    (N : X.Modules) (U : X.Opens) (m : Γ(N, U)) :
    ((restrictFunctorIsoPullback j).inv.app N).app (j ⁻¹ᵁ U) (pullSec j N U m) =
      N.presheaf.map (homOfLE (j.image_preimage_le U)).op m
lemma

pullbackCongr_hom_app_pullSec

L412 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.PullSections.pullbackCongr_hom_app_pullSec
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace PullSections
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X X' : Scheme.{u}} (F : X' ⟶ X)
variable {F} in
Lean source · full declaration
lemma pullbackCongr_hom_app_pullSec {f₁ f₂ : X' ⟶ X} (e : f₁ = f₂) (N : X.Modules) (U : X.Opens)
    (m : Γ(N, U)) :
    ((pullbackCongr e).hom.app N).app (f₁ ⁻¹ᵁ U) (pullSec f₁ N U m) =
      ((Scheme.Modules.pullback f₂).obj N).presheaf.map
        (eqToHom (show f₁ ⁻¹ᵁ U = f₂ ⁻¹ᵁ U by rw [e])).op (pullSec f₂ N U m) := by
  subst e
  simp only [eqToHom_refl, op_id, CategoryTheory.Functor.map_id]
  rfl
lemma

pullbackComp_inv_app_pullSec

L421 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.PullSections.pullbackComp_inv_app_pullSec
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace PullSections
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X X' : Scheme.{u}} (F : X' ⟶ X)
variable {F} in
Lean source · statement
lemma pullbackComp_inv_app_pullSec {Y : Scheme.{u}} (f : X' ⟶ Y) (g : Y ⟶ X) (N : X.Modules)
    (U : X.Opens) (m : Γ(N, U)) :
    ((pullbackComp f g).inv.app N).app ((f ≫ g) ⁻¹ᵁ U) (pullSec (f ≫ g) N U m) =
      pullSec f ((Scheme.Modules.pullback g).obj N) (g ⁻¹ᵁ U) (pullSec g N U m)
lemma

pullbackComp_hom_app_pullSec

L440 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.PullSections.pullbackComp_hom_app_pullSec
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace PullSections
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X X' : Scheme.{u}} (F : X' ⟶ X)
variable {F} in
Lean source · statement
lemma pullbackComp_hom_app_pullSec {Y : Scheme.{u}} (f : X' ⟶ Y) (g : Y ⟶ X) (N : X.Modules)
    (U : X.Opens) (m : Γ(N, U)) :
    ((pullbackComp f g).hom.app N).app ((f ≫ g) ⁻¹ᵁ U)
        (pullSec f ((Scheme.Modules.pullback g).obj N) (g ⁻¹ᵁ U) (pullSec g N U m)) =
      pullSec (f ≫ g) N U m
lemma

app_map

L466 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeBC.app_map
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeBC
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open ZeroSchemeLoc PullSections
variable {X X' : Scheme.{u}} (F : X' ⟶ X) {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M)
Lean source · statement
lemma app_map {Y : Scheme.{u}} {N N' : Y.Modules} (φ : N ⟶ N') {W₁ W₂ : Y.Opens} (i : W₁ ⟶ W₂)
    (x : Γ(N, W₂)) : φ.app W₁ (N.presheaf.map i.op x) = N'.presheaf.map i.op (φ.app W₂ x)
lemma

inv_app_hom_app

L472 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeBC.inv_app_hom_app
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeBC
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open ZeroSchemeLoc PullSections
variable {X X' : Scheme.{u}} (F : X' ⟶ X) {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M)
Lean source · statement
lemma inv_app_hom_app {Y : Scheme.{u}} {N N' : Y.Modules} (e : N ≅ N') (W : Y.Opens) (x : Γ(N,
    W)) :
    e.inv.app W (e.hom.app W x) = x
lemma

pullbackSection_app

L480 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeBC.pullbackSection_app
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeBC
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open ZeroSchemeLoc PullSections
variable {X X' : Scheme.{u}} (F : X' ⟶ X) {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M)
Lean source · statement
lemma pullbackSection_app (U : X.Opens) :
    (pullbackSection F s).app (F ⁻¹ᵁ U) (toUnitSection (F ⁻¹ᵁ U) 1) =
      pullSec F M U (s.app U (toUnitSection U 1))
lemma

G_comp

L498 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeBC.G_comp
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeBC
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open ZeroSchemeLoc PullSections
variable {X X' : Scheme.{u}} (F : X' ⟶ X) {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M)
Lean source · statement
lemma G_comp {U : X.Opens} {Ω : X'.Opens} (hΩ : Ω ≤ F ⁻¹ᵁ U) :
    F.resLE U Ω hΩ ≫ U.ι = Ω.ι ≫ F
def

triv

L502 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeBC.triv
Documentation

The trivialization on a smaller source open induced by the chosen target trivialization.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeBC
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open ZeroSchemeLoc PullSections
variable {X X' : Scheme.{u}} (F : X' ⟶ X) {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M)
Lean source · statement
def triv {U : X.Opens} (τ : M.restrict U.ι ≅ 𝟙_ (U : Scheme.{u}).Modules) {Ω : X'.Opens}
    (hΩ : Ω ≤ F ⁻¹ᵁ U) :
    ((Scheme.Modules.pullback F).obj M).restrict Ω.ι ≅ 𝟙_ (Ω : Scheme.{u}).Modules
lemma

V₀_eq

L513 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeBC.V₀_eq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeBC
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open ZeroSchemeLoc PullSections
variable {X X' : Scheme.{u}} (F : X' ⟶ X) {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M)
Lean source · statement
lemma V₀_eq {U : X.Opens} {Ω : X'.Opens} (hΩ : Ω ≤ F ⁻¹ᵁ U) :
    (Ω.ι ≫ F) ⁻¹ᵁ U = (F.resLE U Ω hΩ ≫ U.ι) ⁻¹ᵁ U
lemma

app_triv_sAt

L517 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeBC.app_triv_sAt
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeBC
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open ZeroSchemeLoc PullSections
variable {X X' : Scheme.{u}} (F : X' ⟶ X) {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M)
Lean source · statement
lemma app_triv_sAt {U : X.Opens} (τ : M.restrict U.ι ≅ 𝟙_ (U : Scheme.{u}).Modules)
    {Ω : X'.Opens} (hΩ : Ω ≤ F ⁻¹ᵁ U) :
    (triv F τ hΩ).hom.app ((Ω.ι ≫ F) ⁻¹ᵁ U) (sAt (pullbackSection F s) Ω ((Ω.ι ≫ F) ⁻¹ᵁ U)) =
      (𝟙_ (Ω : Scheme.{u}).Modules).presheaf.map (eqToHom (V₀_eq F hΩ)).op
        (toUnitSection ((F.resLE U Ω hΩ) ⁻¹ᵁ (U.ι ⁻¹ᵁ U))
          ((F.resLE U Ω hΩ).app (U.ι ⁻¹ᵁ U) (cf s τ.hom (U.ι ⁻¹ᵁ U))))
lemma

gen_eq

L593 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeBC.gen_eq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeBC
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open ZeroSchemeLoc PullSections
variable {X X' : Scheme.{u}} (F : X' ⟶ X) {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M)
Lean source · statement
lemma gen_eq (U : X.affineOpens) (τ : M.restrict U.1.ι ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
    (Ω : X'.affineOpens) (hΩ : (Ω : X'.Opens) ≤ F ⁻¹ᵁ (U : X.Opens)) :
    (F.appLE U Ω hΩ).hom (coeff s U.1 τ.hom) = coeff (pullbackSection F s) Ω.1 (triv F τ hΩ).hom
lemma

ideal_eq_of_le

L615 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeBC.ideal_eq_of_le
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeBC
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open ZeroSchemeLoc PullSections
variable {X X' : Scheme.{u}} (F : X' ⟶ X) {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M)
Lean source · statement
lemma ideal_eq_of_le (hM : Scheme.Modules.IsInvertible M) (U : X.affineOpens) (τ : M.restrict
    U.1.ι ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)
    (Ω : X'.affineOpens) (hΩ : (Ω : X'.Opens) ≤ F ⁻¹ᵁ (U : X.Opens)) :
    ((zeroSchemeIdeal s).comap F).ideal Ω = (zeroSchemeIdeal (pullbackSection F s)).ideal Ω
theorem

comap_zeroSchemeIdeal_eq

L627 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal.ZeroSchemeBC.comap_zeroSchemeIdeal_eq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace ZeroSchemeBC
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open ZeroSchemeLoc PullSections
variable {X X' : Scheme.{u}} (F : X' ⟶ X) {M : X.Modules} (s : 𝟙_ X.Modules ⟶ M)
Lean source · statement
theorem comap_zeroSchemeIdeal_eq (hM : Scheme.Modules.IsInvertible M) :
    (zeroSchemeIdeal s).comap F = zeroSchemeIdeal (pullbackSection F s)
theorem

comap_zeroSchemeIdeal

L640 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.comap_zeroSchemeIdeal
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_comap_zeroSchemeIdeal
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.comap_zeroSchemeIdeal
    {X X' : Scheme.{u}} (F : X' ⟶ X) {M : X.Modules} (hM : Scheme.Modules.IsInvertible M)
    (s : 𝟙_ X.Modules ⟶ M) :
    (Scheme.Modules.zeroSchemeIdeal s).comap F =
      Scheme.Modules.zeroSchemeIdeal (Scheme.Modules.pullbackSection F s)

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