NYLL
Module

Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor
43 declarations indexed from sourceView source ↗

Module documentation

Multiplication of invertible ideal modules

Constructs the isomorphism between the product ideal module and the tensor product of its invertible factors.

Imports7
Imported by13

Declarations

def

sectionsIdeal

L56 ↗
AlgebraicGeometry.Scheme.IdealSheafData.sectionsIdeal
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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

L61 ↗
AlgebraicGeometry.Scheme.IdealSheafData.mem_sectionsIdeal_iff
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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

L67 ↗
AlgebraicGeometry.Scheme.IdealSheafData.sectionsIdeal_eq_ideal
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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

L73 ↗
AlgebraicGeometry.Scheme.IdealSheafData.map_mem_sectionsIdeal
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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

L84 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.sectionsPresheaf
Documentation

The presheaf of additive groups of sections vanishing on the closed subscheme.

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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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)

L105 ↗
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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

L109 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.sectionsPresheaf_map_apply_coe
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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

L114 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.toPresheafOfModules
Documentation

The module presheaf of sections vanishing on the closed subscheme.

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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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

L122 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.toPresheafOfModules_presheaf
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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

L127 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.sectionsSubfunctor
Documentation

The subfunctor of regular functions vanishing on the closed subscheme.

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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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

L132 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.sectionsIso
Documentation

The identification of the two presheaf descriptions of ideal 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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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

L140 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.mem_sectionsIdeal_of_locally
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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

L162 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.isSheaf_toPresheafOfModules
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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

L180 ↗
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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 : X.Modules where
  val := toPresheafOfModules I
  isSheaf := isSheaf_toPresheafOfModules I
lemma

toModule_sections

L186 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.toModule_sections
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.toModuleι_app_apply
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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)
instance

idealMulConcreteHomGroup

L208 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.idealMulConcreteHomGroup
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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 NativeKernel
Lean source · statement
instance idealMulConcreteHomGroup :
    AddCommGroup ((I.toModule : SheafOfModules X.ringCatSheaf) ⟶
      (SheafOfModules.pushforward I.subschemeι.toRingCatSheafHom).obj
        (SheafOfModules.unit I.subscheme.ringCatSheaf))
lemma

toModuleι_comp_unitToPushforwardUnit

L214 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.toModuleι_comp_unitToPushforwardUnit
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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 NativeKernel
local instance idealMulConcreteHomGroup :
    AddCommGroup ((I.toModule : SheafOfModules X.ringCatSheaf) ⟶
      (SheafOfModules.pushforward I.subschemeι.toRingCatSheafHom).obj
        (SheafOfModules.unit I.subscheme.ringCatSheaf)) :=
  (SheafOfModules.fullyFaithfulForget X.ringCatSheaf).homEquiv.addCommGroup
Lean source · statement
lemma toModuleι_comp_unitToPushforwardUnit :
    (I.toModuleι : (I.toModule : SheafOfModules X.ringCatSheaf) ⟶
        SheafOfModules.unit X.ringCatSheaf) ≫ I.subschemeι.unitToPushforwardUnit = 0
def

isLimitKernelFork

L226 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.isLimitKernelFork
Documentation

The ideal section module is the kernel of restriction to the closed 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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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 NativeKernel
local instance idealMulConcreteHomGroup :
    AddCommGroup ((I.toModule : SheafOfModules X.ringCatSheaf) ⟶
      (SheafOfModules.pushforward I.subschemeι.toRingCatSheafHom).obj
        (SheafOfModules.unit I.subscheme.ringCatSheaf)) :=
  (SheafOfModules.fullyFaithfulForget X.ringCatSheaf).homEquiv.addCommGroup
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

L258 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.moduleIsoToModule
Documentation

The canonical ideal module identified with its sectionwise kernel model.

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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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 NativeKernel
local instance idealMulConcreteHomGroup :
    AddCommGroup ((I.toModule : SheafOfModules X.ringCatSheaf) ⟶
      (SheafOfModules.pushforward I.subschemeι.toRingCatSheafHom).obj
        (SheafOfModules.unit I.subscheme.ringCatSheaf)) :=
  (SheafOfModules.fullyFaithfulForget X.ringCatSheaf).homEquiv.addCommGroup
Lean source · statement
def moduleIsoToModule : (I.module : SheafOfModules X.ringCatSheaf) ≅ I.toModule
lemma

exists_affineOpen_le

L264 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.exists_affineOpen_le
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
omit I in
Lean source · statement
lemma exists_affineOpen_le {U : X.Opens} {x : X} (hx : x ∈ U) :
    ∃ V : X.affineOpens, x ∈ (V : X.Opens) ∧ (V : X.Opens) ≤ U
