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.

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

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

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

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 CategoryTheory.Limits.instInhabitedWidePushoutShape (J : Type w) : Inhabited (CategoryTheory.Limits.WidePushoutShape J)

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

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

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

instance CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom : {J : Type u_1} → {a a_1 : CategoryTheory.Limits.WidePullbackShape J} → [inst : DecidableEq J] → DecidableEq (CategoryTheory.Limits.WidePullbackShape.Hom a a_1)

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

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

def CategoryTheory.Limits.WidePullbackShape.evalCasesBash : Lean.Elab.Tactic.TacticM Unit

An aesop tactic for bulk cases on morphisms in WidePushoutShape

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.WidePullbackShape.wideCospan_map {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → objs j ⟶ B) : ∀ {X Y : CategoryTheory.Limits.WidePullbackShape J} (f : X ⟶ Y), (CategoryTheory.Limits.WidePullbackShape.wideCospan B objs arrows).map f = CategoryTheory.Limits.WidePullbackShape.Hom.casesOn J (fun a a_1 t => X = a → Y = a_1 → HEq f t → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y)) X Y f (fun X_1 h => Eq.ndrec (motive := fun X_2 => Y = X_2 → HEq f (CategoryTheory.Limits.WidePullbackShape.Hom.id X_2) → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y)) (fun h => Eq.ndrec (CategoryTheory.Limits.WidePullbackShape J) X (fun {Y} => (f : X ⟶ Y) → HEq f (CategoryTheory.Limits.WidePullbackShape.Hom.id X) → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y)) (fun f h => (_ : CategoryTheory.Limits.WidePullbackShape.Hom.id X = f) ▸ CategoryTheory.CategoryStruct.id ((fun j => Option.casesOn j B objs) X)) Y (_ : X = Y) f) h) (fun j h => Eq.ndrec (CategoryTheory.Limits.WidePullbackShape J) (some j) (fun {X} => (f : X ⟶ Y) → Y = none → HEq f (CategoryTheory.Limits.WidePullbackShape.Hom.term j) → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y)) (fun f h => Eq.ndrec (CategoryTheory.Limits.WidePullbackShape J) none (fun {Y} => (f : some j ⟶ Y) → HEq f (CategoryTheory.Limits.WidePullbackShape.Hom.term j) → ((fun j => Option.casesOn j B objs) (some j) ⟶ (fun j => Option.casesOn j B objs) Y)) (fun f h => (_ : CategoryTheory.Limits.WidePullbackShape.Hom.term j = f) ▸ arrows j) Y (_ : none = Y) f) X (_ : some j = X) f) (_ : X = X) (_ : Y = Y) (_ : HEq f f)

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

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

Construct a cone over a wide cospan.

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

Wide pullback diagrams of equivalent index types are equivalent.

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

Lifting universe and morphism levels preserves wide pullback diagrams.

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

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

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

instance CategoryTheory.Limits.WidePushoutShape.instDecidableEqHom : {J : Type u_1} → {a a_1 : CategoryTheory.Limits.WidePushoutShape J} → [inst : DecidableEq J] → DecidableEq (CategoryTheory.Limits.WidePushoutShape.Hom a a_1)

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

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

def CategoryTheory.Limits.WidePushoutShape.evalCasesBash' : Lean.Elab.Tactic.TacticM Unit

