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.

Equations

• CategoryTheory.Limits.WidePullbackShape J = Option J

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

Equations

• CategoryTheory.Limits.instInhabitedWidePullbackShape J = { default := none }

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

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

Equations

• CategoryTheory.Limits.WidePushoutShape J = Option J

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

Equations

• CategoryTheory.Limits.instInhabitedWidePushoutShape J = { default := none }

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

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

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

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

Equations

• CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom = CategoryTheory.Limits.WidePullbackShape.decEqHom✝

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.Limits.WidePullbackShape.Hom.inhabited = { default := CategoryTheory.Limits.WidePullbackShape.Hom.id none }

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

An aesop tactic for bulk cases on morphisms in WidePushoutShape

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.Limits.WidePullbackShape.category = CategoryTheory.thin_category

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

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.

Equations

• One or more equations did not get rendered due to their size.

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

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

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 : J) => F.obj (some j)) fun (j : J) => F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term j)

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

Equations

• CategoryTheory.Limits.WidePullbackShape.diagramIsoWideCospan F = CategoryTheory.NatIso.ofComponents (fun (j : CategoryTheory.Limits.WidePullbackShape J) => CategoryTheory.eqToIso ⋯) ⋯

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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

Equations

• CategoryTheory.Limits.WidePushoutShape.instDecidableEqHom = CategoryTheory.Limits.WidePushoutShape.decEqHom✝

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.Limits.WidePushoutShape.Hom.inhabited = { default := CategoryTheory.Limits.WidePushoutShape.Hom.id none }

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

An aesop tactic for bulk cases on morphisms in WidePushoutShape

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.Limits.WidePushoutShape.category = CategoryTheory.thin_category

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

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.

Equations

• One or more equations did not get rendered due to their size.

@[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 (motive := fun (a a_1 : CategoryTheory.Limits.WidePushoutShape J) (t : a.Hom a_1) => X✝ = a → Y✝ = a_1 → HEq f t → ((fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) X✝ ⟶ (fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) Y✝)) f (fun (X : CategoryTheory.Limits.WidePushoutShape J) (h : X✝ = X) => Eq.ndrec (motive := fun (X : CategoryTheory.Limits.WidePushoutShape J) => Y✝ = X → HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.id X) → ((fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) X✝ ⟶ (fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) Y✝)) (fun (h : Y✝ = X✝) => Eq.ndrec (motive := fun {Y : CategoryTheory.Limits.WidePushoutShape J} => (f : X✝ ⟶ Y) → HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.id X✝) → ((fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) X✝ ⟶ (fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) Y)) (fun (f : X✝ ⟶ X✝) (h : HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.id X✝)) => CategoryTheory.CategoryStruct.id ((fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) X✝)) ⋯ f) h) (fun (j : J) (h : X✝ = none) => Eq.ndrec (motive := fun {X : CategoryTheory.Limits.WidePushoutShape J} => (f : X ⟶ Y✝) → Y✝ = some j → HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.init j) → ((fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) X ⟶ (fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) Y✝)) (fun (f : none ⟶ Y✝) (h : Y✝ = some j) => Eq.ndrec (motive := fun {Y : CategoryTheory.Limits.WidePushoutShape J} => (f : none ⟶ Y) → HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.init j) → ((fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) none ⟶ (fun (j : CategoryTheory.Limits.WidePushoutShape J) => Option.casesOn j B objs) Y)) (fun (f : none ⟶ some j) (h : HEq f (CategoryTheory.Limits.WidePushoutShape.Hom.init j)) => arrows j) ⋯ 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.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 : J) => F.obj (some j)) fun (j : J) => F.map (CategoryTheory.Limits.WidePushoutShape.Hom.init j)

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

Equations

• CategoryTheory.Limits.WidePushoutShape.diagramIsoWideSpan F = CategoryTheory.NatIso.ofComponents (fun (j : CategoryTheory.Limits.WidePushoutShape J) => CategoryTheory.eqToIso ⋯) ⋯

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