instance

idealMulOppositeSectionsModule

L271 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.idealMulOppositeSectionsModule
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
Lean source · statement
instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U)
instance

idealMulSectionsModule

L274 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.idealMulSectionsModule
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
local instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U) := (P.obj U).isModule
Lean source · statement
instance idealMulSectionsModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U))
lemma

mul_mem_sectionsIdeal_mul

L277 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.mul_mem_sectionsIdeal_mul
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
local instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U) := (P.obj U).isModule
local instance idealMulSectionsModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
Lean source · statement
lemma mul_mem_sectionsIdeal_mul {U : X.Opens} {s t : Γ(X, U)} (hs : s ∈ I.sectionsIdeal U)
    (ht : t ∈ J.sectionsIdeal U) : s * t ∈ (I * J).sectionsIdeal U
lemma

sectionsIdeal_mul_eq

L288 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.sectionsIdeal_mul_eq
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
local instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U) := (P.obj U).isModule
local instance idealMulSectionsModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
Lean source · statement
lemma sectionsIdeal_mul_eq (W : X.Opens) (hW : IsAffineOpen W) :
    (I * J).sectionsIdeal W = I.sectionsIdeal W * J.sectionsIdeal W
def

mulApp

L294 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.mulApp
Documentation

The multiplication map on tensor products of ideal sections.

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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
local instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U) := (P.obj U).isModule
local instance idealMulSectionsModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
Lean source · statement
def mulApp (U : (X.Opens)ᵒᵖ) :
    ((toModule I).val ⊗ (toModule J).val).obj U ⟶ (toModule (I * J)).val.obj U
lemma

mulApp_tmul

L303 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.mulApp_tmul
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
local instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U) := (P.obj U).isModule
local instance idealMulSectionsModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
Lean source · full declaration
lemma mulApp_tmul (U : (X.Opens)ᵒᵖ) (s : (toModule I).val.obj U) (t : (toModule J).val.obj U) :
    (DFunLike.coe (α := (((toModule I).val ⊗ (toModule J).val).obj U :))
      (β := fun _ => (toModule (I * J)).val.obj U)
      (mulApp I J U).hom (s ⊗ₜ[Γ(X, U.unop)] t)).1 = s.1 * t.1 := by
  let : CommRing ((X.ringCatSheaf.obj).obj U) := inferInstanceAs (CommRing Γ(X, U.unop))
  erw [ModuleCat.MonoidalCategory.tensorLift_tmul]
def

mulMap

L311 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.mulMap
Documentation

The presheaf morphism multiplying sections of the two ideal modules.

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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
local instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U) := (P.obj U).isModule
local instance idealMulSectionsModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
Lean source · full declaration
def mulMap : (toModule I).val ⊗ (toModule J).val ⟶ (toModule (I * J)).val where
  app U := mulApp I J U
  naturality {U V} i := ModuleCat.MonoidalCategory.tensor_ext (fun s t => by
    apply Subtype.ext
    change (DFunLike.coe (α := (((toModule I).val ⊗ (toModule J).val).obj V :))
      (β := fun _ => (toModule (I * J)).val.obj V) (mulApp I J V).hom
        (DFunLike.coe (α := (((toModule I).val ⊗ (toModule J).val).obj U :))
          (β := fun _ => (ModuleCat.restrictScalars (X.ringCatSheaf.obj.map i).hom).obj
            (((toModule I).val ⊗ (toModule J).val).obj V))
          (ModuleCat.Hom.hom (((toModule I).val ⊗ (toModule J).val).map i))
            (s ⊗ₜ[Γ(X, U.unop)] t))).1 =
      X.presheaf.map i (DFunLike.coe (α := (((toModule I).val ⊗ (toModule J).val).obj U :))
        (β := fun _ => (toModule (I * J)).val.obj U) (mulApp I J U).hom (s ⊗ₜ[Γ(X, U.unop)] t)).1
    erw [_root_.PresheafOfModules.tensorObj_map_tmul' (R := X.sheaf.obj)
      ((toModule I).val) (G := (toModule J).val) i s t]
    erw [mulApp_tmul, mulApp_tmul]
    exact (map_mul (X.presheaf.map i).hom s.1 t.1).symm)
lemma

mulMap_app_tmul

L329 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.mulMap_app_tmul
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
local instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U) := (P.obj U).isModule
local instance idealMulSectionsModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
Lean source · full declaration
lemma mulMap_app_tmul (U : (X.Opens)ᵒᵖ) (s : (toModule I).val.obj U) (t : (toModule J).val.obj U) :
    (DFunLike.coe (α := (((toModule I).val ⊗ (toModule J).val).obj U :))
      (β := fun _ => (toModule (I * J)).val.obj U)
      ((mulMap I J).app U).hom (s ⊗ₜ[Γ(X, U.unop)] t)).1 = s.1 * t.1 :=
  mulApp_tmul I J U s t
