Module

Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent

35 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules bijective lift tensor Sections Bilin of is Quasicoherent

Imports2

Imported by4

def

modBO

L45 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.modBO

Documentation

The action of sections over U on module sections over a basic open by restriction of scalars.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
section BasicOpen
variable (N : X.Modules) (U : X.Opens) (f : Γ(X, U))

Lean source · statement

def modBO : Module Γ(X, U) Γ(N, X.basicOpen f)

instance

isScalarTower_modBO

L51 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.isScalarTower_modBO

Documentation

The restricted action from U factors through the ring of sections on the basic open.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
section BasicOpen
variable (N : X.Modules) (U : X.Opens) (f : Γ(X, U))
attribute [local instance] modBO

Lean source · statement

instance isScalarTower_modBO : IsScalarTower Γ(X, U) Γ(X, X.basicOpen f) Γ(N, X.basicOpen f)

def

resBO

L57 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.resBO

Documentation

Restrict module sections from U to the basic open, as a linear map over the ring of sections on U.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
section BasicOpen
variable (N : X.Modules) (U : X.Opens) (f : Γ(X, U))
attribute [local instance] modBO

Lean source · full declaration

def resBO : Γ(N, U) →ₗ[Γ(X, U)] Γ(N, X.basicOpen f) where
  toFun := N.presheaf.map (homOfLE (X.basicOpen_le f)).op
  map_add' x y := map_add _ x y
  map_smul' a x := Scheme.Modules.map_smul N (homOfLE (X.basicOpen_le f)) a x

theorem

resBO_apply

L62 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.resBO_apply

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
section BasicOpen
variable (N : X.Modules) (U : X.Opens) (f : Γ(X, U))
attribute [local instance] modBO

Lean source · statement

theorem resBO_apply (x : Γ(N, U)) : resBO N U f x = N.presheaf.map (homOfLE (X.basicOpen_le f)).op
  x

theorem

isLocalizedModule_resBO

L65 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.isLocalizedModule_resBO

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
section BasicOpen
variable (N : X.Modules) (U : X.Opens) (f : Γ(X, U))
attribute [local instance] modBO

Lean source · statement

theorem isLocalizedModule_resBO {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R))
    (hN : (OModulePresheaf.ofModules π N).IsQuasicoherent) (hU : IsAffineOpen U) :
    IsLocalizedModule (Submonoid.powers f) (resBO N U f)

theorem

res_resBO

L88 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.res_resBO

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
section BasicOpen
variable (N : X.Modules) (U : X.Opens) (f : Γ(X, U))
attribute [local instance] modBO

Lean source · statement

theorem res_resBO {g : Γ(X, U)} (h : X.basicOpen g ≤ X.basicOpen f) (x : Γ(N, U)) :
    N.presheaf.map (homOfLE h).op (resBO N U f x) = resBO N U g x

abbrev

theta

L103 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.theta

Documentation

The linear map from the tensor product of section modules to sections of the sheaf tensor product.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Theta
variable (L M : X.Modules)

Lean source · statement

abbrev theta (U : X.Opens) : Γ(L, U) ⊗[Γ(X, U)] Γ(M, U) →ₗ[Γ(X, U)] Γ(L ⊗ M, U)

theorem

theta_tmul

L106 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.theta_tmul

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Theta
variable (L M : X.Modules)

Lean source · statement

theorem theta_tmul (U : X.Opens) (s : Γ(L, U)) (t : Γ(M, U)) :
    theta L M U (s ⊗ₜ t) = Scheme.Modules.tensorSections s t

def

thetaBO

L113 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.thetaBO

Documentation

The tensor-sections map on a basic open viewed over the ring of sections on U.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Theta
variable (L M : X.Modules)
variable (U : X.Opens) (f : Γ(X, U))

Lean source · statement

def thetaBO : Γ(L, X.basicOpen f) ⊗[Γ(X, U)] Γ(M, X.basicOpen f) →ₗ[Γ(X, U)] Γ(L ⊗ M, X.basicOpen
  f)

theorem

thetaBO_tmul

L126 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.thetaBO_tmul

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Theta
variable (L M : X.Modules)
variable (U : X.Opens) (f : Γ(X, U))

Lean source · statement

theorem thetaBO_tmul (x : Γ(L, X.basicOpen f)) (y : Γ(M, X.basicOpen f)) :
    thetaBO L M U f (x ⊗ₜ y) = Scheme.Modules.tensorSections x y

