mathlib3 documentation

category_theory.limits.shapes.wide_pullbacks

Wide pullbacks #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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

Instances for category_theory.limits.wide_pullback_shape.hom
@[protected, instance]
Equations
@[simp]
theorem category_theory.limits.wide_pullback_shape.wide_cospan_obj {J : Type w} {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

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 w} {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 = option.some j), eq.rec (λ (f : option.some j Y) (H_2 : Y = option.none), eq.rec (λ (f : option.some j option.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 w} {C : Type u} [category_theory.category C] {F : category_theory.limits.wide_pullback_shape J C} {X : C} (f : X F.obj option.none) (π : Π (j : J), X F.obj (option.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

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

Instances for category_theory.limits.wide_pushout_shape.hom
@[protected, instance]
Equations
def category_theory.limits.wide_pushout_shape.wide_span {J : Type w} {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 w} {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 = option.none), eq.rec (λ (f : option.none Y) (H_2 : Y = option.some j), eq.rec (λ (f : option.none option.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 w} {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 w} {C : Type u} [category_theory.category C] {F : category_theory.limits.wide_pushout_shape J C} {X : C} (f : F.obj option.none X) (ι : Π (j : J), F.obj (option.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
@[reducible]

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

@[reducible]

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

@[reducible]
def category_theory.limits.has_wide_pullback {J : Type w} {C : Type u} [category_theory.category C] (B : C) (objs : J C) (arrows : Π (j : J), objs j B) :
Prop

has_wide_pullback B objs arrows means that wide_cospan B objs arrows has a limit.

@[reducible]
def category_theory.limits.has_wide_pushout {J : Type w} {C : Type u} [category_theory.category C] (B : C) (objs : J C) (arrows : Π (j : J), B objs j) :
Prop

has_wide_pushout B objs arrows means that wide_span B objs arrows has a colimit.

@[reducible]
noncomputable def category_theory.limits.wide_pullback {J : Type w} {C : Type u} [category_theory.category C] (B : C) (objs : J C) (arrows : Π (j : J), objs j B) [category_theory.limits.has_wide_pullback B objs arrows] :
C

A choice of wide pullback.

@[reducible]
noncomputable def category_theory.limits.wide_pushout {J : Type w} {C : Type u} [category_theory.category C] (B : C) (objs : J C) (arrows : Π (j : J), B objs j) [category_theory.limits.has_wide_pushout B objs arrows] :
C

A choice of wide pushout.

@[reducible]
noncomputable def category_theory.limits.wide_pullback.π {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), objs j B) [category_theory.limits.has_wide_pullback B objs arrows] (j : J) :
category_theory.limits.wide_pullback B (λ (j : J), objs j) arrows objs j

The j-th projection from the pullback.

@[reducible]
noncomputable def category_theory.limits.wide_pullback.base {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), objs j B) [category_theory.limits.has_wide_pullback B objs arrows] :
category_theory.limits.wide_pullback B (λ (j : J), objs j) arrows B

The unique map to the base from the pullback.

@[simp]
theorem category_theory.limits.wide_pullback.π_arrow {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), objs j B) [category_theory.limits.has_wide_pullback B objs arrows] (j : J) :
@[simp]
theorem category_theory.limits.wide_pullback.π_arrow_assoc {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), objs j B) [category_theory.limits.has_wide_pullback B objs arrows] (j : J) {X' : C} (f' : B X') :
@[reducible]
noncomputable def category_theory.limits.wide_pullback.lift {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} {arrows : Π (j : J), objs j B} [category_theory.limits.has_wide_pullback B objs arrows] {X : C} (f : X B) (fs : Π (j : J), X objs j) (w : (j : J), fs j arrows j = f) :
X category_theory.limits.wide_pullback B (λ (j : J), objs j) arrows

Lift a collection of morphisms to a morphism to the pullback.

@[simp]
theorem category_theory.limits.wide_pullback.lift_π_assoc {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), objs j B) [category_theory.limits.has_wide_pullback B objs arrows] {X : C} (f : X B) (fs : Π (j : J), X objs j) (w : (j : J), fs j arrows j = f) (j : J) {X' : C} (f' : objs j X') :
@[simp]
theorem category_theory.limits.wide_pullback.lift_π {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), objs j B) [category_theory.limits.has_wide_pullback B objs arrows] {X : C} (f : X B) (fs : Π (j : J), X objs j) (w : (j : J), fs j arrows j = f) (j : J) :
@[simp]
theorem category_theory.limits.wide_pullback.lift_base_assoc {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), objs j B) [category_theory.limits.has_wide_pullback B objs arrows] {X : C} (f : X B) (fs : Π (j : J), X objs j) (w : (j : J), fs j arrows j = f) {X' : C} (f' : B X') :
@[simp]
theorem category_theory.limits.wide_pullback.lift_base {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), objs j B) [category_theory.limits.has_wide_pullback B objs arrows] {X : C} (f : X B) (fs : Π (j : J), X objs j) (w : (j : J), fs j arrows j = f) :
theorem category_theory.limits.wide_pullback.eq_lift_of_comp_eq {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), objs j B) [category_theory.limits.has_wide_pullback B objs arrows] {X : C} (f : X B) (fs : Π (j : J), X objs j) (w : (j : J), fs j arrows j = f) (g : X category_theory.limits.wide_pullback B (λ (j : J), objs j) arrows) :
theorem category_theory.limits.wide_pullback.hom_eq_lift {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), objs j B) [category_theory.limits.has_wide_pullback B objs arrows] {X : C} (g : X category_theory.limits.wide_pullback B (λ (j : J), objs j) arrows) :
@[ext]
theorem category_theory.limits.wide_pullback.hom_ext {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), objs j B) [category_theory.limits.has_wide_pullback B objs arrows] {X : C} (g1 g2 : X category_theory.limits.wide_pullback B (λ (j : J), objs j) arrows) :
@[reducible]
noncomputable def category_theory.limits.wide_pushout.ι {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), B objs j) [category_theory.limits.has_wide_pushout B objs arrows] (j : J) :
objs j category_theory.limits.wide_pushout B (λ (j : J), objs j) arrows

