Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

CategoryTheory.Limits.WidePullbackShape definition

Full source

/-- A wide pullback shape for any type `J` can be written simply as `Option J`. -/
def WidePullbackShape := Option J

Wide pullback shape

Informal description

The wide pullback shape for any type $J$ is defined as the type `Option J`, which consists of the elements of $J$ together with an additional "none" element representing a terminal object.

CategoryTheory.Limits.instInhabitedWidePullbackShape instance

: Inhabited (WidePullbackShape J)

Full source

instance : Inhabited (WidePullbackShape J) where
  default := none

Inhabitedness of Wide Pullback Shape

Informal description

For any type $J$, the wide pullback shape `WidePullbackShape J` is inhabited (i.e., it has at least one element).

CategoryTheory.Limits.WidePushoutShape definition

Full source

/-- A wide pushout shape for any type `J` can be written simply as `Option J`. -/
def WidePushoutShape := Option J

Wide pushout shape

Informal description

The wide pushout shape for any type $J$ is defined as the type `Option J`, which consists of the elements of $J$ together with an additional element representing the initial object.

CategoryTheory.Limits.instInhabitedWidePushoutShape instance

: Inhabited (WidePushoutShape J)

Full source

instance : Inhabited (WidePushoutShape J) where
  default := none

Inhabited Wide Pushout Shape

Informal description

For any type $J$, the wide pushout shape `WidePushoutShape J` is inhabited, meaning it has at least one element.

CategoryTheory.Limits.WidePullbackShape.Hom inductive

: WidePullbackShape J → WidePullbackShape J → Type w

Full source

/-- The type of arrows for the shape indexing a wide pullback. -/
inductive Hom : WidePullbackShape J → WidePullbackShape J → Type w
  | id : ∀ X, Hom X X
  | term : ∀ j : J, Hom (some j) none
  deriving DecidableEq

Morphisms in wide pullback shape category

Informal description

The type of morphisms in the wide pullback shape category for a type $J$. For any two objects $X$ and $Y$ in the wide pullback shape (which is `Option J`), this type consists of: - The identity morphism when $X = Y$, - A unique morphism from any object to the terminal object (the "none" element of `Option J`), - No other morphisms.

CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom instance

 {J✝} {a✝} {a✝¹} [DecidableEq✝ J✝] : DecidableEq✝ (@CategoryTheory.Limits.WidePullbackShape.Hom✝ J✝ a✝ a✝¹)

Full source

DecidableEq

Decidable Equality of Morphisms in Wide Pullback Shape Category

Informal description

For any type $J$ with decidable equality, the morphisms in the wide pullback shape category between any two objects $a$ and $b$ have decidable equality.

CategoryTheory.Limits.WidePullbackShape.struct instance

: CategoryStruct (WidePullbackShape J)

Full source

instance struct : CategoryStruct (WidePullbackShape J) where
  Hom := Hom
  id j := Hom.id j
  comp f g := by
    cases f
    · exact g
    cases g
    apply Hom.term _

Category Structure on Wide Pullback Shape

Informal description

The wide pullback shape for any type $J$ has a category structure, where the objects are elements of `Option J` (i.e., elements of $J$ plus a terminal object) and the morphisms consist of identity morphisms and unique morphisms to the terminal object.

CategoryTheory.Limits.WidePullbackShape.Hom.inhabited instance

: Inhabited (Hom (none : WidePullbackShape J) none)

Full source

instance Hom.inhabited : Inhabited (Hom (none : WidePullbackShape J) none) :=
  ⟨Hom.id (none : WidePullbackShape J)⟩

Inhabited Morphisms at Terminal Object in Wide Pullback Shape

Informal description

For any type $J$, the morphism set $\mathrm{Hom}(\mathrm{none}, \mathrm{none})$ in the wide pullback shape category is inhabited, where $\mathrm{none}$ is the terminal object.

CategoryTheory.Limits.WidePullbackShape.evalCasesBash definition

: TacticM Unit

Full source