theorem

thetaBO_comp_map

L129 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.thetaBO_comp_map

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Theta
variable (L M : X.Modules)
variable (U : X.Opens) (f : Γ(X, U))

Lean source · statement

theorem thetaBO_comp_map :
    thetaBO L M U f ∘ₗ TensorProduct.map (resBO L U f) (resBO M U f) = resBO (L ⊗ M) U f ∘ₗ theta L
      M U

theorem

thetaBO_map

L137 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.thetaBO_map

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Theta
variable (L M : X.Modules)
variable (U : X.Opens) (f : Γ(X, U))

Lean source · statement

theorem thetaBO_map (z : Γ(L, U) ⊗[Γ(X, U)] Γ(M, U)) :
    thetaBO L M U f (TensorProduct.map (resBO L U f) (resBO M U f) z) = resBO (L ⊗ M) U f (theta L
      M U z)

def

tensorBOEquiv

L144 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.tensorBOEquiv

Documentation

Identify the tensor product over a basic-open localization with the tensor product over sections on U, with scalars restricted to U.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Theta
variable (L M : X.Modules)
variable (U : X.Opens) (f : Γ(X, U))

Lean source · statement

def tensorBOEquiv (hU : IsAffineOpen U) :
    Γ(L, X.basicOpen f) ⊗[Γ(X, X.basicOpen f)] Γ(M, X.basicOpen f) ≃ₗ[Γ(X, U)]
      Γ(L, X.basicOpen f) ⊗[Γ(X, U)] Γ(M, X.basicOpen f)

theorem

tensorBOEquiv_tmul

L151 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.tensorBOEquiv_tmul

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Theta
variable (L M : X.Modules)
variable (U : X.Opens) (f : Γ(X, U))

Lean source · statement

theorem tensorBOEquiv_tmul (hU : IsAffineOpen U) (x : Γ(L, X.basicOpen f)) (y : Γ(M, X.basicOpen
  f)) :
    tensorBOEquiv L M U f hU (x ⊗ₜ[Γ(X, X.basicOpen f)] y) = x ⊗ₜ[Γ(X, U)] y

theorem

thetaBO_tensorBOEquiv

L155 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.thetaBO_tensorBOEquiv

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Theta
variable (L M : X.Modules)
variable (U : X.Opens) (f : Γ(X, U))

Lean source · statement

theorem thetaBO_tensorBOEquiv (hU : IsAffineOpen U)
    (w : Γ(L, X.basicOpen f) ⊗[Γ(X, X.basicOpen f)] Γ(M, X.basicOpen f)) :
    thetaBO L M U f (tensorBOEquiv L M U f hU w) = theta L M (X.basicOpen f) w

theorem

thetaBO_injective_of

L162 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.thetaBO_injective_of

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Theta
variable (L M : X.Modules)
variable (U : X.Opens) (f : Γ(X, U))

Lean source · statement

theorem thetaBO_injective_of (hU : IsAffineOpen U) (h : Function.Injective (theta L M (X.basicOpen
  f))) :
    Function.Injective (thetaBO L M U f)

def

phi

L179 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.phi

Documentation

The underlying presheaf morphism from the tensor presheaf to the sheaf tensor product.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Local
variable (L M : X.Modules)

Lean source · statement

def phi

theorem

phi_isLocallyInjective

L181 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.phi_isLocallyInjective

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Local
variable (L M : X.Modules)

Lean source · statement

theorem phi_isLocallyInjective : Presheaf.IsLocallyInjective (Opens.grothendieckTopology X) (phi L
  M)

theorem

phi_isLocallySurjective

L203 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.phi_isLocallySurjective

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Local
variable (L M : X.Modules)

Lean source · statement

theorem phi_isLocallySurjective : Presheaf.IsLocallySurjective (Opens.grothendieckTopology X) (phi
  L M)

def

phiU

L228 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.phiU

Documentation

The additive map on sections induced by the tensor-sections presheaf morphism.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Local
variable (L M : X.Modules)
variable (U : X.Opens)

Lean source · statement

def phiU : Γ(L, U) ⊗[Γ(X, U)] Γ(M, U) →+ Γ(L ⊗ M, U)

theorem

phiU_eq_theta

L230 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.phiU_eq_theta

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Local
variable (L M : X.Modules)
variable (U : X.Opens)

Lean source · statement

