NYLL
Module

OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor
14 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf is Quasicoherent is Coherent supported In tensor

Imports1
Imported by9

Declarations

def

diag

L40 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor.P2mTensorStableSol.diag
Documentation

The map on tensor products induced by the two compatible linear maps.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorStableSol
section Alg
variable {A : Type*} [CommRing A] (S : Submonoid A) (A' : Type*) [CommRing A'] [Algebra A A']
  [IsLocalization S A']
variable {M N : Type*} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]
variable {M' N' : Type*} [AddCommGroup M'] [Module A' M'] [Module A M'] [IsScalarTower A A' M']
  [AddCommGroup N'] [Module A' N'] [Module A N'] [IsScalarTower A A' N']
variable (lM : M →ₗ[A] M') (lN : N →ₗ[A] N')
Lean source · statement
def diag : M ⊗[A] N →ₗ[A] M' ⊗[A'] N'
theorem

diag_tmul

L48 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor.P2mTensorStableSol.diag_tmul
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorStableSol
section Alg
variable {A : Type*} [CommRing A] (S : Submonoid A) (A' : Type*) [CommRing A'] [Algebra A A']
  [IsLocalization S A']
variable {M N : Type*} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]
variable {M' N' : Type*} [AddCommGroup M'] [Module A' M'] [Module A M'] [IsScalarTower A A' M']
  [AddCommGroup N'] [Module A' N'] [Module A N'] [IsScalarTower A A' N']
variable (lM : M →ₗ[A] M') (lN : N →ₗ[A] N')
Lean source · statement
theorem diag_tmul (x : M) (y : N) : diag A' lM lN (x ⊗ₜ y) = lM x ⊗ₜ[A'] lN y
theorem

isLocalizedModule_diag