def

genEquiv

L344 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.genEquiv
Documentation

Coordinates in a principal ideal generated by a nonzero divisor.

Source context 34 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
local instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U) := (P.obj U).isModule
local instance idealMulSectionsModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section good
variable {I J}
variable {W : X.Opens} (hW : IsAffineOpen W) (a b : Γ(X, W))
  (ha : a ∈ nonZeroDivisors Γ(X, W)) (hb : b ∈ nonZeroDivisors Γ(X, W))
  (hIa : I.sectionsIdeal W = Ideal.span {a}) (hJb : J.sectionsIdeal W = Ideal.span {b})
omit I J in
Lean source · statement
def genEquiv (K : X.IdealSheafData) (g : Γ(X, W)) (hg : g ∈ nonZeroDivisors Γ(X, W))
    (hKg : K.sectionsIdeal W = Ideal.span {g}) : Γ(X, W) ≃ₗ[Γ(X, W)] K.sectionsIdeal W
lemma

genEquiv_apply_coe

L360 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.genEquiv_apply_coe
Source context 34 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
local instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U) := (P.obj U).isModule
local instance idealMulSectionsModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section good
variable {I J}
variable {W : X.Opens} (hW : IsAffineOpen W) (a b : Γ(X, W))
  (ha : a ∈ nonZeroDivisors Γ(X, W)) (hb : b ∈ nonZeroDivisors Γ(X, W))
  (hIa : I.sectionsIdeal W = Ideal.span {a}) (hJb : J.sectionsIdeal W = Ideal.span {b})
omit I J in
Lean source · statement
lemma genEquiv_apply_coe (K : X.IdealSheafData) (g : Γ(X, W)) (hg : g ∈ nonZeroDivisors Γ(X, W))
    (hKg : K.sectionsIdeal W = Ideal.span {g}) (c : Γ(X, W)) :
    (genEquiv K g hg hKg c).1 = c * g
lemma

smul_genEquiv_one

L365 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.smul_genEquiv_one
Source context 34 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
local instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U) := (P.obj U).isModule
local instance idealMulSectionsModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section good
variable {I J}
variable {W : X.Opens} (hW : IsAffineOpen W) (a b : Γ(X, W))
  (ha : a ∈ nonZeroDivisors Γ(X, W)) (hb : b ∈ nonZeroDivisors Γ(X, W))
  (hIa : I.sectionsIdeal W = Ideal.span {a}) (hJb : J.sectionsIdeal W = Ideal.span {b})
omit I J in
Lean source · statement
lemma smul_genEquiv_one (K : X.IdealSheafData) (g : Γ(X, W)) (hg : g ∈ nonZeroDivisors Γ(X, W))
    (hKg : K.sectionsIdeal W = Ideal.span {g}) (c : Γ(X, W)) :
    c • genEquiv K g hg hKg 1 = genEquiv K g hg hKg c
lemma

genEquiv_symm_smul

L371 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.genEquiv_symm_smul
Source context 34 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
local instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U) := (P.obj U).isModule
local instance idealMulSectionsModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section good
variable {I J}
variable {W : X.Opens} (hW : IsAffineOpen W) (a b : Γ(X, W))
  (ha : a ∈ nonZeroDivisors Γ(X, W)) (hb : b ∈ nonZeroDivisors Γ(X, W))
  (hIa : I.sectionsIdeal W = Ideal.span {a}) (hJb : J.sectionsIdeal W = Ideal.span {b})
omit I J in
Lean source · statement
lemma genEquiv_symm_smul (K : X.IdealSheafData) (g : Γ(X, W)) (hg : g ∈ nonZeroDivisors Γ(X, W))
    (hKg : K.sectionsIdeal W = Ideal.span {g}) (u : K.sectionsIdeal W) :
    (genEquiv K g hg hKg).symm u • (genEquiv K g hg hKg 1) = u
lemma

mulApp_bijective

L377 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.mulApp_bijective
Source context 34 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
local instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U) := (P.obj U).isModule
local instance idealMulSectionsModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section good
variable {I J}
variable {W : X.Opens} (hW : IsAffineOpen W) (a b : Γ(X, W))
  (ha : a ∈ nonZeroDivisors Γ(X, W)) (hb : b ∈ nonZeroDivisors Γ(X, W))
  (hIa : I.sectionsIdeal W = Ideal.span {a}) (hJb : J.sectionsIdeal W = Ideal.span {b})
