How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Abelian-group model for spectral-sequence computations
Statement
Abelian groups and homomorphisms form an abelian category. Kernels and images are the ordinary subgroup kernels and images, and cokernels are coset quotients. In particular , , and their finite products are legitimate objects for filtered-complex computations. Multiplication by 2 on is injective with cokernel .
Facts & Assumptions
Given: Abelian groups and additive homomorphisms, with the indicated integer and congruence constructions.
An additive category with kernels and cokernels is abelian when its canonical coimage-to-image map is an isomorphism (Abelian category).
Group homomorphisms preserve the group operation (Monoid homomorphism and group homomorphism).
The integers form a totally ordered commutative ring (The integers form a totally ordered ring).
The congruence-class groups are abelian with addition of representatives (For every natural , is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold).
An equivalence relation gives its set of equivalence classes (Equivalence relation, equivalence class, and the quotient set ).
Division by a positive integer has a unique remainder between zero and that integer (Division with remainder in : for and there are unique with and ).
Proof
For abelian groups A,B the homomorphisms form an abelian group under : additivity follows from commutativity in B, with zero map and pointwise negatives as identity and inverses. The group laws hold pointwise. Composition is bilinear because each map is additive [F2]. Identities and composites are homomorphisms by the same calculation, so this is a preadditive category.
The one-element group 0 is both initial and terminal. The product group with coordinate operations has projections and injections a↦(a,0), b↦(0,b). A pair of maps T→A,B induces t↦(f(t),g(t)), uniquely by coordinates. Maps A→T and B→T induce , uniquely since . These are its product and coproduct properties. Iterating yields every finite biproduct, including the empty one 0.
For f:A→B, the subset is a subgroup: f(0)=0 follows from f(0)=f(0)+f(0), and . Any homomorphism killed by f has values in K and factors uniquely through its inclusion. The image I={f(a):a∈A} is likewise a subgroup, since f(a)-f(a')=f(a-a').
For a subgroup I⊆B define b∼b' by b-b'∈I. Zero, negation and addition in I prove reflexivity, symmetry and transitivity. On the quotient set of [F5], define [b]+[c]=[b+c]; changing b,c by elements of I changes their sum by an element of I, so addition is well defined, and the group laws descend. A homomorphism h:B→T vanishes on I exactly when b↦h(b) is constant on each coset: one direction follows from h(b)-h(b')=h(b-b'), and the other by comparing i and 0 for i∈I. Thus [b]↦h(b) is the unique quotient homomorphism. With I=im f, this is a cokernel of f.
The kernel of B→B/I is exactly I since [b]=[0] iff b∈I. Consequently the categorical image of f is I, and its coimage is A/K. The canonical comparison [a]↦f(a) is well defined, is onto I by definition, and is injective since f(a)=f(a') iff a-a'∈K. Its inverse is the uniquely specified relation sending f(a) to [a], not a chosen representative function; it is additive because both maps preserve addition. Hence [F1] applies to steps 1.1–3.1 and proves the abelian-category assertion.
By [F3] the additive integers are an abelian group. If 2a=0 and a>0, positivity gives 2a>0; if a<0 it gives 2(-a)>0. Thus a=0, proving injectivity. Its image is 2ℤ and its cokernel is ℤ/2ℤ by step 3.1, with the congruence operations of [F4]. Division [F6] for divisors 2 and 4 gives exactly the distinct residue lists {0,1} and {0,1,2,3}. Their additions are modulo 2 and 4, so 1+1=0 in ℤ/2 and 1+1=2≠0, 2+2=0 in ℤ/4. Finite products have the coordinate operations of step 2.1.
Source notes
Stacks, §12.5, Definition 12.5.1 and Lemmas 12.5.11–15. The finite categorical argument below is supplied locally.
Depends on
- Abelian category
- Monoid homomorphism and group homomorphism
- The integers form a totally ordered ring
- For every natural $n$, $(\mathbb{Z}/n,+)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold
- Equivalence relation, equivalence class, and the quotient set $A/{\sim}$
- Division with remainder in $\mathbb{Z}$: for $a \in \mathbb{Z}$ and $b > 0$ there are unique $q, r \in \mathbb{Z}$ with $a = qb + r$ and $0 \le r < b$
Used by
- An exhaustive nonseparated filtration with the wrong naive abutment Counterexample
- Collapse with a nonsplit extension problem Counterexample
- Isomorphic associated graded objects need not give isomorphic filtered objects Counterexample
- Lim one obstruction to completeness Definition
- A filtered complex collapsing at e one Example
- A filtered quasi isomorphism detected on associated graded complexes Example
- A first quadrant five term exact sequence Example
- A nonzero d two differential in a small filtered complex Example
- Acyclic assembly with exact columns Example
- Edge maps from a first quadrant spectral sequence Example
- The cohomological reindexing of a homological spectral sequence Example
- The exact couple of a two step filtration Example
- The two spectral sequences of a two by two double complex Example
- The two step filtration and its spectral sequence Example
- Two filtered abelian groups with the same associated graded Example
- A spectral sequence collapses when one differential is zero False statement
- E r plus one is literally equal to the homology of e r False statement
- E zero and e one page conventions are universal across sources False statement
- Every exact couple is a long exact sequence with no extra grading data False statement
- Exhaustive filtration implies separated and complete filtration False statement
- First quadrant support alone identifies the abutment without a filtration False statement
- The filtration on homology is h n of the filtered subcomplex False statement
- The two spectral sequences of a double complex have identical e one pages False statement
- Countable sequence groups and tail filtrations Lemma
- Collapse with projective associated graded pieces splits the finite filtration noncanonically Proposition
- Failure of separatedness or completeness can destroy the claimed abutment Proposition
- The two double complex spectral sequences have the same abutment but not the same pages Proposition
Dependency tree · two levels
39 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- The Stacks Project, Definition 12.5.1 (axiom checklist; model verified locally) (standard reference, not scraped)