The j-th inclusion to the pushout.

@[reducible]
noncomputable def category_theory.limits.wide_pushout.head {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), B objs j) [category_theory.limits.has_wide_pushout B objs arrows] :

The unique map from the head to the pushout.

@[simp]
theorem category_theory.limits.wide_pushout.arrow_ι_assoc {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), B objs j) [category_theory.limits.has_wide_pushout B objs arrows] (j : J) {X' : C} (f' : category_theory.limits.wide_pushout B (λ (j : J), objs j) arrows X') :
@[simp]
theorem category_theory.limits.wide_pushout.arrow_ι {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), B objs j) [category_theory.limits.has_wide_pushout B objs arrows] (j : J) :
@[reducible]
noncomputable def category_theory.limits.wide_pushout.desc {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} {arrows : Π (j : J), B objs j} [category_theory.limits.has_wide_pushout B objs arrows] {X : C} (f : B X) (fs : Π (j : J), objs j X) (w : (j : J), arrows j fs j = f) :
category_theory.limits.wide_pushout B (λ (j : J), objs j) arrows X

Descend a collection of morphisms to a morphism from the pushout.

@[simp]
theorem category_theory.limits.wide_pushout.ι_desc {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), B objs j) [category_theory.limits.has_wide_pushout B objs arrows] {X : C} (f : B X) (fs : Π (j : J), objs j X) (w : (j : J), arrows j fs j = f) (j : J) :
@[simp]
theorem category_theory.limits.wide_pushout.ι_desc_assoc {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), B objs j) [category_theory.limits.has_wide_pushout B objs arrows] {X : C} (f : B X) (fs : Π (j : J), objs j X) (w : (j : J), arrows j fs j = f) (j : J) {X' : C} (f' : X X') :
@[simp]
theorem category_theory.limits.wide_pushout.head_desc {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), B objs j) [category_theory.limits.has_wide_pushout B objs arrows] {X : C} (f : B X) (fs : Π (j : J), objs j X) (w : (j : J), arrows j fs j = f) :
@[simp]
theorem category_theory.limits.wide_pushout.head_desc_assoc {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), B objs j) [category_theory.limits.has_wide_pushout B objs arrows] {X : C} (f : B X) (fs : Π (j : J), objs j X) (w : (j : J), arrows j fs j = f) {X' : C} (f' : X X') :
theorem category_theory.limits.wide_pushout.eq_desc_of_comp_eq {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), B objs j) [category_theory.limits.has_wide_pushout B objs arrows] {X : C} (f : B X) (fs : Π (j : J), objs j X) (w : (j : J), arrows j fs j = f) (g : category_theory.limits.wide_pushout B (λ (j : J), objs j) arrows X) :
theorem category_theory.limits.wide_pushout.hom_eq_desc {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), B objs j) [category_theory.limits.has_wide_pushout B objs arrows] {X : C} (g : category_theory.limits.wide_pushout B (λ (j : J), objs j) arrows X) :
@[ext]
theorem category_theory.limits.wide_pushout.hom_ext {J : Type w} {C : Type u} [category_theory.category C] {B : C} {objs : J C} (arrows : Π (j : J), B objs j) [category_theory.limits.has_wide_pushout B objs arrows] {X : C} (g1 g2 : category_theory.limits.wide_pushout B (λ (j : J), objs j) arrows X) :

If a category has wide pullbacks on a higher universe level it also has wide pullbacks on a lower universe level.