Equations

• CategoryTheory.Limits.HasWidePullbacks C = ∀ (J : Type ?u.18), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) C

@[reducible, inline]

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

Equations

• CategoryTheory.Limits.HasWidePushouts C = ∀ (J : Type ?u.18), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Limits.WidePushoutShape J) C

@[reducible, inline]

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.

Equations

• CategoryTheory.Limits.HasWidePullback B objs arrows = CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.WidePullbackShape.wideCospan B objs arrows)

@[reducible, inline]

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.

Equations

• CategoryTheory.Limits.HasWidePushout B objs arrows = CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.WidePushoutShape.wideSpan B objs arrows)

@[reducible, inline]

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.

Equations

• CategoryTheory.Limits.widePullback B objs arrows = CategoryTheory.Limits.limit (CategoryTheory.Limits.WidePullbackShape.wideCospan B objs arrows)

@[reducible, inline]

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.

Equations

• CategoryTheory.Limits.widePushout B objs arrows = CategoryTheory.Limits.colimit (CategoryTheory.Limits.WidePushoutShape.wideSpan B objs arrows)

@[reducible, inline]

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] (j : J) : CategoryTheory.Limits.widePullback B objs arrows ⟶ objs j

The j-th projection from the pullback.

Equations

• CategoryTheory.Limits.WidePullback.π arrows j = CategoryTheory.Limits.limit.π (CategoryTheory.Limits.WidePullbackShape.wideCospan B objs arrows) (some j)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.WidePullback.base {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] : CategoryTheory.Limits.widePullback B objs arrows ⟶ B

The unique map to the base from the pullback.

Equations

• CategoryTheory.Limits.WidePullback.base arrows = CategoryTheory.Limits.limit.π (CategoryTheory.Limits.WidePullbackShape.wideCospan B objs arrows) none

@[simp]

theorem CategoryTheory.Limits.WidePullback.π_arrow {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] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π arrows j) (arrows j) = CategoryTheory.Limits.WidePullback.base arrows

@[simp]

