Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Profinite Cover

Abstract

This module supplies the indicated step in the unbounded solidification construction.

Theorem 1.1 (profinite Cover free epi).

Lean statement: D5/S3/HomologicalAlgebra/Solid/Supplier/ProfiniteCover.profiniteCover_free_epi

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/Supplier/ProfiniteCover.profiniteCover_free_epi (✓ std3). ∎

Source. Repository-derived.

Commentary.

The same covering augmentation is epimorphic for the protected free functor.

Theorem 1.2 (binary Interval Cover free epi).

Lean statement: D5/S3/HomologicalAlgebra/Solid/Supplier/ProfiniteCover.binaryIntervalCover_free_epi

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/Supplier/ProfiniteCover.binaryIntervalCover_free_epi (✓ std3). ∎

Source. Repository-derived.

Commentary.

Its free augmentation onto the actual free condensed interval object.

References