NYLL
Module

OModulePresheaf_nonempty_cechEquiv_ofModules_pullback_comap_twist_pushforwardUnit.lean

Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_nonempty_cechEquiv_ofModules_pullback_comap_twist_pushforwardUnit
33 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf nonempty cech Equiv of Modules pullback comap twist pushforward Unit

Imports10
Imported by4

Declarations

abbrev

pb

L45 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.pb
Documentation

The pullback of the module sheaf along the given scheme morphism.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Eta
variable {V W : Scheme.{u}} (γ : W ⟶ V) (N : V.Modules)
Lean source · statement
abbrev pb : W.Modules
abbrev

unitHom

L48 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.unitHom
Documentation

The unit of the pullback-pushforward adjunction at the module sheaf.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Eta
variable {V W : Scheme.{u}} (γ : W ⟶ V) (N : V.Modules)
Lean source · statement
abbrev unitHom : N ⟶ (Scheme.Modules.pushforward γ).obj (pb γ N)
def

eta

L52 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.eta
Documentation

The map on sections induced by the unit of the pullback-pushforward adjunction.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Eta
variable {V W : Scheme.{u}} (γ : W ⟶ V) (N : V.Modules)
Lean source · statement
def eta (U : V.Opens) (s : Γ(N, U)) : Γ(pb γ N, γ ⁻¹ᵁ U)
theorem

eta_add

L54 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.eta_add
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Eta
variable {V W : Scheme.{u}} (γ : W ⟶ V) (N : V.Modules)
Lean source · statement
theorem eta_add (U : V.Opens) (s₁ s₂ : Γ(N, U)) : eta γ N U (s₁ + s₂) = eta γ N U s₁ + eta γ N U s₂
theorem

eta_smul

L58 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.eta_smul
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Eta
variable {V W : Scheme.{u}} (γ : W ⟶ V) (N : V.Modules)
Lean source · statement
theorem eta_smul (U : V.Opens) (a : Γ(V, U)) (s : Γ(N, U)) : eta γ N U (a • s) = γ.app U a • eta γ
  N U s
theorem

app_map

L64 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.app_map
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Eta
variable {V W : Scheme.{u}} (γ : W ⟶ V) (N : V.Modules)
Lean source · statement
theorem app_map {M M' : V.Modules} (φ : M ⟶ M') {U₁ U₂ : V.Opens} (i : U₁ ⟶ U₂) (x : Γ(M, U₂)) :
    φ.app U₁ (M.presheaf.map i.op x) = M'.presheaf.map i.op (φ.app U₂ x)
theorem

map_eta

L68 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.map_eta
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Eta
variable {V W : Scheme.{u}} (γ : W ⟶ V) (N : V.Modules)
Lean source · statement
theorem map_eta {U₁ U₂ : V.Opens} (i : U₁ ⟶ U₂) (k : γ ⁻¹ᵁ U₁ ⟶ γ ⁻¹ᵁ U₂) (s : Γ(N, U₂)) :
    (pb γ N).presheaf.map k.op (eta γ N U₂ s) = eta γ N U₁ (N.presheaf.map i.op s)
theorem

map_map

L73 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.map_map
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Eta
variable {V W : Scheme.{u}} (γ : W ⟶ V) (N : V.Modules)
Lean source · statement
theorem map_map (M : W.Modules) {W₁ W₂ W₃ : W.Opens} (i : W₁ ⟶ W₂) (j : W₂ ⟶ W₃) (k : W₁ ⟶ W₃) (y :
  Γ(M, W₃)) :
    M.presheaf.map i.op (M.presheaf.map j.op y) = M.presheaf.map k.op y
theorem

map_self

L78 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.map_self
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Eta
variable {V W : Scheme.{u}} (γ : W ⟶ V) (N : V.Modules)
Lean source · statement
theorem map_self (M : W.Modules) {O : W.Opens} (i : O ⟶ O) (y : Γ(M, O)) : M.presheaf.map i.op y =
  y
theorem

res_rfl

L90 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.res_rfl
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Chart
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) (γ : W ⟶ V)
  [IsAffineHom γ]
  (N : V.Modules)
