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  :
Type vType v

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

Equations
def category_theory.limits.wide_pushout_shape  :
Type vType 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) :
(Π (j : J), objs j B)category_theory.limits.wide_pullback_shape J C

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) _ _ _

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) :
(Π (j : J), B objs j)category_theory.limits.wide_pushout_shape J C

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

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