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 := Top.of ↥{u : Π (j : J), ↥(F.obj j) | ∀ {i j : J} (f : i ⟶ j), ⇑(F.map f) (u i) = u j} subtype.topological_space, π := {app := λ (j : J), {to_fun := λ (u : ↥(((category_theory.functor.const J).obj (Top.of ↥{u : Π (j : J), ↥(F.obj j) | ∀ {i j : J} (f : i ⟶ j), ⇑(F.map f) (u i) = u j})).obj j)), u.val j, continuous_to_fun := _}, naturality' := _}}

A choice of limit cone for a functor F : J ⥤ Top whose topology is defined as an infimum of topologies infimum. 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_infi 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 = {lift := λ (S : category_theory.limits.cone F), {to_fun := λ (x : ↥(S.X)), ⟨λ (j : J), ⇑(S.π.app j) x, _⟩, continuous_to_fun := _}, fac' := _, uniq' := _}

The chosen cone Top.limit_cone_infi 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_infi_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_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.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))}}

Equations

• Top.forget_preserves_limits = Top.forget_preserves_limits_of_size

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_of_size = {preserves_colimits_of_shape := λ (J : Type v) (𝒥 : category_theory.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))}}

Equations

• Top.forget_preserves_colimits = Top.forget_preserves_colimits_of_size

The terminal object of Top is punit.

Equations

• Top.is_terminal_punit = category_theory.limits.is_terminal.of_unique (Top.of punit)

The initial object of Top is pempty.

Equations

• Top.is_initial_pempty = category_theory.limits.is_initial.of_unique (Top.of pempty)