Module

OModulePresheafTensor.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheafTensor

13 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf Tensor

Imports2

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheafOfModules
Mathlib.LinearAlgebra.TensorProduct.Basic

Imported by18

def

tensorObjModule

L32 ↗

AlgebraicGeometry.OModulePresheaf.tensorObjModule

Documentation

The base-ring module structure on a tensor product of local sections.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.OModulePresheaf
open CategoryTheory TensorProduct
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F G : OModulePresheaf π)

Lean source · statement

def tensorObjModule (U : V.Opens) : Module R (F.obj U ⊗[Γ(V, U)] G.obj U)

def

tensorResₛₗ

L37 ↗

AlgebraicGeometry.OModulePresheaf.tensorResₛₗ

Documentation

The semilinear restriction map on tensor products of local sections.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.OModulePresheaf
open CategoryTheory TensorProduct
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F G : OModulePresheaf π)

Lean source · statement

def tensorResₛₗ {U U' : V.Opens} (h : U ≤ U') :
    F.obj U' ⊗[Γ(V, U')] G.obj U' →ₛₗ[(V.presheaf.map (homOfLE h).op).hom] F.obj U ⊗[Γ(V, U)]
      G.obj U

theorem

tensorResₛₗ_tmul

L48 ↗

AlgebraicGeometry.OModulePresheaf.tensorResₛₗ_tmul

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.OModulePresheaf
open CategoryTheory TensorProduct
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F G : OModulePresheaf π)

Lean source · statement

theorem tensorResₛₗ_tmul {U U' : V.Opens} (h : U ≤ U') (x : F.obj U') (y : G.obj U') :
    F.tensorResₛₗ G h (x ⊗ₜ y) = F.res h x ⊗ₜ G.res h y

def

tensorRes

L52 ↗

AlgebraicGeometry.OModulePresheaf.tensorRes

Documentation

The base-ring linear restriction map on tensor products of local sections.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.OModulePresheaf
open CategoryTheory TensorProduct
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F G : OModulePresheaf π)

Lean source · full declaration

def tensorRes {U U' : V.Opens} (h : U ≤ U') :
    letI := F.tensorObjModule G U; letI := F.tensorObjModule G U'
    F.obj U' ⊗[Γ(V, U')] G.obj U' →ₗ[R] F.obj U ⊗[Γ(V, U)] G.obj U :=
  letI := F.tensorObjModule G U; letI := F.tensorObjModule G U'
  letI := Scheme.TwoAffineOpenCover.algebraOfHom π U
  letI := Scheme.TwoAffineOpenCover.algebraOfHom π U'
  { toFun := F.tensorResₛₗ G h
    map_add' := fun s t => map_add _ s t
    map_smul' := fun r t => by
      change F.tensorResₛₗ G h (algebraMap R Γ(V, U') r • t) = algebraMap R Γ(V, U) r •
        F.tensorResₛₗ G h t
      rw [LinearMap.map_smulₛₗ]
      congr 1
      exact (Scheme.TwoAffineOpenCover.restrictAlgHom π h).commutes r }

def

tensor

L68 ↗

AlgebraicGeometry.OModulePresheaf.tensor

Documentation

The presheaf obtained by tensoring section modules and restriction maps.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.OModulePresheaf
open CategoryTheory TensorProduct
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F G : OModulePresheaf π)

Lean source · full declaration

def tensor : OModulePresheaf π where
  obj U := F.obj U ⊗[Γ(V, U)] G.obj U
  addCommGroup _ := inferInstance
  module U := F.tensorObjModule G U
  moduleSections _ := inferInstance
  isScalarTower U :=
    @IsScalarTower.mk R Γ(V, U) _ (_) (_) (_)
      fun r a t => mul_smul ((Scheme.TwoAffineOpenCover.algebraOfHom π U).algebraMap r) a t
  res h := F.tensorRes G h
  res_smul h a t := (F.tensorResₛₗ G h).map_smulₛₗ a t
  res_refl U := by
    let := F.tensorObjModule G U
    refine LinearMap.ext fun t => ?_
    change F.tensorResₛₗ G (le_refl U) t = t
    induction t using TensorProduct.inductionOn with
    | tmul x y => rw [tensorResₛₗ_tmul, res_refl_apply, res_refl_apply]
    | add s t hs ht => rw [map_add, hs, ht]
  res_comp {U U' U''} h h' := by
    let := F.tensorObjModule G U; let := F.tensorObjModule G U''
    refine LinearMap.ext fun t => ?_
    change F.tensorResₛₗ G (h.trans h') t = F.tensorResₛₗ G h (F.tensorResₛₗ G h' t)
    induction t using TensorProduct.inductionOn with
    | tmul x y => rw [tensorResₛₗ_tmul, tensorResₛₗ_tmul, tensorResₛₗ_tmul, res_res, res_res]
    | add s t hs ht => rw [map_add, hs, ht, map_add, map_add]

theorem

tensor_obj

L93 ↗

AlgebraicGeometry.OModulePresheaf.tensor_obj

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.OModulePresheaf
open CategoryTheory TensorProduct
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F G : OModulePresheaf π)

Lean source · statement

theorem tensor_obj (U : V.Opens) : (F.tensor G).obj U = (F.obj U ⊗[Γ(V, U)] G.obj U)

theorem

tensor_res_tmul

L95 ↗

AlgebraicGeometry.OModulePresheaf.tensor_res_tmul

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.OModulePresheaf
open CategoryTheory TensorProduct
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F G : OModulePresheaf π)

