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.
@[instance]
A wide pullback shape for any type J can be written simply as option J.
Equations
A wide pushout shape for any type J can be written simply as option J.
Equations
@[instance]
@[nolint, instance]
def
category_theory.limits.wide_pullback_shape.hom.decidable_eq
{J : Type v}
[a : decidable_eq J]
(a_1 a_2 : category_theory.limits.wide_pullback_shape J) :
decidable_eq (a_1.hom a_2)
- id : Π {J : Type v} (X : category_theory.limits.wide_pullback_shape J), X.hom X
- term : Π {J : Type v} (j : J), category_theory.limits.wide_pullback_shape.hom (option.some j) option.none
The type of arrows for the shape indexing a wide pullback.
@[instance]
Equations
- category_theory.limits.wide_pullback_shape.struct = {to_has_hom := {hom := category_theory.limits.wide_pullback_shape.hom J}, id := λ (j : category_theory.limits.wide_pullback_shape J), category_theory.limits.wide_pullback_shape.hom.id j, comp := λ (j₁ j₂ j₃ : category_theory.limits.wide_pullback_shape J) (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃), category_theory.limits.wide_pullback_shape.hom.cases_on f (λ (f_1 : category_theory.limits.wide_pullback_shape J) (H_1 : j₁ = f_1), eq.rec (λ (H_2 : j₂ = j₁), eq.rec (λ (f : j₁ ⟶ j₁) (g : j₁ ⟶ j₃) (H_3 : f == category_theory.limits.wide_pullback_shape.hom.id j₁), eq.rec g _) _ f g) H_1) (λ (f_1 : J) (H_1 : j₁ = option.some f_1), eq.rec (λ (f : option.some f_1 ⟶ j₂) (H_2 : j₂ = option.none), eq.rec (λ (g : option.none ⟶ j₃) (f : option.some f_1 ⟶ option.none) (H_3 : f == category_theory.limits.wide_pullback_shape.hom.term f_1), eq.rec (category_theory.limits.wide_pullback_shape.hom.cases_on g (λ (g_1 : category_theory.limits.wide_pullback_shape J) (H_1 : option.none = g_1), eq.rec (λ (H_2 : j₃ = option.none), eq.rec (λ (g : option.none ⟶ option.none) (H_3 : g == category_theory.limits.wide_pullback_shape.hom.id option.none), eq.rec (category_theory.limits.wide_pullback_shape.hom.term f_1) _) _ g) H_1) (λ (g_1 : J) (H_1 : option.none = option.some g_1), option.no_confusion H_1) category_theory.limits.wide_pullback_shape.struct._proof_5 _ _) _) _ g f) _ f) _ _ _}
@[instance]
@[instance]
def
category_theory.limits.wide_pullback_shape.subsingleton_hom
{J : Type v}
(j j' : category_theory.limits.wide_pullback_shape J) :
subsingleton (j ⟶ j')
Equations
- _ = _
@[simp]
theorem
category_theory.limits.wide_pullback_shape.hom_id
{J : Type v}
(X : category_theory.limits.wide_pullback_shape J) :
@[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
@[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 = 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) _ _ _
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
- category_theory.limits.wide_pullback_shape.wide_cospan B objs arrows = {obj := λ (j : category_theory.limits.wide_pullback_shape J), option.cases_on j B objs, map := λ (X Y : category_theory.limits.wide_pullback_shape J) (f : X ⟶ Y), 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) _ _ _, map_id' := _, map_comp' := _}
def
category_theory.limits.wide_pullback_shape.diagram_iso_wide_cospan
{J : Type v}
{C : Type u}
[category_theory.category C]
(F : category_theory.limits.wide_pullback_shape J ⥤ C) :
F ≅ category_theory.limits.wide_pullback_shape.wide_cospan (F.obj option.none) (λ (j : J), F.obj (option.some j)) (λ (j : J), F.map (category_theory.limits.wide_pullback_shape.hom.term j))
Every diagram is naturally isomorphic (actually, equal) to a wide_cospan
@[nolint, instance]
def
category_theory.limits.wide_pushout_shape.hom.decidable_eq
{J : Type v}
[a : decidable_eq J]
(a_1 a_2 : category_theory.limits.wide_pushout_shape J) :
decidable_eq (a_1.hom a_2)
- id : Π {J : Type v} (X : category_theory.limits.wide_pushout_shape J), X.hom X
- init : Π {J : Type v} (j : J), category_theory.limits.wide_pushout_shape.hom option.none (option.some j)
The type of arrows for the shape indexing a wide psuhout.
@[instance]
Equations
- category_theory.limits.wide_pushout_shape.struct = {to_has_hom := {hom := category_theory.limits.wide_pushout_shape.hom J}, id := λ (j : category_theory.limits.wide_pushout_shape J), category_theory.limits.wide_pushout_shape.hom.id j, comp := λ (j₁ j₂ j₃ : category_theory.limits.wide_pushout_shape J) (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃), category_theory.limits.wide_pushout_shape.hom.cases_on f (λ (f_1 : category_theory.limits.wide_pushout_shape J) (H_1 : j₁ = f_1), eq.rec (λ (H_2 : j₂ = j₁), eq.rec (λ (f : j₁ ⟶ j₁) (g : j₁ ⟶ j₃) (H_3 : f == category_theory.limits.wide_pushout_shape.hom.id j₁), eq.rec g _) _ f g) H_1) (λ (f_1 : J) (H_1 : j₁ = option.none), eq.rec (λ (f : option.none ⟶ j₂) (H_2 : j₂ = option.some f_1), eq.rec (λ (g : option.some f_1 ⟶ j₃) (f : option.none ⟶ option.some f_1) (H_3 : f == category_theory.limits.wide_pushout_shape.hom.init f_1), eq.rec (category_theory.limits.wide_pushout_shape.hom.cases_on g (λ (g_1 : category_theory.limits.wide_pushout_shape J) (H_1 : option.some f_1 = g_1), eq.rec (λ (H_2 : j₃ = option.some f_1), eq.rec (λ (g : option.some f_1 ⟶ option.some f_1) (H_3 : g == category_theory.limits.wide_pushout_shape.hom.id (option.some f_1)), eq.rec (category_theory.limits.wide_pushout_shape.hom.init f_1) _) _ g) H_1) (λ (g_1 : J) (H_1 : option.some f_1 = option.none), option.no_confusion H_1) _ _ _) _) _ g f) _ f) _ _ _}
@[instance]
@[instance]
def
category_theory.limits.wide_pushout_shape.subsingleton_hom
{J : Type v}
(j j' : category_theory.limits.wide_pushout_shape J) :
subsingleton (j ⟶ j')
Equations
- _ = _
@[simp]
theorem
category_theory.limits.wide_pushout_shape.hom_id
{J : Type v}
(X : category_theory.limits.wide_pushout_shape J) :
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
- category_theory.limits.wide_pushout_shape.wide_span B objs arrows = {obj := λ (j : category_theory.limits.wide_pushout_shape J), option.cases_on j B objs, map := λ (X Y : category_theory.limits.wide_pushout_shape J) (f : X ⟶ Y), 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) _ _ _, map_id' := _, map_comp' := _}
@[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 = 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 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
def
category_theory.limits.wide_pushout_shape.diagram_iso_wide_span
{J : Type v}
{C : Type u}
[category_theory.category C]
(F : category_theory.limits.wide_pushout_shape J ⥤ C) :
F ≅ category_theory.limits.wide_pushout_shape.wide_span (F.obj option.none) (λ (j : J), F.obj (option.some j)) (λ (j : J), F.map (category_theory.limits.wide_pushout_shape.hom.init j))
Every diagram is naturally isomorphic (actually, equal) to a wide_span
def
category_theory.limits.has_wide_pullbacks
(C : Type u)
[category_theory.category C] :
Type (max (v+1) u)
has_wide_pullbacks represents a choice of wide pullback for every collection of morphisms
def
category_theory.limits.has_wide_pushouts
(C : Type u)
[category_theory.category C] :
Type (max (v+1) u)
has_wide_pushouts represents a choice of wide pushout for every collection of morphisms