NYLL
Module

Scheme_IdealSheafData_IsInvertible_isInvertible_module.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_isInvertible_module
37 declarations indexed from sourceView source ↗

Module documentation

Invertible ideals and invertible module sheaves

Constructs local module trivializations from non-zero-divisor generators of an invertible ideal.

Imports7
Imported by73

Declarations

def

sectionsIdeal

L54 ↗
AlgebraicGeometry.Scheme.IdealSheafData.sectionsIdeal
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
Lean source · statement
def _root_.AlgebraicGeometry.Scheme.IdealSheafData.sectionsIdeal (U : X.Opens) : Ideal
  Γ(X, U)
lemma

mem_sectionsIdeal_iff

L59 ↗
AlgebraicGeometry.Scheme.IdealSheafData.mem_sectionsIdeal_iff
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
lemma _root_.AlgebraicGeometry.Scheme.IdealSheafData.mem_sectionsIdeal_iff {U : X.Opens}
  (s : Γ(X, U)) :
    s ∈ I.sectionsIdeal U ↔ I.subschemeι.app U s = 0
lemma

sectionsIdeal_eq_ideal

L65 ↗
AlgebraicGeometry.Scheme.IdealSheafData.sectionsIdeal_eq_ideal
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
lemma _root_.AlgebraicGeometry.Scheme.IdealSheafData.sectionsIdeal_eq_ideal (U :
  X.affineOpens) : I.sectionsIdeal U = I.ideal U
lemma

map_mem_sectionsIdeal

L71 ↗
AlgebraicGeometry.Scheme.IdealSheafData.map_mem_sectionsIdeal
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
lemma _root_.AlgebraicGeometry.Scheme.IdealSheafData.map_mem_sectionsIdeal {U V :
  X.Opens} (i : V ⟶ U) {s : Γ(X, U)}
    (hs : s ∈ I.sectionsIdeal U) : X.presheaf.map i.op s ∈ I.sectionsIdeal V
def

sectionsPresheaf

L82 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.sectionsPresheaf
Documentation

The presheaf of additive groups of sections in the ideal sheaf.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · full declaration
def sectionsPresheaf : (X.Opens)ᵒᵖ ⥤ Ab.{u} where
  obj U := AddCommGrpCat.of (I.sectionsIdeal U.unop)
  map {U V} i := AddCommGrpCat.ofHom
    { toFun := fun s => ⟨X.presheaf.map i s.1, I.map_mem_sectionsIdeal i.unop s.2⟩
      map_zero' := Subtype.ext (by
        change X.presheaf.map i (0 : Γ(X, U.unop)) = 0
        exact map_zero _)
      map_add' := fun s t => Subtype.ext (by
        change X.presheaf.map i (s.1 + t.1) = X.presheaf.map i s.1 + X.presheaf.map i t.1
        exact map_add _ _ _) }
  map_id U := by
    ext s
    change X.presheaf.map (𝟙 U) s.1 = s.1
    rw [X.presheaf.map_id]
    rfl
  map_comp i j := by
    ext s
    change X.presheaf.map (i ≫ j) s.1 = X.presheaf.map j (X.presheaf.map i s.1)
    rw [X.presheaf.map_comp]
    rfl
instance

(anonymous instance)

L103 ↗
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
instance (U : (X.Opens)ᵒᵖ) : Module ((X.ringCatSheaf.obj).obj U) ((sectionsPresheaf
  I).obj U)
lemma

sectionsPresheaf_map_apply_coe

L107 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.sectionsPresheaf_map_apply_coe
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
lemma sectionsPresheaf_map_apply_coe {U V : (X.Opens)ᵒᵖ} (i : U ⟶ V)
    (s : (sectionsPresheaf I).obj U) :
    ((sectionsPresheaf I).map i s).1 = X.presheaf.map i s.1
def

toPresheafOfModules

L112 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.toPresheafOfModules
Documentation

The ideal-section presheaf with its natural structure-module action.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
def toPresheafOfModules : X.PresheafOfModules
lemma

toPresheafOfModules_presheaf

L120 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.toPresheafOfModules_presheaf
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
lemma toPresheafOfModules_presheaf : (toPresheafOfModules I).presheaf =
  sectionsPresheaf I
def

sectionsSubfunctor

L125 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.sectionsSubfunctor
Documentation

Ideal sections viewed as a subfunctor of the underlying structure presheaf.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · full declaration
def sectionsSubfunctor : Subfunctor (X.presheaf ⋙ CategoryTheory.forget CommRingCat) where
  obj U := {s | s ∈ I.sectionsIdeal U.unop}
  map {_U _V} i _s hs := I.map_mem_sectionsIdeal i.unop hs
def

sectionsIso

L130 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.sectionsIso
Documentation

The identification of ideal-section groups with the corresponding subfunctor.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
def sectionsIso : sectionsPresheaf I ⋙ CategoryTheory.forget Ab ≅ (sectionsSubfunctor
  I).toFunctor
lemma

mem_sectionsIdeal_of_locally

