Sequential Presentation

Abstract

Countable telescope presentations in an AB5 abelian category. New proofs, released under the Apache 2.0 license.

Theorem 1.1 (sequence Projection jointly monic).

Lean statement: D5/S3/HomologicalAlgebra/Solid/SequentialPresentation.sequenceProjection_jointly_monic

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/SequentialPresentation.sequenceProjection_jointly_monic (✓ std3). ∎

Source. Repository-derived.

Commentary.

AB5 makes the canonical map from the sum into the product monic. This is proved by taking the filtered union of its finite split submaps.

Theorem 1.2 (one Minus Sequence mono).

Lean statement: D5/S3/HomologicalAlgebra/Solid/SequentialPresentation.oneMinusSequence_mono

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/SequentialPresentation.oneMinusSequence_mono (✓ std3). ∎

Source. Repository-derived.

Commentary.

One minus the forward transition is monic for every countable sequence; no monicity of the transitions is required.

Truth anchor: D5/S3/HomologicalAlgebra/Solid/SequentialPresentation.oneMinusSequence_mono
Truth anchor: D5/S3/HomologicalAlgebra/Solid/SequentialPresentation.sequenceProjection_jointly_monic