Wide pullbacks

We define the category WidePullbackShape, (resp. WidePushoutShape) 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 wideCospan (wideSpan) constructs a functor from this category, hitting the given morphisms.

We use WidePullbackShape to define ordinary pullbacks (pushouts) by using J := WalkingPair, 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 HasWidePullbacks and HasFiniteWidePullbacks assert the existence of wide pullbacks and finite wide pullbacks.

@[implicit_reducible]

def CategoryTheory.Limits.WidePullbackShape (J : Type w) : Type w

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

@[implicit_reducible]

def CategoryTheory.Limits.WidePushoutShape (J : Type w) : Type w

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

@[instance_reducible]

instance CategoryTheory.Limits.instInhabitedWidePullbackShape (J : Type w) : Inhabited (WidePullbackShape J)

@[instance_reducible]

instance CategoryTheory.Limits.instInhabitedWidePushoutShape (J : Type w) : Inhabited (WidePushoutShape J)

inductive CategoryTheory.Limits.WidePushoutShape.Hom {J : Type w} : WidePushoutShape J → WidePushoutShape J → Type w

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

• id {J : Type w} (X : WidePushoutShape J) : X.Hom X
• init {J : Type w} (j : J) : Hom none (some j)

@[instance_reducible]

instance CategoryTheory.Limits.WidePushoutShape.instDecidableEqHom {J✝ : Type u_1} {a✝ a✝¹ : WidePushoutShape J✝} [DecidableEq J✝] : DecidableEq (a✝.Hom a✝¹)

def CategoryTheory.Limits.WidePushoutShape.instDecidableEqHom.decEq {J✝ : Type u_1} {a✝ a✝¹ : WidePushoutShape J✝} [DecidableEq J✝] (x✝ x✝¹ : a✝.Hom a✝¹) : Decidable (x✝ = x✝¹)

inductive CategoryTheory.Limits.WidePullbackShape.Hom {J : Type w} : WidePullbackShape J → WidePullbackShape J → Type w

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

• id {J : Type w} (X : WidePullbackShape J) : X.Hom X
• term {J : Type w} (j : J) : Hom (some j) none

@[instance_reducible]

instance CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom {J✝ : Type u_1} {a✝ a✝¹ : WidePullbackShape J✝} [DecidableEq J✝] : DecidableEq (a✝.Hom a✝¹)

def CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom.decEq {J✝ : Type u_1} {a✝ a✝¹ : WidePullbackShape J✝} [DecidableEq J✝] (x✝ x✝¹ : a✝.Hom a✝¹) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance CategoryTheory.Limits.WidePullbackShape.struct {J : Type w} : CategoryStruct.{w, w} (WidePullbackShape J)

@[instance_reducible]

instance CategoryTheory.Limits.WidePushoutShape.struct {J : Type w} : CategoryStruct.{w, w} (WidePushoutShape J)

@[instance_reducible]

instance CategoryTheory.Limits.WidePullbackShape.Hom.inhabited {J : Type w} : Inhabited (Hom none none)

@[instance_reducible]

instance CategoryTheory.Limits.WidePushoutShape.Hom.inhabited {J : Type w} : Inhabited (Hom none none)

instance CategoryTheory.Limits.WidePullbackShape.subsingleton_hom {J : Type w} : Quiver.IsThin (WidePullbackShape J)

instance CategoryTheory.Limits.WidePushoutShape.subsingleton_hom {J : Type w} : Quiver.IsThin (WidePushoutShape J)

@[instance_reducible]

instance CategoryTheory.Limits.WidePullbackShape.category {J : Type w} : SmallCategory (WidePullbackShape J)

@[instance_reducible]

instance CategoryTheory.Limits.WidePushoutShape.category {J : Type w} : SmallCategory (WidePushoutShape J)

@[simp]

theorem CategoryTheory.Limits.WidePullbackShape.hom_id {J : Type w} (X : WidePullbackShape J) : Hom.id X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.WidePushoutShape.hom_id {J : Type w} (X : WidePushoutShape J) : Hom.id X = CategoryStruct.id X

@[implicit_reducible]

def CategoryTheory.Limits.WidePullbackShape.wideCospan {J : Type w} {C : Type u} [Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → objs j ⟶ B) : Functor (WidePullbackShape J) C

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

@[implicit_reducible]

def CategoryTheory.Limits.WidePushoutShape.wideSpan {J : Type w} {C : Type u} [Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → B ⟶ objs j) : Functor (WidePushoutShape J) C

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

@[simp]

theorem CategoryTheory.Limits.WidePullbackShape.wideCospan_obj {J : Type w} {C : Type u} [Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → objs j ⟶ B) (j : WidePullbackShape J) : (wideCospan B objs arrows).obj j = Option.casesOn j B objs

@[simp]