include hW ha hb hIa hJb in
Lean source · statement
lemma mulApp_bijective : Function.Bijective (mulApp I J (op W))
lemma

map_mem_nonZeroDivisors_of_eq_basicOpen

L428 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.map_mem_nonZeroDivisors_of_eq_basicOpen
Source context 33 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
local instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U) := (P.obj U).isModule
local instance idealMulSectionsModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section cover
variable {I J}
omit I J in
Lean source · statement
lemma map_mem_nonZeroDivisors_of_eq_basicOpen (B : X.affineOpens) (h : Γ(X, B))
    {g : Γ(X, B)} (hg : g ∈ nonZeroDivisors Γ(X, B)) (W : X.Opens) (e : W = X.basicOpen h) :
    X.presheaf.map (homOfLE (e.trans_le (X.basicOpen_le h))).op g ∈ nonZeroDivisors Γ(X, W)
lemma

sectionsIdeal_eq_span_map

L435 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.sectionsIdeal_eq_span_map
Source context 32 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
local instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U) := (P.obj U).isModule
local instance idealMulSectionsModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section cover
variable {I J}
Lean source · statement
lemma sectionsIdeal_eq_span_map (K : X.IdealSheafData) (B : X.affineOpens) (g : Γ(X, B))
    (hKg : K.ideal B = Ideal.span {g}) (W : X.Opens) (hW : IsAffineOpen W) (h : W ≤ (B : X.Opens)) :
    K.sectionsIdeal W = Ideal.span {X.presheaf.map (homOfLE h).op g}
lemma

exists_good

L443 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.exists_good
Source context 33 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
local instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U) := (P.obj U).isModule
local instance idealMulSectionsModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
section cover
variable {I J}
include I J in
Lean source · statement
lemma exists_good (hI : I.IsInvertible) (hJ : J.IsInvertible) {U : X.Opens} {x : X} (hx : x ∈ U) :
    ∃ (W : X.Opens) (_ : IsAffineOpen W) (a b : Γ(X, W)), a ∈ nonZeroDivisors Γ(X, W) ∧
      b ∈ nonZeroDivisors Γ(X, W) ∧ I.sectionsIdeal W = Ideal.span {a} ∧
      J.sectionsIdeal W = Ideal.span {b} ∧ x ∈ W ∧ W ≤ U
lemma

W_mulMap

L476 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.W_mulMap
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
local instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U) := (P.obj U).isModule
local instance idealMulSectionsModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
Lean source · statement
lemma W_mulMap (hI : I.IsInvertible) (hJ : J.IsInvertible) :
    (Opens.grothendieckTopology X).W ((PresheafOfModules.toPresheaf _).map (mulMap I J))
instance

isIso_sheafify_mulMap

L506 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.isIso_sheafify_mulMap
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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
local instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U) := (P.obj U).isModule
local instance idealMulSectionsModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
Lean source · statement
instance isIso_sheafify_mulMap [Fact I.IsInvertible] [Fact J.IsInvertible] :
    IsIso ((Scheme.Modules.sheafify X).map (mulMap I J))
def

toModuleTensorIso

L517 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor.AlgebraicGeometry.Scheme.IdealSheafData.toModuleTensorIso
Documentation

The tensor product of invertible ideal modules identified with their product module.

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_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
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
variable (J : X.IdealSheafData)
local instance idealMulOppositeSectionsModule (P : X.PresheafOfModules) (U : X.Opensᵒᵖ) :
    Module Γ(X, U.unop) (P.obj U) := (P.obj U).isModule
local instance idealMulSectionsModule (P : X.PresheafOfModules) (U : X.Opens) :
    Module Γ(X, U) (P.obj (op U)) := (P.obj (op U)).isModule
Lean source · statement
def toModuleTensorIso [Fact I.IsInvertible] [Fact J.IsInvertible] :
    toModule I ⊗ toModule J ≅ toModule (I * J)
theorem

nonempty_mul_module_iso_tensor

L529 ↗
AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.nonempty_mul_module_iso_tensor
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_nonempty_mul_module_iso_tensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.TensorProduct
open _root_.AlgebraicGeometry _root_.AlgebraicGeometry.Scheme.IdealSheafData in
with_weak_namespace AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.nonempty_mul_module_iso_tensor
  {X : AlgebraicGeometry.Scheme.{u}} {I J : X.IdealSheafData}
    (hI : I.IsInvertible) (hJ : J.IsInvertible) :
    Nonempty ((I * J).module ≅ I.module ⊗ J.module)

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