Module

Scheme_Modules_IsFrameOn_tensorSections.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_tensorSections

30 declarations indexed from sourceView source ↗

Module documentation

Tensor products of frames

The tensor product of two sections that are frames on the same open is again a frame on that open.

Imports6

Imported by16

instance

frameTensorPresheafModule

L55 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.frameTensorPresheafModule

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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
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

L58 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.bijective_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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L79 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.tsApp

Documentation

Apply the canonical presheaf-to-sheaf tensor comparison to a local tensor section.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L85 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.tensorSections_eq_tsApp

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L90 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.tsApp_smul

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L94 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.tsApp_add

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L98 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.map_tsApp

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L102 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.map_smul_tmul

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L110 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.W_tensorSectionsHom

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L125 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.isLocallySurjective_tensorSectionsHom

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L130 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.isLocallyInjective_tensorSectionsHom

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L135 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.exists_local_preimage

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L143 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.exists_local_eq

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L159 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.restrictRingCatSheafHom

Documentation

The canonical structure-sheaf morphism for restriction to the open subscheme.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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'

L166 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.restrictFunctor'

Documentation

Restriction of modules to the open subscheme via its structure-sheaf morphism.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L169 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.image_le

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L173 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.image_preimage_of_le

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L178 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.secX

Documentation

View a scalar section on the open subscheme as a section on its image in the scheme.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L188 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.smulSectionHom

Documentation

The module morphism from the unit module sending each scalar to its product with the restricted section.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L218 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.smulSectionHom_app_apply

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L224 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.bijective_smul_map_iff_of_eq

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L233 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.bijective_smul_of_isIso

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L251 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.bijective_smul_tmul_res

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L261 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.resL

Documentation

The first frame section restricted to a smaller open subset.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L264 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.resM

Documentation

The second frame section restricted to a smaller open subset.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L267 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.τW

Documentation

The tensor product of the two frame sections after restriction to the chosen open subset.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L270 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.map_τW

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L284 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.isIso_smulSectionHom

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L372 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules.FrameTensor.isFrameOn_tensorSections

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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
noncomputable section
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
namespace FrameTensor
variable {X : Scheme.{u}}
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

L390 ↗

AlgebraicGeometry.Scheme.Modules.IsFrameOn.tensorSections

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_tensorSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TensorProduct
open _root_.TopologicalSpace
with_weak_namespace _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open _root_.AlgebraicGeometry Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry
    _root_.AlgebraicGeometry.Scheme.Modules
    Scheme_Modules_IsFrameOn_tensorSections.AlgebraicGeometry.Scheme.Modules in
with_weak_namespace Scheme_Modules_IsFrameOn_tensorSections

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.IsFrameOn.tensorSections {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

Module documentation

Tensor products of frames

Declarations