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 (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 (WidePushoutShape J)

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 CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom {J✝ : Type u_1} {a✝ a✝¹ : WidePullbackShape J✝} [DecidableEq J✝] : DecidableEq (a✝.Hom a✝¹)

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

instance CategoryTheory.Limits.WidePullbackShape.Hom.inhabited {J : Type w} : Inhabited (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 (WidePullbackShape J)

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

@[simp]

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

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.

@[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} (f : X✝ ⟶ Y✝) : (wideCospan B objs arrows).map f = Hom.casesOn (motive := fun (a a_1 : WidePullbackShape J) (x : a.Hom a_1) => X✝ = a → Y✝ = a_1 → f ≍ x → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y✝ B objs)) f (fun (X : WidePullbackShape J) (h : X✝ = X) => Eq.ndrec (motive := fun (X : WidePullbackShape J) => Y✝ = X → f ≍ Hom.id X → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y✝ B objs)) (fun (h : Y✝ = X✝) => Eq.ndrec (motive := fun {Y : WidePullbackShape J} => (f : X✝ ⟶ Y) → f ≍ Hom.id X✝ → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y B objs)) (fun (f : X✝ ⟶ X✝) (h : f ≍ Hom.id X✝) => CategoryStruct.id (Option.casesOn X✝ B objs)) ⋯ f) h) (fun (j : J) (h : X✝ = some j) => Eq.ndrec (motive := fun {X : WidePullbackShape J} => (f : X ⟶ Y✝) → Y✝ = none → f ≍ Hom.term j → (Option.casesOn X B objs ⟶ Option.casesOn Y✝ B objs)) (fun (f : some j ⟶ Y✝) (h : Y✝ = none) => Eq.ndrec (motive := fun {Y : WidePullbackShape J} => (f : some j ⟶ Y) → f ≍ Hom.term j → (Option.casesOn (some j) B objs ⟶ Option.casesOn Y B objs)) (fun (f : some j ⟶ none) (h : f ≍ Hom.term j) => arrows j) ⋯ f) ⋯ f) ⋯ ⋯ ⋯

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.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.

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

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 CategoryTheory.Limits.WidePushoutShape.instDecidableEqHom {J✝ : Type u_1} {a✝ a✝¹ : WidePushoutShape J✝} [DecidableEq J✝] : DecidableEq (a✝.Hom a✝¹)

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

instance CategoryTheory.Limits.WidePushoutShape.Hom.inhabited {J : Type w} : Inhabited (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 (WidePushoutShape J)

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

@[simp]

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

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.WidePushoutShape.wideSpan_map {J : Type w} {C : Type u} [Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → B ⟶ objs j) {X✝ Y✝ : WidePushoutShape J} (f : X✝ ⟶ Y✝) : (wideSpan B objs arrows).map f = Hom.casesOn (motive := fun (a a_1 : WidePushoutShape J) (x : a.Hom a_1) => X✝ = a → Y✝ = a_1 → f ≍ x → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y✝ B objs)) f (fun (X : WidePushoutShape J) (h : X✝ = X) => Eq.ndrec (motive := fun (X : WidePushoutShape J) => Y✝ = X → f ≍ Hom.id X → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y✝ B objs)) (fun (h : Y✝ = X✝) => Eq.ndrec (motive := fun {Y : WidePushoutShape J} => (f : X✝ ⟶ Y) → f ≍ Hom.id X✝ → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y B objs)) (fun (f : X✝ ⟶ X✝) (h : f ≍ Hom.id X✝) => CategoryStruct.id (Option.casesOn X✝ B objs)) ⋯ f) h) (fun (j : J) (h : X✝ = none) => Eq.ndrec (motive := fun {X : WidePushoutShape J} => (f : X ⟶ Y✝) → Y✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn Y✝ B objs)) (fun (f : none ⟶ Y✝) (h : Y✝ = some j) => Eq.ndrec (motive := fun {Y : WidePushoutShape J} => (f : none ⟶ Y) → f ≍ Hom.init j → (Option.casesOn none B objs ⟶ Option.casesOn Y B objs)) (fun (f : none ⟶ some j) (h : f ≍ Hom.init j) => arrows j) ⋯ f) ⋯ f) ⋯ ⋯ ⋯

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

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.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

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.

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.

@[reducible, inline]

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

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

@[reducible, inline]

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

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

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

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

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

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.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.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.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.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.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.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]

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.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.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

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

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

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.widePullbackShapeOp (J : Type w) : Functor (WidePullbackShape J) (WidePushoutShape J)ᵒᵖ

The obvious functor WidePullbackShape J ⥤ (WidePushoutShape 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.widePullbackShapeOp_obj (J : Type w) (X : WidePullbackShape J) : (widePullbackShapeOp J).obj X = Opposite.op X

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

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

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

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

@[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 Y : WidePushoutShape J} (a✝ : X ⟶ Y) : (widePushoutShapeOp J).map a✝ = widePushoutShapeOpMap J X Y a✝

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

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

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

@[simp]

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

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.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

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.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.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.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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The duality equivalence (WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape 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.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

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.