NYLL
Module

Scheme_Modules_IsInvertible_dual.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_dual
48 declarations indexed from sourceView source ↗

Module documentation

Duals of invertible sheaves of modules

Compatible local generators identify evaluation against the natural-family dual with the structure sheaf. We compare this model with the categorical dual and prove its invertibility.

Imports11
Imported by56

Declarations

abbrev

dual

L56 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.dual
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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 dual : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat)
abbrev

ev

L60 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.ev
Documentation

Evaluates a module presheaf tensor its natural-family dual by uncurrying the identity.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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

L63 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.TrivializationBelow
Documentation

A compatible generator with unique scalar coordinates on all objects below a fixed object.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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
  /-- The chosen generating section at each object below the fixed object. -/
  gen : ∀ {Y : Cᵒᵖ} (_ : X₀ ⟶ Y), F.obj Y
  /-- Restriction maps carry each chosen generator to the generator at the target. -/
  compat : ∀ {Y Z : Cᵒᵖ} (f : X₀ ⟶ Y) (g : Y ⟶ Z), F.map g (gen f) = gen (f ≫ g)
  /-- Each section has a unique scalar coefficient with respect to its chosen generator. -/
  bij : ∀ {Y : Cᵒᵖ} (f : X₀ ⟶ Y), Function.Bijective (fun a : R.obj Y => a • gen f)
def

restrictTo

L76 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.TrivializationBelow.restrictTo
Documentation

Restricts the compatible generator and its scalar coordinates to a smaller region.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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

L82 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.TrivializationBelow.triv
Documentation

The linear equivalence sending a scalar to its multiple of the chosen generator.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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

L86 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.TrivializationBelow.coord
Documentation

The scalar coordinate of a section with respect to the chosen generator.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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

L88 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.TrivializationBelow.coord_smul_gen
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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

L91 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.TrivializationBelow.coord_gen_smul
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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

L94 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.TrivializationBelow.coord_gen
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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

L97 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.TrivializationBelow.coord_map
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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

L104 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.TrivializationBelow.dualGen
Documentation

The natural linear family extracting scalar coordinates from sections.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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

L109 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.TrivializationBelow.dualGen_app
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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

L112 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.TrivializationBelow.eq_smul_dualGen
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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
lemma eq_smul_dualGen (φ : (dual F).obj X₀) :
    φ = (show R.obj X₀ from φ.1 (𝟙 X₀) (D.gen (𝟙 X₀))) • D.dualGen := by
  apply naturalFamilies_ext
  intro Y f x
  erw [InternalHom.smul_app, dualGen_app]
  conv_lhs => rw [← D.coord_smul_gen f x, LinearMap.map_smul]
  have h := InternalHom.naturality φ (𝟙 X₀) f (D.gen (𝟙 X₀))
  rw [D.compat, Category.id_comp] at h
  rw [← h]
  change D.coord f x * R.map f (φ.1 (𝟙 X₀) (D.gen (𝟙 X₀))) =
    R.map f (φ.1 (𝟙 X₀) (D.gen (𝟙 X₀))) * D.coord f x
  exact mul_comm _ _
def

evInv

L127 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.TrivializationBelow.evInv
Documentation

Sends a scalar to the corresponding multiple of the generator tensor its dual coordinate family.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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₀)
lemma

ev_app_tmul

L131 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.TrivializationBelow.ev_app_tmul
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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 · full declaration
lemma ev_app_tmul (x : F.obj X₀) (φ : (dual F).obj X₀) :
    DFunLike.coe (α := (F.obj X₀ ⊗[R.obj X₀] (dual F).obj X₀ :))
      (β := fun _ => (𝟙_ (PresheafOfModules.{u}
      (R ⋙ forget₂ CommRingCat RingCat))).obj X₀)
      ((ev F).app X₀).hom (x ⊗ₜ[R.obj X₀] φ) = φ.1 (𝟙 X₀) x :=
  uncurry'_app_tmul F (𝟙 (dual F)) x φ
lemma

ev_evInv