L138 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.mem_sectionsIdeal_of_locally
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
lemma mem_sectionsIdeal_of_locally {U : X.Opens} (s : Γ(X, U))
    (h : ∀ x ∈ U, ∃ (V : X.Opens) (_ : V ≤ U), x ∈ V ∧
      X.presheaf.map (homOfLE ‹V ≤ U›).op s ∈ I.sectionsIdeal V) :
    s ∈ I.sectionsIdeal U
lemma

isSheaf_toPresheafOfModules

L161 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.isSheaf_toPresheafOfModules
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
lemma isSheaf_toPresheafOfModules :
    Presheaf.IsSheaf (Opens.grothendieckTopology X) (toPresheafOfModules I).presheaf
def

toModule

L179 ↗
AlgebraicGeometry.Scheme.IdealSheafData.toModule
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · full declaration
def _root_.AlgebraicGeometry.Scheme.IdealSheafData.toModule : SheafOfModules
  X.ringCatSheaf where
  val := toPresheafOfModules I
  isSheaf := isSheaf_toPresheafOfModules I
lemma

toModule_sections

L186 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.toModule_sections
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
lemma toModule_sections (U : X.Opens) :
    ((toModule I).val.obj (op U) : Type u) = I.sectionsIdeal U
def

toModuleι

L189 ↗
AlgebraicGeometry.Scheme.IdealSheafData.toModuleι
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
def _root_.AlgebraicGeometry.Scheme.IdealSheafData.toModuleι : toModule I ⟶
  SheafOfModules.unit X.ringCatSheaf
lemma

toModuleι_app_apply

L200 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.toModuleι_app_apply
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
lemma toModuleι_app_apply (U : (X.Opens)ᵒᵖ) (s : (toModule I).val.obj U) :
    (toModuleι I).val.app U s = s.1
instance

(anonymous instance)

L203 ↗
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
instance (U : (X.Opens)ᵒᵖ) : Mono ((toModuleι I).val.app U)
lemma

toModuleι_comp_unitToPushforwardUnit

L206 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.toModuleι_comp_unitToPushforwardUnit
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
lemma toModuleι_comp_unitToPushforwardUnit :
    (I.toModuleι : (I.toModule : SheafOfModules X.ringCatSheaf) ⟶
        SheafOfModules.unit X.ringCatSheaf) ≫ I.subschemeι.unitToPushforwardUnit = 0
def

isLimitKernelFork

L218 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.isLimitKernelFork
Documentation

The universal kernel fork for inclusion of the ideal-section module.

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
def isLimitKernelFork : IsLimit (KernelFork.ofι
    (I.toModuleι : (I.toModule : SheafOfModules X.ringCatSheaf) ⟶ SheafOfModules.unit
      X.ringCatSheaf)
    (toModuleι_comp_unitToPushforwardUnit I))
def

moduleIsoToModule

L250 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.moduleIsoToModule
Documentation

The comparison between the kernel ideal module and its ideal-section model.

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
def moduleIsoToModule : (I.module : SheafOfModules X.ringCatSheaf) ≅ I.toModule
def

restrictRingCatSheafHom

L259 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.restrictRingCatSheafHom
Documentation

The canonical structure-ring map used for restriction to an open subscheme.

Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
section restrict
variable (U : X.Opens)
omit I in
Lean source · statement
def restrictRingCatSheafHom : (U : Scheme.{u}).ringCatSheaf ⟶
    (U.ι.opensFunctor.sheafPushforwardContinuous RingCat.{u}
      (Opens.grothendieckTopology (U : Scheme.{u})) (Opens.grothendieckTopology X)).obj
        X.ringCatSheaf
def

restrictFunctor'

L267 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.restrictFunctor'
Documentation

Restriction of modules to an open subscheme through the canonical ring map.

Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
section restrict
variable (U : X.Opens)
omit I in
Lean source · statement
def restrictFunctor' : X.Modules ⥤ (U : Scheme.{u}).Modules
lemma

restrictFunctor'_eq

L271 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.restrictFunctor'_eq
Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
section restrict
variable (U : X.Opens)
omit I in
Lean source · statement
lemma restrictFunctor'_eq : restrictFunctor' U = Modules.restrictFunctor U.ι
def

restrictFunctor'IsoPullback

L281 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.restrictFunctor'IsoPullback
Documentation

The comparison of this restriction functor with module pullback.

Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
section restrict
variable (U : X.Opens)
omit I in
Lean source · statement
def restrictFunctor'IsoPullback : restrictFunctor' U ≅ Modules.pullback U.ι
lemma

image_preimage_of_le

L286 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.image_preimage_of_le
Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
section restrict
variable (U : X.Opens)
variable {U} in
Lean source · statement
lemma image_preimage_of_le {V : X.Opens} (h : V ≤ U) : U.ι ''ᵁ (U.ι ⁻¹ᵁ V) = V
lemma

image_le

L291 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.image_le
Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
section restrict
variable (U : X.Opens)
variable {U} in
omit I in
Lean source · statement
lemma image_le (W : (U : Scheme.{u}).Opens) : U.ι ''ᵁ W ≤ U
abbrev

secX

