Module

OModulePresheaf_cechFinite_of_affSES_left.lean

Nyll.SchemeTheory.Cohomology.Cech.OModulePresheaf_cechFinite_of_affSES_left

4 declarations indexed from sourceView source ↗

Module documentation

Cech finiteness of the left term of an affine short exact sequence from the other two terms.

Imports6

Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.RingTheory.Noetherian.Basic
Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheafHom
Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_d_comp_d
Nyll.SchemeTheory.RingTheory.Module_Finite_of_ker_le_range_of_isNoetherianRing
Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_AffSES_exists_connectingHom

Imported by3

theorem

mem_comap_range_iff

L48 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_affSES_left.AlgebraicGeometry.OModulePresheaf.LES.mem_comap_range_iff

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_affSES_left
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace LES
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} [IsSeparated π]
variable (K : V.OrderedAffineCover) {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃)
local notation "ιC" => AffHom.cochainMap (π := π) K S.inc
local notation "πC" => AffHom.cochainMap (π := π) K S.proj
omit [IsSeparated π] in

Lean source · statement

theorem mem_comap_range_iff {F : OModulePresheaf π} {i : ℕ} (x : LinearMap.ker (F.d K (i + 1))) :
    x ∈ (LinearMap.range (F.d K i)).comap (LinearMap.ker (F.d K (i + 1))).subtype
      ↔ ∃ c, F.d K i c = x.1

theorem

d_d_apply

L54 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_affSES_left.AlgebraicGeometry.OModulePresheaf.LES.d_d_apply

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_affSES_left
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace LES
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} [IsSeparated π]
variable (K : V.OrderedAffineCover) {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃)
local notation "ιC" => AffHom.cochainMap (π := π) K S.inc
local notation "πC" => AffHom.cochainMap (π := π) K S.proj
omit [IsSeparated π] in

Lean source · statement

theorem d_d_apply (F : OModulePresheaf π) (i : ℕ) (c : F.cochain K i) : F.d K (i + 1) (F.d K i c)
    = 0

theorem

cochain_ses

L59 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_affSES_left.AlgebraicGeometry.OModulePresheaf.LES.cochain_ses

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_affSES_left
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace LES
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
universe u
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} [IsSeparated π]
variable (K : V.OrderedAffineCover) {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃)
local notation "ιC" => AffHom.cochainMap (π := π) K S.inc
local notation "πC" => AffHom.cochainMap (π := π) K S.proj

Lean source · statement

theorem cochain_ses (i : ℕ) :
    Function.Injective (ιC i) ∧ Function.Surjective (πC i) ∧ LinearMap.range (ιC i) =
      LinearMap.ker (πC i)

theorem

cechFinite_of_affSES_left

L90 ↗

AlgebraicGeometry.OModulePresheaf.cechFinite_of_affSES_left

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_affSES_left
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
universe u
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs in
open _root_.AlgebraicGeometry OModulePresheaf_cechFinite_of_affSES_left.AlgebraicGeometry
  _root_.AlgebraicGeometry.OModulePresheaf
  OModulePresheaf_cechFinite_of_affSES_left.AlgebraicGeometry.OModulePresheaf in

Lean source · statement

theorem _root_.AlgebraicGeometry.OModulePresheaf.cechFinite_of_affSES_left {R : Type u} [CommRing
    R] [IsNoetherianRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
    [IsSeparated π] {F₁ F₂ F₃ : OModulePresheaf π} (S : OModulePresheaf.AffSES F₁ F₂ F₃) (K :
      V.OrderedAffineCover)
    (h₂ : F₂.CechFinite K) (h₃ : F₃.CechFinite K) : F₁.CechFinite K

Module documentation

Declarations

mem_comap_range_iff

d_d_apply

cochain_ses

cechFinite_of_affSES_left