L138 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.TrivializationBelow.ev_evInv
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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
lemma ev_evInv (a : R.obj X₀) :
    DFunLike.coe (α := (F.obj X₀ ⊗[R.obj X₀] (dual F).obj X₀ :))
      (β := fun _ => (𝟙_ (PresheafOfModules.{u}
      (R ⋙ forget₂ CommRingCat RingCat))).obj X₀)
      ((ev F).app X₀).hom (D.evInv a) = a := by
  change (show (F.obj X₀ ⊗[R.obj X₀] (dual F).obj X₀) →ₗ[R.obj X₀] R.obj X₀ from
      ((ev F).app X₀).hom) (a • (D.gen (𝟙 X₀) ⊗ₜ[R.obj X₀] D.dualGen)) = a
  rw [LinearMap.map_smul]
  erw [ev_app_tmul]
  rw [dualGen_app, coord_gen, smul_eq_mul, mul_one]
lemma

evInv_ev

L149 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.TrivializationBelow.evInv_ev
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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
lemma evInv_ev (z : (F.obj X₀ ⊗[R.obj X₀] (dual F).obj X₀)) :
    D.evInv (DFunLike.coe (α := (F.obj X₀ ⊗[R.obj X₀] (dual F).obj X₀ :)) (β := fun _ =>
      (𝟙_ (PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))).obj X₀)
        ((ev F).app X₀).hom z) = z := by
  let evMap : (F.obj X₀ ⊗[R.obj X₀] (dual F).obj X₀) →ₗ[R.obj X₀] R.obj X₀ :=
    ((ev F).app X₀).hom
  change D.evInv (evMap z) = z
  induction z using TensorProduct.inductionOn with
  | add z₁ z₂ h₁ h₂ => rw [map_add, map_add, h₁, h₂]
  | tmul x φ =>
    erw [ev_app_tmul]
    set d : R.obj X₀ := φ.1 (𝟙 X₀) (D.gen (𝟙 X₀)) with hd
    have hx : x = D.coord (𝟙 X₀) x • D.gen (𝟙 X₀) := (D.coord_smul_gen _ x).symm
    have hφ : φ = d • D.dualGen := D.eq_smul_dualGen φ
    have h1 : φ.1 (𝟙 X₀) x = D.coord (𝟙 X₀) x * d := by
      conv_lhs => rw [hx]
      rw [LinearMap.map_smul]
      exact smul_eq_mul (D.coord (𝟙 X₀) x) d
    rw [h1]
    conv_rhs => rw [hx, hφ, TensorProduct.smul_tmul_smul]
    rfl
theorem

ev_app_bijective

L171 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.TrivializationBelow.ev_app_bijective
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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

L177 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.W_ev
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
namespace InvertibleDual
open _root_.Opposite
open _root_.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

L228 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.trivializationOfLE
Documentation