theorem CategoryTheory.Limits.WidePullbackShape.wideCospan_map {J : Type w} {C : Type u} [Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → objs j ⟶ B) {X✝ Y✝ : WidePullbackShape J} (x✝ : X✝ ⟶ Y✝) : (wideCospan B objs arrows).map x✝ = match Y✝, X✝, x✝ with | X, .(X), Hom.id .(X) => CategoryStruct.id (Option.casesOn X B objs) | .(none), .(some j), Hom.term j => arrows j

@[simp]

theorem CategoryTheory.Limits.WidePushoutShape.wideSpan_map {J : Type w} {C : Type u} [Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → B ⟶ objs j) {Y✝ X✝ : WidePushoutShape J} (x✝ : Y✝ ⟶ X✝) : (wideSpan B objs arrows).map x✝ = match Y✝, X✝, x✝ with | X, .(X), Hom.id .(X) => CategoryStruct.id (Option.casesOn X B objs) | .(none), .(some j), Hom.init j => arrows j

@[simp]

theorem CategoryTheory.Limits.WidePushoutShape.wideSpan_obj {J : Type w} {C : Type u} [Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → B ⟶ objs j) (j : WidePushoutShape J) : (wideSpan B objs arrows).obj j = Option.casesOn j B objs

def CategoryTheory.Limits.WidePullbackShape.diagramIsoWideCospan {J : Type w} {C : Type u} [Category.{v, u} C] (F : Functor (WidePullbackShape J) C) : F ≅ wideCospan (F.obj none) (fun (j : J) => F.obj (some j)) fun (j : J) => F.map (Hom.term j)

Every diagram is naturally isomorphic (actually, equal) to a wideCospan

def CategoryTheory.Limits.WidePushoutShape.diagramIsoWideSpan {J : Type w} {C : Type u} [Category.{v, u} C] (F : Functor (WidePushoutShape J) C) : F ≅ wideSpan (F.obj none) (fun (j : J) => F.obj (some j)) fun (j : J) => F.map (Hom.init j)

Every diagram is naturally isomorphic (actually, equal) to a wideSpan

@[implicit_reducible]

def CategoryTheory.Limits.WidePullbackShape.mkCone {J : Type w} {C : Type u} [Category.{v, u} C] {F : Functor (WidePullbackShape J) C} {X : C} (f : X ⟶ F.obj none) (π : (j : J) → X ⟶ F.obj (some j)) (w : ∀ (j : J), CategoryStruct.comp (π j) (F.map (Hom.term j)) = f) : Cone F

Construct a cone over a wide cospan.

@[implicit_reducible]

def CategoryTheory.Limits.WidePushoutShape.mkCocone {J : Type w} {C : Type u} [Category.{v, u} C] {F : Functor (WidePushoutShape J) C} {X : C} (f : F.obj none ⟶ X) (π : (j : J) → F.obj (some j) ⟶ X) (w : ∀ (j : J), CategoryStruct.comp (F.map (Hom.init j)) (π j) = f) : Cocone F

Construct a cocone over a wide span.

@[simp]

theorem CategoryTheory.Limits.WidePushoutShape.mkCocone_pt {J : Type w} {C : Type u} [Category.{v, u} C] {F : Functor (WidePushoutShape J) C} {X : C} (f : F.obj none ⟶ X) (π : (j : J) → F.obj (some j) ⟶ X) (w : ∀ (j : J), CategoryStruct.comp (F.map (Hom.init j)) (π j) = f) : (mkCocone f π w).pt = X

@[simp]

theorem CategoryTheory.Limits.WidePullbackShape.mkCone_pt {J : Type w} {C : Type u} [Category.{v, u} C] {F : Functor (WidePullbackShape J) C} {X : C} (f : X ⟶ F.obj none) (π : (j : J) → X ⟶ F.obj (some j)) (w : ∀ (j : J), CategoryStruct.comp (π j) (F.map (Hom.term j)) = f) : (mkCone f π w).pt = X

@[simp]

theorem CategoryTheory.Limits.WidePushoutShape.mkCocone_ι_app {J : Type w} {C : Type u} [Category.{v, u} C] {F : Functor (WidePushoutShape J) C} {X : C} (f : F.obj none ⟶ X) (π : (j : J) → F.obj (some j) ⟶ X) (w : ∀ (j : J), CategoryStruct.comp (F.map (Hom.init j)) (π j) = f) (j : WidePushoutShape J) : (mkCocone f π w).ι.app j = match j with | none => f | some j => π j

@[simp]

theorem CategoryTheory.Limits.WidePullbackShape.mkCone_π_app {J : Type w} {C : Type u} [Category.{v, u} C] {F : Functor (WidePullbackShape J) C} {X : C} (f : X ⟶ F.obj none) (π : (j : J) → X ⟶ F.obj (some j)) (w : ∀ (j : J), CategoryStruct.comp (π j) (F.map (Hom.term j)) = f) (j : WidePullbackShape J) : (mkCone f π w).π.app j = match j with | none => f | some j => π j

def CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv {J : Type w} (J' : Type w') (h : J ≃ J') : WidePullbackShape J ≌ WidePullbackShape J'

Wide pullback diagrams of equivalent index types are equivalent.

def CategoryTheory.Limits.WidePushoutShape.equivalenceOfEquiv {J : Type w} (J' : Type w') (h : J ≃ J') : WidePushoutShape J ≌ WidePushoutShape J'

Wide pushout diagrams of equivalent index types are equivalent.

@[simp]

theorem CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv_functor_obj_none {ι : Type u_1} {ι' : Type u_2} (e : ι ≃ ι') : (equivalenceOfEquiv ι' e).functor.obj none = none

@[simp]

theorem CategoryTheory.Limits.WidePushoutShape.equivalenceOfEquiv_functor_obj_none {ι : Type u_1} {ι' : Type u_2} (e : ι ≃ ι') : (equivalenceOfEquiv ι' e).functor.obj none = none

@[simp]

theorem CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv_functor_obj_some {ι : Type u_1} {ι' : Type u_2} (e : ι ≃ ι') (i : ι) : (equivalenceOfEquiv ι' e).functor.obj (some i) = some (e i)

@[simp]

theorem CategoryTheory.Limits.WidePushoutShape.equivalenceOfEquiv_functor_obj_some {ι : Type u_1} {ι' : Type u_2} (e : ι ≃ ι') (i : ι) : (equivalenceOfEquiv ι' e).functor.obj (some i) = some (e i)

@[simp]

theorem CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv_functor_map_term {ι : Type u_1} {ι' : Type u_2} (e : ι ≃ ι') (i : ι) : (equivalenceOfEquiv ι' e).functor.map (Hom.term i) = Hom.term (e i)

@[simp]

theorem CategoryTheory.Limits.WidePushoutShape.equivalenceOfEquiv_functor_map_init {ι : Type u_1} {ι' : Type u_2} (e : ι ≃ ι') (i : ι) : (equivalenceOfEquiv ι' e).functor.map (Hom.init i) = Hom.init (e i)

def CategoryTheory.Limits.WidePullbackShape.uliftEquivalence {J : Type w} : ULiftHom (ULift.{w', w} (WidePullbackShape J)) ≌ WidePullbackShape (ULift.{w', w} J)

Lifting universe and morphism levels preserves wide pullback diagrams.

def CategoryTheory.Limits.WidePushoutShape.uliftEquivalence {J : Type w} : ULiftHom (ULift.{w', w} (WidePushoutShape J)) ≌ WidePushoutShape (ULift.{w', w} J)

Lifting universe and morphism levels preserves wide pushout diagrams.

def CategoryTheory.Limits.WidePullbackShape.functorExt {C : Type u} [Category.{v, u} C] {ι : Type u_1} {F G : Functor (WidePullbackShape ι) C} (base : F.obj none ≅ G.obj none) (comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)) (w : ∀ (i : ι), CategoryStruct.comp (F.map (Hom.term i)) base.hom = CategoryStruct.comp (comp i).hom (G.map (Hom.term i)) := by cat_disch) : F ≅ G

Show two functors out of a wide pullback shape are isomorphic by showing their components are isomorphic.

@[simp]

theorem CategoryTheory.Limits.WidePullbackShape.functorExt_hom_app {C : Type u} [Category.{v, u} C] {ι : Type u_1} {F G : Functor (WidePullbackShape ι) C} (base : F.obj none ≅ G.obj none) (comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)) (w : ∀ (i : ι), CategoryStruct.comp (F.map (Hom.term i)) base.hom = CategoryStruct.comp (comp i).hom (G.map (Hom.term i)) := by cat_disch) (X : WidePullbackShape ι) : (functorExt base comp w).hom.app X = (match X with | none => base | some i => comp i).hom

@[simp]

theorem CategoryTheory.Limits.WidePullbackShape.functorExt_inv_app {C : Type u} [Category.{v, u} C] {ι : Type u_1} {F G : Functor (WidePullbackShape ι) C} (base : F.obj none ≅ G.obj none) (comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)) (w : ∀ (i : ι), CategoryStruct.comp (F.map (Hom.term i)) base.hom = CategoryStruct.comp (comp i).hom (G.map (Hom.term i)) := by cat_disch) (X : WidePullbackShape ι) : (functorExt base comp w).inv.app X = (match X with | none => base | some i => comp i).inv

@[reducible, inline]

abbrev CategoryTheory.Limits.HasWidePullbacks (C : Type u) [Category.{v, u} C] : Prop

A category HasWidePullbacks if it has all limits of shape WidePullbackShape J, i.e. if it has a wide pullback for every collection of morphisms with the same codomain.

@[reducible, inline]

abbrev CategoryTheory.Limits.HasWidePushouts (C : Type u) [Category.{v, u} C] : Prop

A category HasWidePushouts if it has all colimits of shape WidePushoutShape J, i.e. if it has a wide pushout for every collection of morphisms with the same domain.

@[reducible, inline]

abbrev CategoryTheory.Limits.HasWidePullback {J : Type w} {C : Type u} [Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → objs j ⟶ B) : Prop

HasWidePullback B objs arrows means that wideCospan B objs arrows has a limit.

@[reducible, inline]

abbrev CategoryTheory.Limits.HasWidePushout {J : Type w} {C : Type u} [Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → B ⟶ objs j) : Prop

HasWidePushout B objs arrows means that wideSpan B objs arrows has a colimit.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.widePullback {J : Type w} {C : Type u} [Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → objs j ⟶ B) [HasWidePullback B objs arrows] : C

A choice of wide pullback.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.widePushout {J : Type w} {C : Type u} [Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → B ⟶ objs j) [HasWidePushout B objs arrows] : C

A choice of wide pushout.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.WidePullback.π {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [HasWidePullback B objs arrows] (j : J) : widePullback B objs arrows ⟶ objs j

The j-th projection from the pullback.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.WidePushout.ι {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → B ⟶ objs j) [HasWidePushout B objs arrows] (j : J) : objs j ⟶ widePushout B objs arrows

The j-th inclusion to the pushout.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.WidePullback.base {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [HasWidePullback B objs arrows] : widePullback B objs arrows ⟶ B

The unique map to the base from the pullback.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.WidePushout.head {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → B ⟶ objs j) [HasWidePushout B objs arrows] : B ⟶ widePushout B objs arrows

The unique map from the head to the pushout.

@[simp]

theorem CategoryTheory.Limits.WidePullback.π_arrow {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [HasWidePullback B objs arrows] (j : J) : CategoryStruct.comp (π arrows j) (arrows j) = base arrows

@[simp]

theorem CategoryTheory.Limits.WidePushout.arrow_ι_assoc {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → B ⟶ objs j) [HasWidePushout B objs arrows] (j : J) {Z : C} (h : widePushout B objs arrows ⟶ Z) : CategoryStruct.comp (arrows j) (CategoryStruct.comp (ι arrows j) h) = CategoryStruct.comp (head arrows) h

@[simp]

theorem CategoryTheory.Limits.WidePullback.π_arrow_assoc {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [HasWidePullback B objs arrows] (j : J) {Z : C} (h : B ⟶ Z) : CategoryStruct.comp (π arrows j) (CategoryStruct.comp (arrows j) h) = CategoryStruct.comp (base arrows) h

@[simp]

theorem CategoryTheory.Limits.WidePushout.arrow_ι {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → B ⟶ objs j) [HasWidePushout B objs arrows] (j : J) : CategoryStruct.comp (arrows j) (ι arrows j) = head arrows

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.WidePullback.lift {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} {arrows : (j : J) → objs j ⟶ B} [HasWidePullback B objs arrows] {X : C} (f : X ⟶ B) (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryStruct.comp (fs j) (arrows j) = f) : X ⟶ widePullback B objs arrows

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.WidePushout.desc {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} {arrows : (j : J) → B ⟶ objs j} [HasWidePushout B objs arrows] {X : C} (f : B ⟶ X) (fs : (j : J) → objs j ⟶ X) (w : ∀ (j : J), CategoryStruct.comp (arrows j) (fs j) = f) : widePushout B objs arrows ⟶ X

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

theorem CategoryTheory.Limits.WidePullback.lift_π {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [HasWidePullback B objs arrows] {X : C} (f : X ⟶ B) (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryStruct.comp (fs j) (arrows j) = f) (j : J) : CategoryStruct.comp (lift f fs w) (π arrows j) = fs j

theorem CategoryTheory.Limits.WidePushout.ι_desc_assoc {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → B ⟶ objs j) [HasWidePushout B objs arrows] {X : C} (f : B ⟶ X) (fs : (j : J) → objs j ⟶ X) (w : ∀ (j : J), CategoryStruct.comp (arrows j) (fs j) = f) (j : J) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (ι arrows j) (CategoryStruct.comp (desc f fs w) h) = CategoryStruct.comp (fs j) h

theorem CategoryTheory.Limits.WidePullback.lift_π_assoc {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [HasWidePullback B objs arrows] {X : C} (f : X ⟶ B) (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryStruct.comp (fs j) (arrows j) = f) (j : J) {Z : C} (h : objs j ⟶ Z) : CategoryStruct.comp (lift f fs w) (CategoryStruct.comp (π arrows j) h) = CategoryStruct.comp (fs j) h

theorem CategoryTheory.Limits.WidePushout.ι_desc {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → B ⟶ objs j) [HasWidePushout B objs arrows] {X : C} (f : B ⟶ X) (fs : (j : J) → objs j ⟶ X) (w : ∀ (j : J), CategoryStruct.comp (arrows j) (fs j) = f) (j : J) : CategoryStruct.comp (ι arrows j) (desc f fs w) = fs j

theorem CategoryTheory.Limits.WidePullback.lift_base {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [HasWidePullback B objs arrows] {X : C} (f : X ⟶ B) (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryStruct.comp (fs j) (arrows j) = f) : CategoryStruct.comp (lift f fs w) (base arrows) = f

theorem CategoryTheory.Limits.WidePullback.lift_base_assoc {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [HasWidePullback B objs arrows] {X : C} (f : X ⟶ B) (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryStruct.comp (fs j) (arrows j) = f) {Z : C} (h : B ⟶ Z) : CategoryStruct.comp (lift f fs w) (CategoryStruct.comp (base arrows) h) = CategoryStruct.comp f h

theorem CategoryTheory.Limits.WidePushout.head_desc_assoc {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → B ⟶ objs j) [HasWidePushout B objs arrows] {X : C} (f : B ⟶ X) (fs : (j : J) → objs j ⟶ X) (w : ∀ (j : J), CategoryStruct.comp (arrows j) (fs j) = f) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (head arrows) (CategoryStruct.comp (desc f fs w) h) = CategoryStruct.comp f h

theorem CategoryTheory.Limits.WidePushout.head_desc {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → B ⟶ objs j) [HasWidePushout B objs arrows] {X : C} (f : B ⟶ X) (fs : (j : J) → objs j ⟶ X) (w : ∀ (j : J), CategoryStruct.comp (arrows j) (fs j) = f) : CategoryStruct.comp (head arrows) (desc f fs w) = f

theorem CategoryTheory.Limits.WidePullback.eq_lift_of_comp_eq {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [HasWidePullback B objs arrows] {X : C} (f : X ⟶ B) (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryStruct.comp (fs j) (arrows j) = f) (g : X ⟶ widePullback B objs arrows) : (∀ (j : J), CategoryStruct.comp g (π arrows j) = fs j) → CategoryStruct.comp g (base arrows) = f → g = lift f fs w

theorem CategoryTheory.Limits.WidePushout.eq_desc_of_comp_eq {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → B ⟶ objs j) [HasWidePushout B objs arrows] {X : C} (f : B ⟶ X) (fs : (j : J) → objs j ⟶ X) (w : ∀ (j : J), CategoryStruct.comp (arrows j) (fs j) = f) (g : widePushout B objs arrows ⟶ X) : (∀ (j : J), CategoryStruct.comp (ι arrows j) g = fs j) → CategoryStruct.comp (head arrows) g = f → g = desc f fs w

theorem CategoryTheory.Limits.WidePullback.hom_eq_lift {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [HasWidePullback B objs arrows] {X : C} (g : X ⟶ widePullback B objs arrows) : g = lift (CategoryStruct.comp g (base arrows)) (fun (j : J) => CategoryStruct.comp g (π arrows j)) ⋯

theorem CategoryTheory.Limits.WidePushout.hom_eq_desc {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → B ⟶ objs j) [HasWidePushout B objs arrows] {X : C} (g : widePushout B objs arrows ⟶ X) : g = desc (CategoryStruct.comp (head arrows) g) (fun (j : J) => CategoryStruct.comp (ι arrows j) g) ⋯

theorem CategoryTheory.Limits.WidePullback.hom_ext {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [HasWidePullback B objs arrows] {X : C} (g1 g2 : X ⟶ widePullback B objs arrows) : (∀ (j : J), CategoryStruct.comp g1 (π arrows j) = CategoryStruct.comp g2 (π arrows j)) → CategoryStruct.comp g1 (base arrows) = CategoryStruct.comp g2 (base arrows) → g1 = g2

theorem CategoryTheory.Limits.WidePushout.hom_ext {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → B ⟶ objs j) [HasWidePushout B objs arrows] {X : C} (g1 g2 : widePushout B objs arrows ⟶ X) : (∀ (j : J), CategoryStruct.comp (ι arrows j) g1 = CategoryStruct.comp (ι arrows j) g2) → CategoryStruct.comp (head arrows) g1 = CategoryStruct.comp (head arrows) g2 → g1 = g2

theorem CategoryTheory.Limits.WidePushout.hom_ext_iff {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} {arrows : (j : J) → B ⟶ objs j} [HasWidePushout B objs arrows] {X : C} {g1 g2 : widePushout B objs arrows ⟶ X} : g1 = g2 ↔ (∀ (j : J), CategoryStruct.comp (ι arrows j) g1 = CategoryStruct.comp (ι arrows j) g2) ∧ CategoryStruct.comp (head arrows) g1 = CategoryStruct.comp (head arrows) g2

theorem CategoryTheory.Limits.WidePullback.hom_ext_iff {J : Type w} {C : Type u} [Category.{v, u} C] {B : C} {objs : J → C} {arrows : (j : J) → objs j ⟶ B} [HasWidePullback B objs arrows] {X : C} {g1 g2 : X ⟶ widePullback B objs arrows} : g1 = g2 ↔ (∀ (j : J), CategoryStruct.comp g1 (π arrows j) = CategoryStruct.comp g2 (π arrows j)) ∧ CategoryStruct.comp g1 (base arrows) = CategoryStruct.comp g2 (base arrows)

@[reducible, inline]

abbrev CategoryTheory.Limits.WidePullbackCone {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} (f : (i : ι) → Y i ⟶ X) : Type (max (max u_1 u) v)

A wide pullback cone is a cone on the wide cospan formed by a family of morphisms.

def CategoryTheory.Limits.WidePullbackCone.π {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : WidePullbackCone f) (i : ι) : s.pt ⟶ Y i

The projection on the components of a wide pullback cone.

def CategoryTheory.Limits.WidePullbackCone.base {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : WidePullbackCone f) : s.pt ⟶ X

The projection to the base of a wide pullback cone.

@[simp]

theorem CategoryTheory.Limits.WidePullbackCone.condition {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : WidePullbackCone f) (i : ι) : CategoryStruct.comp (s.π i) (f i) = s.base

@[simp]

theorem CategoryTheory.Limits.WidePullbackCone.condition_assoc {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : WidePullbackCone f) (i : ι) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (s.π i) (CategoryStruct.comp (f i) h) = CategoryStruct.comp s.base h

def CategoryTheory.Limits.WidePullbackCone.mk {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {W : C} (b : W ⟶ X) (π : (i : ι) → W ⟶ Y i) (h : ∀ (i : ι), CategoryStruct.comp (π i) (f i) = b) : WidePullbackCone f

Construct a wide pullback cone from the projections.

@[simp]

theorem CategoryTheory.Limits.WidePullbackCone.mk_pt {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {W : C} (b : W ⟶ X) (π : (i : ι) → W ⟶ Y i) (h : ∀ (i : ι), CategoryStruct.comp (π i) (f i) = b) : (mk b π h).pt = W

@[simp]

theorem CategoryTheory.Limits.WidePullbackCone.mk_base {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {W : C} (b : W ⟶ X) (π : (i : ι) → W ⟶ Y i) (h : ∀ (i : ι), CategoryStruct.comp (π i) (f i) = b) : (mk b π h).base = b

@[simp]

theorem CategoryTheory.Limits.WidePullbackCone.mk_π {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {W : C} (b : W ⟶ X) (π : (i : ι) → W ⟶ Y i) (h : ∀ (i : ι), CategoryStruct.comp (π i) (f i) = b) (i : ι) : (mk b π h).π i = π i

def CategoryTheory.Limits.WidePullbackCone.IsLimit.mk {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : WidePullbackCone f) (lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt) (facbase : ∀ (t : WidePullbackCone f), CategoryStruct.comp (lift t) s.base = t.base) (facπ : ∀ (t : WidePullbackCone f) (i : ι), CategoryStruct.comp (lift t) (s.π i) = t.π i) (uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), CategoryStruct.comp m s.base = t.base → (∀ (i : ι), CategoryStruct.comp m (s.π i) = t.π i) → m = lift t) : IsLimit s

Constructor to show a wide pullback cone is limiting.

theorem CategoryTheory.Limits.WidePullbackCone.IsLimit.hom_ext {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {s : WidePullbackCone f} (hs : IsLimit s) {W : C} {k l : W ⟶ s.pt} (hbase : CategoryStruct.comp k s.base = CategoryStruct.comp l s.base) (hπ : ∀ (i : ι), CategoryStruct.comp k (s.π i) = CategoryStruct.comp l (s.π i)) : k = l

def CategoryTheory.Limits.WidePullbackCone.IsLimit.lift {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {s : WidePullbackCone f} (hs : IsLimit s) {W : C} (b : W ⟶ X) (a : (i : ι) → W ⟶ Y i) (w : ∀ (i : ι), CategoryStruct.comp (a i) (f i) = b) : W ⟶ s.pt

Lift a family of morphisms to a limiting wide pullback cone.

@[simp]

theorem CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_base {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {s : WidePullbackCone f} (hs : IsLimit s) {W : C} (b : W ⟶ X) (a : (i : ι) → W ⟶ Y i) (w : ∀ (i : ι), CategoryStruct.comp (a i) (f i) = b) : CategoryStruct.comp (lift hs b a w) s.base = b

@[simp]

theorem CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_base_assoc {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {s : WidePullbackCone f} (hs : IsLimit s) {W : C} (b : W ⟶ X) (a : (i : ι) → W ⟶ Y i) (w : ∀ (i : ι), CategoryStruct.comp (a i) (f i) = b) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (lift hs b a w) (CategoryStruct.comp s.base h) = CategoryStruct.comp b h

@[simp]

theorem CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_π {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {s : WidePullbackCone f} (hs : IsLimit s) {W : C} (b : W ⟶ X) (a : (i : ι) → W ⟶ Y i) (w : ∀ (i : ι), CategoryStruct.comp (a i) (f i) = b) (i : ι) : CategoryStruct.comp (lift hs b a w) (s.π i) = a i

@[simp]

theorem CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_π_assoc {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {s : WidePullbackCone f} (hs : IsLimit s) {W : C} (b : W ⟶ X) (a : (i : ι) → W ⟶ Y i) (w : ∀ (i : ι), CategoryStruct.comp (a i) (f i) = b) (i : ι) {Z : C} (h : Y i ⟶ Z) : CategoryStruct.comp (lift hs b a w) (CategoryStruct.comp (s.π i) h) = CategoryStruct.comp (a i) h

def CategoryTheory.Limits.WidePullbackCone.ext {C : Type u} [Category.{v, u} C] {ι : Type u_2} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {s t : WidePullbackCone f} (e : s.pt ≅ t.pt) (base : CategoryStruct.comp e.hom t.base = s.base := by cat_disch) (π : ∀ (i : ι), CategoryStruct.comp e.hom (t.π i) = s.π i := by cat_disch) : s ≅ t

To show two wide pullback cones are isomorphic, it suffices to give a compatible isomorphism of their cone points.

def CategoryTheory.Limits.WidePullbackCone.reindex {C : Type u} [Category.{v, u} C] {ι : Type u_2} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : WidePullbackCone f) {ι' : Type u_3} (e : ι' ≃ ι) : WidePullbackCone fun (i : ι') => f (e i)

Reindex a wide pullback cone.

@[simp]

theorem CategoryTheory.Limits.WidePullbackCone.reindex_pt {C : Type u} [Category.{v, u} C] {ι : Type u_2} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : WidePullbackCone f) {ι' : Type u_3} (e : ι' ≃ ι) : (s.reindex e).pt = s.pt

@[simp]

theorem CategoryTheory.Limits.WidePullbackCone.reindex_base {C : Type u} [Category.{v, u} C] {ι : Type u_2} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : WidePullbackCone f) {ι' : Type u_3} (e : ι' ≃ ι) : (s.reindex e).base = s.base

@[simp]

theorem CategoryTheory.Limits.WidePullbackCone.reindex_π {C : Type u} [Category.{v, u} C] {ι : Type u_2} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : WidePullbackCone f) {ι' : Type u_3} (e : ι' ≃ ι) (i : ι') : (s.reindex e).π i = s.π (e i)

def CategoryTheory.Limits.WidePullbackCone.reindexIsLimitEquiv {C : Type u} [Category.{v, u} C] {ι : Type u_2} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (s : WidePullbackCone f) {ι' : Type u_3} (e : ι' ≃ ι) : IsLimit (s.reindex e) ≃ IsLimit s

Reindexing a pullback cone preserves being limiting.

def CategoryTheory.Limits.widePullbackShapeOpMap (J : Type w) (X Y : WidePullbackShape J) : (X ⟶ Y) → (Opposite.op X ⟶ Opposite.op Y)

The action on morphisms of the obvious functor WidePullbackShape_op : WidePullbackShape J ⥤ (WidePushoutShape J)ᵒᵖ

def CategoryTheory.Limits.widePushoutShapeOpMap (J : Type w) (Y X : WidePushoutShape J) : (Y ⟶ X) → (Opposite.op Y ⟶ Opposite.op X)

The action on morphisms of the obvious functor widePushoutShapeOp : WidePushoutShape J ⥤ (WidePullbackShape J)ᵒᵖ

def CategoryTheory.Limits.widePullbackShapeOp (J : Type w) : Functor (WidePullbackShape J) (WidePushoutShape J)ᵒᵖ

The obvious functor WidePullbackShape J ⥤ (WidePushoutShape J)ᵒᵖ

def CategoryTheory.Limits.widePushoutShapeOp (J : Type w) : Functor (WidePushoutShape J) (WidePullbackShape J)ᵒᵖ

The obvious functor WidePushoutShape J ⥤ (WidePullbackShape J)ᵒᵖ

@[simp]

theorem CategoryTheory.Limits.widePullbackShapeOp_map (J : Type w) {X₁ X₂ : WidePullbackShape J} (a✝ : X₁ ⟶ X₂) : (widePullbackShapeOp J).map a✝ = widePullbackShapeOpMap J X₁ X₂ a✝

@[simp]

theorem CategoryTheory.Limits.widePushoutShapeOp_obj (J : Type w) (X : WidePushoutShape J) : (widePushoutShapeOp J).obj X = Opposite.op X

@[simp]

theorem CategoryTheory.Limits.widePushoutShapeOp_map (J : Type w) {X₂ X₁ : WidePushoutShape J} (a✝ : X₂ ⟶ X₁) : (widePushoutShapeOp J).map a✝ = widePushoutShapeOpMap J X₂ X₁ a✝

@[simp]

theorem CategoryTheory.Limits.widePullbackShapeOp_obj (J : Type w) (X : WidePullbackShape J) : (widePullbackShapeOp J).obj X = Opposite.op X

def CategoryTheory.Limits.widePullbackShapeUnop (J : Type w) : Functor (WidePullbackShape J)ᵒᵖ (WidePushoutShape J)

The obvious functor (WidePullbackShape J)ᵒᵖ ⥤ WidePushoutShape J

def CategoryTheory.Limits.widePushoutShapeUnop (J : Type w) : Functor (WidePushoutShape J)ᵒᵖ (WidePullbackShape J)

The obvious functor (WidePushoutShape J)ᵒᵖ ⥤ WidePullbackShape J

@[simp]

theorem CategoryTheory.Limits.widePushoutShapeUnop_obj (J : Type w) (X : (WidePushoutShape J)ᵒᵖ) : (widePushoutShapeUnop J).obj X = Opposite.unop X

@[simp]

theorem CategoryTheory.Limits.widePullbackShapeUnop_obj (J : Type w) (X : (WidePullbackShape J)ᵒᵖ) : (widePullbackShapeUnop J).obj X = Opposite.unop X

@[simp]

theorem CategoryTheory.Limits.widePushoutShapeUnop_map (J : Type w) {X✝ Y✝ : (WidePushoutShape J)ᵒᵖ} (f : X✝ ⟶ Y✝) : (widePushoutShapeUnop J).map f = (widePushoutShapeOpMap J (Opposite.unop Y✝) (Opposite.unop X✝) f.unop).unop

@[simp]

theorem CategoryTheory.Limits.widePullbackShapeUnop_map (J : Type w) {X✝ Y✝ : (WidePullbackShape J)ᵒᵖ} (f : X✝ ⟶ Y✝) : (widePullbackShapeUnop J).map f = (widePullbackShapeOpMap J (Opposite.unop Y✝) (Opposite.unop X✝) f.unop).unop

def CategoryTheory.Limits.widePushoutShapeOpUnop (J : Type w) : (widePushoutShapeUnop J).comp (widePullbackShapeOp J) ≅ Functor.id (WidePushoutShape J)ᵒᵖ

The inverse of the unit isomorphism of the equivalence widePushoutShapeOpEquiv : (WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J

def CategoryTheory.Limits.widePullbackShapeOpUnop (J : Type w) : (widePullbackShapeUnop J).comp (widePushoutShapeOp J) ≅ Functor.id (WidePullbackShape J)ᵒᵖ

The inverse of the unit isomorphism of the equivalence widePullbackShapeOpEquiv : (WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J

def CategoryTheory.Limits.widePushoutShapeUnopOp (J : Type w) : (widePushoutShapeOp J).comp (widePullbackShapeUnop J) ≅ Functor.id (WidePushoutShape J)

The counit isomorphism of the equivalence widePullbackShapeOpEquiv : (WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J

def CategoryTheory.Limits.widePullbackShapeUnopOp (J : Type w) : (widePullbackShapeOp J).comp (widePushoutShapeUnop J) ≅ Functor.id (WidePullbackShape J)

The counit isomorphism of the equivalence widePushoutShapeOpEquiv : (WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J

def CategoryTheory.Limits.widePushoutShapeOpEquiv (J : Type w) : (WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J

The duality equivalence (WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J

def CategoryTheory.Limits.widePullbackShapeOpEquiv (J : Type w) : (WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J

The duality equivalence (WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J

@[simp]

theorem CategoryTheory.Limits.widePullbackShapeOpEquiv_unitIso (J : Type w) : (widePullbackShapeOpEquiv J).unitIso = (widePullbackShapeOpUnop J).symm

@[simp]

theorem CategoryTheory.Limits.widePullbackShapeOpEquiv_inverse (J : Type w) : (widePullbackShapeOpEquiv J).inverse = widePushoutShapeOp J

@[simp]

theorem CategoryTheory.Limits.widePushoutShapeOpEquiv_inverse (J : Type w) : (widePushoutShapeOpEquiv J).inverse = widePullbackShapeOp J

@[simp]

theorem CategoryTheory.Limits.widePullbackShapeOpEquiv_counitIso (J : Type w) : (widePullbackShapeOpEquiv J).counitIso = widePushoutShapeUnopOp J

@[simp]

theorem CategoryTheory.Limits.widePullbackShapeOpEquiv_functor (J : Type w) : (widePullbackShapeOpEquiv J).functor = widePullbackShapeUnop J

@[simp]

theorem CategoryTheory.Limits.widePushoutShapeOpEquiv_functor (J : Type w) : (widePushoutShapeOpEquiv J).functor = widePushoutShapeUnop J

@[simp]

theorem CategoryTheory.Limits.widePushoutShapeOpEquiv_counitIso (J : Type w) : (widePushoutShapeOpEquiv J).counitIso = widePullbackShapeUnopOp J

@[simp]

theorem CategoryTheory.Limits.widePushoutShapeOpEquiv_unitIso (J : Type w) : (widePushoutShapeOpEquiv J).unitIso = (widePushoutShapeOpUnop J).symm

theorem CategoryTheory.Limits.hasWidePushouts_shrink {C : Type u} [Category.{v, u} C] [HasWidePushouts C] : HasWidePushouts C

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

theorem CategoryTheory.Limits.hasWidePullbacks_shrink {C : Type u} [Category.{v, u} C] [HasWidePullbacks C] : HasWidePullbacks C

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