NYLL
Module

Scheme_Modules_IsInvertible_exists_tensor_inverse.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_tensor_inverse
39 declarations indexed from sourceView source ↗

Module documentation

Tensor inverses of invertible module sheaves

Compatible local generators define a natural-family dual. Evaluation becomes an isomorphism after sheafification and supplies an invertible tensor inverse.

Imports7
Imported by14

Declarations

abbrev

dual

L53 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.PresheafOfModules.InvertibleDual.dual
Documentation

The presheaf of homomorphisms from the given module to the structure module.

Source context 15 commands

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

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

L57 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.PresheafOfModules.InvertibleDual.ev
Documentation

The evaluation pairing of a module with its 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_exists_tensor_inverse
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

L60 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.PresheafOfModules.InvertibleDual.TrivializationBelow
Documentation

A compatible generator giving a rank-one trivialization below the chosen 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_exists_tensor_inverse
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 generator over each object below the chosen one. -/
  gen : ∀ {Y : Cᵒᵖ} (_ : X₀ ⟶ Y), F.obj Y
  /-- Restriction takes each generator to the generator on the smaller object. -/
  compat : ∀ {Y Z : Cᵒᵖ} (f : X₀ ⟶ Y) (g : Y ⟶ Z), F.map g (gen f) = gen (f ≫ g)
  /-- Each section has a unique scalar coordinate with respect to its generator. -/
  bij : ∀ {Y : Cᵒᵖ} (f : X₀ ⟶ Y), Function.Bijective (fun a : R.obj Y => a • gen f)
def

restrictTo

L73 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.PresheafOfModules.InvertibleDual.TrivializationBelow.restrictTo
Documentation

Restriction of a compatible trivialization along a morphism.

Source context 17 commands

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

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

L79 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.PresheafOfModules.InvertibleDual.TrivializationBelow.triv
Documentation

The scalar-coordinate linear equivalence determined by the 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_exists_tensor_inverse
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

L83 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.PresheafOfModules.InvertibleDual.TrivializationBelow.coord
Documentation

The coordinate linear map inverse to the generator trivialization.

Source context 17 commands

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

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

L85 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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_exists_tensor_inverse
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

L88 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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_exists_tensor_inverse
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

L91 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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_exists_tensor_inverse
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

L94 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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_exists_tensor_inverse
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

L101 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.PresheafOfModules.InvertibleDual.TrivializationBelow.dualGen
Documentation

The compatible coordinate family defining the dual 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_exists_tensor_inverse
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

L106 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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_exists_tensor_inverse
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

L109 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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_exists_tensor_inverse
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
  change φ.1 f x = R.map f (show R.obj X₀ from φ.1 (𝟙 X₀) (D.gen (𝟙 X₀))) * D.coord f x
  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 (show R.obj X₀ from φ.1 (𝟙 X₀) (D.gen (𝟙 X₀))) =
    R.map f (show R.obj X₀ from φ.1 (𝟙 X₀) (D.gen (𝟙 X₀))) * D.coord f x
  exact mul_comm _ _
def

evInv

L123 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.PresheafOfModules.InvertibleDual.TrivializationBelow.evInv
Documentation

The inverse evaluation map determined by the generator and its dual.

Source context 17 commands

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

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

L127 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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_exists_tensor_inverse
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

L134 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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_exists_tensor_inverse
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

L145 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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_exists_tensor_inverse
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
  induction z using TensorProduct.inductionOn with
  | add z₁ z₂ h₁ h₂ =>
    change D.evInv ((show (F.obj X₀ ⊗[R.obj X₀] (dual F).obj X₀) →ₗ[R.obj X₀] R.obj X₀ from
      ((ev F).app X₀).hom) (z₁ + z₂)) = z₁ + z₂
    rw [map_add, map_add]
    exact congrArg₂ (fun a b : (F.obj X₀ ⊗[R.obj X₀] (dual F).obj X₀) => a + b) 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]
      rfl
    rw [h1]
    conv_rhs => rw [hx, hφ, TensorProduct.smul_tmul_smul]
    rfl
theorem

ev_app_bijective

L168 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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_exists_tensor_inverse
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

L174 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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_exists_tensor_inverse
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

L224 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.AlgebraicGeometry.Scheme.Modules.trivializationOfLE
Documentation

Restriction of a chosen line-module trivialization to a smaller open.

Source context 18 commands

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

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

L233 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.AlgebraicGeometry.Scheme.Modules.dualSheaf
Documentation

The sheaf of homomorphisms from the given module to the structure module.

Source context 18 commands

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

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

L240 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.AlgebraicGeometry.Scheme.Modules.restrictRingCatSheafHom
Documentation

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

Source context 19 commands

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

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

L247 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.AlgebraicGeometry.Scheme.Modules.restrictFunctor'
Documentation

Restriction of module sheaves through the canonical map of structure rings.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse
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 PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
Lean source · statement
def restrictFunctor' : X.Modules ⥤ (U : Scheme.{u}).Modules
lemma

restrictFunctor'_eq

L250 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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.Scheme_Modules_IsInvertible_exists_tensor_inverse
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 PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
Lean source · statement
lemma restrictFunctor'_eq : restrictFunctor' U = Modules.restrictFunctor U.ι
def

restrictFunctor'IsoPullback

L259 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.AlgebraicGeometry.Scheme.Modules.restrictFunctor'IsoPullback
Documentation