Lean source · full declaration

theorem tensor_res_tmul {U U' : V.Opens} (h : U ≤ U') (x : F.obj U') (y : G.obj U') :
    (F.tensor G).res h (show (F.tensor G).obj U' from x ⊗ₜ y)
      = (show (F.tensor G).obj U from F.res h x ⊗ₜ G.res h y) := rfl

theorem

tensor_res_apply

L99 ↗

AlgebraicGeometry.OModulePresheaf.tensor_res_apply

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.OModulePresheaf
open CategoryTheory TensorProduct
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F G : OModulePresheaf π)

Lean source · full declaration

theorem tensor_res_apply {U U' : V.Opens} (h : U ≤ U') (t : F.obj U' ⊗[Γ(V, U')] G.obj U') :
    (F.tensor G).res h (show (F.tensor G).obj U' from t) = (show (F.tensor G).obj U from
      F.tensorResₛₗ G h t) :=
  rfl

theorem

tensor_smul_tmul

L104 ↗

AlgebraicGeometry.OModulePresheaf.tensor_smul_tmul

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.OModulePresheaf
open CategoryTheory TensorProduct
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F G : OModulePresheaf π)

Lean source · full declaration

theorem tensor_smul_tmul (U : V.Opens) (a : Γ(V, U)) (x : F.obj U) (y : G.obj U) :
    a • (show (F.tensor G).obj U from x ⊗ₜ y) = (show (F.tensor G).obj U from (a • x) ⊗ₜ y) := rfl

theorem

tensor_algebraMap_smul

L107 ↗

AlgebraicGeometry.OModulePresheaf.tensor_algebraMap_smul

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.OModulePresheaf
open CategoryTheory TensorProduct
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F G : OModulePresheaf π)

Lean source · statement

theorem tensor_algebraMap_smul (U : V.Opens) (r : R) (t : (F.tensor G).obj U) :
    r • t = (Scheme.TwoAffineOpenCover.algebraOfHom π U).algebraMap r • t

abbrev

twist

L115 ↗

AlgebraicGeometry.OModulePresheaf.twist

Documentation

The tensor product with the presheaf of sections of the given sheaf of modules.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.OModulePresheaf
open CategoryTheory TensorProduct
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F G : OModulePresheaf π)
section Twist
variable (L : V.Modules)

Lean source · statement

abbrev twist : OModulePresheaf π

theorem

twist_obj

L117 ↗

AlgebraicGeometry.OModulePresheaf.twist_obj

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.OModulePresheaf
open CategoryTheory TensorProduct
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F G : OModulePresheaf π)
section Twist
variable (L : V.Modules)

Lean source · statement

theorem twist_obj (U : V.Opens) : (F.twist L).obj U = (F.obj U ⊗[Γ(V, U)] Γ(L, U))

theorem

twist_res_tmul

L119 ↗

AlgebraicGeometry.OModulePresheaf.twist_res_tmul

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.OModulePresheaf
open CategoryTheory TensorProduct
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F G : OModulePresheaf π)
section Twist
variable (L : V.Modules)

Lean source · full declaration

theorem twist_res_tmul {U U' : V.Opens} (h : U ≤ U') (x : F.obj U') (y : Γ(L, U')) :
    (F.twist L).res h (show (F.twist L).obj U' from x ⊗ₜ[Γ(V, U')] (show (ofModules π L).obj U'
      from y))
      = (show (F.twist L).obj U from
          F.res h x ⊗ₜ[Γ(V, U)] (show (ofModules π L).obj U from L.presheaf.map (homOfLE h).op y))
            :=
  rfl

Module documentation

OModule Presheaf Tensor

Declarations