Restricts a pullback trivialization along an inclusion of open subsets.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
Lean source · statement
def trivializationOfLE {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

L237 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.dualSheaf
Documentation

The sheaf of natural linear families from a module to the structure sheaf.

Source context 19 commands

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

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

restrictRingCatSheafHom

L244 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.restrictRingCatSheafHom
Documentation

The identity map of ring sheaves viewed through the pushforward on an open subset.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open 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'

L251 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.restrictFunctor'
Documentation

Restricts module sheaves using the identity map on the restricted ring sheaf.

Source context 20 commands

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

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

restrictFunctor'_eq

L254 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.restrictFunctor'_eq
Source context 20 commands

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

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

restrictFunctor'IsoPullback

L263 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.restrictFunctor'IsoPullback
Documentation

Identifies the explicit restriction functor with pullback along the open immersion.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open 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

L268 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.image_preimage_of_le
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open 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₀

L277 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.gen₀
Documentation

The section obtained by sending one through the inverse of a restriction trivialization.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open 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.val.obj (op (U.ι ''ᵁ W))
lemma

gen₀_spec

L280 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.gen₀_spec
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open 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₀_spec (W : (U : Scheme.{u}).Opens) (b : Γ(X, U.ι ''ᵁ W)) :
    (e.inv.val.app (op W)).hom b = b • (show Γ(L, U.ι ''ᵁ W) from gen₀ L e W) := by
  have h := (e.inv.val.app (op W)).hom.map_smul b (1 : Γ(U, W))
  have hunit : (show Γ(U, W) from b) • (1 : Γ(U, W)) = b :=
    (smul_eq_mul (show Γ(U, W) from b) (1 : Γ(U, W))).trans (mul_one _)
  exact (congrArg (e.inv.val.app (op W)).hom hunit).symm.trans h
lemma

gen₀_bijective

L287 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.gen₀_bijective
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open 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 • (show Γ(L, U.ι ''ᵁ W) from 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

L297 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.gen₀_map
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open 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

L305 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.bijective_smul_map_eqToHom
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open 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.val.obj (op A))
    (h : Function.Bijective (fun b : Γ(X, A) => b • (show Γ(L, A) from t))) :
    Function.Bijective (fun a : Γ(X, B) =>
      a • (show Γ(L, B) from 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 _ _
  simpa only [e1] using h
def

trivializationBelow

L317 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.trivializationBelow
Documentation

The compatible generators and unique scalar coordinates induced by a restriction trivialization.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open 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

L335 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.trivSieve
Documentation

The sieve of open subsets on which the module admits a compatible generator.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open 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

L341 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.trivSieve_mem
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open 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

L350 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.isIso_sheafify_map_ev
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open 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

L365 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.tensorDualSheafIso
Documentation

Identifies an invertible module tensor its natural-family dual sheaf with the unit module.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
Lean source · statement
def tensorDualSheafIso (L : X.Modules) [Fact (Scheme.Modules.IsInvertible L)] :
    L ⊗ dualSheaf L ≅ 𝟙_ X.Modules
theorem

isInvertible_dualSheaf

L378 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.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.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
Lean source · statement
theorem isInvertible_dualSheaf (L : X.Modules) [Fact (Scheme.Modules.IsInvertible L)] :
    Scheme.Modules.IsInvertible (dualSheaf L)
abbrev

toPMod

L405 ↗
AlgebraicGeometry.Scheme.Modules.toPMod
Source context 20 commands

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

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

dualModel

L412 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.dualModel
Documentation

The natural-family dual formed from the canonical presheaf view of a module.

Source context 21 commands

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

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

L416 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.identityRestrictionIso
Source context 21 commands

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

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

L441 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.dualIsoSheafifyModel
Documentation

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

Source context 21 commands

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

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

dualIsoModel

L460 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.dualIsoModel
Documentation

Identifies the categorical dual with its natural-family dual sheaf via the sheafification counit.

Source context 21 commands

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

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

toPMod

L473 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.PresheafOfModules.InvertibleDual.TrivializationBelow.toPMod
Documentation

Views a compatible generator in the canonical presheaf presentation of a module sheaf.

Source context 10 commands

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

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

L497 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.isIso_sheafify_map_ev_model
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open 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 (ev (R := X.sheaf.obj) ((toPMod X).obj L)))
def

tensorDualModelIso

L512 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.tensorDualModelIso
Documentation

Trivializes an invertible module tensor its natural-family dual model using evaluation.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
Lean source · statement
def tensorDualModelIso (L : X.Modules) [Fact (Scheme.Modules.IsInvertible L)] :
    L ⊗ dualModel L ≅ 𝟙_ X.Modules
def

tensorDualIso

L528 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.tensorDualIso
Documentation

Trivializes an invertible module tensor its categorical dual through the natural-family model.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
Lean source · statement
def tensorDualIso (L : X.Modules) [Fact (Scheme.Modules.IsInvertible L)] :
    L ⊗ Scheme.Modules.dual L ≅ 𝟙_ X.Modules
theorem

isInvertible_dual

L532 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual.AlgebraicGeometry.Scheme.Modules.isInvertible_dual
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory.Limits
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TopologicalSpace Opposite
open PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
Lean source · statement
theorem isInvertible_dual (L : X.Modules) [Fact (Scheme.Modules.IsInvertible L)] :
    Scheme.Modules.IsInvertible (Scheme.Modules.dual L)
theorem

dual

L546 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.dual
Source context 8 commands

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

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

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