NYLL
Module

TensorFrames.lean

Nyll.SchemeTheory.Modules.TensorFrames
30 declarations indexed from sourceView source ↗

Module documentation

Tensor products of local frames

The presheaf tensor comparison carries tensor products of generators to frames.

Imports6
Imported by3

Declarations

instance

frameTensorPresheafModule

L70 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.frameTensorPresheafModule
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
Lean source · statement
instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W))
lemma

bijective_smul_tmul

L73 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.bijective_smul_tmul
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
Lean source · full declaration
lemma bijective_smul_tmul {R : Type*} [CommRing R] {A B : Type*} [AddCommGroup A] [AddCommGroup B]
    [Module R A] [Module R B] (a : A) (b : B)
    (ha : Function.Bijective fun r : R => r • a) (hb : Function.Bijective fun r : R => r • b) :
    Function.Bijective fun r : R => r • (a ⊗ₜ[R] b) := by
  let eA : R ≃ₗ[R] A := LinearEquiv.ofBijective (LinearMap.toSpanSingleton R A a) ha
  let eB : R ≃ₗ[R] B := LinearEquiv.ofBijective (LinearMap.toSpanSingleton R B b) hb
  let e : R ≃ₗ[R] A ⊗[R] B := (TensorProduct.lid R R).symm ≪≫ₗ TensorProduct.congr eA eB
  have he : (fun r : R => r • (a ⊗ₜ[R] b)) = e := by
    funext r
    change r • (a ⊗ₜ[R] b) = TensorProduct.congr eA eB ((TensorProduct.lid R R).symm r)
    rw [TensorProduct.lid_symm_apply, TensorProduct.congr_tmul]
    change r • (a ⊗ₜ[R] b) = ((1 : R) • a) ⊗ₜ[R] (r • b)
    rw [one_smul, TensorProduct.tmul_smul]
  rw [he]
  exact e.bijective
def

tsApp

L94 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.tsApp
Documentation

Applies the canonical tensor comparison to a local presheaf tensor.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section locbij
variable (L M : X.Modules)
Lean source · statement
def tsApp (W : X.Opens) (z : (L.val ⊗ M.val).obj (op W)) : Γ(L ⊗ M, W)
lemma

tensorSections_eq_tsApp

L100 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.tensorSections_eq_tsApp
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section locbij
variable (L M : X.Modules)
variable {L M}
Lean source · statement
lemma tensorSections_eq_tsApp {W : X.Opens} (s : Γ(L, W)) (t : Γ(M, W)) :
    Modules.tensorSections s t = tsApp L M W ((s : L.val.obj (op W)) ⊗ₜ[Γ(X, W)] (t : M.val.obj (op
      W)))
lemma

tsApp_smul

L105 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.tsApp_smul
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section locbij
variable (L M : X.Modules)
variable {L M}
Lean source · statement
lemma tsApp_smul {W : X.Opens} (g : Γ(X, W)) (z : (L.val ⊗ M.val).obj (op W)) :
    tsApp L M W (g • z) = g • tsApp L M W z
lemma

tsApp_add

