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.
Equations
- CategoryTheory.Limits.instInhabitedWidePullbackShape J = { default := none }
Equations
- CategoryTheory.Limits.instInhabitedWidePushoutShape J = { default := none }
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
Instances For
Equations
- CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom = CategoryTheory.Limits.WidePullbackShape.decEqHom✝
Equations
- One or more equations did not get rendered due to their size.
Equations
- CategoryTheory.Limits.WidePullbackShape.Hom.inhabited = { default := CategoryTheory.Limits.WidePullbackShape.Hom.id none }
An aesop tactic for bulk cases on morphisms in WidePushoutShape
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- CategoryTheory.Limits.WidePullbackShape.category = CategoryTheory.thin_category
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.
Instances For
Every diagram is naturally isomorphic (actually, equal) to a wideCospan
Equations
Instances For
Construct a cone over a wide cospan.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Wide pullback diagrams of equivalent index types are equivalent.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Lifting universe and morphism levels preserves wide pullback diagrams.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
Instances For
Equations
- CategoryTheory.Limits.WidePushoutShape.instDecidableEqHom = CategoryTheory.Limits.WidePushoutShape.decEqHom✝
Equations
- One or more equations did not get rendered due to their size.
Equations
- CategoryTheory.Limits.WidePushoutShape.Hom.inhabited = { default := CategoryTheory.Limits.WidePushoutShape.Hom.id none }
An aesop tactic for bulk cases on morphisms in WidePushoutShape
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- CategoryTheory.Limits.WidePushoutShape.category = CategoryTheory.thin_category
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.
Instances For
Every diagram is naturally isomorphic (actually, equal) to a wideSpan
Equations
Instances For
Construct a cocone over a wide span.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Wide pushout diagrams of equivalent index types are equivalent.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Lifting universe and morphism levels preserves wide pushout diagrams.
Equations
- One or more equations did not get rendered due to their size.
Instances For
HasWidePullbacks
represents a choice of wide pullback for every collection of morphisms
Equations
Instances For
HasWidePushouts
represents a choice of wide pushout for every collection of morphisms
Equations
Instances For
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)
Instances For
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)
Instances For
A choice of wide pullback.
Equations
- CategoryTheory.Limits.widePullback B objs arrows = CategoryTheory.Limits.limit (CategoryTheory.Limits.WidePullbackShape.wideCospan B objs arrows)
Instances For
A choice of wide pushout.
Equations
- CategoryTheory.Limits.widePushout B objs arrows = CategoryTheory.Limits.colimit (CategoryTheory.Limits.WidePushoutShape.wideSpan B objs arrows)
Instances For
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)
Instances For
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
Instances For
Lift a collection of morphisms to a morphism to the pullback.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
Instances For
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
Instances For
Descend a collection of morphisms to a morphism from the pushout.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
Instances For
The obvious functor WidePullbackShape J ⥤ (WidePushoutShape J)ᵒᵖ
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
Instances For
The obvious functor WidePushoutShape J ⥤ (WidePullbackShape J)ᵒᵖ
Equations
- One or more equations did not get rendered due to their size.
Instances For
The obvious functor (WidePullbackShape J)ᵒᵖ ⥤ WidePushoutShape J
Equations
Instances For
The obvious functor (WidePushoutShape J)ᵒᵖ ⥤ WidePullbackShape J
Equations
Instances For
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.
Instances For
The counit isomorphism of the equivalence
widePullbackShapeOpEquiv : (WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
The counit isomorphism of the equivalence
widePushoutShapeOpEquiv : (WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J
Equations
- One or more equations did not get rendered due to their size.
Instances For
The duality equivalence (WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J
Equations
- One or more equations did not get rendered due to their size.
Instances For
The duality equivalence (WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J
Equations
- One or more equations did not get rendered due to their size.
Instances For
If a category has wide pushouts on a higher universe level it also has wide pushouts on a lower universe level.
If a category has wide pullbacks on a higher universe level it also has wide pullbacks on a lower universe level.