A choice of limit cone for a functor F : J ⥤ Top.
Generally you should just use limit.cone F, unless you need the actual definition
(which is in terms of types.limit_cone).
Equations
- Top.limit_cone F = {X := {α := (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget Top)).X, str := ⨅ (j : J), topological_space.induced ((category_theory.limits.types.limit_cone (F ⋙ category_theory.forget Top)).π.app j) (F.obj j).str}, π := {app := λ (j : J), {to_fun := (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget Top)).π.app j, continuous_to_fun := _}, naturality' := _}}
The chosen cone Top.limit_cone F for a functor F : J ⥤ Top is a limit cone.
Generally you should just use limit.is_limit F, unless you need the actual definition
(which is in terms of types.limit_cone_is_limit).
Equations
- Top.limit_cone_is_limit F = category_theory.limits.is_limit.of_faithful (category_theory.forget Top) (category_theory.limits.types.limit_cone_is_limit (F ⋙ category_theory.forget Top)) (λ (s : category_theory.limits.cone F), {to_fun := λ (v : ((category_theory.forget Top).map_cone s).X), ⟨λ (j : J), ((category_theory.forget Top).map_cone s).π.app j v, _⟩, continuous_to_fun := _}) _
Equations
- Top.forget_preserves_limits = {preserves_limits_of_shape := λ (J : Type u) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ Top), category_theory.limits.preserves_limit_of_preserves_limit_cone (Top.limit_cone_is_limit F) (category_theory.limits.types.limit_cone_is_limit (F ⋙ category_theory.forget Top))}}
A choice of colimit cocone for a functor F : J ⥤ Top.
Generally you should just use colimit.coone F, unless you need the actual definition
(which is in terms of types.colimit_cocone).
Equations
- Top.colimit_cocone F = {X := {α := (category_theory.limits.types.colimit_cocone (F ⋙ category_theory.forget Top)).X, str := ⨆ (j : J), topological_space.coinduced ((category_theory.limits.types.colimit_cocone (F ⋙ category_theory.forget Top)).ι.app j) (F.obj j).str}, ι := {app := λ (j : J), {to_fun := (category_theory.limits.types.colimit_cocone (F ⋙ category_theory.forget Top)).ι.app j, continuous_to_fun := _}, naturality' := _}}
The chosen cocone Top.colimit_cocone F for a functor F : J ⥤ Top is a colimit cocone.
Generally you should just use colimit.is_colimit F, unless you need the actual definition
(which is in terms of types.colimit_cocone_is_colimit).
Equations
- Top.colimit_cocone_is_colimit F = category_theory.limits.is_colimit.of_faithful (category_theory.forget Top) (category_theory.limits.types.colimit_cocone_is_colimit (F ⋙ category_theory.forget Top)) (λ (s : category_theory.limits.cocone F), {to_fun := quot.lift (λ (p : Σ (j : J), (F ⋙ category_theory.forget Top).obj j), ((category_theory.forget Top).map_cocone s).ι.app p.fst p.snd) _, continuous_to_fun := _}) _
Equations
- Top.forget_preserves_colimits = {preserves_colimits_of_shape := λ (J : Type u) (𝒥 : category_theory.small_category J), {preserves_colimit := λ (F : J ⥤ Top), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (Top.colimit_cocone_is_colimit F) (category_theory.limits.types.colimit_cocone_is_colimit (F ⋙ category_theory.forget Top))}}