Module

DoubleComplex.lean

Nyll.SchemeTheory.Cohomology.Sheaves.DoubleComplex

27 declarations indexed from sourceView source ↗

Module documentation

Double complexes, their two spectral-sequence pages and bounded convergence data.

Imports2

Mathlib.LinearAlgebra.Quotient.Basic
Mathlib.Tactic.Ring.RingNF

Imported by12

structure

Bounded

L27 ↗

DoubleComplex.Bounded

Documentation

A first-quadrant double complex with commuting differentials and a common finite bound.

Source context 3 commands

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

noncomputable section
universe u
namespace DoubleComplex

Lean source · full declaration

structure Bounded (R : Type u) [CommRing R] where
  /-- The module carrier in horizontal degree `p` and vertical degree `q`. -/
  C : ℕ → ℕ → Type u
  /-- The additive commutative group structure on each component. -/
  [abGrp : ∀ p q, AddCommGroup (C p q)]
  /-- The coefficient-ring module structure on each component. -/
  [modR : ∀ p q, Module R (C p q)]
  /-- The differential raising horizontal degree by one. -/
  dH : ∀ p q, C p q →ₗ[R] C (p + 1) q
  /-- The differential raising vertical degree by one. -/
  dV : ∀ p q, C p q →ₗ[R] C p (q + 1)
  /-- Consecutive horizontal differentials compose to zero. -/
  dH_sq : ∀ p q, dH (p + 1) q ∘ₗ dH p q = 0
  /-- Consecutive vertical differentials compose to zero. -/
  dV_sq : ∀ p q, dV p (q + 1) ∘ₗ dV p q = 0
  /-- The horizontal and vertical differentials commute. -/
  dHV_comm : ∀ p q, dV (p + 1) q ∘ₗ dH p q = dH p (q + 1) ∘ₗ dV p q
  /-- The common upper bound for both component degrees. -/
  N : ℕ
  /-- Components with either degree at least `N` are subsingletons. -/
  hBound : ∀ p q, N ≤ p ∨ N ≤ q → Subsingleton (C p q)

abbrev

Diag

L56 ↗

DoubleComplex.Diag

Documentation

The pairs of nonnegative bidegrees with total degree n.

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section Tot
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

abbrev Diag (n : ℕ) : Type

abbrev

Tot

L59 ↗

DoubleComplex.Tot

Documentation

The product of the components on the diagonal of total degree n.

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section Tot
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

abbrev Tot (n : ℕ) : Type u

def

dTotH

L63 ↗

DoubleComplex.dTotH

Documentation

The horizontal contribution to the total differential at the target bidegree.

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section Tot
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def dTotH {n : ℕ} (i : Diag (n + 1)) :
    Tot D n →ₗ[R] D.C i.1.1 i.1.2

def

dTotV

L72 ↗

DoubleComplex.dTotV

Documentation

The vertical contribution to the total differential at the target bidegree.

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section Tot
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def dTotV {n : ℕ} (i : Diag (n + 1)) :
    Tot D n →ₗ[R] D.C i.1.1 i.1.2

def

dTot

L81 ↗

DoubleComplex.dTot

Documentation

The total differential, with vertical contribution signed by the horizontal degree.

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section Tot
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def dTot (n : ℕ) :
    Tot D n →ₗ[R] Tot D (n + 1)

def

HTotB

L87 ↗

DoubleComplex.HTotB

Documentation

The total boundaries as a submodule of total cocycles, with no boundaries in degree zero.

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section Tot
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · full declaration

