Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Generator Construction

Abstract

The actual ordinary P reflection is imported; new concrete finite-approximation retract, degree-zero DSolid realization of every reflected free profinite generator, the actual ordinary generator solidification(P), the exact local reflector, protected derived coproduct preservation, and the concrete unbounded lower-truncation telescope. Only new owned construction bodies are assembled to share one import pass. Passed dependencies are imported unchanged. New proofs: Apache-2.0. Research: Juan Esteban Rodríguez Camargo, Notes on Solid Geometry, Theorem 3.3.1 and Lemma 3.3.2. No arbitrary unbounded realization or original HasLeftDerivedFunctor/derived adjunction is assumed.

Definition 1.1 (local Free Stalk Ordinary Realization Iso).

Lean statement: D5/S3/HomologicalAlgebra/Solid/GeneratorConstruction.localFreeStalkOrdinaryRealizationIso

Formalization. D5/S3/HomologicalAlgebra/Solid/GeneratorConstruction.localFreeStalkOrdinaryRealizationIso (✓ std3).

Source. Repository-derived.

Commentary.

The generator realization uses the exact original ordinary reflector.

Theorem 1.2 (solid P detects is Zero).

Lean statement: D5/S3/HomologicalAlgebra/Solid/GeneratorConstruction.solidP_detects_isZero

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

Source. Repository-derived.

Commentary.

The actual protected object solidification(P), rather than an assumed generator, detects every zero solid object.

Theorem 1.3 (lower Truncation Telescope To Input quasi Iso).

Lean statement: D5/S3/HomologicalAlgebra/Solid/GeneratorConstruction.lowerTruncationTelescopeToInput_quasiIso

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

Source. Repository-derived.

Commentary.

A proved quasi-isomorphism for every unbounded input. It provides the actual lower-truncation telescope used in the realization argument.

References