Finite Approximation Difference Relation

Abstract

The full kernel pair of the actual representative-difference cover is covered by its diagonal and its infinity fiber. Both pieces are closed light-profinite spaces, and their finite coproduct maps surjectively onto the whole relation. These concrete data justify free sheaf descent; equality only on ordinary finite points is not substituted for the kernel-pair relation. New proofs, Apache-2.0; Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2.

Theorem 1.1 (finite Approximation Difference Relation infty first).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationDifferenceRelation.finiteApproximationDifferenceRelation_infty_first

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. The full kernel pair of the actual representative-difference cover is covered by its diagonal and its infinity fiber. Both pieces are closed light-profinite spaces, and their finite coproduct maps surjectively onto the whole relation. These concrete data justify free sheaf descent; equality only on ordinary finite points is not substituted for the kernel-pair relation. New proofs, Apache-2.0; Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2.

Theorem 1.2 (finite Approximation Difference Relation infty second).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationDifferenceRelation.finiteApproximationDifferenceRelation_infty_second

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. The full kernel pair of the actual representative-difference cover is covered by its diagonal and its infinity fiber. Both pieces are closed light-profinite spaces, and their finite coproduct maps surjectively onto the whole relation. These concrete data justify free sheaf descent; equality only on ordinary finite points is not substituted for the kernel-pair relation. New proofs, Apache-2.0; Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2.

References

• Truth anchor: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationDifferenceRelation.finiteApproximationDifferenceRelation_infty_first
• Truth anchor: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationDifferenceRelation.finiteApproximationDifferenceRelation_infty_second
• Dependency: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationDifferences