Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30
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.

A chain map carries cycles to cycles and boundaries to boundaries

Statement

Let f:CD be a chain map. For every nZ there are induced morphisms Zn(f):Zn(C)Zn(D),Bn(f):Bn(C)Bn(D), compatible with the canonical inclusions into Cn and Dn.

Facts & Assumptions

Given: A chain map f:CD and an integer n.

[L1]

A chain map satisfies dnDfn=fn1dnC (Chain map).

[L2]

Kernels are universal among arrows killed by the given morphism (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers).

[L3]

Write dn+1C=iCeC and dn+1D=iDeD as epic-monic factorizations, where iC and iD are the boundary inclusions (Every morphism factors as an epimorphism followed by a monomorphism, uniquely up to unique isomorphism).

[L4]

In an abelian category, every monomorphism is the kernel of its cokernel (Every monomorphism is the kernel of its cokernel, and dually every epimorphism is the cokernel of its kernel).

Proof

technique · direct
1.1

Let kC:Zn(C)Cn and kD:Zn(D)Dn be the cycle inclusions. Using [L1], dnDfnkC=fn1dnCkC=0, so [L2] yields a unique map Zn(f):Zn(C)Zn(D) with kDZn(f)=fnkC.

L1L2givenconstruct
2.1

By [L3], fniCeC=fndn+1C=dn+1Dfn+1=iDeDfn+1. Let cD be a cokernel of iD. Then cDfniCeC=cDiDeDfn+1=0. Since eC is epic, this implies cDfniC=0. By [L4], the monomorphism iD is a kernel of cD, so [L2] gives a unique morphism Bn(f):Bn(C)Bn(D) with iDBn(f)=fniC. This is the required boundary map.

L1L2L3L4givenalgebraconstructdischarge-construct

Depends on

Used by

Dependency tree · two levels

17 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