Equations
- Top.limit F = {X := {α := category_theory.limits.limit (F ⋙ category_theory.forget Top) (category_theory.limits.has_limit_of_has_limits_of_shape (F ⋙ category_theory.forget Top)), str := ⨅ (j : J), topological_space.induced (category_theory.limits.limit.π (F ⋙ category_theory.forget Top) j) (F.obj j).str}, π := {app := λ (j : J), {to_fun := category_theory.limits.limit.π (F ⋙ category_theory.forget Top) j, continuous_to_fun := _}, naturality' := _}}
Equations
- Top.limit_is_limit F = category_theory.limits.is_limit.of_faithful (category_theory.forget Top) (category_theory.limits.limit.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 := _}) _
@[instance]
Equations
- Top.Top_has_limits = {has_limits_of_shape := λ (J : Type u) (𝒥 : category_theory.small_category J), {has_limit := λ (F : J ⥤ Top), {cone := Top.limit F, is_limit := Top.limit_is_limit F}}}
@[instance]
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 (category_theory.limits.limit.is_limit F) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget Top))}}
Equations
- Top.colimit F = {X := {α := category_theory.limits.colimit (F ⋙ category_theory.forget Top) (category_theory.limits.has_colimit_of_has_colimits_of_shape (F ⋙ category_theory.forget Top)), str := ⨆ (j : J), topological_space.coinduced (category_theory.limits.colimit.ι (F ⋙ category_theory.forget Top) j) (F.obj j).str}, ι := {app := λ (j : J), {to_fun := category_theory.limits.colimit.ι (F ⋙ category_theory.forget Top) j, continuous_to_fun := _}, naturality' := _}}
Equations
- Top.colimit_is_colimit F = category_theory.limits.is_colimit.of_faithful (category_theory.forget Top) (category_theory.limits.colimit.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 := _}) _
@[instance]
Equations
- Top.Top_has_colimits = {has_colimits_of_shape := λ (J : Type u) (𝒥 : category_theory.small_category J), {has_colimit := λ (F : J ⥤ Top), {cocone := Top.colimit F, is_colimit := Top.colimit_is_colimit F}}}
@[instance]
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 (category_theory.limits.colimit.is_colimit F) (category_theory.limits.colimit.is_colimit (F ⋙ category_theory.forget Top))}}