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.

source
@[protected, instance]
def category_theory.limits.wide_pullback_shape.inhabited (J : Type w) :
inhabited (category_theory.limits.wide_pullback_shape J)
source
def category_theory.limits.wide_pullback_shape (J : Type w) :
Type w

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

Equations
Instances for category_theory.limits.wide_pullback_shape
source
@[protected, instance]
def category_theory.limits.wide_pushout_shape.inhabited (J : Type w) :
inhabited (category_theory.limits.wide_pushout_shape J)
source
def category_theory.limits.wide_pushout_shape (J : Type w) :
Type w

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

Equations
Instances for category_theory.limits.wide_pushout_shape
source
@[protected, nolint, instance]
def category_theory.limits.wide_pullback_shape.hom.decidable_eq {J : Type w} [a : decidable_eq J] (ᾰ ᾰ_1 : category_theory.limits.wide_pullback_shape J) :
decidable_eq (ᾰ.hom ᾰ_1)
source
inductive category_theory.limits.wide_pullback_shape.hom {J : Type w} :
category_theory.limits.wide_pullback_shape J → category_theory.limits.wide_pullback_shape J → Type w

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

Instances for category_theory.limits.wide_pullback_shape.hom
source
@[protected, instance]
def category_theory.limits.wide_pullback_shape.struct {J : Type w} :
category_theory.category_struct (category_theory.limits.wide_pullback_shape J)
Equations
source
@[protected, instance]
def category_theory.limits.wide_pullback_shape.hom.inhabited {J : Type w} :
inhabited (category_theory.limits.wide_pullback_shape.hom option.none option.none)
Equations
source
@[protected, instance]
def category_theory.limits.wide_pullback_shape.subsingleton_hom {J : Type w} :
quiver.is_thin (category_theory.limits.wide_pullback_shape J)
source
@[protected, instance]
def category_theory.limits.wide_pullback_shape.category {J : Type w} :
category_theory.small_category (category_theory.limits.wide_pullback_shape J)
Equations
source
@[simp]
theorem category_theory.limits.wide_pullback_shape.hom_id {J : Type w} (X : category_theory.limits.wide_pullback_shape J) :
category_theory.limits.wide_pullback_shape.hom.id X = 𝟙 X
source
@[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
source
def category_theory.limits.wide_pullback_shape.wide_cospan {J : Type w} {C : Type u} [category_theory.category C] (B : C) (objs : J → C) (arrows : Π (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
source
@[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) _ _ _
source
def category_theory.limits.wide_pullback_shape.diagram_iso_wide_cospan {J : Type w} {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

Equations
source
def category_theory.limits.wide_pullback_shape.mk_cone {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) :
category_theory.limits.cone F

Construct a cone over a wide cospan.

Equations
source
@[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
source
@[simp]
theorem category_theory.limits.wide_pullback_shape.mk_cone_X {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) :
(category_theory.limits.wide_pullback_shape.mk_cone f π w).X = X
source
def category_theory.limits.wide_pullback_shape.equivalence_of_equiv {J : Type w} (J' : Type w') (h : J ≃ J') :
category_theory.limits.wide_pullback_shape J ≌ category_theory.limits.wide_pullback_shape J'

Wide pullback diagrams of equivalent index types are equivlent.

Equations
source
def category_theory.limits.wide_pullback_shape.ulift_equivalence {J : Type w} :
category_theory.ulift_hom (ulift (category_theory.limits.wide_pullback_shape J)) ≌ category_theory.limits.wide_pullback_shape (ulift J)

Lifting universe and morphism levels preserves wide pullback diagrams.

Equations
source
@[protected, nolint, instance]
def category_theory.limits.wide_pushout_shape.hom.decidable_eq {J : Type w} [a : decidable_eq J] (ᾰ ᾰ_1 : category_theory.limits.wide_pushout_shape J) :
decidable_eq (ᾰ.hom ᾰ_1)
source
inductive category_theory.limits.wide_pushout_shape.hom {J : Type w} :
category_theory.limits.wide_pushout_shape J → category_theory.limits.wide_pushout_shape J → Type w

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

Instances for category_theory.limits.wide_pushout_shape.hom
source
@[protected, instance]
def category_theory.limits.wide_pushout_shape.struct {J : Type w} :
category_theory.category_struct (category_theory.limits.wide_pushout_shape J)
Equations
source
@[protected, instance]
def category_theory.limits.wide_pushout_shape.hom.inhabited {J : Type w} :
inhabited (category_theory.limits.wide_pushout_shape.hom option.none option.none)
Equations
source
@[protected, instance]
def category_theory.limits.wide_pushout_shape.subsingleton_hom {J : Type w} :
quiver.is_thin (category_theory.limits.wide_pushout_shape J)
source
@[protected, instance]
def category_theory.limits.wide_pushout_shape.category {J : Type w} :
category_theory.small_category (category_theory.limits.wide_pushout_shape J)
Equations
source
@[simp]
theorem category_theory.limits.wide_pushout_shape.hom_id {J : Type w} (X : category_theory.limits.wide_pushout_shape J) :
category_theory.limits.wide_pushout_shape.hom.id X = 𝟙 X
source
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) :
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
source
@[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) _ _ _
source
@[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
source
def category_theory.limits.wide_pushout_shape.diagram_iso_wide_span {J : Type w} {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

Equations
source
def category_theory.limits.wide_pushout_shape.mk_cocone {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) :
category_theory.limits.cocone F

Construct a cocone over a wide span.

Equations
source
@[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
source
@[simp]
theorem category_theory.limits.wide_pushout_shape.mk_cocone_X {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) :
(category_theory.limits.wide_pushout_shape.mk_cocone f ι w).X = X
source
@[reducible]
def category_theory.limits.has_wide_pullbacks (C : Type u) [category_theory.category C] :
Prop

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

source
@[reducible]
def category_theory.limits.has_wide_pushouts (C : Type u) [category_theory.category C] :
Prop

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

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

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

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

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

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

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

source
@[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) :
category_theory.limits.wide_pullback.π arrows j ≫ arrows j = category_theory.limits.wide_pullback.base arrows
source
@[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') :
category_theory.limits.wide_pullback.π arrows j ≫ arrows j ≫ f' = category_theory.limits.wide_pullback.base arrows ≫ f'
source
@[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.

source
@[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') :
category_theory.limits.wide_pullback.lift f fs w ≫ category_theory.limits.wide_pullback.π arrows j ≫ f' = fs j ≫ f'
source
@[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) :
category_theory.limits.wide_pullback.lift f fs w ≫ category_theory.limits.wide_pullback.π arrows j = fs j
source
@[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') :
category_theory.limits.wide_pullback.lift f fs w ≫ category_theory.limits.wide_pullback.base arrows ≫ f' = f ≫ f'
source
@[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) :
category_theory.limits.wide_pullback.lift f fs w ≫ category_theory.limits.wide_pullback.base arrows = f
source
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) :
(∀ (j : J), g ≫ category_theory.limits.wide_pullback.π arrows j = fs j) → g ≫ category_theory.limits.wide_pullback.base arrows = f → g = category_theory.limits.wide_pullback.lift f fs w
source
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) :
g = category_theory.limits.wide_pullback.lift (g ≫ category_theory.limits.wide_pullback.base arrows) (λ (j : J), g ≫ category_theory.limits.wide_pullback.π arrows j) _
source
@[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) :
(∀ (j : J), g1 ≫ category_theory.limits.wide_pullback.π arrows j = g2 ≫ category_theory.limits.wide_pullback.π arrows j) → g1 ≫ category_theory.limits.wide_pullback.base arrows = g2 ≫ category_theory.limits.wide_pullback.base arrows → g1 = g2
source
@[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.

source
@[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] :
B ⟶ category_theory.limits.wide_pushout B objs arrows

The unique map from the head to the pushout.

source
@[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') :
arrows j ≫ category_theory.limits.wide_pushout.ι arrows j ≫ f' = category_theory.limits.wide_pushout.head arrows ≫ f'
source
@[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) :
arrows j ≫ category_theory.limits.wide_pushout.ι arrows j = category_theory.limits.wide_pushout.head arrows
source
@[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.

source
@[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) :
category_theory.limits.wide_pushout.ι arrows j ≫ category_theory.limits.wide_pushout.desc f fs w = fs j
source
@[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') :
category_theory.limits.wide_pushout.ι arrows j ≫ category_theory.limits.wide_pushout.desc f fs w ≫ f' = fs j ≫ f'
source
@[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) :
category_theory.limits.wide_pushout.head arrows ≫ category_theory.limits.wide_pushout.desc f fs w = f
source
@[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') :
category_theory.limits.wide_pushout.head arrows ≫ category_theory.limits.wide_pushout.desc f fs w ≫ f' = f ≫ f'
source
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) :
(∀ (j : J), category_theory.limits.wide_pushout.ι arrows j ≫ g = fs j) → category_theory.limits.wide_pushout.head arrows ≫ g = f → g = category_theory.limits.wide_pushout.desc f fs w
source
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) :
g = category_theory.limits.wide_pushout.desc (category_theory.limits.wide_pushout.head arrows ≫ g) (λ (j : J), category_theory.limits.wide_pushout.ι arrows j ≫ g) _
source
@[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) :
(∀ (j : J), category_theory.limits.wide_pushout.ι arrows j ≫ g1 = category_theory.limits.wide_pushout.ι arrows j ≫ g2) → category_theory.limits.wide_pushout.head arrows ≫ g1 = category_theory.limits.wide_pushout.head arrows ≫ g2 → g1 = g2
source
def category_theory.limits.wide_pullback_shape_op_map (J : Type w) (X Y : category_theory.limits.wide_pullback_shape J) :
(X ⟶ Y) → (opposite.op X ⟶ opposite.op Y)

The action on morphisms of the obvious functor wide_pullback_shape_op : wide_pullback_shape J ⥤ (wide_pushout_shape J)ᵒᵖ

Equations
source
@[simp]
theorem category_theory.limits.wide_pullback_shape_op_obj (J : Type w) (X : category_theory.limits.wide_pullback_shape J) :
(category_theory.limits.wide_pullback_shape_op J).obj X = opposite.op X
source
def category_theory.limits.wide_pullback_shape_op (J : Type w) :
category_theory.limits.wide_pullback_shape J ⥤ (category_theory.limits.wide_pushout_shape J)ᵒᵖ

The obvious functor wide_pullback_shape J ⥤ (wide_pushout_shape J)ᵒᵖ

Equations
source
@[simp]
theorem category_theory.limits.wide_pullback_shape_op_map_2 (J : Type w) (X Y : category_theory.limits.wide_pullback_shape J) (ᾰ : X ⟶ Y) :
(category_theory.limits.wide_pullback_shape_op J).map ᾰ = category_theory.limits.wide_pullback_shape_op_map J X Y ᾰ
source
def category_theory.limits.wide_pushout_shape_op_map (J : Type w) (X Y : category_theory.limits.wide_pushout_shape J) :
(X ⟶ Y) → (opposite.op X ⟶ opposite.op Y)

The action on morphisms of the obvious functor wide_pushout_shape_op :wide_pushout_shape J ⥤ (wide_pullback_shape J)ᵒᵖ`

Equations
source
def category_theory.limits.wide_pushout_shape_op (J : Type w) :
category_theory.limits.wide_pushout_shape J ⥤ (category_theory.limits.wide_pullback_shape J)ᵒᵖ

The obvious functor wide_pushout_shape J ⥤ (wide_pullback_shape J)ᵒᵖ

Equations
source
@[simp]
theorem category_theory.limits.wide_pushout_shape_op_map_2 (J : Type w) (X Y : category_theory.limits.wide_pushout_shape J) (ᾰ : X ⟶ Y) :
(category_theory.limits.wide_pushout_shape_op J).map ᾰ = category_theory.limits.wide_pushout_shape_op_map J X Y ᾰ
source
@[simp]
theorem category_theory.limits.wide_pushout_shape_op_obj (J : Type w) (X : category_theory.limits.wide_pushout_shape J) :
(category_theory.limits.wide_pushout_shape_op J).obj X = opposite.op X
source
@[simp]
theorem category_theory.limits.wide_pullback_shape_unop_map (J : Type w) (X Y : (category_theory.limits.wide_pullback_shape J)ᵒᵖ) (f : X ⟶ Y) :
(category_theory.limits.wide_pullback_shape_unop J).map f = (category_theory.limits.wide_pullback_shape_op_map J (opposite.unop Y) (opposite.unop X) f.unop).unop
source
@[simp]
theorem category_theory.limits.wide_pullback_shape_unop_obj (J : Type w) (X : (category_theory.limits.wide_pullback_shape J)ᵒᵖ) :
(category_theory.limits.wide_pullback_shape_unop J).obj X = opposite.unop X
source
def category_theory.limits.wide_pullback_shape_unop (J : Type w) :
(category_theory.limits.wide_pullback_shape J)ᵒᵖ ⥤ category_theory.limits.wide_pushout_shape J

The obvious functor (wide_pullback_shape J)ᵒᵖ ⥤ wide_pushout_shape J

Equations
source
def category_theory.limits.wide_pushout_shape_unop (J : Type w) :
(category_theory.limits.wide_pushout_shape J)ᵒᵖ ⥤ category_theory.limits.wide_pullback_shape J

The obvious functor (wide_pushout_shape J)ᵒᵖ ⥤ wide_pullback_shape J

Equations
source
@[simp]
theorem category_theory.limits.wide_pushout_shape_unop_map (J : Type w) (X Y : (category_theory.limits.wide_pushout_shape J)ᵒᵖ) (f : X ⟶ Y) :
(category_theory.limits.wide_pushout_shape_unop J).map f = (category_theory.limits.wide_pushout_shape_op_map J (opposite.unop Y) (opposite.unop X) f.unop).unop
source
@[simp]
theorem category_theory.limits.wide_pushout_shape_unop_obj (J : Type w) (X : (category_theory.limits.wide_pushout_shape J)ᵒᵖ) :
(category_theory.limits.wide_pushout_shape_unop J).obj X = opposite.unop X
source
def category_theory.limits.wide_pushout_shape_op_unop (J : Type w) :
category_theory.limits.wide_pushout_shape_unop J ⋙ category_theory.limits.wide_pullback_shape_op J ≅ 𝟭 (category_theory.limits.wide_pushout_shape J)ᵒᵖ

The inverse of the unit isomorphism of the equivalence wide_pushout_shape_op_equiv : (wide_pushout_shape J)ᵒᵖ ≌ wide_pullback_shape J

Equations
source
def category_theory.limits.wide_pushout_shape_unop_op (J : Type w) :
category_theory.limits.wide_pushout_shape_op J ⋙ category_theory.limits.wide_pullback_shape_unop J ≅ 𝟭 (category_theory.limits.wide_pushout_shape J)

The counit isomorphism of the equivalence wide_pullback_shape_op_equiv : (wide_pullback_shape J)ᵒᵖ ≌ wide_pushout_shape J

Equations
source
def category_theory.limits.wide_pullback_shape_op_unop (J : Type w) :
category_theory.limits.wide_pullback_shape_unop J ⋙ category_theory.limits.wide_pushout_shape_op J ≅ 𝟭 (category_theory.limits.wide_pullback_shape J)ᵒᵖ

The inverse of the unit isomorphism of the equivalence wide_pullback_shape_op_equiv : (wide_pullback_shape J)ᵒᵖ ≌ wide_pushout_shape J

Equations
source
def category_theory.limits.wide_pullback_shape_unop_op (J : Type w) :
category_theory.limits.wide_pullback_shape_op J ⋙ category_theory.limits.wide_pushout_shape_unop J ≅ 𝟭 (category_theory.limits.wide_pullback_shape J)

The counit isomorphism of the equivalence wide_pushout_shape_op_equiv : (wide_pushout_shape J)ᵒᵖ ≌ wide_pullback_shape J

Equations
source
@[simp]
theorem category_theory.limits.wide_pushout_shape_op_equiv_inverse (J : Type w) :
(category_theory.limits.wide_pushout_shape_op_equiv J).inverse = category_theory.limits.wide_pullback_shape_op J
source
@[simp]
theorem category_theory.limits.wide_pushout_shape_op_equiv_functor (J : Type w) :
(category_theory.limits.wide_pushout_shape_op_equiv J).functor = category_theory.limits.wide_pushout_shape_unop J
source
@[simp]
theorem category_theory.limits.wide_pushout_shape_op_equiv_counit_iso (J : Type w) :
(category_theory.limits.wide_pushout_shape_op_equiv J).counit_iso = category_theory.limits.wide_pullback_shape_unop_op J
source
@[simp]
theorem category_theory.limits.wide_pushout_shape_op_equiv_unit_iso (J : Type w) :
(category_theory.limits.wide_pushout_shape_op_equiv J).unit_iso = (category_theory.limits.wide_pushout_shape_op_unop J).symm
source
def category_theory.limits.wide_pushout_shape_op_equiv (J : Type w) :
(category_theory.limits.wide_pushout_shape J)ᵒᵖ ≌ category_theory.limits.wide_pullback_shape J

The duality equivalence (wide_pushout_shape J)ᵒᵖ ≌ wide_pullback_shape J

Equations
source
@[simp]
theorem category_theory.limits.wide_pullback_shape_op_equiv_functor (J : Type w) :
(category_theory.limits.wide_pullback_shape_op_equiv J).functor = category_theory.limits.wide_pullback_shape_unop J
source
@[simp]
theorem category_theory.limits.wide_pullback_shape_op_equiv_unit_iso (J : Type w) :
(category_theory.limits.wide_pullback_shape_op_equiv J).unit_iso = (category_theory.limits.wide_pullback_shape_op_unop J).symm
source
@[simp]
theorem category_theory.limits.wide_pullback_shape_op_equiv_inverse (J : Type w) :
(category_theory.limits.wide_pullback_shape_op_equiv J).inverse = category_theory.limits.wide_pushout_shape_op J
source
@[simp]
theorem category_theory.limits.wide_pullback_shape_op_equiv_counit_iso (J : Type w) :
(category_theory.limits.wide_pullback_shape_op_equiv J).counit_iso = category_theory.limits.wide_pushout_shape_unop_op J
source
def category_theory.limits.wide_pullback_shape_op_equiv (J : Type w) :
(category_theory.limits.wide_pullback_shape J)ᵒᵖ ≌ category_theory.limits.wide_pushout_shape J

The duality equivalence (wide_pullback_shape J)ᵒᵖ ≌ wide_pushout_shape J

Equations
source
theorem category_theory.limits.has_wide_pullbacks_shrink (C : Type u) [category_theory.category C] [category_theory.limits.has_wide_pullbacks C] :
category_theory.limits.has_wide_pullbacks C

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