Lean source · statement
theorem res_rfl {X : Scheme.{u}} (O : X.Opens) (x : Γ(X, O)) : X.presheaf.map (homOfLE (le_refl
  O)).op x = x
theorem

appLE_rfl_apply

L95 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.appLE_rfl_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Chart
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) (γ : W ⟶ V)
  [IsAffineHom γ]
  (N : V.Modules)
omit [IsAffineHom γ] in
Lean source · statement
theorem appLE_rfl_apply (U : V.Opens) (a : Γ(V, U)) : γ.appLE U (γ ⁻¹ᵁ U) le_rfl a = γ.app U a
def

algVW

L100 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.algVW
Documentation

The algebra structure on inverse-image sections induced by the scheme morphism.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Chart
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) (γ : W ⟶ V)
  [IsAffineHom γ]
  (N : V.Modules)
Lean source · statement
def algVW (U : V.Opens) : Algebra Γ(V, U) Γ(W, γ ⁻¹ᵁ U)
def

kappa

L104 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.kappa
Documentation

The linear identification of the pushed-forward unit module with sections on the inverse image.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Chart
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) (γ : W ⟶ V)
  [IsAffineHom γ]
  (N : V.Modules)
Lean source · full declaration
def kappa (U : V.Opens) :
    letI := algVW γ U
    (OModulePresheaf.pushforwardUnit π γ).obj U ≃ₗ[Γ(V, U)] Γ(W, γ ⁻¹ᵁ U) :=
  letI := algVW γ U
  { toFun := fun x => (show Γ(W, γ ⁻¹ᵁ U) from x)
    invFun := fun y => (show (OModulePresheaf.pushforwardUnit π γ).obj U from y)
    map_add' := fun _ _ => rfl
    map_smul' := fun a x => by
      change γ.appLE U (γ ⁻¹ᵁ U) le_rfl a * (show Γ(W, γ ⁻¹ᵁ U) from x) = γ.app U a * (show Γ(W, γ
        ⁻¹ᵁ U) from x)
      rw [appLE_rfl_apply]
    left_inv := fun _ => rfl
    right_inv := fun _ => rfl }
theorem

kappa_apply

L119 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.kappa_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Chart
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) (γ : W ⟶ V)
  [IsAffineHom γ]
  (N : V.Modules)
omit [IsAffineHom γ] in
Lean source · full declaration
theorem kappa_apply (U : V.Opens) (x : Γ(W, γ ⁻¹ᵁ U)) :
    kappa π γ U (show (OModulePresheaf.pushforwardUnit π γ).obj U from x) = x := rfl
abbrev

Tobj

L130 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.Tobj
Documentation

The tensor product of pushed-forward unit sections with sections of the original module.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Chart
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) (γ : W ⟶ V)
  [IsAffineHom γ]
  (N : V.Modules)
variable (β : ∀ U : V.affineOpens,
    letI := algVW γ U.1
    Γ(W, γ ⁻¹ᵁ U.1) ⊗[Γ(V, U.1)] Γ(N, U.1) ≃ₗ[Γ(W, γ ⁻¹ᵁ U.1)] Γ(pb γ N, γ ⁻¹ᵁ U.1))
  (hβ : ∀ (U : V.affineOpens) (s : Γ(N, U.1)),
    letI := algVW γ U.1
    β U ((1 : Γ(W, γ ⁻¹ᵁ U.1)) ⊗ₜ[Γ(V, U.1)] s) = eta γ N U.1 s)
Lean source · statement
abbrev Tobj (U : V.Opens) : Type u
def

theta

L135 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.theta
Documentation

The additive comparison from the tensor product to pullback sections on an affine open.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Chart
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) (γ : W ⟶ V)
  [IsAffineHom γ]
  (N : V.Modules)
variable (β : ∀ U : V.affineOpens,
    letI := algVW γ U.1
    Γ(W, γ ⁻¹ᵁ U.1) ⊗[Γ(V, U.1)] Γ(N, U.1) ≃ₗ[Γ(W, γ ⁻¹ᵁ U.1)] Γ(pb γ N, γ ⁻¹ᵁ U.1))
  (hβ : ∀ (U : V.affineOpens) (s : Γ(N, U.1)),
    letI := algVW γ U.1
    β U ((1 : Γ(W, γ ⁻¹ᵁ U.1)) ⊗ₜ[Γ(V, U.1)] s) = eta γ N U.1 s)
