NYLL
Module

Scheme_Modules_IsInvertible_dual_monoidalV2.lean

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

Module documentation

Duals and evaluation for invertible modules

Local trivializations identify generators and their duals, and restriction compatibility transports the resulting maps to sheaves of modules.

Imports16
Imported by4

Declarations

def

toPresheafHom

L81 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InternalHom.toPresheafHom
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_5b3a613b
universe u v' u'
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
open _root_.Opposite
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InternalHom
open _root_.PresheafOfModules.InternalHom
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
Lean source · full declaration
def toPresheafHom (X : Cᵒᵖ) (φ : naturalFamilies F N X) :
    (presheafHom F.presheaf N.presheaf).obj X where
  app Y := AddCommGrpCat.ofHom (φ.1 Y.unop.hom.op).toAddMonoidHom
  naturality {Y Y'} k := by
    ext x
    change φ.1 Y'.unop.hom.op (F.map k.unop.left.op x) = N.map k.unop.left.op (φ.1 Y.unop.hom.op x)
    rw [φ.2 Y.unop.hom.op k.unop.left.op x]
    exact congr_app φ (by rw [← op_comp, Over.w]) _
abbrev

appAt

L91 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InternalHom.appAt
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_5b3a613b
universe u v' u'
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
open _root_.Opposite
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InternalHom
open _root_.PresheafOfModules.InternalHom
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
variable {F N} in
Lean source · statement
abbrev appAt {X : Cᵒᵖ} (s : (presheafHom F.presheaf N.presheaf).obj X) (Y : (Over X.unop)ᵒᵖ)
    (x : F.obj (Opposite.op Y.unop.left)) : N.obj (Opposite.op Y.unop.left)
lemma

appAt_toPresheafHom

L95 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InternalHom.appAt_toPresheafHom
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_5b3a613b
universe u v' u'
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
open _root_.Opposite
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InternalHom
open _root_.PresheafOfModules.InternalHom
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
variable {F N} in
Lean source · statement
lemma appAt_toPresheafHom (X : Cᵒᵖ) (φ : naturalFamilies F N X) (Y : (Over
  X.unop)ᵒᵖ)
    (x : F.obj (Opposite.op Y.unop.left)) :
    appAt (toPresheafHom F N X φ) Y x = φ.1 Y.unop.hom.op x
def

linearSub

L100 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InternalHom.linearSub
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_5b3a613b
universe u v' u'
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
open _root_.Opposite
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InternalHom
open _root_.PresheafOfModules.InternalHom
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
variable {F N} in
Lean source · full declaration
def linearSub : Subfunctor (presheafHom F.presheaf N.presheaf) where
  obj X := { s | ∀ (Y : (Over X.unop)ᵒᵖ) (r : R.obj (Opposite.op Y.unop.left))
    (x : F.obj (Opposite.op Y.unop.left)), appAt s Y (r • x) = r • appAt s Y x }
  map h _ hs Y r x := hs (Opposite.op ((Over.map h.unop).obj Y.unop)) r x
def

ofPresheafHom

L105 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InternalHom.ofPresheafHom
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_5b3a613b
universe u v' u'
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
open _root_.Opposite
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InternalHom
open _root_.PresheafOfModules.InternalHom
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
variable {F N} in
Lean source · statement
def ofPresheafHom (X : Cᵒᵖ) (s : (linearSub F N).obj X) : naturalFamilies F N
  X
lemma

ofPresheafHom_app

L117 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InternalHom.ofPresheafHom_app
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_5b3a613b
universe u v' u'
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
open _root_.Opposite
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InternalHom
open _root_.PresheafOfModules.InternalHom
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
variable {F N} in
Lean source · statement
lemma ofPresheafHom_app (X : Cᵒᵖ) (s : (linearSub F N).obj X) {Y : Cᵒᵖ} (f : X ⟶ Y)
    (x : F.obj Y) :
    (ofPresheafHom F N X s).1 f x = appAt s.1 (Opposite.op (Over.mk f.unop)) x
def

equivLinearSub

L121 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InternalHom.equivLinearSub
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_5b3a613b
universe u v' u'
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
open _root_.Opposite
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InternalHom
open _root_.PresheafOfModules.InternalHom
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
variable {F N} in
Lean source · full declaration
def equivLinearSub (X : Cᵒᵖ) : naturalFamilies F N X ≃ (linearSub F N).obj X
  where
  toFun φ := ⟨toPresheafHom F N X φ, fun Y r x => (φ.1 Y.unop.hom.op).map_smul r x⟩
  invFun s := ofPresheafHom F N X s
  left_inv φ := by
    apply naturalFamilies_ext; intro Y f x; rfl
  right_inv s := by rfl
def

isoLinearSub

L129 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InternalHom.isoLinearSub
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_5b3a613b
universe u v' u'
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
open _root_.Opposite
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InternalHom
open _root_.PresheafOfModules.InternalHom
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
variable {F N} in
Lean source · statement
def isoLinearSub :
    InternalHom.presheaf F N ⋙ forget AddCommGrpCat ≅ (linearSub F N).toFunctor
lemma

linearSub_local

L135 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InternalHom.linearSub_local
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_5b3a613b
universe u v' u'
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
open _root_.Opposite
noncomputable section
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InternalHom
open _root_.PresheafOfModules.InternalHom
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
variable {F N} in
variable {F N}
Lean source · statement
lemma linearSub_local {J : GrothendieckTopology C}
    (hNsep : Presieve.IsSeparated J (N.presheaf ⋙ forget AddCommGrpCat))
    (X : Cᵒᵖ) (s : (presheafHom F.presheaf N.presheaf).obj X)
    (hs : (linearSub F N).sieveOfSection s ∈ J X.unop) : s ∈ (linearSub F N).obj X
theorem

isSheaf_ihomObj

L174 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.isSheaf_ihomObj
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_5b3a613b
universe u v' u'
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
open _root_.Opposite
open scoped _root_.PresheafOfModules in
Lean source · statement
theorem PresheafOfModules.isSheaf_ihomObj {C : Type u} [Category.{u} C]
    {R : Cᵒᵖ ⥤ CommRingCat.{u}} (F N : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
    {J : GrothendieckTopology C} (hN : Presheaf.IsSheaf J N.presheaf) :
    Presheaf.IsSheaf J (PresheafOfModules.ihomObj F N).presheaf
abbrev

dual

L227 ↗
PresheafOfModules.InvertibleDual.dual
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
Lean source · statement
abbrev _root_.PresheafOfModules.InvertibleDual.dual : PresheafOfModules.{u}
  (R ⋙ forget₂ CommRingCat RingCat)
abbrev

ev

L235 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.ev
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
Lean source · statement
abbrev ev : F ⊗ dual F ⟶ 𝟙_ _
structure

TrivializationBelow

L237 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.TrivializationBelow
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
Lean source · full declaration
structure TrivializationBelow (X₀ : Cᵒᵖ) where
  gen : ∀ {Y : Cᵒᵖ} (_ : X₀ ⟶ Y), F.obj Y
  compat : ∀ {Y Z : Cᵒᵖ} (f : X₀ ⟶ Y) (g : Y ⟶ Z), F.map g (gen f) = gen (f ≫ g)
  bij : ∀ {Y : Cᵒᵖ} (f : X₀ ⟶ Y), Function.Bijective (fun a : R.obj Y => a • gen f)
def

restrictTo

L246 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.TrivializationBelow.restrictTo
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
variable {F} {X₀ : Cᵒᵖ} (D : TrivializationBelow F X₀)
namespace TrivializationBelow
Lean source · full declaration
def restrictTo {Y : Cᵒᵖ} (f : X₀ ⟶ Y) : TrivializationBelow F Y where
  gen g := D.gen (f ≫ g)
  compat g g' := by rw [D.compat, Category.assoc]
  bij g := D.bij (f ≫ g)
def

triv

L251 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.TrivializationBelow.triv
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
variable {F} {X₀ : Cᵒᵖ} (D : TrivializationBelow F X₀)
namespace TrivializationBelow
Lean source · statement
def triv {Y : Cᵒᵖ} (f : X₀ ⟶ Y) : R.obj Y ≃ₗ[R.obj Y] F.obj Y
def

coord

L254 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.TrivializationBelow.coord
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
variable {F} {X₀ : Cᵒᵖ} (D : TrivializationBelow F X₀)
namespace TrivializationBelow
Lean source · statement
def coord {Y : Cᵒᵖ} (f : X₀ ⟶ Y) : F.obj Y →ₗ[R.obj Y] R.obj Y
lemma

coord_smul_gen

L257 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.TrivializationBelow.coord_smul_gen
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
variable {F} {X₀ : Cᵒᵖ} (D : TrivializationBelow F X₀)
namespace TrivializationBelow
Lean source · statement
lemma coord_smul_gen {Y : Cᵒᵖ} (f : X₀ ⟶ Y) (x : F.obj Y) : D.coord f x • D.gen f = x
lemma

coord_gen_smul

L260 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.TrivializationBelow.coord_gen_smul
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
variable {F} {X₀ : Cᵒᵖ} (D : TrivializationBelow F X₀)
namespace TrivializationBelow
Lean source · statement
lemma coord_gen_smul {Y : Cᵒᵖ} (f : X₀ ⟶ Y) (a : R.obj Y) : D.coord f (a • D.gen f) = a
lemma

coord_gen

L263 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.TrivializationBelow.coord_gen
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
variable {F} {X₀ : Cᵒᵖ} (D : TrivializationBelow F X₀)
namespace TrivializationBelow
Lean source · statement
lemma coord_gen {Y : Cᵒᵖ} (f : X₀ ⟶ Y) : D.coord f (D.gen f) = 1
lemma

coord_map

L266 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.TrivializationBelow.coord_map
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
variable {F} {X₀ : Cᵒᵖ} (D : TrivializationBelow F X₀)
namespace TrivializationBelow
Lean source · statement
lemma coord_map {Y Z : Cᵒᵖ} (f : X₀ ⟶ Y) (g : Y ⟶ Z) (x : F.obj Y) :
    D.coord (f ≫ g) (F.map g x) = R.map g (D.coord f x)
def

dualGen

L272 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.TrivializationBelow.dualGen
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
variable {F} {X₀ : Cᵒᵖ} (D : TrivializationBelow F X₀)
namespace TrivializationBelow
Lean source · statement
def dualGen : (dual F).obj X₀
lemma

dualGen_app

L277 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.TrivializationBelow.dualGen_app
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
variable {F} {X₀ : Cᵒᵖ} (D : TrivializationBelow F X₀)
namespace TrivializationBelow
Lean source · statement
lemma dualGen_app {Y : Cᵒᵖ} (f : X₀ ⟶ Y) (x : F.obj Y) :
    (D.dualGen).1 f x = D.coord f x
lemma

eq_smul_dualGen

L280 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.TrivializationBelow.eq_smul_dualGen
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
variable {F} {X₀ : Cᵒᵖ} (D : TrivializationBelow F X₀)
namespace TrivializationBelow
Lean source · statement
lemma eq_smul_dualGen (φ : (dual F).obj X₀) : φ = SMul.smul (M := R.obj X₀) (α := (dual
  F).obj X₀)
      (φ.1 (𝟙 X₀) (D.gen (𝟙 X₀))) D.dualGen
def

evInv

L294 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.TrivializationBelow.evInv
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
variable {F} {X₀ : Cᵒᵖ} (D : TrivializationBelow F X₀)
namespace TrivializationBelow
Lean source · statement
def evInv : R.obj X₀ →ₗ[R.obj X₀] (F.obj X₀ ⊗[R.obj X₀] (dual F).obj X₀)
def

evLinear

L297 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.TrivializationBelow.evLinear
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
variable {F} {X₀ : Cᵒᵖ} (D : TrivializationBelow F X₀)
namespace TrivializationBelow
Lean source · statement
def evLinear
    (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat)) (X₀ : Cᵒᵖ) :
    (F.obj X₀ ⊗[R.obj X₀] (dual F).obj X₀) →ₗ[R.obj X₀] R.obj X₀
lemma

ev_app_tmul

L303 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.TrivializationBelow.ev_app_tmul
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
variable {F} {X₀ : Cᵒᵖ} (D : TrivializationBelow F X₀)
namespace TrivializationBelow
omit D in
Lean source · statement
lemma ev_app_tmul (x : F.obj X₀) (φ : (dual F).obj X₀) :
    (evLinear F X₀) (x ⊗ₜ[R.obj X₀] φ) = φ.1 (𝟙 X₀) x
lemma

ev_evInv

L307 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.TrivializationBelow.ev_evInv
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
variable {F} {X₀ : Cᵒᵖ} (D : TrivializationBelow F X₀)
namespace TrivializationBelow
Lean source · statement
lemma ev_evInv (a : R.obj X₀) :
    (evLinear F X₀) (D.evInv a) = a
lemma

evInv_ev

L314 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.TrivializationBelow.evInv_ev
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
variable {F} {X₀ : Cᵒᵖ} (D : TrivializationBelow F X₀)
namespace TrivializationBelow
Lean source · statement
lemma evInv_ev (z : (F.obj X₀ ⊗[R.obj X₀] (dual F).obj X₀)) :
    D.evInv ((evLinear F X₀) z) = z
theorem

ev_app_bijective

L331 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.TrivializationBelow.ev_app_bijective
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
variable {F} {X₀ : Cᵒᵖ} (D : TrivializationBelow F X₀)
namespace TrivializationBelow
Lean source · statement
theorem ev_app_bijective (D : TrivializationBelow F X₀) : Function.Bijective ((ev F).app
  X₀)
theorem

W_ev

L338 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.W_ev
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.PresheafOfModules.InternalHom
open PresheafOfModules.InternalHom
open _root_.TensorProduct
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
variable {F} {X₀ : Cᵒᵖ} (D : TrivializationBelow F X₀)
variable (F) in
Lean source · statement
theorem W_ev {J : GrothendieckTopology C} [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
    (hloc : ∀ (U : C), ∃ (S : Sieve U), S ∈ J U ∧
      ∀ ⦃V : C⦄ (f : V ⟶ U), S f → Nonempty (TrivializationBelow F (op V))) :
    J.W ((toPresheaf _).map (ev F))
def

trivializationOfLE_bbe2083f

L405 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.trivializationOfLE_bbe2083f
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
Lean source · statement
def trivializationOfLE_bbe2083f {U V : X.Opens} (h : V ≤ U) (L : X.Modules)
    (e : (Modules.pullback U.ι).obj L ≅ SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf) :
    (Modules.pullback V.ι).obj L ≅ SheafOfModules.unit (V : Scheme.{u}).ringCatSheaf
def

dualSheaf

L413 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.dualSheaf
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
Lean source · full declaration
def dualSheaf (L : X.Modules) : X.Modules where
  val := PresheafOfModules.ihomObj L.val (𝟙_ X.PresheafOfModules)
  isSheaf := PresheafOfModules.isSheaf_ihomObj L.val _ (SheafOfModules.unit X.ringCatSheaf).isSheaf
def

restrictRingCatSheafHom

L419 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.restrictRingCatSheafHom
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
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'

L425 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.restrictFunctor'
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
Lean source · statement
def restrictFunctor' : X.Modules ⥤ (U : Scheme.{u}).Modules
lemma

restrictFunctor'_eq

L428 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.restrictFunctor'_eq
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
Lean source · statement
lemma restrictFunctor'_eq : restrictFunctor' U = Modules.restrictFunctor U.ι
def

restrictFunctor'IsoPullback

L436 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.restrictFunctor'IsoPullback
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
Lean source · statement
def restrictFunctor'IsoPullback : restrictFunctor' U ≅ Modules.pullback U.ι
lemma

image_preimage_of_le

L441 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.image_preimage_of_le
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
Lean source · statement
lemma image_preimage_of_le {V : X.Opens} (h : V ≤ U) : U.ι ''ᵁ (U.ι ⁻¹ᵁ V) = V
def

gen₀

L449 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.gen₀
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
section
variable (e : (restrictFunctor' U).obj L ≅ SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf)
Lean source · statement
def gen₀ (W : (U : Scheme.{u}).Opens) : Γ(L, U.ι ''ᵁ W)
lemma

gen₀_spec

L452 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.gen₀_spec
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
section
variable (e : (restrictFunctor' U).obj L ≅ SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf)
Lean source · statement
lemma gen₀_spec (W : (U : Scheme.{u}).Opens) (b : Γ(X, U.ι ''ᵁ W)) :
    (e.inv.val.app (op W)).hom b = b • gen₀ L e W
lemma

gen₀_bijective

L459 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.gen₀_bijective
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
section
variable (e : (restrictFunctor' U).obj L ≅ SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf)
Lean source · full declaration
lemma gen₀_bijective (W : (U : Scheme.{u}).Opens) :
    Function.Bijective (fun b : Γ(X, U.ι ''ᵁ W) => b • gen₀ L e W) := by
  have h : Function.Bijective ((e.inv.val.app (op W)).hom) := by
    refine Function.bijective_iff_has_inverse.2 ⟨(e.hom.val.app (op W)).hom, fun b => ?_, fun m =>
      ?_⟩
    · exact congr($(e.inv_hom_id).val.app (op W) |>.hom b)
    · exact congr($(e.hom_inv_id).val.app (op W) |>.hom m)
  exact (funext (gen₀_spec L e W) ▸ h :)
lemma

gen₀_map

L468 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.gen₀_map
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
section
variable (e : (restrictFunctor' U).obj L ≅ SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf)
Lean source · statement
lemma gen₀_map {W W' : (U : Scheme.{u}).Opens} (i : W' ⟶ W) :
    L.val.map (U.ι.opensFunctor.map i).op (gen₀ L e W) = gen₀ L e W'
lemma

bijective_smul_map_eqToHom

L476 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.bijective_smul_map_eqToHom
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
section
variable (e : (restrictFunctor' U).obj L ≅ SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf)
omit e in
Lean source · full declaration
lemma bijective_smul_map_eqToHom {A B : X.Opens} (q : A = B) (t : Γ(L, A))
    (h : Function.Bijective (fun b : Γ(X, A) => b • t)) :
    Function.Bijective (fun a : Γ(X, B) => SMul.smul (M := Γ(X, B)) (α := Γ(L, B))
      a (L.val.map (eqToHom q.symm : B ⟶ A).op t)) := by
  subst q
  have e1 : L.val.map (eqToHom (rfl : A = A) : A ⟶ A).op t = t := by
    rw [eqToHom_refl, op_id]
    exact PresheafOfModules.InternalHom.map_id_apply (R := X.sheaf.obj) L.val _ _
  simp only [e1]
  exact h
def

trivializationBelow

L487 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.trivializationBelow
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
section
variable (e : (restrictFunctor' U).obj L ≅ SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf)
Lean source · full declaration
def trivializationBelow : TrivializationBelow L.val (op U) where
  gen {Y} f := L.val.map (eqToHom (image_preimage_of_le (U := U) f.unop.le).symm :
      Y.unop ⟶ U.ι ''ᵁ (U.ι ⁻¹ᵁ Y.unop)).op (gen₀ L e (U.ι ⁻¹ᵁ Y.unop))
  compat {Y Z} f g := by
    have hle : U.ι ⁻¹ᵁ Z.unop ≤ U.ι ⁻¹ᵁ Y.unop := fun x hx => g.unop.le hx
    dsimp only
    rw [← gen₀_map L e (homOfLE hle)]
    erw [← PresheafOfModules.map_comp_apply, ← PresheafOfModules.map_comp_apply]
    exact congrFun (congrArg
      (fun φ : (op (U.ι ''ᵁ (U.ι ⁻¹ᵁ Y.unop)) ⟶ Z) =>
        ((L.val.map φ).hom : L.val.obj (op (U.ι ''ᵁ (U.ι ⁻¹ᵁ Y.unop))) → L.val.obj Z))
      (Subsingleton.elim _ _)) _
  bij {Y} f := bijective_smul_map_eqToHom L (image_preimage_of_le (U := U) f.unop.le) _
    (gen₀_bijective L e _)
def

trivSieve

L504 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.trivSieve
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
Lean source · full declaration
def trivSieve (V : X.Opens) : Sieve V where
  arrows W _ := Nonempty (TrivializationBelow L.val (op W))
  downward_closed {W W'} f hf g := by
    obtain ⟨D⟩ := hf
    exact ⟨D.restrictTo g.op⟩
lemma

trivSieve_mem

L510 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.trivSieve_mem
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
Lean source · statement
lemma trivSieve_mem (hL : Scheme.Modules.IsInvertible L) (V : X.Opens) :
    trivSieve L V ∈ Opens.grothendieckTopology X V
instance

isIso_sheafify_map_ev

L519 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.isIso_sheafify_map_ev
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
Lean source · statement
instance isIso_sheafify_map_ev (L : X.Modules) [Fact (Scheme.Modules.IsInvertible L)]
  :
    IsIso ((Modules.sheafify X).map (ev (R := X.sheaf.obj) L.val))
def

tensorDualSheafIso

L534 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.tensorDualSheafIso
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
private local instance isIso_sheafify_map_ev (L : X.Modules) [Fact (Scheme.Modules.IsInvertible L)]
  :
    IsIso ((Modules.sheafify X).map (ev (R := X.sheaf.obj) L.val)) := by
  have hW : (Opens.grothendieckTopology X).W ((PresheafOfModules.toPresheaf _).map
      (ev (R := X.sheaf.obj) L.val)) :=
    W_ev (R := X.sheaf.obj) L.val (fun V => ⟨trivSieve L V, trivSieve_mem L Fact.out V,
      fun W i hi => hi⟩)
  have h : ((MorphismProperty.isomorphisms _).inverseImage
      (PresheafOfModules.sheafification (R := X.ringCatSheaf) (𝟙 X.ringCatSheaf.obj)))
      (ev (R := X.sheaf.obj) L.val) := by
    rw [← PresheafOfModules.inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms
      (J := Opens.grothendieckTopology X) (R := X.ringCatSheaf) (𝟙 X.ringCatSheaf.obj)]
    exact hW
  exact h
Lean source · statement
def tensorDualSheafIso (L : X.Modules) [Fact (Scheme.Modules.IsInvertible L)]
  :
    L ⊗ dualSheaf L ≅ 𝟙_ X.Modules
theorem

isInvertible_dualSheaf

L549 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.isInvertible_dualSheaf
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
private local instance isIso_sheafify_map_ev (L : X.Modules) [Fact (Scheme.Modules.IsInvertible L)]
  :
    IsIso ((Modules.sheafify X).map (ev (R := X.sheaf.obj) L.val)) := by
  have hW : (Opens.grothendieckTopology X).W ((PresheafOfModules.toPresheaf _).map
      (ev (R := X.sheaf.obj) L.val)) :=
    W_ev (R := X.sheaf.obj) L.val (fun V => ⟨trivSieve L V, trivSieve_mem L Fact.out V,
      fun W i hi => hi⟩)
  have h : ((MorphismProperty.isomorphisms _).inverseImage
      (PresheafOfModules.sheafification (R := X.ringCatSheaf) (𝟙 X.ringCatSheaf.obj)))
      (ev (R := X.sheaf.obj) L.val) := by
    rw [← PresheafOfModules.inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms
      (J := Opens.grothendieckTopology X) (R := X.ringCatSheaf) (𝟙 X.ringCatSheaf.obj)]
    exact hW
  exact h
Lean source · statement
theorem isInvertible_dualSheaf (L : X.Modules) [Fact (Scheme.Modules.IsInvertible L)] :
    Scheme.Modules.IsInvertible (dualSheaf L)
abbrev

toPMod

L595 ↗
AlgebraicGeometry.Scheme.Modules.toPMod
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (X) in
Lean source · statement
abbrev _root_.AlgebraicGeometry.Scheme.Modules.toPMod : X.Modules ⥤
  X.PresheafOfModules
def

dualModel

L603 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.dualModel
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (X) in
Lean source · full declaration
def dualModel (L : X.Modules) : X.Modules where
  val := PresheafOfModules.InvertibleDual.dual (R := X.sheaf.obj) ((toPMod X).obj L)
  isSheaf := PresheafOfModules.isSheaf_ihomObj _ _ (SheafOfModules.unit X.ringCatSheaf).isSheaf
def

identityRestrictionIso

L607 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.identityRestrictionIso
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (X) in
Lean source · statement
def identityRestrictionIso
    {C : Type u} [Category.{u} C] (R : Cᵒᵖ ⥤ RingCat.{u})
    (M : _root_.PresheafOfModules.{u} R) :
    (_root_.PresheafOfModules.restrictScalars (𝟙 R)).obj M ≅ M
def

dualIsoSheafifyModel

L632 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.dualIsoSheafifyModel
Documentation

Identifies the categorical dual with the sheafification of its natural-family model.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (X) in
Lean source · statement
def dualIsoSheafifyModel (L : X.Modules) :
    Scheme.Modules.dual L ≅ (Modules.sheafify X).obj ((toPMod X).obj (dualModel L))
def

dualIsoModel

L649 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.dualIsoModel
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (X) in
Lean source · statement
def dualIsoModel (L : X.Modules) : Scheme.Modules.dual L ≅ dualModel L
def

toPMod

L661 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual.TrivializationBelow.toPMod
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules.InvertibleDual.TrivializationBelow
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : _root_.AlgebraicGeometry.Scheme.{u}}
Lean source · full declaration
def toPMod
    {L : X.Modules} {X₀ : (X.Opens)ᵒᵖ} (D : TrivializationBelow (R := X.sheaf.obj) L.val X₀) :
    TrivializationBelow (R := X.sheaf.obj) ((toPMod X).obj L) X₀ where
  gen f := D.gen f
  compat f g := D.compat f g
  bij f := D.bij f
instance

isIso_sheafify_map_ev_model

L679 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.isIso_sheafify_map_ev_model
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
Lean source · statement
instance isIso_sheafify_map_ev_model (L : X.Modules) [Fact
  (Scheme.Modules.IsInvertible L)] :
    IsIso ((Modules.sheafify X).map (PresheafOfModules.InvertibleDual.ev (R := X.sheaf.obj)
      ((toPMod X).obj L)))
def

tensorDualModelIso

L695 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.tensorDualModelIso
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
private local instance isIso_sheafify_map_ev_model (L : X.Modules) [Fact
  (Scheme.Modules.IsInvertible L)] :
    IsIso ((Modules.sheafify X).map (PresheafOfModules.InvertibleDual.ev (R := X.sheaf.obj)
      ((toPMod X).obj L))) := by
  have hW : (Opens.grothendieckTopology X).W ((PresheafOfModules.toPresheaf _).map
      (PresheafOfModules.InvertibleDual.ev (R := X.sheaf.obj) ((toPMod X).obj L))) :=
    W_ev (R := X.sheaf.obj) ((toPMod X).obj L) (fun V => ⟨trivSieve L V,
      trivSieve_mem L Fact.out V, fun W i hi => by obtain ⟨D⟩ := hi; exact ⟨D.toPMod⟩⟩)
  have h : ((MorphismProperty.isomorphisms _).inverseImage
      (PresheafOfModules.sheafification (R := X.ringCatSheaf) (𝟙 X.ringCatSheaf.obj)))
      (PresheafOfModules.InvertibleDual.ev (R := X.sheaf.obj) ((toPMod X).obj L)) := by
    rw [← PresheafOfModules.inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms
      (J := Opens.grothendieckTopology X) (R := X.ringCatSheaf) (𝟙 X.ringCatSheaf.obj)]
    exact hW
  exact h
Lean source · statement
def tensorDualModelIso (L : X.Modules) [Fact (Scheme.Modules.IsInvertible L)]
  :
    L ⊗ dualModel L ≅ 𝟙_ X.Modules
def

tensorDualIso

L712 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.tensorDualIso
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
private local instance isIso_sheafify_map_ev_model (L : X.Modules) [Fact
  (Scheme.Modules.IsInvertible L)] :
    IsIso ((Modules.sheafify X).map (PresheafOfModules.InvertibleDual.ev (R := X.sheaf.obj)
      ((toPMod X).obj L))) := by
  have hW : (Opens.grothendieckTopology X).W ((PresheafOfModules.toPresheaf _).map
      (PresheafOfModules.InvertibleDual.ev (R := X.sheaf.obj) ((toPMod X).obj L))) :=
    W_ev (R := X.sheaf.obj) ((toPMod X).obj L) (fun V => ⟨trivSieve L V,
      trivSieve_mem L Fact.out V, fun W i hi => by obtain ⟨D⟩ := hi; exact ⟨D.toPMod⟩⟩)
  have h : ((MorphismProperty.isomorphisms _).inverseImage
      (PresheafOfModules.sheafification (R := X.ringCatSheaf) (𝟙 X.ringCatSheaf.obj)))
      (PresheafOfModules.InvertibleDual.ev (R := X.sheaf.obj) ((toPMod X).obj L)) := by
    rw [← PresheafOfModules.inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms
      (J := Opens.grothendieckTopology X) (R := X.ringCatSheaf) (𝟙 X.ringCatSheaf.obj)]
    exact hW
  exact h
Lean source · statement
def tensorDualIso (L : X.Modules) [Fact (Scheme.Modules.IsInvertible L)] :
    L ⊗ Scheme.Modules.dual L ≅ 𝟙_ X.Modules
theorem

isInvertible_dual

L716 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual_monoidalV2.AlgebraicGeometry.Scheme.Modules.isInvertible_dual
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open Scheme_Modules_IsInvertible_dual_monoidalV2.PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
private local instance isIso_sheafify_map_ev_model (L : X.Modules) [Fact
  (Scheme.Modules.IsInvertible L)] :
    IsIso ((Modules.sheafify X).map (PresheafOfModules.InvertibleDual.ev (R := X.sheaf.obj)
      ((toPMod X).obj L))) := by
  have hW : (Opens.grothendieckTopology X).W ((PresheafOfModules.toPresheaf _).map
      (PresheafOfModules.InvertibleDual.ev (R := X.sheaf.obj) ((toPMod X).obj L))) :=
    W_ev (R := X.sheaf.obj) ((toPMod X).obj L) (fun V => ⟨trivSieve L V,
      trivSieve_mem L Fact.out V, fun W i hi => by obtain ⟨D⟩ := hi; exact ⟨D.toPMod⟩⟩)
  have h : ((MorphismProperty.isomorphisms _).inverseImage
      (PresheafOfModules.sheafification (R := X.ringCatSheaf) (𝟙 X.ringCatSheaf.obj)))
      (PresheafOfModules.InvertibleDual.ev (R := X.sheaf.obj) ((toPMod X).obj L)) := by
    rw [← PresheafOfModules.inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms
      (J := Opens.grothendieckTopology X) (R := X.ringCatSheaf) (𝟙 X.ringCatSheaf.obj)]
    exact hW
  exact h
Lean source · statement
theorem isInvertible_dual (L : X.Modules) [Fact (Scheme.Modules.IsInvertible L)] :
    Scheme.Modules.IsInvertible (Scheme.Modules.dual L)
theorem

dual

L754 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.dual
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
section LinkageInlined_bbe2083f
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry.Scheme.Modules.IsInvertible
open scoped _root_.AlgebraicGeometry in
open scoped _root_.AlgebraicGeometry.Scheme in
open scoped _root_.AlgebraicGeometry.Scheme.Modules in
open scoped _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible in
open _root_.AlgebraicGeometry AlgebraicGeometry _root_.AlgebraicGeometry.Scheme.Modules
  AlgebraicGeometry.Scheme.Modules in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.dual {X :
  AlgebraicGeometry.Scheme.{u}} {L : X.Modules}
    (hL : AlgebraicGeometry.Scheme.Modules.IsInvertible L) :
    AlgebraicGeometry.Scheme.Modules.IsInvertible (AlgebraicGeometry.Scheme.Modules.dual L) ∧
      Nonempty (L ⊗ AlgebraicGeometry.Scheme.Modules.dual L ≅ 𝟙_ X.Modules)
theorem

dual_monoidalV2

L782 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.dual_monoidalV2
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace
  Scheme_Modules_IsInvertible_dual_monoidalV2
universe u
open CategoryTheory _root_.CategoryTheory.MonoidalCategory in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.dual_monoidalV2
    {X : AlgebraicGeometry.Scheme.{u}} {L : X.Modules}
    (hL : AlgebraicGeometry.Scheme.Modules.IsInvertible L) :
    AlgebraicGeometry.Scheme.Modules.IsInvertible (AlgebraicGeometry.Scheme.Modules.dual L) ∧
      Nonempty (L ⊗ AlgebraicGeometry.Scheme.Modules.dual L ≅ 𝟙_ X.Modules)

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