mathlib documentation

category_theory.limits.shapes.wide_pullbacks

Wide pullbacks #

We define the category wide_pullback_shape, (resp. wide_pushout_shape) which is the category obtained from a discrete category of type J by adjoining a terminal (resp. initial) element. Limits of this shape are wide pullbacks (pushouts). The convenience method wide_cospan (wide_span) constructs a functor from this category, hitting the given morphisms.

We use wide_pullback_shape to define ordinary pullbacks (pushouts) by using J := walking_pair, which allows easy proofs of some related lemmas. Furthermore, wide pullbacks are used to show the existence of limits in the slice category. Namely, if C has wide pullbacks then C/B has limits for any object B in C.

Typeclasses has_wide_pullbacks and has_finite_wide_pullbacks assert the existence of wide pullbacks and finite wide pullbacks.

def category_theory.limits.wide_pullback_shape (J : Type v) :
Type v

A wide pullback shape for any type J can be written simply as option J.

Equations
def category_theory.limits.wide_pushout_shape (J : Type v) :
Type v

A wide pushout shape for any type J can be written simply as option J.

Equations

The type of arrows for the shape indexing a wide pullback.

@[instance]
Equations
@[simp]
theorem category_theory.limits.wide_pullback_shape.wide_cospan_obj {J : Type v} {C : Type u} [category_theory.category C] (B : C) (objs : J → C) (arrows : Π (j : J), objs j B) (j : category_theory.limits.wide_pullback_shape J) :
(category_theory.limits.wide_pullback_shape.wide_cospan B objs arrows).obj j = option.cases_on j B objs
def category_theory.limits.wide_pullback_shape.wide_cospan {J : Type v} {C : Type u} [category_theory.category C] (B : C) (objs : J → C) (arrows : Π (j : J), objs j B) :

Construct a functor out of the wide pullback shape given a J-indexed collection of arrows to a fixed object.

Equations
@[simp]
theorem category_theory.limits.wide_pullback_shape.wide_cospan_map {J : Type v} {C : Type u} [category_theory.category C] (B : C) (objs : J → C) (arrows : Π (j : J), objs j B) (X Y : category_theory.limits.wide_pullback_shape J) (f : X Y) :
(category_theory.limits.wide_pullback_shape.wide_cospan B objs arrows).map f = category_theory.limits.wide_pullback_shape.hom.cases_on f (λ (f_1 : category_theory.limits.wide_pullback_shape J) (H_1 : X = f_1), eq.rec (λ (H_2 : Y = X), eq.rec (λ (f : X X) (H_3 : f == category_theory.limits.wide_pullback_shape.hom.id X), eq.rec (𝟙 (option.cases_on X B objs)) _) _ f) H_1) (λ (j : J) (H_1 : X = some j), eq.rec (λ (f : some j Y) (H_2 : Y = none), eq.rec (λ (f : some j none) (H_3 : f == category_theory.limits.wide_pullback_shape.hom.term j), eq.rec (arrows j) _) _ f) _ f) _ _ _

Construct a cone over a wide cospan.

Equations
@[simp]
theorem category_theory.limits.wide_pullback_shape.mk_cone_π_app {J : Type v} {C : Type u} [category_theory.category C] {F : category_theory.limits.wide_pullback_shape J C} {X : C} (f : X F.obj none) (π : Π (j : J), X F.obj (some j)) (w : ∀ (j : J), «π» j F.map (category_theory.limits.wide_pullback_shape.hom.term j) = f) (j : category_theory.limits.wide_pullback_shape J) :
(category_theory.limits.wide_pullback_shape.mk_cone f «π» w).π.app j = category_theory.limits.wide_pullback_shape.mk_cone._match_1 f «π» j
@[simp]

The type of arrows for the shape indexing a wide psuhout.

@[instance]
Equations
def category_theory.limits.wide_pushout_shape.wide_span {J : Type v} {C : Type u} [category_theory.category C] (B : C) (objs : J → C) (arrows : Π (j : J), B objs j) :

Construct a functor out of the wide pushout shape given a J-indexed collection of arrows from a fixed object.

Equations
@[simp]
theorem category_theory.limits.wide_pushout_shape.wide_span_map {J : Type v} {C : Type u} [category_theory.category C] (B : C) (objs : J → C) (arrows : Π (j : J), B objs j) (X Y : category_theory.limits.wide_pushout_shape J) (f : X Y) :
(category_theory.limits.wide_pushout_shape.wide_span B objs arrows).map f = category_theory.limits.wide_pushout_shape.hom.cases_on f (λ (f_1 : category_theory.limits.wide_pushout_shape J) (H_1 : X = f_1), eq.rec (λ (H_2 : Y = X), eq.rec (λ (f : X X) (H_3 : f == category_theory.limits.wide_pushout_shape.hom.id X), eq.rec (𝟙 (option.cases_on X B objs)) _) _ f) H_1) (λ (j : J) (H_1 : X = none), eq.rec (λ (f : none Y) (H_2 : Y = some j), eq.rec (λ (f : none some j) (H_3 : f == category_theory.limits.wide_pushout_shape.hom.init j), eq.rec (arrows j) _) _ f) _ f) _ _ _
@[simp]
theorem category_theory.limits.wide_pushout_shape.wide_span_obj {J : Type v} {C : Type u} [category_theory.category C] (B : C) (objs : J → C) (arrows : Π (j : J), B objs j) (j : category_theory.limits.wide_pushout_shape J) :
(category_theory.limits.wide_pushout_shape.wide_span B objs arrows).obj j = option.cases_on j B objs

Construct a cocone over a wide span.

Equations
@[simp]
theorem category_theory.limits.wide_pushout_shape.mk_cocone_ι_app {J : Type v} {C : Type u} [category_theory.category C] {F : category_theory.limits.wide_pushout_shape J C} {X : C} (f : F.obj none X) (ι : Π (j : J), F.obj (some j) X) (w : ∀ (j : J), F.map (category_theory.limits.wide_pushout_shape.hom.init j) ι j = f) (j : category_theory.limits.wide_pushout_shape J) :
(category_theory.limits.wide_pushout_shape.mk_cocone f ι w).ι.app j = category_theory.limits.wide_pushout_shape.mk_cocone._match_1 f ι j

has_wide_pullbacks represents a choice of wide pullback for every collection of morphisms

has_wide_pushouts represents a choice of wide pushout for every collection of morphisms