Commit 2024-09-03 09:13 79c4b69e

feat(Topology/CompHaus): sigma-comparison map (#15525) This PR defines the map CompHausLike.sigmaComparison associated to a presheaf X on CompHausLike P, and a finite family S₁,...,Sₙ of spaces in CompHausLike P, where P is stable under taking finite disjoint unions. The map sigmaComparison is the canonical map X(S₁ ⊔ ... ⊔ Sₙ) ⟶ X(S₁) × ... × X(Sₙ) induced by the inclusion maps Sᵢ ⟶ S₁ ⊔ ... ⊔ Sₙ, and it is an isomorphism when X preserves finite products.