Corollary B.6
OpenQAlgorithms.Papers.Independent.Intakethird100.P07.kSpace_inclusion_preservesColimitsFor the inclusion of the full category of compactly Hausdorff generated spaces into all topological spaces,
Consequently colimits of k-spaces computed in kTop agree, via the inclusion and their cocone maps, with those computed in Top. No Hausdorffness restriction is imposed.
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P07
noncomputable section
universe u v
namespace QAlgorithms.Papers.Independent.Intakethird100.P07
open CategoryTheory Topology TopologicalSpace
/-- Corollary B.6, PDF p. 36: the inclusion preserves categorical colimits. -/
theorem kSpace_inclusion_preservesColimits :
Limits.PreservesColimits
(CompactlyGenerated.compactlyGeneratedToTop.{u, u}) := by sorry
end QAlgorithms.Papers.Independent.Intakethird100.P07
end
Read-back
What the Lean code literally says, in plain math · gpt-6.1-sol
The inclusion functor from spaces in universe that are compactly generated with respect to compact Hausdorff spaces in universe into topological spaces in universe , leaving their spaces and continuous maps unchanged, preserves colimits. Explicitly, for every diagram of the universe sizes covered by this assertion, any colimit cocone in the compactly generated category remains a colimit cocone in the category of topological spaces after applying the inclusion. Here compact generation means that a subset is open exactly when its inverse image is open under every continuous map from a compact Hausdorff space in universe . Preservation includes empty diagrams and does not itself assert the existence of a colimit for every diagram.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.