/-- An aesop tactic for bulk cases on morphisms in `WidePushoutShape` -/
def evalCasesBash : TacticM Unit := do
  evalTacticevalTactic
    (← `(tactic| casesm* WidePullbackShape _,
      (_ : WidePullbackShape _) ⟶ (_ : WidePullbackShape _) ))

Case analysis tactic for wide pullback morphisms

Informal description

An automated tactic that performs case analysis on morphisms in the category `WidePullbackShape J`, handling all possible cases of objects and morphisms in this shape. The tactic is designed to simplify proofs involving wide pullback diagrams by automatically considering all possible cases of morphisms between objects in the wide pullback shape.

CategoryTheory.Limits.WidePullbackShape.subsingleton_hom instance

: Quiver.IsThin (WidePullbackShape J)

Full source

instance subsingleton_hom : Quiver.IsThin (WidePullbackShape J) := fun _ _ => by
  constructor
  intro a b
  casesm* WidePullbackShape _, (_ : WidePullbackShape _) ⟶ (_ : WidePullbackShape _)
  · rfl
  · rfl
  · rfl

Wide Pullback Shape is a Thin Quiver

Informal description

The wide pullback shape category for any type $J$ is a thin quiver, meaning there is at most one morphism between any two objects.

CategoryTheory.Limits.WidePullbackShape.category instance

: SmallCategory (WidePullbackShape J)

Full source

instance category : SmallCategory (WidePullbackShape J) :=
  thin_category

Category Structure on Wide Pullback Shape

Informal description

For any type $J$, the wide pullback shape $\mathrm{WidePullbackShape}\,J$ forms a small category where the objects are elements of $J$ together with an additional terminal object, and there is at most one morphism between any two objects. The morphisms consist of identity morphisms and unique morphisms to the terminal object.

CategoryTheory.Limits.WidePullbackShape.hom_id theorem

(X : WidePullbackShape J) : Hom.id X = 𝟙 X

Full source

@[simp]
theorem hom_id (X : WidePullbackShape J) : Hom.id X = 𝟙 X :=
  rfl

Identity Morphism Equality in Wide Pullback Shape

Informal description

For any object $X$ in the wide pullback shape category, the identity morphism $\mathrm{Hom.id}(X)$ is equal to the identity morphism $\mathbb{1}_X$ in the category structure.

CategoryTheory.Limits.WidePullbackShape.wideCospan definition

(B : C) (objs : J → C) (arrows : ∀ j : J, objs j ⟶ B) : WidePullbackShape J ⥤ C

Full source

/-- Construct a functor out of the wide pullback shape given a J-indexed collection of arrows to a
fixed object.
-/
@[simps]
def wideCospan (B : C) (objs : J → C) (arrows : ∀ j : J, objs j ⟶ B) : WidePullbackShapeWidePullbackShape J ⥤ C where
  obj j := Option.casesOn j B objs
  map f := by
    obtain - | j := f
    · apply 𝟙 _
    · exact arrows j

Wide cospan functor

Informal description

Given an object $B$ in a category $C$, a family of objects $(X_j)_{j \in J}$ indexed by a type $J$, and a family of morphisms $(f_j : X_j \to B)_{j \in J}$, the functor $\mathrm{wideCospan}$ constructs a diagram in $C$ of the form: \[ \begin{tikzcd} & & B \\ X_j \arrow[r, "f_j"] & B & \text{for each } j \in J \end{tikzcd} \] This functor maps the terminal object in $\mathrm{WidePullbackShape}\,J$ to $B$ and each non-terminal object $j \in J$ to $X_j$, with the morphisms given by the $f_j$.

CategoryTheory.Limits.WidePullbackShape.diagramIsoWideCospan definition

(F : WidePullbackShape J ⥤ C) : F ≅ wideCospan (F.obj none) (fun j => F.obj (some j)) fun j => F.map (Hom.term j)

Full source

/-- Every diagram is naturally isomorphic (actually, equal) to a `wideCospan` -/
def diagramIsoWideCospan (F : WidePullbackShapeWidePullbackShape J ⥤ C) :
    F ≅ wideCospan (F.obj none) (fun j => F.obj (some j)) fun j => F.map (Hom.term j) :=
  NatIso.ofComponents fun j => eqToIso <| by aesop_cat

Natural isomorphism between a functor and its wide cospan representation

Informal description

For any functor $ F $ from the wide pullback shape category $\mathrm{WidePullbackShape}\,J$ to a category $ C $, there is a natural isomorphism between $ F $ and the wide cospan functor constructed from: - The object $ F(\mathrm{none}) $ (the image of the terminal object), - The family of objects $ F(\mathrm{some}\,j) $ for each $ j \in J $, - The family of morphisms $ F(\mathrm{Hom.term}\,j) $ for each $ j \in J $. This isomorphism shows that every such functor $ F $ is naturally isomorphic to a diagram formed by a cospan with a common target $ F(\mathrm{none}) $ and sources $ F(\mathrm{some}\,j) $, connected by the morphisms $ F(\mathrm{Hom.term}\,j) $.

CategoryTheory.Limits.WidePullbackShape.mkCone definition

 {F : WidePullbackShape J ⥤ C} {X : C} (f : X ⟶ F.obj none) (π : ∀ j, X ⟶ F.obj (some j))
  (w : ∀ j, π j ≫ F.map (Hom.term j) = f) : Cone F

Full source

/-- Construct a cone over a wide cospan. -/
@[simps]
def mkCone {F : WidePullbackShapeWidePullbackShape J ⥤ C} {X : C} (f : X ⟶ F.obj none) (π : ∀ j, X ⟶ F.obj (some j))
    (w : ∀ j, π j ≫ F.map (Hom.term j) = f) : Cone F :=
  { pt := X
    π :=
      { app := fun j =>
          match j with
          | none => f
          | some j => π j
        naturality := fun j j' f => by
          cases j <;> cases j' <;> cases f <;> dsimp <;> simp [w] } }

Construction of a cone over a wide cospan

Informal description

Given a functor $F \colon \mathrm{WidePullbackShape}\,J \to C$, an object $X$ in $C$, a morphism $f \colon X \to F(\mathrm{none})$, and a family of morphisms $\pi_j \colon X \to F(\mathrm{some}\,j)$ for each $j \in J$ such that $\pi_j \circ F(\mathrm{Hom.term}\,j) = f$ for all $j$, this constructs a cone over $F$ with apex $X$. The cone's natural transformation has components $f$ at $\mathrm{none}$ and $\pi_j$ at each $\mathrm{some}\,j$.

CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv definition

(J' : Type w') (h : J ≃ J') : WidePullbackShape J ≌ WidePullbackShape J'

Full source

/-- Wide pullback diagrams of equivalent index types are equivalent. -/
def equivalenceOfEquiv (J' : Type w') (h : J ≃ J') :
    WidePullbackShapeWidePullbackShape J ≌ WidePullbackShape J' where
  functor := wideCospan none (fun j => some (h j)) fun j => Hom.term (h j)
  inverse := wideCospan none (fun j => some (h.invFun j)) fun j => Hom.term (h.invFun j)
  unitIso := NatIso.ofComponents (fun j => by cases j <;> exact eqToIso (by simp))
  counitIso := NatIso.ofComponents (fun j => by cases j <;> exact eqToIso (by simp))

Equivalence of wide pullback shapes under index type equivalence

Informal description

Given an equivalence $h : J \simeq J'$ between index types $J$ and $J'$, the categories $\mathrm{WidePullbackShape}\,J$ and $\mathrm{WidePullbackShape}\,J'$ are equivalent. The equivalence is constructed using the functors induced by $h$ and its inverse, with natural isomorphisms witnessing the equivalence.

CategoryTheory.Limits.WidePullbackShape.uliftEquivalence definition

: ULiftHom.{w'} (ULift.{w'} (WidePullbackShape J)) ≌ WidePullbackShape (ULift J)

Full source

/-- Lifting universe and morphism levels preserves wide pullback diagrams. -/
def uliftEquivalence :
    ULiftHomULiftHom.{w'} (ULift.{w'} (WidePullbackShape J)) ≌ WidePullbackShape (ULift J) :=
  (ULiftHomULiftCategory.equiv.{w', w', w, w} (WidePullbackShape J)).symm.trans
    (equivalenceOfEquiv _ (Equiv.ulift.{w', w}.symm : J ≃ ULift.{w'} J))

Equivalence between double-lifted wide pullback shape and wide pullback shape of lifted indices

Informal description

The equivalence between the double universe-lifted wide pullback shape $\mathrm{ULiftHom}_{\{w'\}} (\mathrm{ULift}_{\{w'\}} (\mathrm{WidePullbackShape}\,J))$ and the wide pullback shape $\mathrm{WidePullbackShape}\,(\mathrm{ULift}\,J)$ is constructed by: 1. Taking the symmetric equivalence of the double-lifted category $\mathrm{ULiftHom}_{\{w'\}} (\mathrm{ULift}_{\{w'\}} (\mathrm{WidePullbackShape}\,J)) \simeq \mathrm{WidePullbackShape}\,J$, and 2. Composing with the equivalence induced by the symmetric universe-lifting equivalence $J \simeq \mathrm{ULift}\,J$. This equivalence preserves the categorical structure while lifting both objects and morphisms to higher universes.

CategoryTheory.Limits.WidePushoutShape.Hom inductive

: WidePushoutShape J → WidePushoutShape J → Type w

Full source

/-- The type of arrows for the shape indexing a wide pushout. -/
inductive Hom : WidePushoutShape J → WidePushoutShape J → Type w
  | id : ∀ X, Hom X X
  | init : ∀ j : J, Hom none (some j)
  deriving DecidableEq

Morphisms in wide pushout shape category

Informal description

The type of morphisms between objects in the wide pushout shape category, which is constructed by adjoining an initial object to a discrete category indexed by a type $J$. The morphisms include: - Identity morphisms for each object. - Unique morphisms from the initial object to any other object in the category.

CategoryTheory.Limits.WidePushoutShape.instDecidableEqHom instance

 {J✝} {a✝} {a✝¹} [DecidableEq✝ J✝] : DecidableEq✝ (@CategoryTheory.Limits.WidePushoutShape.Hom✝ J✝ a✝ a✝¹)

Full source

DecidableEq

Decidable Equality of Morphisms in Wide Pushout Shape Category

Informal description

For any type $J$ with decidable equality, the morphisms in the wide pushout shape category (formed by adjoining an initial object to $J$) have decidable equality.

CategoryTheory.Limits.WidePushoutShape.struct instance

: CategoryStruct (WidePushoutShape J)

Full source

instance struct : CategoryStruct (WidePushoutShape J) where
  Hom := Hom
  id j := Hom.id j
  comp f g := by
    cases f
    · exact g
    cases g
    apply Hom.init _

Category Structure on Wide Pushout Shape

Informal description

The wide pushout shape category for any type $J$ has a canonical category structure, where the objects are the elements of $J$ together with an initial object, and the morphisms include identity morphisms and unique morphisms from the initial object to any other object.

CategoryTheory.Limits.WidePushoutShape.Hom.inhabited instance

: Inhabited (Hom (none : WidePushoutShape J) none)

Full source

instance Hom.inhabited : Inhabited (Hom (none : WidePushoutShape J) none) :=
  ⟨Hom.id (none : WidePushoutShape J)⟩

Inhabited Morphisms from Initial Object to Itself in Wide Pushout Shape

Informal description

For any type $J$, the morphism set $\mathrm{Hom}(\mathrm{none}, \mathrm{none})$ in the wide pushout shape category (formed by adjoining an initial object $\mathrm{none}$ to $J$) is inhabited.

CategoryTheory.Limits.WidePushoutShape.evalCasesBash' definition

: TacticM Unit

Full source

/-- An aesop tactic for bulk cases on morphisms in `WidePushoutShape` -/
def evalCasesBash' : TacticM Unit := do
  evalTacticevalTactic
    (← `(tactic| casesm* WidePushoutShape _,
      (_ : WidePushoutShape _) ⟶ (_ : WidePushoutShape _) ))

