Documentation

Mathlib.CategoryTheory.Limits.Constructions.WidePullbackOfTerminal

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.

source
@[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.

Equations
Instances For
    source
    @[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.

    Equations
    Instances For
      source
      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.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        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