NYLL
Module

Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2
35 declarations indexed from sourceView source ↗

Module documentation

Tensor sections on affine opens

The tensor-sections map of quasicoherent modules is bijective on affine opens.

Imports17
  • Mathlib.AlgebraicGeometry.Modules.Sheaf
  • Mathlib.AlgebraicGeometry.AffineScheme
  • Mathlib.Algebra.Module.LocalizedModule.IsLocalization
  • Mathlib.RingTheory.Localization.BaseChange
  • Mathlib.RingTheory.Ideal.Operations
  • Mathlib.RingTheory.Ideal.Basic
  • Mathlib.CategoryTheory.Sites.LocallyInjective
  • Mathlib.CategoryTheory.Sites.LocallySurjective
  • Mathlib.CategoryTheory.Sites.LocallyBijective
  • Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
  • Mathlib.Data.Finset.Lattice.Fold
  • Mathlib.Tactic.Choose
  • Mathlib.Tactic.Ext
  • Mathlib.Tactic.Convert
  • Mathlib.Tactic.Ring
  • Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesSectionsTensorV2
  • Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheafOfModules
Imported by2

Declarations

def

modBO

L63 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.P2mQcTensorCompare.modBO
Documentation

The scalar action on basic-open sections induced by restriction.

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_monoidalV2
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

L68 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.P2mQcTensorCompare.isScalarTower_modBO
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_monoidalV2
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

L73 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.P2mQcTensorCompare.resBO
Documentation

Restriction of module sections to a basic open, as a linear map.

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_monoidalV2
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

L78 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L81 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L104 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L118 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.P2mQcTensorCompare.theta
Documentation

The tensor-sections linear map.

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_monoidalV2
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

L121 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L128 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.P2mQcTensorCompare.thetaBO
Documentation

The tensor-sections map over a basic open with scalars restricted to the source.

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_monoidalV2
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

L141 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L144 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L152 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L158 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.P2mQcTensorCompare.tensorBOEquiv
Documentation

Compare tensor products before and after localization.

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_monoidalV2
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

L165 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L169 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L176 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L193 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.P2mQcTensorCompare.phi
Documentation

The tensor-sections comparison on underlying presheaves.

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_monoidalV2
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

L195 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L222 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L252 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.P2mQcTensorCompare.phiU
Documentation

The additive tensor-sections map on an open subset.

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_monoidalV2
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

L254 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L260 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.P2mQcTensorCompare.resT
Documentation

Restriction in the tensor presheaf.

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_monoidalV2
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

L263 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L273 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L279 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L290 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L306 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L314 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L322 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L358 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L376 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L391 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L418 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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

L500 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2.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_monoidalV2
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_monoidalV2

L526 ↗
AlgebraicGeometry.Scheme.Modules.bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2
Source context 6 commands

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

section ProofImplementation
open AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry TensorProduct Opposite
namespace AlgebraicGeometry.Scheme.Modules
universe u
Lean source · statement
theorem bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2
    {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))

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