Module

DoubleComplex_boundedSpectralSequence.lean

Nyll.SchemeTheory.HomologicalAlgebra.DoubleComplex_boundedSpectralSequence

71 declarations indexed from sourceView source ↗

Module documentation

The bounded spectral sequence and its filtration for a double complex.

Imports2

Mathlib.LinearAlgebra.Isomorphisms
Nyll.SchemeTheory.Cohomology.Sheaves.DoubleComplex

Imported by2

def

leOfSubsingleton

L34 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.leOfSubsingleton

Documentation

The linear equivalence between two subsingleton modules.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex

Lean source · full declaration

def leOfSubsingleton (R : Type u) [CommRing R]
    (M N : Type u) [AddCommGroup M] [Module R M] [Subsingleton M]
    [AddCommGroup N] [Module R N] [Subsingleton N] : M ≃ₗ[R] N where
  toFun _ := 0
  invFun _ := 0
  map_add' _ _ := Subsingleton.elim _ _
  map_smul' _ _ := Subsingleton.elim _ _
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

def

FilTot

L49 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.FilTot

Documentation

The submodule of total-degree n terms whose components in columns below p vanish.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section FilTot
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def FilTot (p n : ℕ) : Submodule R (Tot D n)

theorem

mem_FilTot

L54 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.mem_FilTot

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section FilTot
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem mem_FilTot {p n : ℕ} (c : Tot D n) :
    c ∈ FilTot D p n ↔ ∀ i : Diag n, i.1.1 < p → c i = 0

theorem

FilTot_antitone

L58 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.FilTot_antitone

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section FilTot
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · full declaration

