Corollary B.7
OpenQAlgorithms.Papers.Independent.Intakethird100.P07.kification_preservesLimitsLet be the functor assigning the final compact-Hausdorff-probe topology to each underlying set and the same function to each continuous map. Then
This is the categorical meaning of the source's word “continuous” for the coreflector, for arbitrary topological spaces without a separation axiom.
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.7, PDF p. 36: the specified coreflector preserves
categorical limits. No continuity of an unrelated function is substituted. -/
theorem kification_preservesLimits :
Limits.PreservesLimits kCoreflector.{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 functor from topological spaces in universe to compactly generated spaces in universe that sends to and leaves underlying functions unchanged preserves limits. Here has the underlying set of , with a subset open exactly when its inverse image is open under every originally continuous map from a compact Hausdorff space in universe ; the target category uses compact generation with respect to those spaces. Explicitly, for every diagram of the universe sizes covered by this assertion, applying this functor to any limit cone in topological spaces produces a limit cone in the compactly generated category. This includes empty diagrams and does not itself assert the existence of a limit for every diagram.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.