The comparison between this restriction functor and module pullback.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse
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 PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
Lean source · statement
def restrictFunctor'IsoPullback : restrictFunctor' U ≅ Modules.pullback U.ι
instance

(anonymous instance)

L264 ↗
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse
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 PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
Lean source · statement
instance (A : X.Opens) : Module Γ(X, A) (L.val.obj (op A))
lemma

image_preimage_of_le

L267 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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_exists_tensor_inverse
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 PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
local instance (A : X.Opens) : Module Γ(X, A) (L.val.obj (op A)) :=
  (L.val.obj (op A)).isModule
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_exists_tensor_inverse.AlgebraicGeometry.Scheme.Modules.gen₀
Documentation

The section corresponding to one under the chosen local 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_exists_tensor_inverse
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 PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
local instance (A : X.Opens) : Module Γ(X, A) (L.val.obj (op A)) :=
  (L.val.obj (op A)).isModule
section
variable (e : ((restrictFunctor' U).obj L : SheafOfModules (U : Scheme.{u}).ringCatSheaf) ≅
  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_exists_tensor_inverse.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_exists_tensor_inverse
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 PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
local instance (A : X.Opens) : Module Γ(X, A) (L.val.obj (op A)) :=
  (L.val.obj (op A)).isModule
section
variable (e : ((restrictFunctor' U).obj L : SheafOfModules (U : Scheme.{u}).ringCatSheaf) ≅
  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

L286 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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_exists_tensor_inverse
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 PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
local instance (A : X.Opens) : Module Γ(X, A) (L.val.obj (op A)) :=
  (L.val.obj (op A)).isModule
section
variable (e : ((restrictFunctor' U).obj L : SheafOfModules (U : Scheme.{u}).ringCatSheaf) ≅
  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

L295 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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_exists_tensor_inverse
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 PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
local instance (A : X.Opens) : Module Γ(X, A) (L.val.obj (op A)) :=
  (L.val.obj (op A)).isModule
section
variable (e : ((restrictFunctor' U).obj L : SheafOfModules (U : Scheme.{u}).ringCatSheaf) ≅
  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

L303 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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_exists_tensor_inverse
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 PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
local instance (A : X.Opens) : Module Γ(X, A) (L.val.obj (op A)) :=
  (L.val.obj (op A)).isModule
section
variable (e : ((restrictFunctor' U).obj L : SheafOfModules (U : Scheme.{u}).ringCatSheaf) ≅
  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 • t)) :
    Function.Bijective (fun a : Γ(X, B) => a • (show L.val.obj (op 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

L314 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.AlgebraicGeometry.Scheme.Modules.trivializationBelow
Documentation

A compatible generator family obtained from the local sheaf 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_exists_tensor_inverse
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 PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
local instance (A : X.Opens) : Module Γ(X, A) (L.val.obj (op A)) :=
  (L.val.obj (op A)).isModule
section
variable (e : ((restrictFunctor' U).obj L : SheafOfModules (U : Scheme.{u}).ringCatSheaf) ≅
  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

L332 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.AlgebraicGeometry.Scheme.Modules.trivSieve
Documentation

The sieve of opens 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_exists_tensor_inverse
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 PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
local instance (A : X.Opens) : Module Γ(X, A) (L.val.obj (op A)) :=
  (L.val.obj (op A)).isModule
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

L338 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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_exists_tensor_inverse
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 PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
local instance (A : X.Opens) : Module Γ(X, A) (L.val.obj (op A)) :=
  (L.val.obj (op A)).isModule
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

L347 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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_exists_tensor_inverse
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 PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
local instance (A : X.Opens) : Module Γ(X, A) (L.val.obj (op A)) :=
  (L.val.obj (op A)).isModule
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

L362 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.AlgebraicGeometry.Scheme.Modules.tensorDualSheafIso
Documentation

The tensor evaluation isomorphism of an invertible module with its dual.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse
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 PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
local instance (A : X.Opens) : Module Γ(X, A) (L.val.obj (op A)) :=
  (L.val.obj (op A)).isModule
Lean source · statement
def tensorDualSheafIso (L : X.Modules) [Fact (Scheme.Modules.IsInvertible L)] :
    L ⊗ dualSheaf L ≅ 𝟙_ X.Modules
theorem

isInvertible_dualSheaf

L373 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse.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_exists_tensor_inverse
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 PresheafOfModules.InvertibleDual
variable {X : Scheme.{u}}
variable (U : X.Opens)
variable {U} (L : X.Modules)
local instance (A : X.Opens) : Module Γ(X, A) (L.val.obj (op A)) :=
  (L.val.obj (op A)).isModule
Lean source · statement
theorem isInvertible_dualSheaf (L : X.Modules) [Fact (Scheme.Modules.IsInvertible L)] :
    Scheme.Modules.IsInvertible (dualSheaf L)
theorem

exists_tensor_inverse

L387 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.exists_tensor_inverse
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_tensor_inverse
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.exists_tensor_inverse {X :
    AlgebraicGeometry.Scheme.{u}} {L : X.Modules}
    (hL : AlgebraicGeometry.Scheme.Modules.IsInvertible L) :
    ∃ M : X.Modules, AlgebraicGeometry.Scheme.Modules.IsInvertible M ∧
      Nonempty (L ⊗ M ≅ 𝟙_ X.Modules)

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