Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite Free Solid

Abstract

Actual solidity of the free object on a finite light-profinite space, including the empty case. The point/free/discrete comparison is reused from the immutable, independently audited Apache-2.0 CWComparison supplier. This supplies the finite initial term in the concrete generator retract; it makes no bounded-only replacement of the full target. New proofs, Apache-2.0; finite coproduct/limits APIs are from pinned Mathlib.

Theorem 1.1 (is Solid free finite).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteFreeSolid.isSolid_free_finite

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

Source. Repository-derived.

Commentary.

Solidity follows from a genuine preserved finite coproduct, also for an empty index. No comparison only on ordinary points is substituted.

Theorem 1.2 (is Solid free initial Component).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteFreeSolid.isSolid_free_initialComponent

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

Source. Repository-derived.

Commentary.

In particular the actual initial finite quotient used in the retract has a solid free object; it is not silently treated as an infinite space.

References