An aesop tactic for bulk cases on morphisms in WidePushoutShape

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.WidePushoutShape.wideSpan_map {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → B ⟶ objs j) : ∀ {X Y : CategoryTheory.Limits.WidePushoutShape J} (f : X ⟶ Y), (CategoryTheory.Limits.WidePushoutShape.wideSpan B objs arrows).map f = CategoryTheory.Limits.WidePushoutShape.Hom.casesOn J (fun a a_1 t => X = a → Y = a_1 → HEq f t → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y)) X Y f (fun X_1 h => Eq.ndrec (motive := fun X_2 => Y = X_2 → HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.id X_2) → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y)) (fun h => Eq.ndrec (CategoryTheory.Limits.WidePushoutShape J) X (fun {Y} => (f : X ⟶ Y) → HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.id X) → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y)) (fun f h => (_ : CategoryTheory.Limits.WidePushoutShape.Hom.id X = f) ▸ CategoryTheory.CategoryStruct.id ((fun j => Option.casesOn j B objs) X)) Y (_ : X = Y) f) h) (fun j h => Eq.ndrec (CategoryTheory.Limits.WidePushoutShape J) none (fun {X} => (f : X ⟶ Y) → Y = some j → HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.init j) → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y)) (fun f h => Eq.ndrec (CategoryTheory.Limits.WidePushoutShape J) (some j) (fun {Y} => (f : none ⟶ Y) → HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.init j) → ((fun j => Option.casesOn j B objs) none ⟶ (fun j => Option.casesOn j B objs) Y)) (fun f h => (_ : CategoryTheory.Limits.WidePushoutShape.Hom.init j = f) ▸ arrows j) Y (_ : some j = Y) f) X (_ : none = X) f) (_ : X = X) (_ : Y = Y) (_ : HEq f f)

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

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

Construct a cocone over a wide span.

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

Wide pushout diagrams of equivalent index types are equivalent.

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

Lifting universe and morphism levels preserves wide pushout diagrams.

@[inline, reducible]

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

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

@[inline, reducible]

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

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

@[inline, reducible]

abbrev CategoryTheory.Limits.HasWidePullback {J : Type w} {C : Type u} [CategoryTheory.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.

@[inline, reducible]

abbrev CategoryTheory.Limits.HasWidePushout {J : Type w} {C : Type u} [CategoryTheory.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.

@[inline, reducible]

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

A choice of wide pullback.

@[inline, reducible]

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

A choice of wide pushout.

@[inline, reducible]

noncomputable abbrev CategoryTheory.Limits.WidePullback.π {J : Type w} {D : Type u_1} [CategoryTheory.Category.{v₂, u_1} D] {B : D} {objs : J → D} (arrows : (j : J) → objs j ⟶ B) [CategoryTheory.Limits.HasWidePullback B objs arrows] (j : J) : CategoryTheory.Limits.widePullback B (fun j => objs j) arrows ⟶ objs j

The j-th projection from the pullback.

@[inline, reducible]

noncomputable abbrev CategoryTheory.Limits.WidePullback.base {J : Type w} {D : Type u_1} [CategoryTheory.Category.{v₂, u_1} D] {B : D} {objs : J → D} (arrows : (j : J) → objs j ⟶ B) [CategoryTheory.Limits.HasWidePullback B objs arrows] : CategoryTheory.Limits.widePullback B (fun j => objs j) arrows ⟶ B

The unique map to the base from the pullback.

@[simp]

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

@[simp]

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

@[inline, reducible]

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

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

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

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

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

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

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

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

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

@[inline, reducible]

noncomputable abbrev CategoryTheory.Limits.WidePushout.ι {J : Type w} {D : Type u_1} [CategoryTheory.Category.{v₂, u_1} D] {B : D} {objs : J → D} (arrows : (j : J) → B ⟶ objs j) [CategoryTheory.Limits.HasWidePushout B objs arrows] (j : J) : objs j ⟶ CategoryTheory.Limits.widePushout B (fun j => objs j) arrows

The j-th inclusion to the pushout.

@[inline, reducible]

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

The unique map from the head to the pushout.

@[simp]

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

@[simp]

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

@[inline, reducible]

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.widePushoutShapeOp_map (J : Type w) {X : CategoryTheory.Limits.WidePushoutShape J} {Y : CategoryTheory.Limits.WidePushoutShape J} : ∀ (a : X ⟶ Y), (CategoryTheory.Limits.widePushoutShapeOp J).map a = CategoryTheory.Limits.widePushoutShapeOpMap J X Y a

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem CategoryTheory.Limits.hasWidePushouts_shrink {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasWidePushouts C] : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasWidePullbacks C] : CategoryTheory.Limits.HasWidePullbacks C

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