Bulk case analysis tactic for wide pushout morphisms

Informal description

An Aesop tactic for performing bulk case analysis on morphisms in the category `WidePushoutShape J`, which is used to handle wide pushouts.

CategoryTheory.Limits.WidePushoutShape.subsingleton_hom instance

: Quiver.IsThin (WidePushoutShape J)

Full source

instance subsingleton_hom : Quiver.IsThin (WidePushoutShape J) := fun _ _ => by
  constructor
  intro a b
  casesm* WidePushoutShape _, (_ : WidePushoutShape _) ⟶ (_ : WidePushoutShape _)
  repeat rfl

Wide Pushout Shape is a Thin Quiver

Informal description

The wide pushout shape category for any type $J$ is a thin quiver, meaning there is at most one morphism between any two objects.

CategoryTheory.Limits.WidePushoutShape.category instance

: SmallCategory (WidePushoutShape J)

Full source

instance category : SmallCategory (WidePushoutShape J) :=
  thin_category

Small Category Structure on Wide Pushout Shape

Informal description

For any type $J$, the wide pushout shape category (formed by adjoining an initial object to $J$) has the structure of a small category, where there is at most one morphism between any two objects.

CategoryTheory.Limits.WidePushoutShape.hom_id theorem

(X : WidePushoutShape J) : Hom.id X = 𝟙 X

Full source

@[simp]
theorem hom_id (X : WidePushoutShape J) : Hom.id X = 𝟙 X :=
  rfl

Identity Morphism in Wide Pushout Shape Category

Informal description

For any object $X$ in the wide pushout shape category, the identity morphism $\mathrm{Hom.id}\, X$ is equal to the identity morphism $\mathbb{1}_X$ in the category.

CategoryTheory.Limits.WidePushoutShape.wideSpan definition

(B : C) (objs : J → C) (arrows : ∀ j : J, B ⟶ objs j) : WidePushoutShape J ⥤ C

Full source

/-- Construct a functor out of the wide pushout shape given a J-indexed collection of arrows from a
fixed object.
-/
@[simps]
def wideSpan (B : C) (objs : J → C) (arrows : ∀ j : J, B ⟶ objs j) : WidePushoutShapeWidePushoutShape J ⥤ C where
  obj j := Option.casesOn j B objs
  map f := by
    obtain - | j := f
    · apply 𝟙 _
    · exact arrows j
  map_comp := fun f g => by
    cases f
    · simp only [Eq.ndrec, hom_id, eq_rec_constant, Category.id_comp]; congr
    · cases g
      simp only [Eq.ndrec, hom_id, eq_rec_constant, Category.comp_id]; congr

Wide pushout diagram functor

Informal description

Given an object $B$ in a category $C$, a $J$-indexed family of objects $(objs_j)_{j \in J}$ in $C$, and a $J$-indexed family of morphisms $(arrows_j : B \to objs_j)_{j \in J}$, the functor `wideSpan` constructs a diagram in $C$ shaped like a wide pushout. Specifically: - The functor maps the initial object (represented by `none`) to $B$. - The functor maps each $j \in J$ (represented by `some j`) to $objs_j$. - The functor maps the unique morphism from the initial object to each $j \in J$ to the corresponding morphism $arrows_j$. This functor is used to define wide pushout diagrams in $C$.

CategoryTheory.Limits.WidePushoutShape.diagramIsoWideSpan definition

(F : WidePushoutShape J ⥤ C) : F ≅ wideSpan (F.obj none) (fun j => F.obj (some j)) fun j => F.map (Hom.init j)

Full source

/-- Every diagram is naturally isomorphic (actually, equal) to a `wideSpan` -/
def diagramIsoWideSpan (F : WidePushoutShapeWidePushoutShape J ⥤ C) :
    F ≅ wideSpan (F.obj none) (fun j => F.obj (some j)) fun j => F.map (Hom.init j) :=
  NatIso.ofComponents fun j => eqToIso <| by cases j; repeat rfl

Natural isomorphism between a functor and its wide pushout diagram

Informal description

For any functor $ F $ from the wide pushout shape category (for some type $ J $) to a category $ C $, there is a natural isomorphism between $ F $ and the wide pushout diagram functor `wideSpan` constructed from: - The object $ F(\text{none}) $ (the image of the initial object), - The family of objects $ F(\text{some } j) $ for each $ j \in J $, - The family of morphisms $ F(\text{Hom.init } j) : F(\text{none}) \to F(\text{some } j) $ for each $ j \in J $. This isomorphism is componentwise given by the identity morphism, since the objects and morphisms are definitionally equal.

CategoryTheory.Limits.WidePushoutShape.mkCocone definition

 {F : WidePushoutShape J ⥤ C} {X : C} (f : F.obj none ⟶ X) (ι : ∀ j, F.obj (some j) ⟶ X)
  (w : ∀ j, F.map (Hom.init j) ≫ ι j = f) : Cocone F

Full source

/-- Construct a cocone over a wide span. -/
@[simps]
def mkCocone {F : WidePushoutShapeWidePushoutShape J ⥤ C} {X : C} (f : F.obj none ⟶ X) (ι : ∀ j, F.obj (some j) ⟶ X)
    (w : ∀ j, F.map (Hom.init j) ≫ ι j = f) : Cocone F :=
  { pt := X
    ι :=
      { app := fun j =>
          match j with
          | none => f
          | some j => ι j
        naturality := fun j j' f => by
          cases j <;> cases j' <;> cases f <;> dsimp <;> simp [w] } }

Cocone construction for wide pushout shape

Informal description

Given a functor $ F $ from the wide pushout shape category (for some type $ J $) to a category $ C $, an object $ X $ in $ C $, a morphism $ f : F(\text{none}) \to X $, and for each $ j \in J $ a morphism $ \iota_j : F(\text{some } j) \to X $ such that for all $ j $, the composition $ F(\text{Hom.init } j) \circ \iota_j = f $, this constructs a cocone over $ F $ with apex $ X $. The cocone's natural transformation has components $ f $ at none and $ \iota_j $ at each some $ j $, and the naturality condition is satisfied by the given compatibility condition $ w $.

CategoryTheory.Limits.WidePushoutShape.equivalenceOfEquiv definition

(J' : Type w') (h : J ≃ J') : WidePushoutShape J ≌ WidePushoutShape J'

Full source

/-- Wide pushout diagrams of equivalent index types are equivalent. -/
def equivalenceOfEquiv (J' : Type w') (h : J ≃ J') : WidePushoutShapeWidePushoutShape J ≌ WidePushoutShape J' where
  functor := wideSpan none (fun j => some (h j)) fun j => Hom.init (h j)
  inverse := wideSpan none (fun j => some (h.invFun j)) fun j => Hom.init (h.invFun j)
  unitIso := NatIso.ofComponents (fun j => by cases j <;> exact eqToIso (by simp))
  counitIso := NatIso.ofComponents (fun j => by cases j <;> exact eqToIso (by simp))

Equivalence of wide pushout shapes under type equivalence

Informal description

Given an equivalence $h : J \simeq J'$ between types $J$ and $J'$, the wide pushout shapes $\text{WidePushoutShape } J$ and $\text{WidePushoutShape } J'$ are equivalent as categories. The equivalence is constructed using the functors induced by $h$ and its inverse, with natural isomorphisms witnessing the equivalence.

CategoryTheory.Limits.WidePushoutShape.uliftEquivalence definition

: ULiftHom.{w'} (ULift.{w'} (WidePushoutShape J)) ≌ WidePushoutShape (ULift J)

Full source

/-- Lifting universe and morphism levels preserves wide pushout diagrams. -/
def uliftEquivalence :
    ULiftHomULiftHom.{w'} (ULift.{w'} (WidePushoutShape J)) ≌ WidePushoutShape (ULift J) :=
  (ULiftHomULiftCategory.equiv.{w', w', w, w} (WidePushoutShape J)).symm.trans
    (equivalenceOfEquiv _ (Equiv.ulift.{w', w}.symm : J ≃ ULift.{w'} J))

Equivalence between double-lifted and universe-lifted wide pushout shapes

Informal description

The equivalence between the double universe-lifted wide pushout shape $\mathrm{ULiftHom}_{\{w'\}} (\mathrm{ULift}_{\{w'\}} (\text{WidePushoutShape } J))$ and the wide pushout shape $\text{WidePushoutShape } (\mathrm{ULift} J)$ is constructed by: 1. Taking the symmetric equivalence of the double-lifted category $\mathrm{ULiftHom}_{\{w'\}} (\mathrm{ULift}_{\{w'\}} (\text{WidePushoutShape } J)) \simeq \text{WidePushoutShape } J$, and 2. Composing with the equivalence $\text{WidePushoutShape } J \simeq \text{WidePushoutShape } (\mathrm{ULift} J)$ induced by the type equivalence $\mathrm{ULift}^{-1} : J \simeq \mathrm{ULift} J$. This equivalence preserves the categorical structure while lifting both objects and morphisms to higher universes.