Lean source · statement
def theta (U : V.affineOpens) : Tobj π γ N U.1 →+ Γ(pb γ N, γ ⁻¹ᵁ U.1)
theorem

theta_apply

L142 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.theta_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Chart
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) (γ : W ⟶ V)
  [IsAffineHom γ]
  (N : V.Modules)
variable (β : ∀ U : V.affineOpens,
    letI := algVW γ U.1
    Γ(W, γ ⁻¹ᵁ U.1) ⊗[Γ(V, U.1)] Γ(N, U.1) ≃ₗ[Γ(W, γ ⁻¹ᵁ U.1)] Γ(pb γ N, γ ⁻¹ᵁ U.1))
  (hβ : ∀ (U : V.affineOpens) (s : Γ(N, U.1)),
    letI := algVW γ U.1
    β U ((1 : Γ(W, γ ⁻¹ᵁ U.1)) ⊗ₜ[Γ(V, U.1)] s) = eta γ N U.1 s)
omit [IsAffineHom γ] in
Lean source · full declaration
theorem theta_apply (U : V.affineOpens) (x : Tobj π γ N U.1) :
    letI := algVW γ U.1
    theta π γ N β U x = β U (TensorProduct.congr (kappa π γ U.1) (LinearEquiv.refl Γ(V, U.1)
      ((OModulePresheaf.ofModules π N).obj U.1)) x) := rfl
theorem

theta_bijective

L148 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.theta_bijective
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Chart
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) (γ : W ⟶ V)
  [IsAffineHom γ]
  (N : V.Modules)
variable (β : ∀ U : V.affineOpens,
    letI := algVW γ U.1
    Γ(W, γ ⁻¹ᵁ U.1) ⊗[Γ(V, U.1)] Γ(N, U.1) ≃ₗ[Γ(W, γ ⁻¹ᵁ U.1)] Γ(pb γ N, γ ⁻¹ᵁ U.1))
  (hβ : ∀ (U : V.affineOpens) (s : Γ(N, U.1)),
    letI := algVW γ U.1
    β U ((1 : Γ(W, γ ⁻¹ᵁ U.1)) ⊗ₜ[Γ(V, U.1)] s) = eta γ N U.1 s)
omit [IsAffineHom γ] in
Lean source · statement
theorem theta_bijective (U : V.affineOpens) : Function.Bijective (theta π γ N β U)
theorem

theta_tmul

L155 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.theta_tmul
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Chart
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) (γ : W ⟶ V)
  [IsAffineHom γ]
  (N : V.Modules)
variable (β : ∀ U : V.affineOpens,
    letI := algVW γ U.1
    Γ(W, γ ⁻¹ᵁ U.1) ⊗[Γ(V, U.1)] Γ(N, U.1) ≃ₗ[Γ(W, γ ⁻¹ᵁ U.1)] Γ(pb γ N, γ ⁻¹ᵁ U.1))
  (hβ : ∀ (U : V.affineOpens) (s : Γ(N, U.1)),
    letI := algVW γ U.1
    β U ((1 : Γ(W, γ ⁻¹ᵁ U.1)) ⊗ₜ[Γ(V, U.1)] s) = eta γ N U.1 s)
include hβ in
omit [IsAffineHom γ] in
Lean source · full declaration
theorem theta_tmul (U : V.affineOpens) (b : Γ(W, γ ⁻¹ᵁ U.1)) (s : Γ(N, U.1)) :
    theta π γ N β U ((show (OModulePresheaf.pushforwardUnit π γ).obj U.1 from b) ⊗ₜ[Γ(V, U.1)]
      (show (OModulePresheaf.ofModules π N).obj U.1 from s)) = b • eta γ N U.1 s := by
  let := algVW γ U.1
  rw [theta_apply, TensorProduct.congr_tmul, kappa_apply, LinearEquiv.refl_apply]
  have h1 : β U (b ⊗ₜ[Γ(V, U.1)] s) = b • eta γ N U.1 s := by
    rw [show b ⊗ₜ[Γ(V, U.1)] s = b • ((1 : Γ(W, γ ⁻¹ᵁ U.1)) ⊗ₜ[Γ(V, U.1)] s) by
        rw [TensorProduct.smul_tmul', smul_eq_mul, mul_one],
      LinearEquiv.map_smul, hβ]
  exact h1
theorem

theta_smulA

L167 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.theta_smulA
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Chart
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) (γ : W ⟶ V)
  [IsAffineHom γ]
  (N : V.Modules)