theorem FilTot_antitone (n : ℕ) : Antitone (fun p => FilTot D p n) := by
  intro p p' hpp'
  simp only [IsConcreteLE.le_iff, mem_FilTot]
  intro c hc i hi
  exact hc i (lt_of_lt_of_le hi hpp')

theorem

FilTot_zero

L64 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.FilTot_zero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section FilTot
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem FilTot_zero (n : ℕ) : FilTot D 0 n = ⊤

theorem

FilTot_top

L67 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.FilTot_top

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section FilTot
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem FilTot_top (n : ℕ) : FilTot D (n + 1) n = ⊥

theorem

FilTot_N_subsingleton

L73 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.FilTot_N_subsingleton

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section FilTot
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem FilTot_N_subsingleton (n : ℕ) (c : Tot D n)
    (hc : c ∈ FilTot D D.N n) (i : Diag n) : c i = 0

theorem

FilTot_N

L79 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.FilTot_N

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section FilTot
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem FilTot_N (n : ℕ) : FilTot D D.N n = ⊥

theorem

dTot_FilTot_le

L83 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.dTot_FilTot_le

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section FilTot
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem dTot_FilTot_le (p n : ℕ) :
    (FilTot D p n).map (dTot D n)
      ≤ FilTot D p (n + 1)

abbrev

edgeSlot

L110 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.edgeSlot

Documentation

The diagonal position in column p and row zero.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Edge
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

abbrev edgeSlot (p : ℕ) : Diag p

theorem

ne_edgeSlot_of_lt

L112 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.ne_edgeSlot_of_lt

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Edge
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem ne_edgeSlot_of_lt {p : ℕ} (i : Diag p)
    (hi : i.1.1 < p) : i ≠ edgeSlot p

theorem

Diag_col_lt_of_ne

L116 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.Diag_col_lt_of_ne

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Edge
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem Diag_col_lt_of_ne {p : ℕ} (i : Diag p)
    (hi : i ≠ edgeSlot p) : i.1.1 < p

abbrev

edgeSingle

L126 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.edgeSingle

Documentation

The total-degree p term supported only at the row-zero edge position.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Edge
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

abbrev edgeSingle (p : ℕ) (x : D.C p 0) : Tot D p

theorem

edgeSingle_mem_FilTot

L130 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.edgeSingle_mem_FilTot

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Edge
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem edgeSingle_mem_FilTot (p : ℕ) (x : D.C p 0) :
    edgeSingle D p x ∈ FilTot D p p

def

edgeProj

L138 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.edgeProj

Documentation

The linear equivalence identifying the edge-filtered total-degree p terms with the module in column p and row zero.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Edge
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · full declaration

def edgeProj (p : ℕ) : ↥(FilTot D p p) ≃ₗ[R] D.C p 0 where
  toFun c := c.1 (edgeSlot p)
  invFun x := ⟨edgeSingle D p x, edgeSingle_mem_FilTot D p x⟩
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  left_inv c := by
    refine Subtype.ext (funext fun i => ?_)
    change edgeSingle D p (c.1 (edgeSlot p)) i = c.1 i
    rcases eq_or_ne i (edgeSlot p) with rfl | hi
    · exact Pi.single_eq_same _ _
    · rw [show edgeSingle D p (c.1 (edgeSlot p)) i = 0 from
          Pi.single_eq_of_ne (M := fun j : Diag p => D.C j.1.1 j.1.2) hi _,
        (mem_FilTot D _).mp c.2 i (Diag_col_lt_of_ne i hi)]
  right_inv x := Pi.single_eq_same _ _

theorem

neg_one_pow_zsmul_eq_zero

L153 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.neg_one_pow_zsmul_eq_zero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Edge
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem neg_one_pow_zsmul_eq_zero {M : Type*} [AddCommGroup M] (n : ℕ) (x : M) :
    ((-1 : ℤ) ^ n) • x = 0 ↔ x = 0

theorem

edge_ker_fwd

L159 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.edge_ker_fwd

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Edge
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem edge_ker_fwd (p : ℕ) (c : Tot D p)
    (hcF : c ∈ FilTot D p p)
    (hker : c ∈ LinearMap.ker (dTot D p)) :
    c (edgeSlot p) ∈ LinearMap.ker (D.dH p 0) ⊓ LinearMap.ker (D.dV p 0)

theorem

edge_ker_rev

L177 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.edge_ker_rev

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Edge
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem edge_ker_rev (p : ℕ) (x : D.C p 0)
    (hH : x ∈ LinearMap.ker (D.dH p 0)) (hV : x ∈ LinearMap.ker (D.dV p 0)) :
    edgeSingle D p x ∈ LinearMap.ker (dTot D p)

abbrev

KerHV

L216 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.KerHV

Documentation

The simultaneous kernel of the horizontal and vertical differentials at the row-zero edge.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section KerHV
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

abbrev KerHV (p : ℕ) : Submodule R (D.C p 0)

def

FilH

L220 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.FilH

Documentation

The image in total cohomology of total cycles lying in the column filtration.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section KerHV
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def FilH (p n : ℕ) : Submodule R (HTot D n)

theorem

FilH_zero

L224 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.FilH_zero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section KerHV
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem FilH_zero (n : ℕ) : FilH D 0 n = ⊤

theorem

FilH_top

L228 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.FilH_top

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section KerHV
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem FilH_top (n : ℕ) : FilH D (n + 1) n = ⊥

def

colH0_equiv

L234 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.colH0_equiv

Documentation

The equivalence identifying degree-zero column cohomology with the kernel of the vertical differential.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section KerHV
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def colH0_equiv (p : ℕ) :
    colH D p 0 ≃ₗ[R] ↥(LinearMap.ker (D.dV p 0))

def

toColH

L239 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.toColH

Documentation

The degree-zero column-cohomology class of a simultaneous horizontal and vertical cycle.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section KerHV
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def toColH (p : ℕ) :
    ↥(KerHV D p) →ₗ[R] colH D p 0

theorem

KerHV_le_ker_colHdH

L244 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.KerHV_le_ker_colHdH

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section KerHV
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem KerHV_le_ker_colHdH (p : ℕ) (x : ↥(KerHV D p)) :
    toColH D p x ∈ LinearMap.ker (colHdH D p 0)

def

toE₂

L252 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.toE₂

Documentation

The row-zero second-page class of a simultaneous horizontal and vertical cycle.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section KerHV
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def toE₂ (p : ℕ) :
    ↥(KerHV D p) →ₗ[R] E₂I D p 0

theorem

toE₂_surjective

L258 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.toE₂_surjective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section KerHV
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem toE₂_surjective (p : ℕ) :
    Function.Surjective (toE₂ D p)

def

zigTarget

L282 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.zigTarget

Documentation

The submodule of total-degree p terms whose total differential is supported at the next row-zero edge.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def zigTarget (p : ℕ) : Submodule R (Tot D p)

def

A

L286 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.A

Documentation

The submodule of zig-zag inputs whose components below column p+1-r vanish.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def A (r p : ℕ) : Submodule R (Tot D p)

theorem

A_mono

L289 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.A_mono

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · full declaration

theorem A_mono (p : ℕ) : Monotone fun r => A D r p := by
  intro r r' hrr'
  exact inf_le_inf_right _ (FilTot_antitone D p (by omega))

theorem

A_zero

L293 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.A_zero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem A_zero (p : ℕ) : A D 0 p = ⊥

theorem

A_full

L296 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.A_full

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem A_full (p : ℕ) : A D (p + 1) p = zigTarget D p

def

zigOut

L300 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.zigOut

Documentation

The row-zero edge component of the total differential.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def zigOut (p : ℕ) : Tot D p →ₗ[R] D.C (p + 1) 0

theorem

zigOut_apply

L306 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.zigOut_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem zigOut_apply (p : ℕ) (b : Tot D p) :
    zigOut D p b = D.dH p 0 (b (edgeSlot p))

theorem

dTot_eq_edgeSingle_zigOut

L311 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.dTot_eq_edgeSingle_zigOut

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem dTot_eq_edgeSingle_zigOut (p : ℕ) (b : Tot D p)
    (hb : b ∈ zigTarget D p) :
    dTot D p b
      = edgeSingle D (p + 1) (zigOut D p b)

theorem

zigOut_mem_KerHV

L318 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.zigOut_mem_KerHV

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem zigOut_mem_KerHV (p : ℕ) (b : Tot D p)
    (hb : b ∈ zigTarget D p) :
    zigOut D p b ∈ KerHV D (p + 1)

def

B

L328 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.B

Documentation

The image of the filtered zig-zag submodule A in the next row-zero second-page term.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def B (r p : ℕ) : Submodule R (E₂I D (p + 1) 0)

theorem

B_mono

L336 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.B_mono

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · full declaration

theorem B_mono (p : ℕ) : Monotone fun r => B D r p := fun _ _ h =>
  Submodule.map_mono (Submodule.comap_mono (A_mono D p h))

theorem

B_zero

L339 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.B_zero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem B_zero (p : ℕ) : B D 0 p = ⊥

theorem

A_inter_FilTot

L343 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.A_inter_FilTot

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem A_inter_FilTot (r p : ℕ) (hr : 1 ≤ r) :
    A D r p ⊓ FilTot D (p + 2 - r) p = A D (r - 1) p

theorem

θ_mem_ker_dV

L350 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.θ_mem_ker_dV

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem θ_mem_ker_dV (p a q : ℕ) (haq : a + q = p) (ha : a ≤ p - q)
    (b : Tot D p) (hbF : b ∈ FilTot D a p)
    (hbT : b ∈ zigTarget D p) :
    D.dV a q (b ⟨(a, q), haq⟩) = 0

theorem

toE₂_dH_kerV

L370 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.toE₂_dH_kerV

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · full declaration

theorem toE₂_dH_kerV (p : ℕ) (y : D.C p 0) (hy : y ∈ LinearMap.ker (D.dV p 0)) :
    toE₂ D (p + 1)
      ⟨D.dH p 0 y, LinearMap.mem_ker.mpr (LinearMap.congr_fun (D.dH_sq p 0) y),
        LinearMap.mem_ker.mpr (by
          rw [← LinearMap.comp_apply, D.dHV_comm, LinearMap.comp_apply,
            LinearMap.mem_ker.mp hy, map_zero])⟩ = 0 := by
  refine (Submodule.Quotient.mk_eq_zero _).mpr ?_
  refine Submodule.mem_comap.mpr ⟨(colB D p 0).mkQ ⟨y, hy⟩, ?_⟩
  simp only [Submodule.coe_subtype, LinearMap.codRestrict_apply]
  exact congrArg (colB D (p + 1) 0).mkQ (Subtype.ext rfl)

theorem

B_one

L381 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.B_one

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem B_one (p : ℕ) : B D 1 p = ⊥

theorem

zigzag_dH

L393 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.zigzag_dH

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · full declaration

theorem zigzag_dH (p a q' : ℕ) (haq : a + (q' + 1) = p)
    (b : Tot D p) (hbT : b ∈ zigTarget D p) :
    D.dH a (q' + 1) (b ⟨(a, q' + 1), haq⟩)
      = ((-1 : ℤ) ^ a) • D.dV (a + 1) q' (b ⟨(a + 1, q'), by omega⟩) := by
  have hT := (mem_FilTot D _).mp (Submodule.mem_comap.mp hbT)
  have hlt1 : (a + 1 : ℕ) < p + 1 := by omega
  have h0 : dTot D p b ⟨(a + 1, q' + 1), by omega⟩ = 0 :=
    hT ⟨(a + 1, q' + 1), by omega⟩ hlt1
  rw [dTot_apply_succ_succ] at h0
  have hres := eq_neg_of_add_eq_zero_left h0
  rwa [← neg_one_smul ℤ ((_ : ℤ)^_ • _), smul_smul,
    show (-1 : ℤ) * (-1)^(a+1) = (-1)^a from by ring] at hres

theorem

θ_dH_mem_colB

L406 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.θ_dH_mem_colB

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · full declaration

theorem θ_dH_mem_colB (p a q' : ℕ) (haq : a + (q' + 1) = p)
    (b : Tot D p) (hbT : b ∈ zigTarget D p)
    (hbV : D.dV a (q' + 1) (b ⟨(a, q' + 1), haq⟩) = 0) :
    (⟨D.dH a (q' + 1) (b ⟨(a, q' + 1), haq⟩), LinearMap.mem_ker.mpr (by
        rw [← LinearMap.comp_apply, D.dHV_comm, LinearMap.comp_apply, hbV, map_zero])⟩
      : ↥(LinearMap.ker (D.dV (a + 1) (q' + 1))))
        ∈ colB D (a + 1) (q' + 1) := by
  refine Submodule.mem_comap.mpr ?_
  simp only [Submodule.coe_subtype, LinearMap.mem_range]
  exact ⟨((-1 : ℤ) ^ a) • b ⟨(a + 1, q'), by omega⟩, by
    rw [map_zsmul, ← zigzag_dH D p a q' haq b hbT]⟩

abbrev

η

L420 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.η

Documentation

The row-zero second-page class of the edge component of the total differential on a zig-zag input.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

abbrev η (p : ℕ) :
    ↥(zigTarget D p) →ₗ[R] E₂I D (p + 1) 0

abbrev

totSingle

L428 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.totSingle

Documentation

The total-complex term supported at the specified diagonal position.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

abbrev totSingle {n : ℕ} (i : Diag n)
    (v : D.C i.1.1 i.1.2) : Tot D n

theorem

totSingle_mem_FilTot

L432 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.totSingle_mem_FilTot

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem totSingle_mem_FilTot {n : ℕ} (i : Diag n)
    (v : D.C i.1.1 i.1.2) : totSingle D i v ∈ FilTot D i.1.1 n

theorem

dTot_totSingle_col_same

L438 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.dTot_totSingle_col_same

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · full declaration

theorem dTot_totSingle_col_same {n a q : ℕ} (haq : a + q = n) (v : D.C a q) :
    dTot D n (totSingle D ⟨(a, q), haq⟩ v) ⟨(a, q + 1), by omega⟩
      = ((-1 : ℤ) ^ a) • D.dV a q v := by
  match a, haq with
  | 0, haq =>
    rw [dTot_apply_zero_succ, pow_zero, one_smul]
    exact congrArg _ (Pi.single_eq_same _ _)
  | a' + 1, haq =>
    rw [dTot_apply_succ_succ,
      show totSingle D ⟨(a' + 1, q), haq⟩ v ⟨(a', q + 1), by omega⟩ = 0 from
        Pi.single_eq_of_ne (M := fun j : Diag n => D.C j.1.1 j.1.2)
          (fun h => by injection (congrArg Subtype.val h) with h1; omega) _,
      map_zero, zero_add]
    exact congrArg _ (congrArg _ (Pi.single_eq_same _ _))

theorem

dTot_totSingle_col_succ

L453 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.dTot_totSingle_col_succ

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · full declaration

theorem dTot_totSingle_col_succ {n a q : ℕ} (haq : a + q = n) (v : D.C a q) :
    dTot D n (totSingle D ⟨(a, q), haq⟩ v) ⟨(a + 1, q), by omega⟩
      = D.dH a q v := by
  match q, haq with
  | 0, haq =>
    rw [dTot_apply_succ_zero]
    exact congrArg _ (Pi.single_eq_same _ _)
  | q'' + 1, haq =>
    rw [dTot_apply_succ_succ,
      show totSingle D ⟨(a, q'' + 1), haq⟩ v ⟨(a + 1, q''), by omega⟩ = 0 from
        Pi.single_eq_of_ne (M := fun j : Diag n => D.C j.1.1 j.1.2)
          (fun h => by injection (congrArg Subtype.val h) with h1; omega) _,
      map_zero, smul_zero, add_zero]
    exact congrArg _ (Pi.single_eq_same _ _)

theorem

sub_dTot_mem_zigTarget

L468 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.sub_dTot_mem_zigTarget

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem sub_dTot_mem_zigTarget (p' : ℕ) (b : Tot D (p' + 1))
    (hbT : b ∈ zigTarget D (p' + 1)) (w : Tot D p') :
    b - dTot D p' w ∈ zigTarget D (p' + 1)

theorem

zigOut_sub_dTot

L476 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.zigOut_sub_dTot

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem zigOut_sub_dTot (p' : ℕ) (b : Tot D (p' + 1))
    (w : Tot D p') :
    zigOut D (p' + 1) (b - dTot D p' w)
      = zigOut D (p' + 1) b

theorem

mem_FilTot_succ_iff

L485 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.mem_FilTot_succ_iff

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem mem_FilTot_succ_iff {p a q : ℕ} (haq : a + q = p)
    (c : Tot D p) :
    c ∈ FilTot D (a + 1) p
      ↔ c ∈ FilTot D a p ∧ c ⟨(a, q), haq⟩ = 0

def

ψ₁

L500 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.ψ₁

Documentation

The vertical cycle obtained from the column-a component of a filtered zig-zag input.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def ψ₁ (p a q' : ℕ) (haq : a + (q' + 1) = p) :
    ↥(FilTot D a p ⊓ zigTarget D p)
      →ₗ[R] ↥(LinearMap.ker (D.dV a (q' + 1)))

def

ψ

L512 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.ψ

Documentation

The second-page class of the column-a component of a filtered zig-zag input.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def ψ (p a q' : ℕ) (haq : a + (q' + 1) = p) :
    ↥(FilTot D a p ⊓ zigTarget D p)
      →ₗ[R] E₂I D a (q' + 1)

theorem

ψ_eq_zero_iff

L525 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.ψ_eq_zero_iff

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · full declaration

theorem ψ_eq_zero_iff (p a q' : ℕ) (haq : a + (q' + 1) = p)
    (b : ↥(FilTot D a p ⊓ zigTarget D p)) :
    ψ D p a q' haq b = 0
      ↔ (⟨(colB D a (q' + 1)).mkQ (ψ₁ D p a q' haq b), by
            refine LinearMap.mem_ker.mpr ?_
            change Submodule.mapQ _ _ _ _ (Submodule.Quotient.mk _) = 0
            rw [Submodule.mapQ_apply, Submodule.Quotient.mk_eq_zero]
            exact θ_dH_mem_colB D p a q' haq b.1 b.2.2
              (LinearMap.mem_ker.mp (ψ₁ D p a q' haq b).2)⟩
          : ↥(LinearMap.ker (colHdH D a (q' + 1))))
        ∈ E₂IB D a (q' + 1) := by
  exact Submodule.Quotient.mk_eq_zero _

theorem

η_mem_B_of_zigOut_eq

L538 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.η_mem_B_of_zigOut_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem η_mem_B_of_zigOut_eq (p a q' : ℕ) (haq : a + (q' + 1) = p)
    (bT : ↥(zigTarget D p)) (c : Tot D p)
    (hcF : c ∈ FilTot D (a + 1) p) (hcT : c ∈ zigTarget D p)
    (hcO : zigOut D p c = zigOut D p bT.1) :
    η D p bT ∈ B D (q' + 1) p

theorem

core_mem_B_pred

L547 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.core_mem_B_pred

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem core_mem_B_pred (p a q' : ℕ) (haq : a + (q' + 1) = p)
    (b : ↥(FilTot D a p ⊓ zigTarget D p))
    (hψ0 : ψ D p a q' haq b = 0) :
    η D p ⟨b.1, b.2.2⟩ ∈ B D (q' + 1) p

def

φ

L630 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.φ

Documentation

The map from filtered zig-zag inputs to the quotient of consecutive B submodules induced by the edge second-page class.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def φ (p a q' : ℕ) (haq : a + (q' + 1) = p) :
    ↥(FilTot D a p ⊓ zigTarget D p) →ₗ[R]
      ↥(B D (q' + 2) p)
        ⧸ (B D (q' + 1) p).comap (B D (q' + 2) p).subtype

theorem

B_gr_subquot

L642 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.B_gr_subquot

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section ZigZag
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem B_gr_subquot (p a q' : ℕ) (haq : a + (q' + 1) = p) :
    ∃ s : SubQuot R (E₂I D a (q' + 1)),
      Nonempty ((↥(B D (q' + 2) p)
          ⧸ (B D (q' + 1) p).comap (B D (q' + 2) p).subtype)
        ≃ₗ[R] s.carrier)

def

Bfilt

L678 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.Bfilt

Documentation

The finite filtration of row-zero second-page terms by images of filtered zig-zag inputs.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Bfilt
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · full declaration

def Bfilt : ∀ p', Fin (D.N + 1) → Submodule R (E₂I D p' 0)
  | 0, _ => ⊥
  | p + 1, i => B D (i.1 + 1) p

theorem

Bfilt_gr

L682 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.Bfilt_gr

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Bfilt
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem Bfilt_gr (p' : ℕ) (i : Fin D.N) :
    ∃ a q, 1 ≤ q ∧ ∃ s : SubQuot R (E₂I D a q),
      Nonempty ((↥(Bfilt D p' i.succ)
          ⧸ (Bfilt D p' i.castSucc).comap (Bfilt D p' i.succ).subtype)
        ≃ₗ[R] s.carrier)

def

Einf

L722 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.Einf

Documentation

The second-page subquotients retaining row zero modulo the terminal B filtration and making positive rows zero.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Hfilt
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · full declaration

def Einf : ∀ p q, SubQuot R (E₂I D p q)
  | p, 0 => ⟨⊤, Bfilt D p (Fin.last D.N), le_top⟩
  | _, _ + 1 => ⟨⊤, ⊤, le_refl ⊤⟩

def

τ

L727 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.τ

Documentation

The map from simultaneous edge cycles to their classes in edge-filtered total cohomology.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Hfilt
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def τ (p : ℕ) : ↥(KerHV D p) →ₗ[R] ↥(FilH D p p)

theorem

dTot_edgeSingle_of_ker_dV

L737 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.dTot_edgeSingle_of_ker_dV

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Hfilt
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem dTot_edgeSingle_of_ker_dV (p' : ℕ) (y : D.C p' 0)
    (hy : y ∈ LinearMap.ker (D.dV p' 0)) :
    dTot D p' (edgeSingle D p' y)
      = edgeSingle D (p' + 1) (D.dH p' 0 y)

def

σ

L758 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.σ

Documentation

The map from simultaneous edge cycles to their row-zero Einf classes.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Hfilt
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def σ (p : ℕ) :
    ↥(KerHV D p) →ₗ[R] (Einf D p 0).carrier

def

FilH_edge_iso

L763 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.FilH_edge_iso

Documentation

The linear equivalence from edge-filtered total cohomology to the row-zero Einf subquotient.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Hfilt
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def FilH_edge_iso (p : ℕ) :
    ↥(FilH D p p) ≃ₗ[R] (Einf D p 0).carrier

def

Hfilt

L848 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.Hfilt

Documentation

The finite filtration of total cohomology assembled from the edge piece and the zero and whole submodules.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Hfilt
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

def Hfilt (n : ℕ) (k : Fin (D.N + 2)) : Submodule R (HTot D n)

theorem

Hfilt_gr

L852 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.Hfilt_gr

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex
section Hfilt
variable {R : Type u} [CommRing R] (D : Bounded R)

Lean source · statement

theorem Hfilt_gr (p : Fin (D.N + 1)) :
    Nonempty (((Hfilt D (↑p) p.succ)
        ⧸ (Hfilt D (↑p) p.castSucc).comap (Hfilt D (↑p) p.succ).subtype)
      ≃ₗ[R] (Einf D (↑p) 0).carrier)

theorem

boundedSpectralSequence

L892 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.DoubleComplex_boundedSpectralSequence.DoubleComplex.boundedSpectralSequence

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section
namespace DoubleComplex
open _root_.DoubleComplex
open _root_.DoubleComplex

Lean source · statement

theorem boundedSpectralSequence : BoundedSpectralSequence.{u}

theorem

boundedSpectralSequence

L927 ↗

DoubleComplex.boundedSpectralSequence

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace DoubleComplex_boundedSpectralSequence
universe u
noncomputable section

Lean source · statement

theorem _root_.DoubleComplex.boundedSpectralSequence : DoubleComplex.BoundedSpectralSequence.{u}

Module documentation

Declarations