CategoryTheory.Limits.HasWidePullbacks abbrev

: Prop

Full source

/-- `HasWidePullbacks` represents a choice of wide pullback for every collection of morphisms -/
abbrev HasWidePullbacks : Prop :=
  ∀ J : Type w, HasLimitsOfShape (WidePullbackShape J) C

Existence of Wide Pullbacks in a Category

Informal description

A category $\mathcal{C}$ has wide pullbacks if for every type $J$ and every collection of morphisms $\{f_j : X_j \to B\}_{j \in J}$ in $\mathcal{C}$, there exists a wide pullback (i.e., a limit of the corresponding wide cospan diagram).

CategoryTheory.Limits.HasWidePushouts abbrev

: Prop

Full source

/-- `HasWidePushouts` represents a choice of wide pushout for every collection of morphisms -/
abbrev HasWidePushouts : Prop :=
  ∀ J : Type w, HasColimitsOfShape (WidePushoutShape J) C

Existence of Wide Pushouts in a Category

Informal description

A category $\mathcal{C}$ has wide pushouts if for every collection of morphisms with a common domain, there exists a colimit cocone (i.e., a pushout) for the corresponding diagram.

CategoryTheory.Limits.HasWidePullback abbrev

(B : C) (objs : J → C) (arrows : ∀ j : J, objs j ⟶ B) : Prop

Full source

/-- `HasWidePullback B objs arrows` means that `wideCospan B objs arrows` has a limit. -/
abbrev HasWidePullback (B : C) (objs : J → C) (arrows : ∀ j : J, objs j ⟶ B) : Prop :=
  HasLimit (WidePullbackShape.wideCospan B objs arrows)

Existence of Wide Pullback for a Given Cospan

Informal description

Given a category $\mathcal{C}$, an object $B$ in $\mathcal{C}$, a family of objects $(X_j)_{j \in J}$ indexed by a type $J$, and a family of morphisms $(f_j : X_j \to B)_{j \in J}$, the proposition $\mathrm{HasWidePullback}\,B\,(X_j)\,(f_j)$ asserts that the wide cospan diagram formed by $B$, $(X_j)$, and $(f_j)$ has a limit in $\mathcal{C}$.

CategoryTheory.Limits.HasWidePushout abbrev

(B : C) (objs : J → C) (arrows : ∀ j : J, B ⟶ objs j) : Prop

Full source

/-- `HasWidePushout B objs arrows` means that `wideSpan B objs arrows` has a colimit. -/
abbrev HasWidePushout (B : C) (objs : J → C) (arrows : ∀ j : J, B ⟶ objs j) : Prop :=
  HasColimit (WidePushoutShape.wideSpan B objs arrows)

Existence of Wide Pushout for Given Diagram

Informal description

Given a category $\mathcal{C}$, an object $B$ in $\mathcal{C}$, a family of objects $(objs_j)_{j \in J}$ in $\mathcal{C}$, and a family of morphisms $(arrows_j : B \to objs_j)_{j \in J}$, the proposition $\text{HasWidePushout}(B, objs, arrows)$ asserts that the diagram formed by these objects and morphisms (via the functor $\text{wideSpan}$) has a colimit in $\mathcal{C}$. This colimit is called a *wide pushout*.

CategoryTheory.Limits.widePullback abbrev

(B : C) (objs : J → C) (arrows : ∀ j : J, objs j ⟶ B) [HasWidePullback B objs arrows] : C

Full source

/-- A choice of wide pullback. -/
noncomputable abbrev widePullback (B : C) (objs : J → C) (arrows : ∀ j : J, objs j ⟶ B)
    [HasWidePullback B objs arrows] : C :=
  limit (WidePullbackShape.wideCospan B objs arrows)

Wide Pullback Object for a Given Cospan

Informal description

Given a category $\mathcal{C}$, an object $B$ in $\mathcal{C}$, a family of objects $(X_j)_{j \in J}$ indexed by a type $J$, and a family of morphisms $(f_j : X_j \to B)_{j \in J}$, the object $\mathrm{widePullback}\,B\,(X_j)\,(f_j)$ is the limit of the wide cospan diagram formed by these objects and morphisms, provided that such a limit exists (i.e., when $\mathrm{HasWidePullback}\,B\,(X_j)\,(f_j)$ holds). This object satisfies the universal property of being the vertex of a cone over the wide cospan diagram, with a unique morphism from any other such cone.

CategoryTheory.Limits.widePushout abbrev

(B : C) (objs : J → C) (arrows : ∀ j : J, B ⟶ objs j) [HasWidePushout B objs arrows] : C

Full source

/-- A choice of wide pushout. -/
noncomputable abbrev widePushout (B : C) (objs : J → C) (arrows : ∀ j : J, B ⟶ objs j)
    [HasWidePushout B objs arrows] : C :=
  colimit (WidePushoutShape.wideSpan B objs arrows)

Wide pushout of a family of morphisms

Informal description

Given a category $\mathcal{C}$, an object $B$ in $\mathcal{C}$, a family of objects $(X_j)_{j \in J}$ in $\mathcal{C}$, and a family of morphisms $(f_j : B \to X_j)_{j \in J}$, the wide pushout $\text{widePushout}(B, X_j, f_j)$ is the colimit of the diagram formed by these objects and morphisms (when it exists).

CategoryTheory.Limits.WidePullback.π abbrev

(j : J) : widePullback _ _ arrows ⟶ objs j

Full source

/-- The `j`-th projection from the pullback. -/
noncomputable abbrev π (j : J) : widePullbackwidePullback _ _ arrows ⟶ objs j :=
  limit.π (WidePullbackShape.wideCospan _ _ _) (Option.some j)

Projection morphism from wide pullback to $j$-th object

Informal description

For each index $j$ in the indexing type $J$, the morphism $\pi_j : \mathrm{widePullback}\,B\,(X_k)\,(f_k) \to X_j$ is the $j$-th projection from the wide pullback object to the object $X_j$ in the diagram.

CategoryTheory.Limits.WidePullback.base abbrev

: widePullback _ _ arrows ⟶ B

Full source

/-- The unique map to the base from the pullback. -/
noncomputable abbrev base : widePullbackwidePullback _ _ arrows ⟶ B :=
  limit.π (WidePullbackShape.wideCospan _ _ _) Option.none

Base Morphism from Wide Pullback to Base Object

Informal description

Given a category $\mathcal{C}$, an object $B$ in $\mathcal{C}$, a family of objects $(X_j)_{j \in J}$ indexed by a type $J$, and a family of morphisms $(f_j : X_j \to B)_{j \in J}$, the morphism $\mathrm{base} : \mathrm{widePullback}\,B\,(X_j)\,(f_j) \to B$ is the unique map from the wide pullback object to the base object $B$, induced by the universal property of the wide pullback.