L109 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.tsApp_add
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section locbij
variable (L M : X.Modules)
variable {L M}
Lean source · statement
lemma tsApp_add {W : X.Opens} (z z' : (L.val ⊗ M.val).obj (op W)) :
    tsApp L M W (z + z') = tsApp L M W z + tsApp L M W z'
lemma

map_tsApp

L113 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.map_tsApp
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section locbij
variable (L M : X.Modules)
variable {L M}
Lean source · statement
lemma map_tsApp {W W' : X.Opens} (i : W' ⟶ W) (z : (L.val ⊗ M.val).obj (op W)) :
    (L ⊗ M).presheaf.map i.op (tsApp L M W z) = tsApp L M W' ((L.val ⊗ M.val).map i.op z)
lemma

map_smul_tmul

L117 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.map_smul_tmul
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section locbij
variable (L M : X.Modules)
variable {L M}
Lean source · statement
lemma map_smul_tmul {W W' : X.Opens} (i : W' ⟶ W) (g : Γ(X, W)) (s : Γ(L, W)) (t : Γ(M, W)) :
    (L.val ⊗ M.val).map i.op (g • ((s : L.val.obj (op W)) ⊗ₜ[Γ(X, W)] (t : M.val.obj (op W)))) =
      X.presheaf.map i.op g • ((L.presheaf.map i.op s : L.val.obj (op W')) ⊗ₜ[Γ(X, W')]
        (M.presheaf.map i.op t : M.val.obj (op W')))
lemma

W_tensorSectionsHom

L125 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.W_tensorSectionsHom
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section locbij
variable (L M : X.Modules)
variable {L M}
variable (L M) in
Lean source · statement
lemma W_tensorSectionsHom :
    (Opens.grothendieckTopology X).W ((PresheafOfModules.toPresheaf _).map (tensorSectionsHom L
        M))
instance

isLocallySurjective_tensorSectionsHom

L140 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.isLocallySurjective_tensorSectionsHom
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section locbij
variable (L M : X.Modules)
variable {L M}
variable (L M) in
Lean source · statement
instance isLocallySurjective_tensorSectionsHom : Presheaf.IsLocallySurjective
  (Opens.grothendieckTopology X)
    ((PresheafOfModules.toPresheaf _).map (tensorSectionsHom L M))
instance

isLocallyInjective_tensorSectionsHom

L145 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.isLocallyInjective_tensorSectionsHom
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section locbij
variable (L M : X.Modules)
variable {L M}
variable (L M) in
Lean source · statement
instance isLocallyInjective_tensorSectionsHom : Presheaf.IsLocallyInjective
  (Opens.grothendieckTopology X)
    ((PresheafOfModules.toPresheaf _).map (tensorSectionsHom L M))
lemma

exists_local_preimage

L150 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.exists_local_preimage
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section locbij
variable (L M : X.Modules)
variable {L M}
variable (L M) in
Lean source · statement
lemma exists_local_preimage {W : X.Opens} (y : Γ(L ⊗ M, W)) {x : X} (hx : x ∈ W) :
    ∃ (W' : X.Opens) (i : W' ⟶ W), x ∈ W' ∧ ∃ z : (L.val ⊗ M.val).obj (op W'),
      tsApp L M W' z = (L ⊗ M).presheaf.map i.op y
lemma

exists_local_eq

L158 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.exists_local_eq
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section locbij
variable (L M : X.Modules)
variable {L M}
variable (L M) in
Lean source · statement
lemma exists_local_eq {W : X.Opens} (z₁ z₂ : (L.val ⊗ M.val).obj (op W))
    (h : tsApp L M W z₁ = tsApp L M W z₂) {x : X} (hx : x ∈ W) :
    ∃ (W' : X.Opens) (i : W' ⟶ W), x ∈ W' ∧ (L.val ⊗ M.val).map i.op z₁ = (L.val ⊗ M.val).map i.op
      z₂
def

restrictRingCatSheafHom

L174 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.restrictRingCatSheafHom
Documentation

The identity ring-sheaf map used to restrict to 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_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section restrict
variable (W : X.Opens)
Lean source · statement
def restrictRingCatSheafHom : (W : Scheme.{u}).ringCatSheaf ⟶
    (W.ι.opensFunctor.sheafPushforwardContinuous RingCat.{u}
      (Opens.grothendieckTopology (W : Scheme.{u})) (Opens.grothendieckTopology X)).obj
        X.ringCatSheaf
def

restrictFunctor'

L181 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.restrictFunctor'
Documentation

Restricts a module sheaf to an open subset by pushforward along the open inclusion.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section restrict
variable (W : X.Opens)
Lean source · statement
def restrictFunctor' : X.Modules ⥤ (W : Scheme.{u}).Modules
lemma

image_le

L184 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.image_le
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section restrict
variable (W : X.Opens)
Lean source · statement
lemma image_le (W' : (W : Scheme.{u}).Opens) : W.ι ''ᵁ W' ≤ W
lemma

image_preimage_of_le

L188 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.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_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section restrict
variable (W : X.Opens)
variable {W} in
Lean source · statement
lemma image_preimage_of_le {W₂ : X.Opens} (h : W₂ ≤ W) : W.ι ''ᵁ (W.ι ⁻¹ᵁ W₂) = W₂
abbrev

secX

L193 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.secX
Documentation

Views a function on an open subscheme as a function on its image.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section restrict
variable (W : X.Opens)
variable {W} in
Lean source · statement
abbrev secX (W' : (W : Scheme.{u}).Opens) (a : Γ(W, W')) : Γ(X, W.ι ''ᵁ W')
def

smulSectionHom

L202 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.smulSectionHom
Documentation

The map from the unit module sending functions to multiples of a section.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section smulHom
variable (N : X.Modules) (W : X.Opens) (τ : Γ(N, W))
Lean source · statement
def smulSectionHom : SheafOfModules.unit ((W : X.Opens) : Scheme.{u}).ringCatSheaf ⟶
    (restrictFunctor' W).obj N
lemma

smulSectionHom_app_apply

L232 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.smulSectionHom_app_apply
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section smulHom
variable (N : X.Modules) (W : X.Opens) (τ : Γ(N, W))
Lean source · statement
lemma smulSectionHom_app_apply (W' : (((W : X.Opens) : Scheme.{u}).Opens)ᵒᵖ) (a : Γ(W, W'.unop)) :
    (smulSectionHom N W τ).val.app W' a =
      secX W W'.unop a • N.presheaf.map (homOfLE (image_le W W'.unop)).op τ
lemma

bijective_smul_map_iff_of_eq

L238 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.bijective_smul_map_iff_of_eq
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section smulHom
variable (N : X.Modules) (W : X.Opens) (τ : Γ(N, W))
variable {N W τ}
Lean source · full declaration
lemma bijective_smul_map_iff_of_eq {A B : X.Opens} (q : A = B) (τ : Γ(N, B)) :
    (Function.Bijective fun a : Γ(X, A) => a • N.presheaf.map (homOfLE q.le).op τ) ↔
      Function.Bijective fun g : Γ(X, B) => g • τ := by
  subst q
  have e : N.presheaf.map (homOfLE (le_refl A)).op τ = τ := by
    rw [show (homOfLE (le_refl A) : A ⟶ A) = 𝟙 A from rfl, op_id, N.presheaf.map_id]
    rfl
  simp only [e]
lemma

bijective_smul_of_isIso

L247 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.bijective_smul_of_isIso
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section smulHom
variable (N : X.Modules) (W : X.Opens) (τ : Γ(N, W))
variable {N W τ}
Lean source · full declaration
lemma bijective_smul_of_isIso (h : IsIso (smulSectionHom N W τ)) :
    Function.Bijective fun g : Γ(X, W) => g • τ := by
  let e := asIso (smulSectionHom N W τ)
  have hb : Function.Bijective (e.hom.val.app (op ⊤)).hom := by
    refine Function.bijective_iff_has_inverse.2 ⟨(e.inv.val.app (op ⊤)).hom, fun a => ?_, fun m =>
      ?_⟩
    · exact congr($(e.hom_inv_id).val.app (op ⊤) |>.hom a)
    · exact congr($(e.inv_hom_id).val.app (op ⊤) |>.hom m)
  have hb' : Function.Bijective fun a : Γ(X, W.ι ''ᵁ ⊤) =>
      a • N.presheaf.map (homOfLE (Scheme.Opens.ι_image_top W).le).op τ := hb
  exact (bijective_smul_map_iff_of_eq (Scheme.Opens.ι_image_top W) τ).1 hb'
lemma

bijective_smul_tmul_res

L265 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.bijective_smul_tmul_res
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section main
variable {L M : X.Modules} {U V : X.Opens} {s : Γ(L, U)} {t : Γ(M, U)}
Lean source · full declaration
lemma bijective_smul_tmul_res (hs : IsFrameOn s V) (ht : IsFrameOn t V) {W : X.Opens}
    (hWU : W ≤ U) (hWV : W ≤ V) :
    Function.Bijective fun g : Γ(X, W) =>
      g • ((L.presheaf.map (homOfLE hWU).op s : L.val.obj (op W)) ⊗ₜ[Γ(X, W)]
        (M.presheaf.map (homOfLE hWU).op t : M.val.obj (op W))) :=
  bijective_smul_tmul (R := Γ(X, W)) _ _ (hs hWU hWV) (ht hWU hWV)
abbrev

resL

L275 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.resL
Documentation

Restricts the first frame to a smaller open subset.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section main
variable {L M : X.Modules} {U V : X.Opens} {s : Γ(L, U)} {t : Γ(M, U)}
variable (W : X.Opens) (hWU : W ≤ U)
Lean source · statement
abbrev resL (W' : X.Opens) (h : W' ≤ W) : Γ(L, W')
abbrev

resM

L278 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.resM
Documentation

Restricts the second frame to a smaller open subset.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section main
variable {L M : X.Modules} {U V : X.Opens} {s : Γ(L, U)} {t : Γ(M, U)}
variable (W : X.Opens) (hWU : W ≤ U)
Lean source · statement
abbrev resM (W' : X.Opens) (h : W' ≤ W) : Γ(M, W')
abbrev

τW

L281 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.τW
Documentation

The tensor product section restricted to an open subset.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section main
variable {L M : X.Modules} {U V : X.Opens} {s : Γ(L, U)} {t : Γ(M, U)}
variable (W : X.Opens) (hWU : W ≤ U)
Lean source · statement
abbrev τW : Γ(L ⊗ M, W)
lemma

map_τW

L284 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.map_τW
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section main
variable {L M : X.Modules} {U V : X.Opens} {s : Γ(L, U)} {t : Γ(M, U)}
variable (W : X.Opens) (hWU : W ≤ U)
Lean source · statement
lemma map_τW (W' : X.Opens) (h : W' ≤ W) :
    (L ⊗ M).presheaf.map (homOfLE h).op (τW (s := s) (t := t) W hWU) =
      tsApp L M W' ((resL (s := s) W hWU W' h : L.val.obj (op W')) ⊗ₜ[Γ(X, W')]
        (resM (t := t) W hWU W' h : M.val.obj (op W')))
theorem

isIso_smulSectionHom

L298 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.isIso_smulSectionHom
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
section main
variable {L M : X.Modules} {U V : X.Opens} {s : Γ(L, U)} {t : Γ(M, U)}
variable (W : X.Opens) (hWU : W ≤ U)
Lean source · statement
theorem isIso_smulSectionHom (hs : IsFrameOn s V) (ht : IsFrameOn t V) (hWV : W ≤ V) :
    IsIso (smulSectionHom (L ⊗ M) W (τW (s := s) (t := t) W hWU))
theorem

isFrameOn_tensorSections

L386 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2.AlgebraicGeometry.Scheme.Modules.FrameTensor.isFrameOn_tensorSections
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace FrameTensor
variable {X : Scheme.{u}}
private local instance frameTensorPresheafModule (P : X.PresheafOfModules) (W : X.Opens) :
    Module Γ(X, W) (P.obj (op W)) := (P.obj (op W)).isModule
Lean source · statement
theorem isFrameOn_tensorSections {L M : X.Modules} {U V : X.Opens} {s : Γ(L, U)} {t : Γ(M, U)}
    (hs : IsFrameOn s V) (ht : IsFrameOn t V) : IsFrameOn (Modules.tensorSections s t) V
theorem

tensorSections_monoidalV2

L410 ↗
AlgebraicGeometry.Scheme.Modules.IsFrameOn.tensorSections_monoidalV2
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections_monoidalV2
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry _root_.AlgebraicGeometry.Scheme.Modules in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.IsFrameOn.tensorSections_monoidalV2 {X :
  AlgebraicGeometry.Scheme.{u}} {L M : X.Modules} {U V : X.Opens}
    {s : Γ(L, U)} {t : Γ(M, U)}
    (hs : AlgebraicGeometry.Scheme.Modules.IsFrameOn s V)
    (ht : AlgebraicGeometry.Scheme.Modules.IsFrameOn t V) :
    AlgebraicGeometry.Scheme.Modules.IsFrameOn (AlgebraicGeometry.Scheme.Modules.tensorSections s
      t) V

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