L51 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor.P2mTensorStableSol.isLocalizedModule_diag
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorStableSol
section Alg
variable {A : Type*} [CommRing A] (S : Submonoid A) (A' : Type*) [CommRing A'] [Algebra A A']
  [IsLocalization S A']
variable {M N : Type*} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]
variable {M' N' : Type*} [AddCommGroup M'] [Module A' M'] [Module A M'] [IsScalarTower A A' M']
  [AddCommGroup N'] [Module A' N'] [Module A N'] [IsScalarTower A A' N']
variable (lM : M →ₗ[A] M') (lN : N →ₗ[A] N')
include S in
Lean source · statement
theorem isLocalizedModule_diag [IsLocalizedModule S lM] [IsLocalizedModule S lN] :
    IsLocalizedModule S (diag A' lM lN)
def

modBO

L71 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor.P2mTensorStableSol.modBO
Documentation

The module structure on sections of a basic open obtained by restricting scalars.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorStableSol
section Datum
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
Lean source · statement
def modBO (F : OModulePresheaf π) (U : V.Opens) (f : Γ(V, U)) :
    Module Γ(V, U) (F.obj (V.basicOpen f))
theorem

isScalarTower_modBO

L75 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor.P2mTensorStableSol.isScalarTower_modBO
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorStableSol
section Datum
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
Lean source · full declaration
theorem isScalarTower_modBO (F : OModulePresheaf π) (U : V.Opens) (f : Γ(V, U)) :
    letI := modBO F U f
    IsScalarTower Γ(V, U) Γ(V, V.basicOpen f) (F.obj (V.basicOpen f)) :=
  letI := modBO F U f
  IsScalarTower.of_algebraMap_smul fun _ _ => rfl
def

resBO

L82 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor.P2mTensorStableSol.resBO
Documentation

Restriction to a basic open, as a linear map over the ring of sections on the original open.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorStableSol
section Datum
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
Lean source · full declaration
def resBO (F : OModulePresheaf π) (U : V.Opens) (f : Γ(V, U)) :
    letI := modBO F U f
    F.obj U →ₗ[Γ(V, U)] F.obj (V.basicOpen f) :=
  letI := modBO F U f
  { toFun := F.res (V.basicOpen_le f)
    map_add' := fun x y => map_add _ x y
    map_smul' := fun a x => F.res_smul (V.basicOpen_le f) a x }
theorem

resBO_apply

L90 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor.P2mTensorStableSol.resBO_apply
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorStableSol
section Datum
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
Lean source · full declaration
theorem resBO_apply (F : OModulePresheaf π) (U : V.Opens) (f : Γ(V, U)) (x : F.obj U) :
    letI := modBO F U f
    resBO F U f x = F.res (V.basicOpen_le f) x := rfl
theorem

isLocalizedModule_resBO

L94 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor.P2mTensorStableSol.isLocalizedModule_resBO
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorStableSol
section Datum
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
Lean source · full declaration
theorem isLocalizedModule_resBO (F : OModulePresheaf π) (hF : F.IsQuasicoherent) (U : V.affineOpens)
    (f : Γ(V, U.1)) :
    letI := modBO F U.1 f
    IsLocalizedModule (Submonoid.powers f) (resBO F U.1 f) := by
  let := modBO F U.1 f
  have := isScalarTower_modBO F U.1 f
  have : IsLocalization.Away f Γ(V, V.basicOpen f) := U.2.isLocalization_basicOpen f
  obtain ⟨h1, h2⟩ := hF U f
  refine ⟨?_, ?_, ?_⟩
  · rintro ⟨s, n, rfl⟩
    rw [Module.End.isUnit_iff]
    have hu : IsUnit (algebraMap Γ(V, U.1) Γ(V, V.basicOpen f) (f ^ n)) := by
      rw [map_pow]; exact (IsLocalization.Away.algebraMap_isUnit f).pow n
    have := hu.smul_bijective (β := F.obj (V.basicOpen f))
    exact this
  · intro y
    obtain ⟨n, x, hx⟩ := h1 y
    exact ⟨⟨x, ⟨f ^ n, n, rfl⟩⟩, hx.symm⟩
  · intro x₁ x₂ h
    have h0 : F.res (V.basicOpen_le f) (x₁ - x₂) = 0 := by
      rw [map_sub]; exact sub_eq_zero.mpr h
    obtain ⟨n, hn⟩ := h2 (x₁ - x₂) h0
    refine ⟨⟨f ^ n, n, rfl⟩, ?_⟩
    rw [Submonoid.smul_def, Submonoid.smul_def, ← sub_eq_zero, ← smul_sub]
    exact hn
theorem

qcAt_of_isLocalizedModule

L120 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor.P2mTensorStableSol.qcAt_of_isLocalizedModule
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorStableSol
section Datum
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
Lean source · full declaration
theorem qcAt_of_isLocalizedModule (F : OModulePresheaf π) (U : V.affineOpens) (f : Γ(V, U.1))
    (h : letI := modBO F U.1 f; IsLocalizedModule (Submonoid.powers f) (resBO F U.1 f)) :
    (∀ x : F.obj (V.basicOpen f), ∃ (n : ℕ) (y : F.obj U.1),
        F.res (V.basicOpen_le f) y = (V.presheaf.map (homOfLE (V.basicOpen_le f)).op).hom (f ^ n) •
          x)
      ∧ (∀ y : F.obj U.1, F.res (V.basicOpen_le f) y = 0 → ∃ n : ℕ, (f ^ n : Γ(V, U.1)) • y = 0) :=
        by
  let := modBO F U.1 f
  refine ⟨fun x => ?_, fun y hy => ?_⟩
  · obtain ⟨⟨y, ⟨s, n, rfl⟩⟩, hs⟩ := h.surj x
    exact ⟨n, y, hs.symm⟩
  · have h0 : resBO F U.1 f y = resBO F U.1 f 0 := by rw [map_zero]; exact hy
    obtain ⟨⟨s, n, rfl⟩, hs⟩ := h.exists_of_eq h0
    refine ⟨n, ?_⟩
    simpa [Submonoid.smul_def] using hs
theorem

isQuasicoherent_tensor

L142 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor.P2mTensorStableSol.isQuasicoherent_tensor
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorStableSol
section Card
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F G : OModulePresheaf π)
Lean source · statement
theorem isQuasicoherent_tensor (hF : F.IsQuasicoherent) (hG : G.IsQuasicoherent) :
    (F.tensor G).IsQuasicoherent
theorem

isCoherent_tensor

L166 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor.P2mTensorStableSol.isCoherent_tensor
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorStableSol
section Card
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F G : OModulePresheaf π)
Lean source · statement
theorem isCoherent_tensor (hF : F.IsCoherent) (hG : G.IsCoherent) : (F.tensor G).IsCoherent
theorem

supportedIn_tensor

L172 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor.P2mTensorStableSol.supportedIn_tensor
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorStableSol
section Card
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F G : OModulePresheaf π)
Lean source · statement
theorem supportedIn_tensor (Y : TopologicalSpace.Closeds V) (h : F.SupportedIn Y ∨ G.SupportedIn Y)
  :
    (F.tensor G).SupportedIn Y
theorem

main

L181 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor.P2mTensorStableSol.main
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorStableSol
section Card
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F G : OModulePresheaf π)
Lean source · statement
theorem main :
    (F.IsQuasicoherent → G.IsQuasicoherent → (F.tensor G).IsQuasicoherent) ∧
    (F.IsCoherent → G.IsCoherent → (F.tensor G).IsCoherent) ∧
    (∀ Y : TopologicalSpace.Closeds V, F.SupportedIn Y ∨ G.SupportedIn Y → (F.tensor G).SupportedIn
      Y)
theorem

isQuasicoherent_isCoherent_supportedIn_tensor

L192 ↗
AlgebraicGeometry.OModulePresheaf.isQuasicoherent_isCoherent_supportedIn_tensor
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isQuasicoherent_isCoherent_supportedIn_tensor
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.isQuasicoherent_isCoherent_supportedIn_tensor
    {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F G : OModulePresheaf π) :
    (F.IsQuasicoherent → G.IsQuasicoherent → (F.tensor G).IsQuasicoherent) ∧
    (F.IsCoherent → G.IsCoherent → (F.tensor G).IsCoherent) ∧
    (∀ Y : TopologicalSpace.Closeds V, F.SupportedIn Y ∨ G.SupportedIn Y → (F.tensor G).SupportedIn
      Y)

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