theorem CategoryTheory.Limits.WidePullback.π_arrow_assoc {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] (j : J) {Z : C} (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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.WidePullback.lift {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] {X : C} (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 objs arrows

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

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.WidePullback.lift_π {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] {X : C} (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_π_assoc {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] {X : C} (f : X ⟶ B) (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) (j : J) {Z : C} (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_base {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] {X : C} (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.lift_base_assoc {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] {X : C} (f : X ⟶ B) (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) {Z : C} (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.eq_lift_of_comp_eq {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] {X : C} (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 objs 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} {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] {X : C} (g : X ⟶ CategoryTheory.Limits.widePullback B objs arrows) : g = CategoryTheory.Limits.WidePullback.lift (CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.WidePullback.base arrows)) (fun (j : J) => CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.WidePullback.π arrows j)) ⋯

theorem CategoryTheory.Limits.WidePullback.hom_ext {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] {X : C} (g1 g2 : X ⟶ CategoryTheory.Limits.widePullback B objs 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

@[reducible, inline]

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] (j : J) : objs j ⟶ CategoryTheory.Limits.widePushout B objs arrows

The j-th inclusion to the pushout.

Equations

• CategoryTheory.Limits.WidePushout.ι arrows j = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.WidePushoutShape.wideSpan B objs arrows) (some j)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.WidePushout.head {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] : B ⟶ CategoryTheory.Limits.widePushout B objs arrows

The unique map from the head to the pushout.

Equations

• CategoryTheory.Limits.WidePushout.head arrows = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.WidePushoutShape.wideSpan B objs arrows) none

@[simp]

theorem CategoryTheory.Limits.WidePushout.arrow_ι {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] (j : J) : CategoryTheory.CategoryStruct.comp (arrows j) (CategoryTheory.Limits.WidePushout.ι arrows j) = CategoryTheory.Limits.WidePushout.head arrows

@[simp]

theorem CategoryTheory.Limits.WidePushout.arrow_ι_assoc {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] (j : J) {Z : C} (h : CategoryTheory.Limits.widePushout B objs 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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.WidePushout.desc {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] {X : C} (f : B ⟶ X) (fs : (j : J) → objs j ⟶ X) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (arrows j) (fs j) = f) : CategoryTheory.Limits.widePushout B objs arrows ⟶ X

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

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.WidePushout.ι_desc {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] {X : C} (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.ι_desc_assoc {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] {X : C} (f : B ⟶ X) (fs : (j : J) → objs j ⟶ X) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (arrows j) (fs j) = f) (j : J) {Z : C} (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.head_desc {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] {X : C} (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.head_desc_assoc {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] {X : C} (f : B ⟶ X) (fs : (j : J) → objs j ⟶ X) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (arrows j) (fs j) = f) {Z : C} (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.eq_desc_of_comp_eq {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] {X : C} (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 objs 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} {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] {X : C} (g : CategoryTheory.Limits.widePushout B objs arrows ⟶ X) : g = CategoryTheory.Limits.WidePushout.desc (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.head arrows) g) (fun (j : J) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.ι arrows j) g) ⋯

theorem CategoryTheory.Limits.WidePushout.hom_ext {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] {X : C} (g1 g2 : CategoryTheory.Limits.widePushout B objs 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 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)ᵒᵖ

Equations

• CategoryTheory.Limits.widePullbackShapeOpMap J x x (CategoryTheory.Limits.WidePullbackShape.Hom.id x) = Quiver.Hom.op (CategoryTheory.Limits.WidePushoutShape.Hom.id x)
• CategoryTheory.Limits.widePullbackShapeOpMap J (some j) none (CategoryTheory.Limits.WidePullbackShape.Hom.term j) = Quiver.Hom.op (CategoryTheory.Limits.WidePushoutShape.Hom.init j)

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

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

Equations

• One or more equations did not get rendered due to their size.

@[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₁ X₂ : CategoryTheory.Limits.WidePullbackShape J} (a✝ : X₁ ⟶ X₂) : (CategoryTheory.Limits.widePullbackShapeOp J).map a✝ = CategoryTheory.Limits.widePullbackShapeOpMap J X₁ X₂ a✝

def CategoryTheory.Limits.widePushoutShapeOpMap (J : Type w) (X 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)ᵒᵖ

Equations

• CategoryTheory.Limits.widePushoutShapeOpMap J x x (CategoryTheory.Limits.WidePushoutShape.Hom.id x) = Quiver.Hom.op (CategoryTheory.Limits.WidePullbackShape.Hom.id x)
• CategoryTheory.Limits.widePushoutShapeOpMap J none (some j) (CategoryTheory.Limits.WidePushoutShape.Hom.init j) = Quiver.Hom.op (CategoryTheory.Limits.WidePullbackShape.Hom.term j)

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.widePullbackShapeUnop J = (CategoryTheory.Limits.widePullbackShapeOp J).leftOp

@[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 (Opposite.unop Y✝) (Opposite.unop X✝) f.unop).unop

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.widePushoutShapeUnop J = (CategoryTheory.Limits.widePushoutShapeOp J).leftOp

@[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 (Opposite.unop Y✝) (Opposite.unop X✝) f.unop).unop

@[simp]

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

def CategoryTheory.Limits.widePushoutShapeOpUnop (J : Type w) : (CategoryTheory.Limits.widePushoutShapeUnop J).comp (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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.widePullbackShapeOpUnop (J : Type w) : (CategoryTheory.Limits.widePullbackShapeUnop J).comp (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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.widePullbackShapeOpEquiv_functor (J : Type w) : (CategoryTheory.Limits.widePullbackShapeOpEquiv J).functor = CategoryTheory.Limits.widePullbackShapeUnop 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.