CategoryTheory.Limits.WidePullback.π_arrow theorem

(j : J) : π arrows j ≫ arrows _ = base arrows

Full source

@[reassoc (attr := simp)]
theorem π_arrow (j : J) : ππ arrows j ≫ arrows _ = base arrows := by
  apply limit.w (WidePullbackShape.wideCospan _ _ _) (WidePullbackShape.Hom.term j)

Commutativity of Wide Pullback Projections with Base Morphism

Informal description

For each index $j$ in the indexing type $J$, the composition of the projection morphism $\pi_j \colon \mathrm{widePullback}\,B\,(X_k)\,(f_k) \to X_j$ with the morphism $f_j \colon X_j \to B$ equals the base morphism $\mathrm{base} \colon \mathrm{widePullback}\,B\,(X_k)\,(f_k) \to B$. In other words, the diagram \[ \begin{tikzcd} \mathrm{widePullback}\,B\,(X_k)\,(f_k) \arrow[rd, "\mathrm{base}"'] \arrow[r, "\pi_j"] & X_j \arrow[d, "f_j"] \\ & B \end{tikzcd} \] commutes for all $j \in J$.

CategoryTheory.Limits.WidePullback.lift abbrev

{X : C} (f : X ⟶ B) (fs : ∀ j : J, X ⟶ objs j) (w : ∀ j, fs j ≫ arrows j = f) : X ⟶ widePullback _ _ arrows

Full source

/-- Lift a collection of morphisms to a morphism to the pullback. -/
noncomputable abbrev lift {X : C} (f : X ⟶ B) (fs : ∀ j : J, X ⟶ objs j)
    (w : ∀ j, fs j ≫ arrows j = f) : X ⟶ widePullback _ _ arrows :=
  limit.lift (WidePullbackShape.wideCospan _ _ _) (WidePullbackShape.mkCone f fs <| w)

Universal Property of Wide Pullback

Informal description

Given a category $\mathcal{C}$, an object $B$ in $\mathcal{C}$, a family of objects $(X_j)_{j \in J}$ indexed by a type $J$, and a family of morphisms $(f_j : X_j \to B)_{j \in J}$ forming a wide cospan, suppose the wide pullback of this cospan exists. Then for any object $X$ in $\mathcal{C}$ equipped with a morphism $f : X \to B$ and a family of morphisms $(g_j : X \to X_j)_{j \in J}$ such that $g_j \circ f_j = f$ for all $j \in J$, there exists a unique morphism $\mathrm{lift}(f, (g_j), w) : X \to \mathrm{widePullback}(B, (X_j), (f_j))$ that factors through the wide pullback diagram.

CategoryTheory.Limits.WidePullback.lift_π theorem

(j : J) : lift f fs w ≫ π arrows j = fs _

Full source

@[reassoc]
theorem lift_π (j : J) : liftlift f fs w ≫ π arrows j = fs _ := by
  simp only [limit.lift_π, WidePullbackShape.mkCone_pt, WidePullbackShape.mkCone_π_app]

Commutativity of the Universal Morphism with Projections in a Wide Pullback

Informal description

Given a wide pullback diagram in a category $\mathcal{C}$ with objects $(X_j)_{j \in J}$ and morphisms $(f_j : X_j \to B)_{j \in J}$, for any object $X$ equipped with a morphism $f : X \to B$ and a family of morphisms $(g_j : X \to X_j)_{j \in J}$ such that $g_j \circ f_j = f$ for all $j \in J$, the composition of the induced morphism $\mathrm{lift}(f, (g_j), w) : X \to \mathrm{widePullback}(B, (X_j), (f_j))$ with the $j$-th projection $\pi_j$ equals $g_j$, i.e., \[ \mathrm{lift}(f, (g_j), w) \circ \pi_j = g_j. \]

CategoryTheory.Limits.WidePullback.lift_base theorem

: lift f fs w ≫ base arrows = f

Full source

@[reassoc]
theorem lift_base : liftlift f fs w ≫ base arrows = f := by
  simp only [limit.lift_π, WidePullbackShape.mkCone_pt, WidePullbackShape.mkCone_π_app]

Commutativity of the Induced Morphism with the Base Morphism in a Wide Pullback

Informal description

Given a category $\mathcal{C}$, an object $B$ in $\mathcal{C}$, a family of objects $(X_j)_{j \in J}$ indexed by a type $J$, and a family of morphisms $(f_j : X_j \to B)_{j \in J}$ forming a wide cospan, suppose the wide pullback of this cospan exists. Let $X$ be an object in $\mathcal{C}$ equipped with a morphism $f : X \to B$ and a family of morphisms $(g_j : X \to X_j)_{j \in J}$ such that $g_j \circ f_j = f$ for all $j \in J$. Then the composition of the induced morphism $\mathrm{lift}(f, (g_j)) : X \to \mathrm{widePullback}(B, (X_j), (f_j))$ with the base morphism $\mathrm{base} : \mathrm{widePullback}(B, (X_j), (f_j)) \to B$ equals $f$, i.e., \[ \mathrm{lift}(f, (g_j)) \circ \mathrm{base} = f. \]

CategoryTheory.Limits.WidePullback.hom_eq_lift theorem

(g : X ⟶ widePullback _ _ arrows) : g = lift (g ≫ base arrows) (fun j => g ≫ π arrows j) (by simp)

Full source

theorem hom_eq_lift (g : X ⟶ widePullback _ _ arrows) :
    g = lift (g ≫ base arrows) (fun j => g ≫ π arrows j) (by simp) := by
  apply eq_lift_of_comp_eq
  · simp
  · rfl

Universal Property of Wide Pullback Induces Unique Morphism Factorization

Informal description

Let $\mathcal{C}$ be a category with a wide pullback of a cospan consisting of an object $B$ and a family of objects $(X_j)_{j \in J}$ with morphisms $(f_j : X_j \to B)_{j \in J}$. For any morphism $g : X \to \mathrm{widePullback}(B, X_j, f_j)$, $g$ is equal to the unique morphism induced by the universal property of the wide pullback, constructed from the compositions $g \circ \mathrm{base}$ and $(g \circ \pi_j)_{j \in J}$, where $\mathrm{base} : \mathrm{widePullback}(B, X_j, f_j) \to B$ is the base morphism and $\pi_j : \mathrm{widePullback}(B, X_j, f_j) \to X_j$ are the projection morphisms.

CategoryTheory.Limits.WidePullback.hom_ext theorem

 (g1 g2 : X ⟶ widePullback _ _ arrows) :
  (∀ j : J, g1 ≫ π arrows j = g2 ≫ π arrows j) → g1 ≫ base arrows = g2 ≫ base arrows → g1 = g2

Full source

@[ext 1100]
theorem hom_ext (g1 g2 : X ⟶ widePullback _ _ arrows) : (∀ j : J,
    g1 ≫ π arrows j = g2 ≫ π arrows j) → g1 ≫ base arrows = g2 ≫ base arrows → g1 = g2 := by
  intro h1 h2
  apply limit.hom_ext
  rintro (_ | _)
  · apply h2
  · apply h1

Uniqueness of Morphisms into Wide Pullback via Projections and Base Map

Informal description

Let $\mathcal{C}$ be a category, $B$ an object in $\mathcal{C}$, $(X_j)_{j \in J}$ a family of objects indexed by $J$, and $(f_j : X_j \to B)_{j \in J}$ a family of morphisms forming a wide cospan. For any object $X$ in $\mathcal{C}$ and any two morphisms $g_1, g_2 : X \to \mathrm{widePullback}(B, X_j, f_j)$, if for all $j \in J$ the compositions $g_1 \circ \pi_j = g_2 \circ \pi_j$ (where $\pi_j$ is the projection to $X_j$) and $g_1 \circ \mathrm{base} = g_2 \circ \mathrm{base}$ (where $\mathrm{base}$ is the morphism to $B$), then $g_1 = g_2$.

CategoryTheory.Limits.WidePushout.ι abbrev

(j : J) : objs j ⟶ widePushout _ _ arrows

Full source

/-- The `j`-th inclusion to the pushout. -/
noncomputable abbrev ι (j : J) : objs j ⟶ widePushout _ _ arrows :=
  colimit.ι (WidePushoutShape.wideSpan _ _ _) (Option.some j)

Inclusion morphism into wide pushout

Informal description

For each index $j$ in the indexing type $J$, the morphism $\iota_j : X_j \to \text{widePushout}(B, X_j, f_j)$ is the canonical inclusion from the object $X_j$ into the wide pushout of the family of morphisms $(f_j : B \to X_j)_{j \in J}$.

CategoryTheory.Limits.WidePushout.head abbrev

: B ⟶ widePushout B objs arrows

Full source

/-- The unique map from the head to the pushout. -/
noncomputable abbrev head : B ⟶ widePushout B objs arrows :=
  colimit.ι (WidePushoutShape.wideSpan _ _ _) Option.none

Universal Morphism from Base to Wide Pushout

Informal description

Given a category $\mathcal{C}$, an object $B$ in $\mathcal{C}$, a family of objects $(X_j)_{j \in J}$ in $\mathcal{C}$, and a family of morphisms $(f_j : B \to X_j)_{j \in J}$, the morphism $\text{head} : B \to \text{widePushout}(B, X_j, f_j)$ is the unique map from $B$ to the wide pushout object.

CategoryTheory.Limits.WidePushout.arrow_ι theorem

(j : J) : arrows j ≫ ι arrows j = head arrows

Full source

@[reassoc, simp]
theorem arrow_ι (j : J) : arrows j ≫ ι arrows j = head arrows := by
  apply colimit.w (WidePushoutShape.wideSpan _ _ _) (WidePushoutShape.Hom.init j)

Commutativity of Wide Pushout Diagram: $f_j \circ \iota_j = \text{head}$

Informal description

For any index $j$ in the indexing type $J$, the composition of the morphism $f_j \colon B \to X_j$ with the inclusion morphism $\iota_j \colon X_j \to \text{widePushout}(B, (X_j)_{j \in J}, (f_j)_{j \in J})$ equals the universal morphism $\text{head} \colon B \to \text{widePushout}(B, (X_j)_{j \in J}, (f_j)_{j \in J})$. In other words, the diagram \[ B \xrightarrow{f_j} X_j \xrightarrow{\iota_j} \text{widePushout}(B, (X_j)_{j \in J}, (f_j)_{j \in J}) \] commutes for all $j \in J$.

CategoryTheory.Limits.WidePushout.desc abbrev

{X : C} (f : B ⟶ X) (fs : ∀ j : J, objs j ⟶ X) (w : ∀ j, arrows j ≫ fs j = f) : widePushout _ _ arrows ⟶ X

Full source

/-- Descend a collection of morphisms to a morphism from the pushout. -/
noncomputable abbrev desc {X : C} (f : B ⟶ X) (fs : ∀ j : J, objs j ⟶ X)
    (w : ∀ j, arrows j ≫ fs j = f) : widePushoutwidePushout _ _ arrows ⟶ X :=
  colimit.desc (WidePushoutShape.wideSpan B objs arrows) (WidePushoutShape.mkCocone f fs <| w)

Universal Property of Wide Pushout

Informal description

Given a category $\mathcal{C}$, an object $B$ in $\mathcal{C}$, a family of objects $(X_j)_{j \in J}$ in $\mathcal{C}$, and a family of morphisms $(f_j : B \to X_j)_{j \in J}$ such that the wide pushout $\text{widePushout}(B, X_j, f_j)$ exists, suppose we have: - A morphism $f : B \to X$ to some object $X$ in $\mathcal{C}$, - For each $j \in J$, a morphism $g_j : X_j \to X$, such that for all $j \in J$, the diagram commutes: $f_j \circ g_j = f$. Then there exists a unique morphism $\text{desc}(f, (g_j)_{j \in J}) : \text{widePushout}(B, X_j, f_j) \to X$ that makes all resulting diagrams commute.

CategoryTheory.Limits.WidePushout.ι_desc theorem

(j : J) : ι arrows j ≫ desc f fs w = fs _

Full source

@[reassoc]
theorem ι_desc (j : J) : ιι arrows j ≫ desc f fs w = fs _ := by
  simp only [colimit.ι_desc, WidePushoutShape.mkCocone_pt, WidePushoutShape.mkCocone_ι_app]

Commutativity of Inclusion with Universal Morphism in Wide Pushout

Informal description

For any index $j \in J$, the composition of the inclusion morphism $\iota_j \colon X_j \to \text{widePushout}(B, X_j, f_j)$ with the universal morphism $\text{desc}(f, (g_j)_{j \in J}) \colon \text{widePushout}(B, X_j, f_j) \to X$ equals the morphism $g_j \colon X_j \to X$.

CategoryTheory.Limits.WidePushout.head_desc theorem

: head arrows ≫ desc f fs w = f

Full source

@[reassoc]
theorem head_desc : headhead arrows ≫ desc f fs w = f := by
  simp only [colimit.ι_desc, WidePushoutShape.mkCocone_pt, WidePushoutShape.mkCocone_ι_app]

Commutativity of Head with Descending Morphism in Wide Pushout

Informal description

Given a category $\mathcal{C}$, an object $B$ in $\mathcal{C}$, a family of objects $(X_j)_{j \in J}$ in $\mathcal{C}$, and a family of morphisms $(f_j : B \to X_j)_{j \in J}$ such that the wide pushout $\text{widePushout}(B, X_j, f_j)$ exists, suppose we have: - A morphism $f : B \to X$ to some object $X$ in $\mathcal{C}$, - For each $j \in J$, a morphism $g_j : X_j \to X$, such that for all $j \in J$, the diagram commutes: $f_j \circ g_j = f$. Then the composition of the universal morphism $\text{head} : B \to \text{widePushout}(B, X_j, f_j)$ with the descending morphism $\text{desc}(f, (g_j)_{j \in J}) : \text{widePushout}(B, X_j, f_j) \to X$ equals $f$.

CategoryTheory.Limits.WidePushout.hom_eq_desc theorem

 (g : widePushout _ _ arrows ⟶ X) :
  g =
    desc (head arrows ≫ g) (fun j => ι arrows j ≫ g) fun j =>
      by
      rw [← Category.assoc]
      simp

Full source

theorem hom_eq_desc (g : widePushoutwidePushout _ _ arrows ⟶ X) :
    g =
      desc (headhead arrows ≫ g) (fun j => ιι arrows j ≫ g) fun j => by
        rw [← Category.assoc]
        simp := by
  apply eq_desc_of_comp_eq
  · simp
  · rfl

Universal Property of Wide Pushout: Morphism Factorization via Desc

Informal description

Let $\mathcal{C}$ be a category, $B$ an object in $\mathcal{C}$, $(X_j)_{j \in J}$ a family of objects in $\mathcal{C}$, and $(f_j : B \to X_j)_{j \in J}$ a family of morphisms with a wide pushout $\text{widePushout}(B, X_j, f_j)$. For any morphism $g : \text{widePushout}(B, X_j, f_j) \to X$ to some object $X$ in $\mathcal{C}$, we have \[ g = \text{desc}(\text{head} \circ g, (\iota_j \circ g)_{j \in J}), \] where $\text{desc}$ is the universal morphism from the wide pushout, $\text{head} : B \to \text{widePushout}(B, X_j, f_j)$ is the canonical morphism, and $\iota_j : X_j \to \text{widePushout}(B, X_j, f_j)$ are the inclusion morphisms.

CategoryTheory.Limits.WidePushout.hom_ext theorem

 (g1 g2 : widePushout _ _ arrows ⟶ X) :
  (∀ j : J, ι arrows j ≫ g1 = ι arrows j ≫ g2) → head arrows ≫ g1 = head arrows ≫ g2 → g1 = g2

Full source

@[ext 1100]
theorem hom_ext (g1 g2 : widePushoutwidePushout _ _ arrows ⟶ X) : (∀ j : J,
    ιι arrows j ≫ g1 = ιι arrows j ≫ g2) → headhead arrows ≫ g1 = headhead arrows ≫ g2 → g1 = g2 := by
  intro h1 h2
  apply colimit.hom_ext
  rintro (_ | _)
  · apply h2
  · apply h1

Uniqueness of Morphisms from Wide Pushout via Commuting Diagrams

Informal description

Let $\mathcal{C}$ be a category, $B$ an object in $\mathcal{C}$, $(X_j)_{j \in J}$ a family of objects in $\mathcal{C}$, and $(f_j : B \to X_j)_{j \in J}$ a family of morphisms with a wide pushout $\text{widePushout}(B, X_j, f_j)$. For any object $X$ in $\mathcal{C}$ and any two morphisms $g_1, g_2 : \text{widePushout}(B, X_j, f_j) \to X$, if: 1. For all $j \in J$, the compositions $\iota_j \circ g_1 = \iota_j \circ g_2$ (where $\iota_j : X_j \to \text{widePushout}(B, X_j, f_j)$ are the inclusion morphisms), and 2. The compositions $\text{head} \circ g_1 = \text{head} \circ g_2$ (where $\text{head} : B \to \text{widePushout}(B, X_j, f_j)$ is the universal morphism), then $g_1 = g_2$.

CategoryTheory.Limits.widePullbackShapeOpMap definition

 : ∀ X Y : WidePullbackShape J, (X ⟶ Y) → ((op X : (WidePushoutShape J)ᵒᵖ) ⟶ (op Y : (WidePushoutShape J)ᵒᵖ))

Full source

/-- The action on morphisms of the obvious functor
  `WidePullbackShape_op : WidePullbackShape J ⥤ (WidePushoutShape J)ᵒᵖ` -/
def widePullbackShapeOpMap :
    ∀ X Y : WidePullbackShape J,
      (X ⟶ Y) → ((op X : (WidePushoutShape J)ᵒᵖ) ⟶ (op Y : (WidePushoutShape J)ᵒᵖ))
  | _, _, WidePullbackShape.Hom.id X => Quiver.Hom.op (WidePushoutShape.Hom.id _)
  | _, _, WidePullbackShape.Hom.term _ => Quiver.Hom.op (WidePushoutShape.Hom.init _)

Opposite morphism mapping for wide pullback shapes

Informal description

The function maps a morphism $f : X \longrightarrow Y$ in the wide pullback shape category to its opposite morphism $\mathrm{op}\, f : \mathrm{op}\, Y \longrightarrow \mathrm{op}\, X$ in the opposite of the wide pushout shape category. Specifically: - The identity morphism $\mathrm{id}_X$ is mapped to the opposite of the identity morphism $\mathrm{id}_{\mathrm{op}\, X}$. - The unique morphism $\mathrm{term}_j$ to the terminal object is mapped to the opposite of the unique morphism $\mathrm{init}_j$ from the initial object.

CategoryTheory.Limits.widePullbackShapeOp definition

: WidePullbackShape J ⥤ (WidePushoutShape J)ᵒᵖ

Full source

/-- The obvious functor `WidePullbackShape J ⥤ (WidePushoutShape J)ᵒᵖ` -/
@[simps]
def widePullbackShapeOp : WidePullbackShapeWidePullbackShape J ⥤ (WidePushoutShape J)ᵒᵖ where
  obj X := op X
  map {X₁} {X₂} := widePullbackShapeOpMap J X₁ X₂

Opposite functor between wide pullback and pushout shapes

Informal description

The functor from the wide pullback shape category over a type $J$ to the opposite of the wide pushout shape category over $J$. It maps objects $X$ to their opposites $\mathrm{op}\, X$ and morphisms $f : X \to Y$ to their opposites $\mathrm{op}\, f : \mathrm{op}\, Y \to \mathrm{op}\, X$.

CategoryTheory.Limits.widePushoutShapeOpMap definition

 : ∀ X Y : WidePushoutShape J, (X ⟶ Y) → ((op X : (WidePullbackShape J)ᵒᵖ) ⟶ (op Y : (WidePullbackShape J)ᵒᵖ))

Full source

/-- The action on morphisms of the obvious functor
`widePushoutShapeOp : WidePushoutShape J ⥤ (WidePullbackShape J)ᵒᵖ` -/
def widePushoutShapeOpMap :
    ∀ X Y : WidePushoutShape J,
      (X ⟶ Y) → ((op X : (WidePullbackShape J)ᵒᵖ) ⟶ (op Y : (WidePullbackShape J)ᵒᵖ))
  | _, _, WidePushoutShape.Hom.id X => Quiver.Hom.op (WidePullbackShape.Hom.id _)
  | _, _, WidePushoutShape.Hom.init _ => Quiver.Hom.op (WidePullbackShape.Hom.term _)

Opposite morphism mapping for wide pushout shapes

Informal description

The function maps morphisms in the wide pushout shape category to their opposites in the opposite of the wide pullback shape category. Specifically: - The identity morphism $\text{id}_X$ is mapped to the opposite of the identity morphism $\text{id}_{\text{op}\,X}$. - The unique morphism $\text{init}_j$ from the initial object is mapped to the opposite of the unique morphism $\text{term}_j$ to the terminal object.

CategoryTheory.Limits.widePushoutShapeOp definition

: WidePushoutShape J ⥤ (WidePullbackShape J)ᵒᵖ

Full source

/-- The obvious functor `WidePushoutShape J ⥤ (WidePullbackShape J)ᵒᵖ` -/
@[simps]
def widePushoutShapeOp : WidePushoutShapeWidePushoutShape J ⥤ (WidePullbackShape J)ᵒᵖ where
  obj X := op X
  map := fun {X} {Y} => widePushoutShapeOpMap J X Y

Opposite functor from wide pushout to wide pullback shapes

Informal description

The functor from the wide pushout shape category to the opposite of the wide pullback shape category, which maps objects by taking opposites and morphisms via the function `widePushoutShapeOpMap`.

CategoryTheory.Limits.widePullbackShapeUnop definition

: (WidePullbackShape J)ᵒᵖ ⥤ WidePushoutShape J

Full source

/-- The obvious functor `(WidePullbackShape J)ᵒᵖ ⥤ WidePushoutShape J` -/
@[simps!]
def widePullbackShapeUnop : (WidePullbackShape J)ᵒᵖ(WidePullbackShape J)ᵒᵖ ⥤ WidePushoutShape J :=
  (widePullbackShapeOp J).leftOp

Unopposite functor from wide pullback to wide pushout shapes

Informal description

The functor from the opposite of the wide pullback shape category over a type $J$ to the wide pushout shape category over $J$. It maps objects $X$ in $(WidePullbackShape J)^{\mathrm{op}}$ to their unopposite versions in $WidePushoutShape J$, and similarly for morphisms. This functor is constructed as the left opposite of the functor $widePullbackShapeOp J$.

CategoryTheory.Limits.widePushoutShapeUnop definition

: (WidePushoutShape J)ᵒᵖ ⥤ WidePullbackShape J

Full source

/-- The obvious functor `(WidePushoutShape J)ᵒᵖ ⥤ WidePullbackShape J` -/
@[simps!]
def widePushoutShapeUnop : (WidePushoutShape J)ᵒᵖ(WidePushoutShape J)ᵒᵖ ⥤ WidePullbackShape J :=
  (widePushoutShapeOp J).leftOp

Opposite functor from wide pushout to wide pullback shapes

Informal description

The functor from the opposite of the wide pushout shape category to the wide pullback shape category, obtained by applying the left opposite construction to the functor `widePushoutShapeOp`.

CategoryTheory.Limits.widePushoutShapeOpUnop definition

: widePushoutShapeUnop J ⋙ widePullbackShapeOp J ≅ 𝟭 _

Full source

/-- The inverse of the unit isomorphism of the equivalence
`widePushoutShapeOpEquiv : (WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J` -/
def widePushoutShapeOpUnop : widePushoutShapeUnopwidePushoutShapeUnop J ⋙ widePullbackShapeOp JwidePushoutShapeUnop J ⋙ widePullbackShapeOp J ≅ 𝟭 _ :=
  NatIso.ofComponents fun _ => Iso.refl _

Isomorphism between composed pushout-pullback functors and identity

Informal description

The natural isomorphism witnessing that the composition of the functor `widePushoutShapeUnop J` (from the opposite of the wide pushout shape to the wide pullback shape) with the functor `widePullbackShapeOp J` (from the wide pullback shape to the opposite of the wide pushout shape) is isomorphic to the identity functor on the opposite of the wide pushout shape. Concretely, this means that for every object $X$ in $(WidePushoutShape J)^{\mathrm{op}}$, there is an isomorphism $(widePushoutShapeUnop J \circ widePullbackShapeOp J)(X) \cong X$ which is natural in $X$.

CategoryTheory.Limits.widePushoutShapeUnopOp definition

: widePushoutShapeOp J ⋙ widePullbackShapeUnop J ≅ 𝟭 _

Full source

/-- The counit isomorphism of the equivalence
`widePullbackShapeOpEquiv : (WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J` -/
def widePushoutShapeUnopOp : widePushoutShapeOpwidePushoutShapeOp J ⋙ widePullbackShapeUnop JwidePushoutShapeOp J ⋙ widePullbackShapeUnop J ≅ 𝟭 _ :=
  NatIso.ofComponents fun _ => Iso.refl _

Identity isomorphism for wide pushout shape unop-op composition

Informal description

The natural isomorphism witnessing that the composition of the functor `widePushoutShapeOp` from the wide pushout shape to the opposite of the wide pullback shape, followed by the functor `widePullbackShapeUnop` from the opposite of the wide pullback shape back to the wide pushout shape, is naturally isomorphic to the identity functor on the wide pushout shape category. Concretely, for every object in the wide pushout shape, this isomorphism is given by the identity isomorphism.

CategoryTheory.Limits.widePullbackShapeOpUnop definition

: widePullbackShapeUnop J ⋙ widePushoutShapeOp J ≅ 𝟭 _

Full source

/-- The inverse of the unit isomorphism of the equivalence
`widePullbackShapeOpEquiv : (WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J` -/
def widePullbackShapeOpUnop : widePullbackShapeUnopwidePullbackShapeUnop J ⋙ widePushoutShapeOp JwidePullbackShapeUnop J ⋙ widePushoutShapeOp J ≅ 𝟭 _ :=
  NatIso.ofComponents fun _ => Iso.refl _

Isomorphism between composition of wide pullback/pushout shape functors and identity

Informal description

The natural isomorphism witnessing that the composition of the functor `widePullbackShapeUnop J` (from the opposite of the wide pullback shape to the wide pushout shape) with the functor `widePushoutShapeOp J` (from the wide pushout shape to the opposite of the wide pullback shape) is isomorphic to the identity functor on `(WidePullbackShape J)ᵒᵖ`.

CategoryTheory.Limits.widePullbackShapeUnopOp definition

: widePullbackShapeOp J ⋙ widePushoutShapeUnop J ≅ 𝟭 _

Full source

/-- The counit isomorphism of the equivalence
`widePushoutShapeOpEquiv : (WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J` -/
def widePullbackShapeUnopOp : widePullbackShapeOpwidePullbackShapeOp J ⋙ widePushoutShapeUnop JwidePullbackShapeOp J ⋙ widePushoutShapeUnop J ≅ 𝟭 _ :=
  NatIso.ofComponents fun _ => Iso.refl _

Natural isomorphism between composed functors and identity functor on wide pullback shape

Informal description

The natural isomorphism between the composition of the functors `widePullbackShapeOp` and `widePushoutShapeUnop` and the identity functor on `WidePullbackShape J`. For each object, the isomorphism is given by the identity isomorphism.

CategoryTheory.Limits.widePushoutShapeOpEquiv definition

: (WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J

Full source

/-- The duality equivalence `(WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J` -/
@[simps]
def widePushoutShapeOpEquiv : (WidePushoutShape J)ᵒᵖ(WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J where
  functor := widePushoutShapeUnop J
  inverse := widePullbackShapeOp J
  unitIso := (widePushoutShapeOpUnop J).symm
  counitIso := widePullbackShapeUnopOp J

Duality equivalence between opposite wide pushout shape and wide pullback shape

Informal description

The duality equivalence between the opposite category of the wide pushout shape over a type $J$ and the wide pullback shape over $J$. This equivalence consists of: - A functor from $(WidePushoutShape J)^{\mathrm{op}}$ to $WidePullbackShape J$, - An inverse functor from $WidePullbackShape J$ to $(WidePushoutShape J)^{\mathrm{op}}$, - Natural isomorphisms witnessing that these functors form an equivalence of categories.

CategoryTheory.Limits.widePullbackShapeOpEquiv definition

: (WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J

Full source

/-- The duality equivalence `(WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J` -/
@[simps]
def widePullbackShapeOpEquiv : (WidePullbackShape J)ᵒᵖ(WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J where
  functor := widePullbackShapeUnop J
  inverse := widePushoutShapeOp J
  unitIso := (widePullbackShapeOpUnop J).symm
  counitIso := widePushoutShapeUnopOp J

Duality equivalence between wide pullback and pushout shapes

Informal description

The duality equivalence between the opposite of the wide pullback shape category $(WidePullbackShape\,J)^{\mathrm{op}}$ and the wide pushout shape category $WidePushoutShape\,J$. This equivalence consists of: - A functor from $(WidePullbackShape\,J)^{\mathrm{op}}$ to $WidePushoutShape\,J$ (given by `widePullbackShapeUnop`), - An inverse functor from $WidePushoutShape\,J$ to $(WidePullbackShape\,J)^{\mathrm{op}}$ (given by `widePushoutShapeOp`), - Natural isomorphisms witnessing that these functors form an equivalence of categories.

CategoryTheory.Limits.hasWidePushouts_shrink theorem

[HasWidePushouts.{max w w'} C] : HasWidePushouts.{w} C

Full source

/-- If a category has wide pushouts on a higher universe level it also has wide pushouts
on a lower universe level. -/
theorem hasWidePushouts_shrink [HasWidePushouts.{max w w'} C] : HasWidePushouts.{w} C := fun _ =>
  hasColimitsOfShape_of_equivalence (WidePushoutShape.equivalenceOfEquiv _ Equiv.ulift.{w'})

Universe Level Reduction for Wide Pushouts

Informal description

If a category $\mathcal{C}$ has wide pushouts for diagrams indexed by types in a higher universe level, then it also has wide pushouts for diagrams indexed by types in a lower universe level.

CategoryTheory.Limits.hasWidePullbacks_shrink theorem

[HasWidePullbacks.{max w w'} C] : HasWidePullbacks.{w} C

Full source

/-- If a category has wide pullbacks on a higher universe level it also has wide pullbacks
on a lower universe level. -/
theorem hasWidePullbacks_shrink [HasWidePullbacks.{max w w'} C] : HasWidePullbacks.{w} C := fun _ =>
  hasLimitsOfShape_of_equivalence (WidePullbackShape.equivalenceOfEquiv _ Equiv.ulift.{w'})

Universe Level Reduction for Wide Pullbacks

Informal description

If a category $\mathcal{C}$ has wide pullbacks for index types in a higher universe level (specifically, for types in `Type (max w w')`), then it also has wide pullbacks for index types in a lower universe level (`Type w`).