NYLL
Module

OModulePresheaf_AffSES_exists_connectingHom.lean

Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_AffSES_exists_connectingHom
14 declarations indexed from sourceView source ↗

Module documentation

Connecting homomorphisms for affine short exact sequences

Imports4
Imported by4

Declarations

theorem

mem_comap_range_iff

L47 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom.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.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom
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

L53 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom.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.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom
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

L58 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom.AlgebraicGeometry.OModulePresheaf.LES.cochain_ses
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom
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

snake_data

L82 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom.AlgebraicGeometry.OModulePresheaf.LES.snake_data
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom
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 snake_data (i : ℕ) (z : LinearMap.ker (F₃.d K i)) :
    ∃ (k₀ : LinearMap.ker (F₁.d K (i + 1))) (f₀ : F₂.cochain K i),
      πC i f₀ = z.1 ∧ ιC (i + 1) k₀.1 = F₂.d K i f₀ ∧
        ∀ f, πC i f = z.1 → ∃ h, ιC (i + 1) k₀.1 = F₂.d K i f + ιC (i + 1) (F₁.d K i h)
def

delta0

L107 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom.AlgebraicGeometry.OModulePresheaf.LES.delta0
Documentation

The connecting map from cocycles to the next Čech cohomology group.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom
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
def delta0 (i : ℕ) : LinearMap.ker (F₃.d K i) →ₗ[R] F₁.HSucc K i
theorem

delta0_spec

L129 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom.AlgebraicGeometry.OModulePresheaf.LES.delta0_spec
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom
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 delta0_spec (i : ℕ) (z : LinearMap.ker (F₃.d K i)) :
    ∃ (k₀ : LinearMap.ker (F₁.d K (i + 1))) (f₀ : F₂.cochain K i),
      delta0 K S i z = Submodule.Quotient.mk k₀ ∧ πC i f₀ = z.1 ∧ ιC (i + 1) k₀.1 = F₂.d K i f₀ ∧
        ∀ f, πC i f = z.1 → ∃ h, ιC (i + 1) k₀.1 = F₂.d K i f + ιC (i + 1) (F₁.d K i h)
theorem

delta0_eq_zero_of_mem_range

L137 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom.AlgebraicGeometry.OModulePresheaf.LES.delta0_eq_zero_of_mem_range
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom
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 delta0_eq_zero_of_mem_range (j : ℕ) (z : LinearMap.ker (F₃.d K (j + 1)))
    (hz : ∃ w, F₃.d K j w = z.1) : delta0 K S (j + 1) z = 0
def

delta

L151 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom.AlgebraicGeometry.OModulePresheaf.LES.delta
Documentation

The connecting homomorphism induced on positive-degree Čech cohomology.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom
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
def delta (i : ℕ) : F₃.HSucc K i →ₗ[R] F₁.HSucc K (i + 1)
theorem

delta_mk

L156 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom.AlgebraicGeometry.OModulePresheaf.LES.delta_mk
Documentation

The connecting map on a quotient representative is the cocycle connecting map.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom
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 delta_mk (i : ℕ) (z : LinearMap.ker (F₃.d K (i + 1))) :
    delta K S i (Submodule.Quotient.mk z) = delta0 K S (i + 1) z
theorem

ker_delta0_le_range

L159 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom.AlgebraicGeometry.OModulePresheaf.LES.ker_delta0_le_range
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom
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 ker_delta0_le_range (i : ℕ) :
    LinearMap.ker (delta0 K S i) ≤ LinearMap.range (S.proj.kerMap K i)
theorem

ker_delta_le_range

L174 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom.AlgebraicGeometry.OModulePresheaf.LES.ker_delta_le_range
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom
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 ker_delta_le_range (i : ℕ) :
    LinearMap.ker (delta K S i) ≤ LinearMap.range (S.proj.HSuccMap K i)
theorem

ker_HSuccMap_zero_le_range_delta0

L183 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom.AlgebraicGeometry.OModulePresheaf.LES.ker_HSuccMap_zero_le_range_delta0
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom
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 ker_HSuccMap_zero_le_range_delta0 :
    LinearMap.ker (S.inc.HSuccMap K 0) ≤ LinearMap.range (delta0 K S 0)
theorem

ker_HSuccMap_succ_le_range_delta

L204 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom.AlgebraicGeometry.OModulePresheaf.LES.ker_HSuccMap_succ_le_range_delta
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom
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 ker_HSuccMap_succ_le_range_delta (i : ℕ) :
    LinearMap.ker (S.inc.HSuccMap K (i + 1)) ≤ LinearMap.range (delta K S i)
theorem

exists_connectingHom

L232 ↗
AlgebraicGeometry.OModulePresheaf.AffSES.exists_connectingHom
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_AffSES_exists_connectingHom
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
universe u
open _root_.AlgebraicGeometry AlgebraicGeometry _root_.AlgebraicGeometry.OModulePresheaf
  AlgebraicGeometry.OModulePresheaf in
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.AffSES.exists_connectingHom {R : Type u}
    [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} [IsSeparated π]
    {F₁ F₂ F₃ : OModulePresheaf π} (S : OModulePresheaf.AffSES F₁ F₂ F₃) (K :
      V.OrderedAffineCover) :
    ∃ (δ₀ : F₃.H0 K →ₗ[R] F₁.HSucc K 0) (δ : ∀ i : ℕ, F₃.HSucc K i →ₗ[R] F₁.HSucc K (i + 1)),
      LinearMap.ker δ₀ ≤ LinearMap.range (S.proj.H0Map K) ∧ (∀ i, LinearMap.ker (δ i) ≤
      LinearMap.range (S.proj.HSuccMap K i)) ∧ LinearMap.ker (S.inc.HSuccMap K 0) ≤
      LinearMap.range δ₀ ∧ (∀ i, LinearMap.ker (S.inc.HSuccMap K (i + 1)) ≤ LinearMap.range (δ i))

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