Discrete Int

Abstract

Algebra for the proof that ℤ is solid This file contains the finite-support sequence calculation used in the proof that the light condensed abelian group of integers is solid. The finite-difference operator a ↦ (fun n => a n - a (n + 1)) is an automorphism of finitely supported integer sequences, with inverse given by finite tail sums.

Theorem 1.1 (one Minus Shift component is Iso).

Lean statement: D5/S3/HomologicalAlgebra/Solid/DiscreteInt.oneMinusShift_component_isIso

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. # Algebra for the proof that ℤ is solid This file contains the finite-support sequence calculation used in the proof that the light condensed abelian group of integers is solid. The finite-difference operator a ↦ (fun n => a n - a (n + 1)) is an automorphism of finitely supported integer sequences, with inverse given by finite tail sums.

Theorem 1.2 (is Solid int).

Lean statement: D5/S3/HomologicalAlgebra/Solid/DiscreteInt.isSolid_int

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. # Algebra for the proof that ℤ is solid This file contains the finite-support sequence calculation used in the proof that the light condensed abelian group of integers is solid. The finite-difference operator a ↦ (fun n => a n - a (n + 1)) is an automorphism of finitely supported integer sequences, with inverse given by finite tail sums.

References

• Truth anchor: D5/S3/HomologicalAlgebra/Solid/DiscreteInt.isSolid_int
• Truth anchor: D5/S3/HomologicalAlgebra/Solid/DiscreteInt.oneMinusShift_component_isIso
• Dependency: D5/S3/HomologicalAlgebra/Solid/Reflection