NYLL
Module

OModulePresheaf_exists_affSES_tensor_of_flat.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_affSES_tensor_of_flat
9 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf exists aff SES tensor of flat

Imports2
Imported by8

Declarations

def

appT

L35 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_affSES_tensor_of_flat.P2mTensorExact.appT
Documentation

The sectionwise linear map induced by tensoring the given affine morphism with the identity.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_affSES_tensor_of_flat
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorExact
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (G : OModulePresheaf π)
Lean source · full declaration
def appT {F F' : OModulePresheaf π} (φ : AffHom F F') (U : V.affineOpens) :
    (F.tensor G).obj U.1 →ₗ[R] (F'.tensor G).obj U.1 where
  toFun t := show (F'.tensor G).obj U.1 from
    (φ.appSections U).rTensor (G.obj U.1) (show F.obj U.1 ⊗[Γ(V, U.1)] G.obj U.1 from t)
  map_add' s t := map_add ((φ.appSections U).rTensor (G.obj U.1)) s t
  map_smul' r t := map_smul ((φ.appSections U).rTensor (G.obj U.1))
    ((Scheme.TwoAffineOpenCover.algebraOfHom π U.1).algebraMap r) t
theorem

appT_apply

L43 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_affSES_tensor_of_flat.P2mTensorExact.appT_apply
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_affSES_tensor_of_flat
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorExact
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (G : OModulePresheaf π)
Lean source · full declaration
theorem appT_apply {F F' : OModulePresheaf π} (φ : AffHom F F') (U : V.affineOpens)
    (t : F.obj U.1 ⊗[Γ(V, U.1)] G.obj U.1) :
    appT G φ U (show (F.tensor G).obj U.1 from t) =
      (show (F'.tensor G).obj U.1 from (φ.appSections U).rTensor (G.obj U.1) t) := rfl
theorem

appT_tmul

L48 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_affSES_tensor_of_flat.P2mTensorExact.appT_tmul
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_affSES_tensor_of_flat
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorExact
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (G : OModulePresheaf π)
Lean source · full declaration
theorem appT_tmul {F F' : OModulePresheaf π} (φ : AffHom F F') (U : V.affineOpens) (x : F.obj U.1)
  (y : G.obj U.1) :
    appT G φ U (show (F.tensor G).obj U.1 from x ⊗ₜ y) = (show (F'.tensor G).obj U.1 from φ.app U x
      ⊗ₜ y) := rfl
def

rTensorAffHom

L54 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_affSES_tensor_of_flat.P2mTensorExact.rTensorAffHom
Documentation

The affine morphism obtained by tensoring the given morphism on the right.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_affSES_tensor_of_flat
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorExact
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (G : OModulePresheaf π)
Lean source · full declaration
def rTensorAffHom {F F' : OModulePresheaf π} (φ : AffHom F F') : AffHom (F.tensor G)
  (F'.tensor G) where
  app U := appT G φ U
  app_smul U a t := map_smul ((φ.appSections U).rTensor (G.obj U.1)) a t
  naturality {U U'} h := by
    refine LinearMap.ext fun t => ?_
    change (φ.appSections U).rTensor (G.obj U.1) (F.tensorResₛₗ G h t) =
      F'.tensorResₛₗ G h ((φ.appSections U').rTensor (G.obj U'.1) t)
    induction t using TensorProduct.inductionOn with
    | tmul x y =>
      rw [tensorResₛₗ_tmul, LinearMap.rTensor_tmul, LinearMap.rTensor_tmul, tensorResₛₗ_tmul,
        AffHom.appSections_apply, AffHom.appSections_apply, φ.naturality_apply h]
    | add s t hs ht => simp only [map_add, hs, ht]
theorem

rTensorAffHom_app

L68 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_affSES_tensor_of_flat.P2mTensorExact.rTensorAffHom_app
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_affSES_tensor_of_flat
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorExact
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (G : OModulePresheaf π)
Lean source · statement
theorem rTensorAffHom_app {F F' : OModulePresheaf π} (φ : AffHom F F') (U : V.affineOpens) :
    (rTensorAffHom G φ).app U = appT G φ U
theorem

exact_appSections

L74 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_affSES_tensor_of_flat.P2mTensorExact.exact_appSections
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_affSES_tensor_of_flat
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorExact
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (G : OModulePresheaf π)
variable {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃)
  (hG : ∀ U : V.affineOpens, Module.Flat Γ(V, U.1) (G.obj U.1))
Lean source · statement
theorem exact_appSections (U : V.affineOpens) : Function.Exact (S.inc.appSections U)
  (S.proj.appSections U)
def

affSES

L80 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_affSES_tensor_of_flat.P2mTensorExact.affSES
Documentation

The affine short exact sequence obtained by tensoring with a module flat on affine opens.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_affSES_tensor_of_flat
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorExact
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (G : OModulePresheaf π)
variable {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃)
  (hG : ∀ U : V.affineOpens, Module.Flat Γ(V, U.1) (G.obj U.1))
Lean source · full declaration
def affSES : AffSES (F₁.tensor G) (F₂.tensor G) (F₃.tensor G) where
  inc := rTensorAffHom G S.inc
  proj := rTensorAffHom G S.proj
  injective U := by
    have := hG U
    exact Module.Flat.rTensor_preserves_injective_linearMap (S.inc.appSections U) (S.injective U)
  surjective U := LinearMap.rTensor_surjective (G.obj U.1) (S.surjective U)
  exact U := by
    have := hG U
    have h := Module.Flat.rTensor_exact (G.obj U.1) (exact_appSections S U)
    have h' : Function.Exact ((rTensorAffHom G S.inc).app U) ((rTensorAffHom G S.proj).app U) := h
    exact (LinearMap.exact_iff.mp h').symm
theorem

main

L94 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_affSES_tensor_of_flat.P2mTensorExact.main
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_affSES_tensor_of_flat
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
namespace P2mTensorExact
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (G : OModulePresheaf π)
variable {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃)
  (hG : ∀ U : V.affineOpens, Module.Flat Γ(V, U.1) (G.obj U.1))
include hG in
Lean source · full declaration
theorem main :
    ∃ S' : AffSES (F₁.tensor G) (F₂.tensor G) (F₃.tensor G),
      ∀ U : V.affineOpens,
        (∀ (x : F₁.obj U.1) (y : G.obj U.1),
          S'.inc.app U (show (F₁.tensor G).obj U.1 from x ⊗ₜ[Γ(V, U.1)] y) =
            (show (F₂.tensor G).obj U.1 from S.inc.app U x ⊗ₜ[Γ(V, U.1)] y)) ∧
        (∀ (x : F₂.obj U.1) (y : G.obj U.1),
          S'.proj.app U (show (F₂.tensor G).obj U.1 from x ⊗ₜ[Γ(V, U.1)] y) =
            (show (F₃.tensor G).obj U.1 from S.proj.app U x ⊗ₜ[Γ(V, U.1)] y)) :=
  ⟨affSES G S hG, fun _ => ⟨fun _ _ => rfl, fun _ _ => rfl⟩⟩
theorem

exists_affSES_tensor_of_flat

L107 ↗
AlgebraicGeometry.OModulePresheaf.exists_affSES_tensor_of_flat
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_exists_affSES_tensor_of_flat
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
Lean source · full declaration
theorem _root_.AlgebraicGeometry.OModulePresheaf.exists_affSES_tensor_of_flat
    {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
    {F₁ F₂ F₃ : OModulePresheaf π} (S : OModulePresheaf.AffSES F₁ F₂ F₃) (G : OModulePresheaf π)
    (hG : ∀ U : V.affineOpens, Module.Flat Γ(V, U.1) (G.obj U.1)) :
    ∃ S' : OModulePresheaf.AffSES (F₁.tensor G) (F₂.tensor G) (F₃.tensor G),
      ∀ U : V.affineOpens,
        (∀ (x : F₁.obj U.1) (y : G.obj U.1),
          S'.inc.app U (show (F₁.tensor G).obj U.1 from x ⊗ₜ[Γ(V, U.1)] y) =
            (show (F₂.tensor G).obj U.1 from S.inc.app U x ⊗ₜ[Γ(V, U.1)] y)) ∧
        (∀ (x : F₂.obj U.1) (y : G.obj U.1),
          S'.proj.app U (show (F₂.tensor G).obj U.1 from x ⊗ₜ[Γ(V, U.1)] y) =
            (show (F₃.tensor G).obj U.1 from S.proj.app U x ⊗ₜ[Γ(V, U.1)] y)) :=
  P2mTensorExact.main G S hG

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