theorem phiU_eq_theta (z : Γ(L, U) ⊗[Γ(X, U)] Γ(M, U)) : phiU L M U z = theta L M U z

def

resT

L236 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.resT

Documentation

Restriction of the tensor presheaf along an inclusion of open subsets.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Local
variable (L M : X.Modules)
variable (U : X.Opens)

Lean source · statement

def resT {W : X.Opens} (i : W ⟶ U) : Γ(L, U) ⊗[Γ(X, U)] Γ(M, U) →+ Γ(L, W) ⊗[Γ(X, W)] Γ(M, W)

theorem

resT_tmul

L239 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.resT_tmul

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Local
variable (L M : X.Modules)
variable (U : X.Opens)

Lean source · statement

theorem resT_tmul {W : X.Opens} (i : W ⟶ U) (s : Γ(L, U)) (t : Γ(M, U)) :
    resT L M U i (s ⊗ₜ t) = L.presheaf.map i.op s ⊗ₜ M.presheaf.map i.op t

theorem

resT_comp

L249 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.resT_comp

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Extract
variable (L M : X.Modules) (U : X.Opens)

Lean source · statement

theorem resT_comp {W W' : X.Opens} (i : W ⟶ U) (j : W' ⟶ W) (z : Γ(L, U) ⊗[Γ(X, U)] Γ(M, U)) :
    resT L M U (j ≫ i) z = resT L M W j (resT L M U i z)

theorem

exists_resT_eq_of_theta_eq

L255 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.exists_resT_eq_of_theta_eq

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Extract
variable (L M : X.Modules) (U : X.Opens)

Lean source · statement

theorem exists_resT_eq_of_theta_eq (z z' : Γ(L, U) ⊗[Γ(X, U)] Γ(M, U)) (h : theta L M U z = theta L
  M U z')
    {x : X} (hx : x ∈ U) : ∃ (W : X.Opens) (i : W ⟶ U), x ∈ W ∧ resT L M U i z = resT L M U i z'

theorem

exists_theta_eq_res

L266 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.exists_theta_eq_res

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Extract
variable (L M : X.Modules) (U : X.Opens)

Lean source · statement

theorem exists_theta_eq_res (y : Γ(L ⊗ M, U)) {x : X} (hx : x ∈ U) :
    ∃ (W : X.Opens) (i : W ⟶ U), x ∈ W ∧
      ∃ w : Γ(L, W) ⊗[Γ(X, W)] Γ(M, W), theta L M W w = (L ⊗ M).presheaf.map i.op y

theorem

theta_resT

L282 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.theta_resT

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Injective
variable (L M : X.Modules)

Lean source · statement

theorem theta_resT {W W' : X.Opens} (j : W' ⟶ W) (w : Γ(L, W) ⊗[Γ(X, W)] Γ(M, W)) :
    theta L M W' (resT L M W j w) = (L ⊗ M).presheaf.map j.op (theta L M W w)

theorem

tensorBOEquiv_resT

L290 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.tensorBOEquiv_resT

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Injective
variable (L M : X.Modules)

Lean source · statement

theorem tensorBOEquiv_resT (U : X.Opens) (hU : IsAffineOpen U) (g : Γ(X, U)) (z : Γ(L, U) ⊗[Γ(X,
  U)] Γ(M, U)) :
    tensorBOEquiv L M U g hU (resT L M U (homOfLE (X.basicOpen_le g)) z) =
      TensorProduct.map (resBO L U g) (resBO M U g) z

theorem

theta_injective

L298 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.theta_injective

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Injective
variable (L M : X.Modules)

Lean source · statement

theorem theta_injective {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R))
    (hL : (OModulePresheaf.ofModules π L).IsQuasicoherent) (hM : (OModulePresheaf.ofModules π
      M).IsQuasicoherent)
    (U : X.Opens) (hU : IsAffineOpen U) : Function.Injective (theta L M U)

theorem

exists_basicOpen_theta_res

L334 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.exists_basicOpen_theta_res

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Surjective
variable (L M : X.Modules) {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R))
  (hL : (OModulePresheaf.ofModules π L).IsQuasicoherent) (hM : (OModulePresheaf.ofModules π
    M).IsQuasicoherent)
  (U : X.Opens) (hU : IsAffineOpen U)
include hL hM hU in

Lean source · statement