variable (β : ∀ U : V.affineOpens,
    letI := algVW γ U.1
    Γ(W, γ ⁻¹ᵁ U.1) ⊗[Γ(V, U.1)] Γ(N, U.1) ≃ₗ[Γ(W, γ ⁻¹ᵁ U.1)] Γ(pb γ N, γ ⁻¹ᵁ U.1))
  (hβ : ∀ (U : V.affineOpens) (s : Γ(N, U.1)),
    letI := algVW γ U.1
    β U ((1 : Γ(W, γ ⁻¹ᵁ U.1)) ⊗ₜ[Γ(V, U.1)] s) = eta γ N U.1 s)
omit [IsAffineHom γ] in
Lean source · statement
theorem theta_smulA (U : V.affineOpens) (a : Γ(V, U.1)) (x : Tobj π γ N U.1) :
    theta π γ N β U (a • x) = γ.app U.1 a • theta π γ N β U x
theorem

theta_res

L179 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.theta_res
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Chart
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) (γ : W ⟶ V)
  [IsAffineHom γ]
  (N : V.Modules)
variable (β : ∀ U : V.affineOpens,
    letI := algVW γ U.1
    Γ(W, γ ⁻¹ᵁ U.1) ⊗[Γ(V, U.1)] Γ(N, U.1) ≃ₗ[Γ(W, γ ⁻¹ᵁ U.1)] Γ(pb γ N, γ ⁻¹ᵁ U.1))
  (hβ : ∀ (U : V.affineOpens) (s : Γ(N, U.1)),
    letI := algVW γ U.1
    β U ((1 : Γ(W, γ ⁻¹ᵁ U.1)) ⊗ₜ[Γ(V, U.1)] s) = eta γ N U.1 s)