L296 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.secX
Documentation

A section on an open subscheme viewed as a section on its image.

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
section restrict
variable (U : X.Opens)
variable {U} in
omit I in
Lean source · statement
abbrev secX (W : (U : Scheme.{u}).Opens) (a : Γ(U, W)) : Γ(X, U.ι ''ᵁ W)
def

gOn

L307 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.gOn
Documentation

The restriction of the chosen affine ideal generator to a smaller open.

Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
section trivialization
variable (B : X.affineOpens) (g : Γ(X, B)) (hg : g ∈ nonZeroDivisors Γ(X, B))
  (hIg : I.ideal B = Ideal.span {g})
omit I in
Lean source · statement
def gOn (W : X.Opens) (h : W ≤ (B : X.Opens)) : Γ(X, W)
lemma

gOn_res

L310 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.gOn_res
Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
section trivialization
variable (B : X.affineOpens) (g : Γ(X, B)) (hg : g ∈ nonZeroDivisors Γ(X, B))
  (hIg : I.ideal B = Ideal.span {g})
omit I in
Lean source · statement
lemma gOn_res {W W' : X.Opens} (h : W ≤ (B : X.Opens)) (i : W' ⟶ W) :
    X.presheaf.map i.op (gOn B g W h) = gOn B g W' (i.le.trans h)
lemma

gOn_mem

L317 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.gOn_mem
Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
section trivialization
variable (B : X.affineOpens) (g : Γ(X, B)) (hg : g ∈ nonZeroDivisors Γ(X, B))
  (hIg : I.ideal B = Ideal.span {g})
include hIg in
Lean source · statement
lemma gOn_mem (W : X.Opens) (h : W ≤ (B : X.Opens)) : gOn B g W h ∈ I.sectionsIdeal W
lemma

sectionsIdeal_eq_span

L323 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.sectionsIdeal_eq_span
Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
section trivialization
variable (B : X.affineOpens) (g : Γ(X, B)) (hg : g ∈ nonZeroDivisors Γ(X, B))
  (hIg : I.ideal B = Ideal.span {g})
include hIg in
Lean source · statement
lemma sectionsIdeal_eq_span (W : X.Opens) (hW : IsAffineOpen W) (h : W ≤ (B : X.Opens)) :
    I.sectionsIdeal W = Ideal.span {gOn B g W h}
lemma

gOn_mem_nonZeroDivisors

L331 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.gOn_mem_nonZeroDivisors
Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
section trivialization
variable (B : X.affineOpens) (g : Γ(X, B)) (hg : g ∈ nonZeroDivisors Γ(X, B))
  (hIg : I.ideal B = Ideal.span {g})
omit I in
include hg in
Lean source · statement
lemma gOn_mem_nonZeroDivisors (h' : Γ(X, B)) (W : X.Opens) (e : W = X.basicOpen h') :
    gOn B g W (e.trans_le (X.basicOpen_le h')) ∈ nonZeroDivisors Γ(X, W)
def

mulGen

L338 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.mulGen
Documentation

Multiplication by the local generator, as a morphism to the ideal-section module.

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
section trivialization
variable (B : X.affineOpens) (g : Γ(X, B)) (hg : g ∈ nonZeroDivisors Γ(X, B))
  (hIg : I.ideal B = Ideal.span {g})
Lean source · statement
def mulGen : SheafOfModules.unit ((B : X.Opens) : Scheme.{u}).ringCatSheaf ⟶
    (restrictFunctor' (B : X.Opens)).obj I.toModule
lemma

mulGen_app_apply_coe

L364 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.mulGen_app_apply_coe
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
section trivialization
variable (B : X.affineOpens) (g : Γ(X, B)) (hg : g ∈ nonZeroDivisors Γ(X, B))
  (hIg : I.ideal B = Ideal.span {g})
Lean source · statement
lemma mulGen_app_apply_coe (W : (((B : X.Opens) : Scheme.{u}).Opens)ᵒᵖ)
    (a : Γ((B : X.Opens), W.unop)) :
    ((mulGen I B g hIg).val.app W a).1 =
      secX (B : X.Opens) W.unop a * gOn B g _ (image_le _ W.unop)
lemma

isIso_mulGen

L370 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_isInvertible_module.AlgebraicGeometry.Scheme.IdealSheafData.isIso_mulGen
Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (I : X.IdealSheafData)
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
section trivialization
variable (B : X.affineOpens) (g : Γ(X, B)) (hg : g ∈ nonZeroDivisors Γ(X, B))
  (hIg : I.ideal B = Ideal.span {g})
include hg in
Lean source · statement
lemma isIso_mulGen : IsIso (mulGen I B g hIg)
theorem

isInvertible_module

L425 ↗
AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.isInvertible_module
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_module
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.AlgebraicGeometry _root_.AlgebraicGeometry.Scheme.IdealSheafData in
with_weak_namespace AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.isInvertible_module {X :
  AlgebraicGeometry.Scheme.{u}} {I : X.IdealSheafData} (hI : I.IsInvertible) :
    AlgebraicGeometry.Scheme.Modules.IsInvertible I.module

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