theorem exists_basicOpen_theta_res (y : Γ(L ⊗ M, U)) {x : X} (hx : x ∈ U) :
    ∃ g : Γ(X, U), x ∈ X.basicOpen g ∧ ∃ (z : Γ(L, U) ⊗[Γ(X, U)] Γ(M, U)) (n : ℕ),
      resBO (L ⊗ M) U g (theta L M U z) = resBO (L ⊗ M) U g (g ^ n • y)

theorem

bump

L352 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.bump

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Surjective
variable (L M : X.Modules) {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R))
  (hL : (OModulePresheaf.ofModules π L).IsQuasicoherent) (hM : (OModulePresheaf.ofModules π
    M).IsQuasicoherent)
  (U : X.Opens) (hU : IsAffineOpen U)

Lean source · statement

theorem bump (y : Γ(L ⊗ M, U)) (g : Γ(X, U)) (z : Γ(L, U) ⊗[Γ(X, U)] Γ(M, U)) (n m : ℕ)
    (h : resBO (L ⊗ M) U g (theta L M U z) = resBO (L ⊗ M) U g (g ^ n • y)) :
    resBO (L ⊗ M) U g (theta L M U (g ^ m • z)) = resBO (L ⊗ M) U g (g ^ (m + n) • y)

theorem

exists_pow_smul_sub_eq_zero

L367 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.exists_pow_smul_sub_eq_zero

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Glue
variable (L M : X.Modules) {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R))
  (hL : (OModulePresheaf.ofModules π L).IsQuasicoherent) (hM : (OModulePresheaf.ofModules π
    M).IsQuasicoherent)
  (U : X.Opens) (hU : IsAffineOpen U)
include hL hM hU in

Lean source · statement

theorem exists_pow_smul_sub_eq_zero (y : Γ(L ⊗ M, U)) (g g' : Γ(X, U))
    (z z' : Γ(L, U) ⊗[Γ(X, U)] Γ(M, U)) (n : ℕ)
    (hz : resBO (L ⊗ M) U g (theta L M U z) = resBO (L ⊗ M) U g (g ^ n • y))
    (hz' : resBO (L ⊗ M) U g' (theta L M U z') = resBO (L ⊗ M) U g' (g' ^ n • y)) :
    ∃ m : ℕ, (g * g') ^ m • (g' ^ n • z - g ^ n • z') = 0

theorem

theta_surjective

L393 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.theta_surjective

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO
section Glue
variable (L M : X.Modules) {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R))
  (hL : (OModulePresheaf.ofModules π L).IsQuasicoherent) (hM : (OModulePresheaf.ofModules π
    M).IsQuasicoherent)
  (U : X.Opens) (hU : IsAffineOpen U)
include hL hM hU in

Lean source · statement

theorem theta_surjective : Function.Surjective (theta L M U)

theorem

theta_bijective

L475 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent.P2mQcTensorCompare.theta_bijective

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
noncomputable section
namespace P2mQcTensorCompare
variable {X : Scheme.{u}}
attribute [local instance] modBO

Lean source · statement

theorem theta_bijective (L M : X.Modules) {R : Type u} [CommRing R] (π : X ⟶ Spec (.of R))
    (hL : (OModulePresheaf.ofModules π L).IsQuasicoherent) (hM : (OModulePresheaf.ofModules π
      M).IsQuasicoherent)
    (U : X.affineOpens) : Function.Bijective (theta L M U.1)

theorem

bijective_lift_tensorSectionsBilin_of_isQuasicoherent

L486 ↗

AlgebraicGeometry.Scheme.Modules.bijective_lift_tensorSectionsBilin_of_isQuasicoherent

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TensorProduct
open _root_.Opposite
open P2mQcTensorCompare in

Lean source · statement

theorem
  _root_.AlgebraicGeometry.Scheme.Modules.bijective_lift_tensorSectionsBilin_of_isQuasicoherent
    {R : Type u} [CommRing R] {X : Scheme.{u}} (π : X ⟶ Spec (.of R)) {L M : X.Modules}
    (hL : (OModulePresheaf.ofModules π L).IsQuasicoherent) (hM : (OModulePresheaf.ofModules π
      M).IsQuasicoherent)
    (U : X.affineOpens) :
    Function.Bijective (TensorProduct.lift (Scheme.Modules.tensorSectionsBilin L M U) :
      Γ(L, U) ⊗[Γ(X, U)] Γ(M, U) →ₗ[Γ(X, U)] Γ(L ⊗ M, U))

Module documentation

Scheme Modules bijective lift tensor Sections Bilin of is Quasicoherent

Declarations