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

Equations

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

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

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

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

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

Equations

• CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom.decEq (CategoryTheory.Limits.WidePullbackShape.Hom.id a✝) (CategoryTheory.Limits.WidePullbackShape.Hom.id a✝) = isTrue ⋯
• CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom.decEq (CategoryTheory.Limits.WidePullbackShape.Hom.term a_2) (CategoryTheory.Limits.WidePullbackShape.Hom.term a_2) = isTrue ⋯

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

Equations

• CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom = CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom.decEq

instance CategoryTheory.Limits.WidePullbackShape.struct {J : Type w} : CategoryStruct.{w, w} (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 (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 (WidePullbackShape J)

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

Equations

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

@[simp]

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

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

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

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} [Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → objs j ⟶ B) (j : WidePullbackShape J) : (wideCospan B objs arrows).obj j = Option.casesOn j B objs

@[simp]

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

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

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

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} [Category.{v, u} C] {F : Functor (WidePullbackShape J) C} {X : C} (f : X ⟶ F.obj none) (π : (j : J) → X ⟶ F.obj (some j)) (w : ∀ (j : J), CategoryStruct.comp (π j) (F.map (Hom.term j)) = f) : Cone F

Construct a cone over a wide cospan.

Equations

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

@[simp]

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

@[simp]

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

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

Wide pullback diagrams of equivalent index types are equivalent.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Lifting universe and morphism levels preserves wide pullback diagrams.

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

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

Equations

• CategoryTheory.Limits.WidePushoutShape.instDecidableEqHom.decEq (CategoryTheory.Limits.WidePushoutShape.Hom.id a✝) (CategoryTheory.Limits.WidePushoutShape.Hom.id a✝) = isTrue ⋯
• CategoryTheory.Limits.WidePushoutShape.instDecidableEqHom.decEq (CategoryTheory.Limits.WidePushoutShape.Hom.init a_2) (CategoryTheory.Limits.WidePushoutShape.Hom.init a_2) = isTrue ⋯

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

Equations

• CategoryTheory.Limits.WidePushoutShape.instDecidableEqHom = CategoryTheory.Limits.WidePushoutShape.instDecidableEqHom.decEq

instance CategoryTheory.Limits.WidePushoutShape.struct {J : Type w} : CategoryStruct.{w, w} (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 (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 (WidePushoutShape J)

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

Equations

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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} [Category.{v, u} C] {F : Functor (WidePushoutShape J) C} {X : C} (f : F.obj none ⟶ X) (ι : (j : J) → F.obj (some j) ⟶ X) (w : ∀ (j : J), CategoryStruct.comp (F.map (Hom.init j)) (ι j) = f) : Cocone F

Construct a cocone over a wide span.

Equations

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

@[simp]

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

@[simp]

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

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

Wide pushout diagrams of equivalent index types are equivalent.

Equations

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

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

Lifting universe and morphism levels preserves wide pushout diagrams.

Equations

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

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} [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} [Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → objs j ⟶ B) [HasWidePullback B objs arrows] : C

A choice of wide pullback.

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} [Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → B ⟶ objs j) [HasWidePushout B objs arrows] : C

A choice of wide pushout.

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} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [HasWidePullback B objs arrows] (j : J) : widePullback B objs arrows ⟶ objs j

The j-th projection from the pullback.

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} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [HasWidePullback B objs arrows] : widePullback B objs arrows ⟶ B

The unique map to the base from the pullback.

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} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [HasWidePullback B objs arrows] (j : J) : CategoryStruct.comp (π arrows j) (arrows j) = base arrows

@[simp]

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

@[reducible, inline]

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

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

Equations

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

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

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

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

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

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

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

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

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

@[reducible, inline]

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

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

Equations

• CategoryTheory.Limits.WidePullbackCone f = CategoryTheory.Limits.Cone (CategoryTheory.Limits.WidePullbackShape.wideCospan X Y f)

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

The projection on the components of a wide pullback cone.

Equations

• s.π i = s.π.app (some i)

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

The projection to the base of a wide pullback cone.

Equations

• s.base = s.π.app none

@[simp]

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

@[simp]

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

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

Construct a wide pullback cone from the projections.

Equations

• CategoryTheory.Limits.WidePullbackCone.mk b π h = CategoryTheory.Limits.WidePullbackShape.mkCone b π h

@[simp]

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

@[simp]

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

@[simp]

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

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

Constructor to show a wide pullback cone is limiting.

Equations

• CategoryTheory.Limits.WidePullbackCone.IsLimit.mk s lift facbase facπ uniq = { lift := lift, fac := ⋯, uniq := ⋯ }

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

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

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

Equations

• CategoryTheory.Limits.WidePullbackCone.IsLimit.lift hs b a w = hs.lift (CategoryTheory.Limits.WidePullbackCone.mk b a w)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.WidePullbackCone.ext e base π = CategoryTheory.Limits.Cones.ext e ⋯

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

Reindex a wide pullback cone.

Equations

• s.reindex e = CategoryTheory.Limits.WidePullbackCone.mk s.base (fun (i : ι') => s.π (e i)) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

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

Reindexing a pullback cone preserves being limiting.

Equations

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

@[reducible, inline]

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

The j-th inclusion to the pushout.

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} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → B ⟶ objs j) [HasWidePushout B objs arrows] : B ⟶ widePushout B objs arrows

The unique map from the head to the pushout.

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} [Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → B ⟶ objs j) [HasWidePushout B objs arrows] (j : J) : CategoryStruct.comp (arrows j) (ι arrows j) = head arrows

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

@[reducible, inline]

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

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

Equations

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

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

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

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

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

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

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

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

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

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

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

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) : Functor (WidePullbackShape J) (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_map (J : Type w) {X₁ X₂ : WidePullbackShape J} (a✝ : X₁ ⟶ X₂) : (widePullbackShapeOp J).map a✝ = widePullbackShapeOpMap J X₁ X₂ a✝

@[simp]

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

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

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

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.widePushoutShapeUnop (J : Type w) : Functor (WidePushoutShape J)ᵒᵖ (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✝ : (WidePushoutShape J)ᵒᵖ} (f : X✝ ⟶ Y✝) : (widePushoutShapeUnop J).map f = (widePushoutShapeOpMap J (Opposite.unop Y✝) (Opposite.unop X✝) f.unop).unop

@[simp]

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

def CategoryTheory.Limits.widePushoutShapeOpEquiv (J : Type w) : (WidePushoutShape J)ᵒᵖ ≌ 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_unitIso (J : Type w) : (widePushoutShapeOpEquiv J).unitIso = (widePushoutShapeOpUnop J).symm

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.widePullbackShapeOpEquiv (J : Type w) : (WidePullbackShape J)ᵒᵖ ≌ 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) : (widePullbackShapeOpEquiv J).unitIso = (widePullbackShapeOpUnop J).symm

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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