Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Free Flat

Abstract

Tensor exactness for the concrete cells used in solidification. The proof uses flat free modules in presheaves and left exact sheafification; it does not assume enough projectives in light condensed abelian groups.

Theorem 1.1 (tensor Free preserves Finite Limits).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FreeFlat.tensorFree_preservesFiniteLimits

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

Source. Repository-derived.

Commentary.

Free light condensed abelian groups are flat, including free groups on arbitrary light condensed sets.

Theorem 1.2 (tensor P preserves Finite Limits).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FreeFlat.tensorP_preservesFiniteLimits

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

Source. Repository-derived.

Commentary.

Tensoring with the protected P is exact. This is a tensor-flatness statement, separate from the protected internal-projectivity instance.

References