Existence of wide pullbacks when the target object is terminal

In this file, we show that the wide pullback of a family of arrows objs j ⟶ B exists when B is terminal and the product of the objects objs j exists.

@[reducible, inline]

abbrev CategoryTheory.Limits.WidePullbackCone.toFan {C : Type u} [Category.{v, u} C] {ι : Type w} {B : C} {objs : ι → C} (arrows : (j : ι) → objs j ⟶ B) (s : WidePullbackCone arrows) : Fan objs

The fan that is induced by a wide pullback cone.

@[reducible, inline]

abbrev CategoryTheory.Limits.WidePullbackCone.ofFan {C : Type u} [Category.{v, u} C] {ι : Type w} {B : C} {objs : ι → C} (arrows : (j : ι) → objs j ⟶ B) (c : Fan objs) (hB : IsTerminal B) : WidePullbackCone arrows

The wide pullback cone given by a fan, when the base object is terminal.

def CategoryTheory.Limits.WidePullbackCone.isLimitOfFan {C : Type u} [Category.{v, u} C] {ι : Type w} {B : C} {objs : ι → C} (arrows : (j : ι) → objs j ⟶ B) {c : Fan objs} (hc : IsLimit c) (hB : IsTerminal B) : IsLimit (ofFan arrows c hB)

When the base object is terminal, a limit wide pullback cone can be obtained from a limit fan.

theorem CategoryTheory.Limits.hasWidePullback_of_isTerminal {C : Type u} [Category.{v, u} C] {ι : Type w} {B : C} {objs : ι → C} (arrows : (j : ι) → objs j ⟶ B) [HasProduct objs] (hB : IsTerminal B) : HasWidePullback B objs arrows