def HTotB : (n : ℕ) → Submodule R (LinearMap.ker (dTot D n))
  | 0 => ⊥
  | n' + 1 => (LinearMap.range (dTot D n')).comap
      (LinearMap.ker (dTot D (n' + 1))).subtype

abbrev

HTot

L93 ↗

DoubleComplex.HTot

Documentation

The cohomology of the total complex in degree n.

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section Tot
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

abbrev HTot (n : ℕ) : Type u

theorem

dTot_apply_zero_succ

L102 ↗

DoubleComplex.dTot_apply_zero_succ

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section DTotGeneric
variable {R : Type u} [CommRing R] {D : Bounded R}

Lean source · full declaration

theorem dTot_apply_zero_succ {n q' : ℕ} (h : 0 + (q' + 1) = n + 1)
    (c : Tot D n) :
    dTot D n c ⟨(0, q' + 1), h⟩ = D.dV 0 q' (c ⟨(0, q'), by omega⟩) := by
  simp only [dTot, LinearMap.pi_apply,
    dTotH, dTotV,
    LinearMap.comp_apply, LinearMap.proj_apply, pow_zero, one_smul, zero_add]

theorem

dTot_apply_succ_zero

L109 ↗

DoubleComplex.dTot_apply_succ_zero

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section DTotGeneric
variable {R : Type u} [CommRing R] {D : Bounded R}

Lean source · full declaration

theorem dTot_apply_succ_zero {n p' : ℕ} (h : p' + 1 + 0 = n + 1)
    (c : Tot D n) :
    dTot D n c ⟨(p' + 1, 0), h⟩ = D.dH p' 0 (c ⟨(p', 0), by omega⟩) := by
  simp only [dTot, LinearMap.pi_apply,
    dTotH, dTotV,
    LinearMap.comp_apply, LinearMap.proj_apply, smul_zero, add_zero]

theorem

dTot_apply_succ_succ

L116 ↗

DoubleComplex.dTot_apply_succ_succ

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section DTotGeneric
variable {R : Type u} [CommRing R] {D : Bounded R}

Lean source · full declaration

theorem dTot_apply_succ_succ {n p' q' : ℕ} (h : p' + 1 + (q' + 1) = n + 1)
    (c : Tot D n) :
    dTot D n c ⟨(p' + 1, q' + 1), h⟩
      = D.dH p' (q' + 1) (c ⟨(p', q' + 1), by omega⟩)
        + ((-1 : ℤ) ^ (p' + 1)) • D.dV (p' + 1) q' (c ⟨(p' + 1, q'), by omega⟩) := by
  rfl

theorem

dTot_comp_dTot

L123 ↗

DoubleComplex.dTot_comp_dTot

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section DTotGeneric
variable {R : Type u} [CommRing R] {D : Bounded R}

Lean source · statement

theorem dTot_comp_dTot (D : Bounded R) (n : ℕ) :
    dTot D (n + 1) ∘ₗ dTot D n = 0

def

colB

L165 ↗

DoubleComplex.colB

Documentation

The vertical boundaries as a submodule of vertical cocycles in column p.

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section E2
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · full declaration

def colB (p : ℕ) : (q : ℕ) → Submodule R (LinearMap.ker (D.dV p q))
  | 0 => ⊥
  | q' + 1 => (LinearMap.range (D.dV p q')).comap (LinearMap.ker (D.dV p (q' + 1))).subtype

abbrev

colH

L170 ↗

DoubleComplex.colH

Documentation

The vertical cohomology of column p in degree q.

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section E2
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

abbrev colH (p q : ℕ) : Type u

def

colHdH

L174 ↗

DoubleComplex.colHdH

Documentation

The map on vertical cohomology induced by the horizontal differential.

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section E2
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def colHdH (p q : ℕ) :
    colH D p q →ₗ[R] colH D (p + 1) q

def

E₂IB

L189 ↗

DoubleComplex.E₂IB

Documentation

The horizontal boundaries within the cocycles of the induced column-cohomology differential.

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section E2
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · full declaration

def E₂IB :
    (p q : ℕ) → Submodule R (LinearMap.ker (colHdH D p q))
  | 0, _ => ⊥
  | p' + 1, q => (LinearMap.range (colHdH D p' q)).comap
      (LinearMap.ker (colHdH D (p' + 1) q)).subtype

abbrev

E₂I

L196 ↗

DoubleComplex.E₂I

Documentation

The first second-page term, computed as horizontal cohomology of vertical cohomology.

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section E2
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

abbrev E₂I (p q : ℕ) : Type u

def

transpose

L202 ↗

DoubleComplex.transpose

Documentation

The bounded double complex obtained by exchanging the two component degrees and differentials.

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section E2
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · full declaration

def transpose : Bounded R where
  C a b := D.C b a
  dH a b := D.dV b a
  dV a b := D.dH b a
  dH_sq a b := D.dV_sq b a
  dV_sq a b := D.dH_sq b a
  dHV_comm a b := (D.dHV_comm b a).symm
  N := D.N
  hBound a b h := D.hBound b a h.symm

abbrev

E₂II

L213 ↗

DoubleComplex.E₂II

Documentation

The second second-page term, computed from the transposed double complex.

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section E2
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

abbrev E₂II (p q : ℕ) : Type u

instance

(anonymous instance)

L216 ↗

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section E2
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

instance (p q : ℕ) : AddCommGroup (E₂I D p q)

instance

(anonymous instance)

L218 ↗

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section E2
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

instance (p q : ℕ) : Module R (E₂I D p q)

instance

(anonymous instance)

L220 ↗

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section E2
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

instance (p q : ℕ) : AddCommGroup (E₂II D p q)

instance

(anonymous instance)

L222 ↗

Source context 6 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR
section E2
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

instance (p q : ℕ) : Module R (E₂II D p q)

structure

SubQuot

L228 ↗

DoubleComplex.SubQuot

Documentation

A pair of nested submodules presenting a subquotient of a module.

Source context 4 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR

Lean source · full declaration

structure SubQuot (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] where
  /-- The submodule whose elements represent the subquotient. -/
  Z : Submodule R M
  /-- The submodule of elements identified with zero in the subquotient. -/
  B : Submodule R M
  /-- The denominator submodule is contained in the numerator submodule. -/
  hBZ : B ≤ Z

abbrev

carrier

L237 ↗

DoubleComplex.SubQuot.carrier

Documentation

The quotient of the numerator by the denominator pulled back along its inclusion.

Source context 4 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR

Lean source · statement

abbrev SubQuot.carrier {R : Type u} [CommRing R] {M : Type u} [AddCommGroup M] [Module R M]
    (s : SubQuot R M) : Type u

structure

Convergence

L241 ↗

DoubleComplex.Convergence

Documentation

Subquotient and filtration data relating a second page to the graded modules H.

Source context 4 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR

Lean source · full declaration

structure Convergence (R : Type u) [CommRing R]
    (E₂ : ℕ → ℕ → Type u) [∀ p q, AddCommGroup (E₂ p q)] [∀ p q, Module R (E₂ p q)]
    (H : ℕ → Type u) [∀ n, AddCommGroup (H n)] [∀ n, Module R (H n)] (N : ℕ) where
  /-- The limiting subquotient selected from each second-page term. -/
  Einf : ∀ p q, SubQuot R (E₂ p q)
  /-- Every element of a zeroth-row term belongs to the limiting numerator. -/
  hZ0 : ∀ p, (Einf p 0).Z = ⊤
  /-- The finite filtration of each zeroth-row term leading to its limiting denominator. -/
  Bfilt : ∀ p, Fin (N + 1) → Submodule R (E₂ p 0)
  /-- The denominator filtrations are increasing. -/
  Bfilt_mono : ∀ p, Monotone (Bfilt p)
  /-- Each denominator filtration starts at the zero submodule. -/
  Bfilt_bot : ∀ p, Bfilt p 0 = ⊥
  /-- Each denominator filtration ends at the limiting denominator. -/
  Bfilt_top : ∀ p, Bfilt p (Fin.last N) = (Einf p 0).B
  /-- Each successive denominator-filtration quotient is a subquotient of a positive-row term. -/
  Bfilt_gr : ∀ p (i : Fin N), ∃ p' q', 1 ≤ q' ∧ ∃ (s : SubQuot R (E₂ p' q')),
    Nonempty (((Bfilt p i.succ) ⧸ (Bfilt p i.castSucc).comap (Bfilt p i.succ).subtype)
      ≃ₗ[R] s.carrier)
  /-- The finite filtration on each module `H n`. -/
  Hfilt : ∀ n, Fin (N + 2) → Submodule R (H n)
  /-- The filtrations on `H` are increasing. -/
  Hfilt_mono : ∀ n, Monotone (Hfilt n)
  /-- Each filtration on `H` starts at the zero submodule. -/
  Hfilt_bot : ∀ n, Hfilt n 0 = ⊥
  /-- Each filtration on `H` ends at the whole module. -/
  Hfilt_top : ∀ n, Hfilt n (Fin.last (N + 1)) = ⊤
  /-- The designated quotient of the filtration on `H p` is the limiting zeroth-row subquotient. -/
  Hfilt_gr : ∀ (p : Fin (N + 1)),
    Nonempty (((Hfilt (↑p) p.succ) ⧸ (Hfilt (↑p) p.castSucc).comap (Hfilt (↑p) p.succ).subtype)
      ≃ₗ[R] (Einf p 0).carrier)

def

BoundedSpectralSequence

L274 ↗

DoubleComplex.BoundedSpectralSequence

Documentation

The assertion that every bounded double complex admits the specified convergence data.

Source context 4 commands

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

noncomputable section
universe u
namespace DoubleComplex
attribute [instance] Bounded.abGrp Bounded.modR

Lean source · statement

def BoundedSpectralSequence : Prop

Module documentation

Declarations