include hβ in
omit [IsAffineHom γ] in
Lean source · statement
theorem theta_res {U U' : V.affineOpens} (h : U.1 ≤ U'.1) (x : Tobj π γ N U'.1) :
    theta π γ N β U (OModulePresheaf.tensorResₛₗ (OModulePresheaf.pushforwardUnit π γ)
      (OModulePresheaf.ofModules π N) h x) =
      (pb γ N).presheaf.map (homOfLE (Scheme.Hom.preimage_mono γ h)).op (theta π γ N β U' x)
theorem

res_app_algebraMap

L218 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.res_app_algebraMap
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Complex
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
  (γ : W ⟶ V) [IsAffineHom γ] (K : V.OrderedAffineCover) (N : V.Modules)
  (β : ∀ U : V.affineOpens,
    letI := algVW γ U.1
    Γ(W, γ ⁻¹ᵁ U.1) ⊗[Γ(V, U.1)] Γ(N, U.1) ≃ₗ[Γ(W, γ ⁻¹ᵁ U.1)] Γ(pb γ N, γ ⁻¹ᵁ U.1))
  (hβ : ∀ (U : V.affineOpens) (s : Γ(N, U.1)),
    letI := algVW γ U.1
    β U ((1 : Γ(W, γ ⁻¹ᵁ U.1)) ⊗ₜ[Γ(V, U.1)] s) = eta γ N U.1 s)
local notation "F₁" => OModulePresheaf.ofModules (γ ≫ π) (pb γ N)
local notation "F₂" => OModulePresheaf.twist (OModulePresheaf.pushforwardUnit π γ) N
omit [IsSeparated π] [IsAffineHom γ] in
Lean source · statement
theorem res_app_algebraMap (U : V.Opens) (O : W.Opens) (hO : O ≤ γ ⁻¹ᵁ U) (r : R) :
    (W.presheaf.map (homOfLE hO).op).hom (γ.app U ((Scheme.TwoAffineOpenCover.algebraOfHom π
      U).algebraMap r)) =
      (Scheme.TwoAffineOpenCover.algebraOfHom (γ ≫ π) O).algebraMap r
def

phiComp

L229 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.phiComp
Documentation

The linear comparison on one intersection in the original and pulled-back Čech covers.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Complex
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
  (γ : W ⟶ V) [IsAffineHom γ] (K : V.OrderedAffineCover) (N : V.Modules)
  (β : ∀ U : V.affineOpens,
    letI := algVW γ U.1
    Γ(W, γ ⁻¹ᵁ U.1) ⊗[Γ(V, U.1)] Γ(N, U.1) ≃ₗ[Γ(W, γ ⁻¹ᵁ U.1)] Γ(pb γ N, γ ⁻¹ᵁ U.1))
  (hβ : ∀ (U : V.affineOpens) (s : Γ(N, U.1)),
    letI := algVW γ U.1
    β U ((1 : Γ(W, γ ⁻¹ᵁ U.1)) ⊗ₜ[Γ(V, U.1)] s) = eta γ N U.1 s)
local notation "F₁" => OModulePresheaf.ofModules (γ ≫ π) (pb γ N)
local notation "F₂" => OModulePresheaf.twist (OModulePresheaf.pushforwardUnit π γ) N
Lean source · full declaration
def phiComp {n : ℕ} (s : K.Idx n) : (F₂).obj (K.inter s) →ₗ[R] (F₁).obj ((K.comap γ).inter s) where
  toFun x := (F₁).res (K.comap_inter_le γ s)
    (show (F₁).obj (γ ⁻¹ᵁ K.inter s) from theta π γ N β (K.affineInter π s) (show Tobj π γ N
      (K.inter s) from x))
  map_add' x y := by
    change (pb γ N).presheaf.map (homOfLE (K.comap_inter_le γ s)).op
        (theta π γ N β (K.affineInter π s) ((show Tobj π γ N (K.inter s) from x) + (show Tobj π γ N
          (K.inter s) from y))) =
      (pb γ N).presheaf.map (homOfLE (K.comap_inter_le γ s)).op (theta π γ N β (K.affineInter π s)
        (show Tobj π γ N (K.inter s) from x)) +
        (pb γ N).presheaf.map (homOfLE (K.comap_inter_le γ s)).op (theta π γ N β (K.affineInter π
          s) (show Tobj π γ N (K.inter s) from y))
    rw [map_add, map_add]
  map_smul' r x := by
    have h1 : theta π γ N β (K.affineInter π s) (show Tobj π γ N (K.inter s) from r • x) =
        γ.app (K.inter s) ((Scheme.TwoAffineOpenCover.algebraOfHom π (K.inter s)).algebraMap r) •
          theta π γ N β (K.affineInter π s) (show Tobj π γ N (K.inter s) from x) :=
      theta_smulA π γ N β (K.affineInter π s) _ _
    change (pb γ N).presheaf.map (homOfLE (K.comap_inter_le γ s)).op
        (theta π γ N β (K.affineInter π s) (show Tobj π γ N (K.inter s) from r • x)) =
      (Scheme.TwoAffineOpenCover.algebraOfHom (γ ≫ π) ((K.comap γ).inter s)).algebraMap r •
        (pb γ N).presheaf.map (homOfLE (K.comap_inter_le γ s)).op
          (theta π γ N β (K.affineInter π s) (show Tobj π γ N (K.inter s) from x))
    rw [h1, Scheme.Modules.map_smul, res_app_algebraMap]
theorem

phiComp_apply

L254 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.phiComp_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Complex
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
  (γ : W ⟶ V) [IsAffineHom γ] (K : V.OrderedAffineCover) (N : V.Modules)
  (β : ∀ U : V.affineOpens,
    letI := algVW γ U.1
    Γ(W, γ ⁻¹ᵁ U.1) ⊗[Γ(V, U.1)] Γ(N, U.1) ≃ₗ[Γ(W, γ ⁻¹ᵁ U.1)] Γ(pb γ N, γ ⁻¹ᵁ U.1))
  (hβ : ∀ (U : V.affineOpens) (s : Γ(N, U.1)),
    letI := algVW γ U.1
    β U ((1 : Γ(W, γ ⁻¹ᵁ U.1)) ⊗ₜ[Γ(V, U.1)] s) = eta γ N U.1 s)
local notation "F₁" => OModulePresheaf.ofModules (γ ≫ π) (pb γ N)
local notation "F₂" => OModulePresheaf.twist (OModulePresheaf.pushforwardUnit π γ) N
Lean source · full declaration
theorem phiComp_apply {n : ℕ} (s : K.Idx n) (x : (F₂).obj (K.inter s)) :
    phiComp π γ K N β s x =
      (F₁).res (K.comap_inter_le γ s) (show (F₁).obj (γ ⁻¹ᵁ K.inter s) from
        theta π γ N β (K.affineInter π s) (show Tobj π γ N (K.inter s) from x)) :=
  rfl
theorem

phiComp_bijective

L260 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.phiComp_bijective
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Complex
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
  (γ : W ⟶ V) [IsAffineHom γ] (K : V.OrderedAffineCover) (N : V.Modules)
  (β : ∀ U : V.affineOpens,
    letI := algVW γ U.1
    Γ(W, γ ⁻¹ᵁ U.1) ⊗[Γ(V, U.1)] Γ(N, U.1) ≃ₗ[Γ(W, γ ⁻¹ᵁ U.1)] Γ(pb γ N, γ ⁻¹ᵁ U.1))
  (hβ : ∀ (U : V.affineOpens) (s : Γ(N, U.1)),
    letI := algVW γ U.1
    β U ((1 : Γ(W, γ ⁻¹ᵁ U.1)) ⊗ₜ[Γ(V, U.1)] s) = eta γ N U.1 s)
local notation "F₁" => OModulePresheaf.ofModules (γ ≫ π) (pb γ N)
local notation "F₂" => OModulePresheaf.twist (OModulePresheaf.pushforwardUnit π γ) N
Lean source · statement
theorem phiComp_bijective {n : ℕ} (s : K.Idx n) : Function.Bijective (phiComp π γ K N β s)
def

phi

L273 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.phi
Documentation

The linear comparison of Čech cochains obtained from the component maps.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Complex
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
  (γ : W ⟶ V) [IsAffineHom γ] (K : V.OrderedAffineCover) (N : V.Modules)
  (β : ∀ U : V.affineOpens,
    letI := algVW γ U.1
    Γ(W, γ ⁻¹ᵁ U.1) ⊗[Γ(V, U.1)] Γ(N, U.1) ≃ₗ[Γ(W, γ ⁻¹ᵁ U.1)] Γ(pb γ N, γ ⁻¹ᵁ U.1))
  (hβ : ∀ (U : V.affineOpens) (s : Γ(N, U.1)),
    letI := algVW γ U.1
    β U ((1 : Γ(W, γ ⁻¹ᵁ U.1)) ⊗ₜ[Γ(V, U.1)] s) = eta γ N U.1 s)
local notation "F₁" => OModulePresheaf.ofModules (γ ≫ π) (pb γ N)
local notation "F₂" => OModulePresheaf.twist (OModulePresheaf.pushforwardUnit π γ) N
Lean source · statement
def phi (n : ℕ) : (F₂).cochain K n →ₗ[R] (F₁).cochain (K.comap γ) n
theorem

phi_apply

L279 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.phi_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Complex
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
  (γ : W ⟶ V) [IsAffineHom γ] (K : V.OrderedAffineCover) (N : V.Modules)
  (β : ∀ U : V.affineOpens,
    letI := algVW γ U.1
    Γ(W, γ ⁻¹ᵁ U.1) ⊗[Γ(V, U.1)] Γ(N, U.1) ≃ₗ[Γ(W, γ ⁻¹ᵁ U.1)] Γ(pb γ N, γ ⁻¹ᵁ U.1))
  (hβ : ∀ (U : V.affineOpens) (s : Γ(N, U.1)),
    letI := algVW γ U.1
    β U ((1 : Γ(W, γ ⁻¹ᵁ U.1)) ⊗ₜ[Γ(V, U.1)] s) = eta γ N U.1 s)
local notation "F₁" => OModulePresheaf.ofModules (γ ≫ π) (pb γ N)
local notation "F₂" => OModulePresheaf.twist (OModulePresheaf.pushforwardUnit π γ) N
Lean source · statement
theorem phi_apply (n : ℕ) (c : (F₂).cochain K n) (s : K.Idx n) :
    phi π γ K N β n c s = phiComp π γ K N β s (c s)
theorem

phi_bijective

L282 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.phi_bijective
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Complex
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
  (γ : W ⟶ V) [IsAffineHom γ] (K : V.OrderedAffineCover) (N : V.Modules)
  (β : ∀ U : V.affineOpens,
    letI := algVW γ U.1
    Γ(W, γ ⁻¹ᵁ U.1) ⊗[Γ(V, U.1)] Γ(N, U.1) ≃ₗ[Γ(W, γ ⁻¹ᵁ U.1)] Γ(pb γ N, γ ⁻¹ᵁ U.1))
  (hβ : ∀ (U : V.affineOpens) (s : Γ(N, U.1)),
    letI := algVW γ U.1
    β U ((1 : Γ(W, γ ⁻¹ᵁ U.1)) ⊗ₜ[Γ(V, U.1)] s) = eta γ N U.1 s)
local notation "F₁" => OModulePresheaf.ofModules (γ ≫ π) (pb γ N)
local notation "F₂" => OModulePresheaf.twist (OModulePresheaf.pushforwardUnit π γ) N
Lean source · statement
theorem phi_bijective (n : ℕ) : Function.Bijective (phi π γ K N β n)
theorem

phiComp_res

L293 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.phiComp_res
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Complex
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
  (γ : W ⟶ V) [IsAffineHom γ] (K : V.OrderedAffineCover) (N : V.Modules)
  (β : ∀ U : V.affineOpens,
    letI := algVW γ U.1
    Γ(W, γ ⁻¹ᵁ U.1) ⊗[Γ(V, U.1)] Γ(N, U.1) ≃ₗ[Γ(W, γ ⁻¹ᵁ U.1)] Γ(pb γ N, γ ⁻¹ᵁ U.1))
  (hβ : ∀ (U : V.affineOpens) (s : Γ(N, U.1)),
    letI := algVW γ U.1
    β U ((1 : Γ(W, γ ⁻¹ᵁ U.1)) ⊗ₜ[Γ(V, U.1)] s) = eta γ N U.1 s)
local notation "F₁" => OModulePresheaf.ofModules (γ ≫ π) (pb γ N)
local notation "F₂" => OModulePresheaf.twist (OModulePresheaf.pushforwardUnit π γ) N
include hβ in
Lean source · statement
theorem phiComp_res {n : ℕ} (t : K.Idx (n + 1)) (j : Fin (n + 2)) (y : (F₂).obj (K.inter (K.face t
  j))) :
    phiComp π γ K N β t ((F₂).res (K.inter_le_inter_face t j) y) =
      (F₁).res ((K.comap γ).inter_le_inter_face t j) (phiComp π γ K N β (K.face t j) y)
theorem

d_phi

L318 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.d_phi
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Complex
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
  (γ : W ⟶ V) [IsAffineHom γ] (K : V.OrderedAffineCover) (N : V.Modules)
  (β : ∀ U : V.affineOpens,
    letI := algVW γ U.1
    Γ(W, γ ⁻¹ᵁ U.1) ⊗[Γ(V, U.1)] Γ(N, U.1) ≃ₗ[Γ(W, γ ⁻¹ᵁ U.1)] Γ(pb γ N, γ ⁻¹ᵁ U.1))
  (hβ : ∀ (U : V.affineOpens) (s : Γ(N, U.1)),
    letI := algVW γ U.1
    β U ((1 : Γ(W, γ ⁻¹ᵁ U.1)) ⊗ₜ[Γ(V, U.1)] s) = eta γ N U.1 s)
local notation "F₁" => OModulePresheaf.ofModules (γ ≫ π) (pb γ N)
local notation "F₂" => OModulePresheaf.twist (OModulePresheaf.pushforwardUnit π γ) N
include hβ in
Lean source · statement
theorem d_phi (n : ℕ) (c : (F₂).cochain K n) :
    (F₁).d (K.comap γ) n (phi π γ K N β n c) = phi π γ K N β (n + 1) ((F₂).d K n c)
theorem

main_of_beta

L345 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.main_of_beta
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
section Complex
variable {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
  (γ : W ⟶ V) [IsAffineHom γ] (K : V.OrderedAffineCover) (N : V.Modules)
  (β : ∀ U : V.affineOpens,
    letI := algVW γ U.1
    Γ(W, γ ⁻¹ᵁ U.1) ⊗[Γ(V, U.1)] Γ(N, U.1) ≃ₗ[Γ(W, γ ⁻¹ᵁ U.1)] Γ(pb γ N, γ ⁻¹ᵁ U.1))
  (hβ : ∀ (U : V.affineOpens) (s : Γ(N, U.1)),
    letI := algVW γ U.1
    β U ((1 : Γ(W, γ ⁻¹ᵁ U.1)) ⊗ₜ[Γ(V, U.1)] s) = eta γ N U.1 s)
local notation "F₁" => OModulePresheaf.ofModules (γ ≫ π) (pb γ N)
local notation "F₂" => OModulePresheaf.twist (OModulePresheaf.pushforwardUnit π γ) N
include hβ in
Lean source · statement
theorem main_of_beta :
    Nonempty ((F₁).H0 (K.comap γ) ≃ₗ[R] (F₂).H0 K) ∧
      ∀ i : ℕ, Nonempty ((F₁).HSucc (K.comap γ) i ≃ₗ[R] (F₂).HSucc K i)
theorem

main

L365 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback.P2mAffCech.main
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace TensorProduct
namespace P2mAffCech
Lean source · statement
theorem main {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
    (γ : W ⟶ V) [IsAffineHom γ] (K : V.OrderedAffineCover) (N : V.Modules)
    (hN : ∀ x : V, ∃ (U : V.Opens), x ∈ U ∧
      Nonempty ((Scheme.Modules.pullback U.ι).obj N ≅ SheafOfModules.unit U.toScheme.ringCatSheaf))
        :
    Nonempty ((OModulePresheaf.ofModules (γ ≫ π) ((Scheme.Modules.pullback γ).obj N)).H0 (K.comap
      γ) ≃ₗ[R]
        ((OModulePresheaf.pushforwardUnit π γ).twist N).H0 K) ∧
      ∀ i : ℕ, Nonempty ((OModulePresheaf.ofModules (γ ≫ π) ((Scheme.Modules.pullback γ).obj
        N)).HSucc
          (K.comap γ) i ≃ₗ[R] ((OModulePresheaf.pushforwardUnit π γ).twist N).HSucc K i)
theorem

nonempty_cechEquiv_ofModules_pullback_comap_twist_pushforwardUnit

L405 ↗
AlgebraicGeometry.OModulePresheaf.nonempty_cechEquiv_ofModules_pullback_comap_twist_pushforwardUnit
Documentation

Cech cohomology of a pulled-back locally trivial module agrees with the twisted pushforward.

Source context 6 commands

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

section ProofImplementation
section PublicStatement
universe u
open
  _root_.CategoryTheory
  _root_.AlgebraicGeometry
  _root_.Opposite
  _root_.TopologicalSpace
  _root_.TensorProduct
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOfModulesPullback
namespace AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem nonempty_cechEquiv_ofModules_pullback_comap_twist_pushforwardUnit
    {R : Type u} [CommRing R] {V W : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsSeparated π]
    (γ : W ⟶ V) [IsAffineHom γ] (K : V.OrderedAffineCover) (N : V.Modules)
    (hN : ∀ x : V, ∃ (U : V.Opens), x ∈ U ∧
      Nonempty ((Scheme.Modules.pullback U.ι).obj N ≅ SheafOfModules.unit U.toScheme.ringCatSheaf))
        :
    Nonempty ((OModulePresheaf.ofModules (γ ≫ π) ((Scheme.Modules.pullback γ).obj N)).H0 (K.comap
      γ) ≃ₗ[R]
        ((OModulePresheaf.pushforwardUnit π γ).twist N).H0 K) ∧
      ∀ i : ℕ, Nonempty ((OModulePresheaf.ofModules (γ ≫ π) ((Scheme.Modules.pullback γ).obj
        N)).HSucc
          (K.comap γ) i ≃ₗ[R] ((OModulePresheaf.pushforwardUnit π γ).twist N).HSucc K i)

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