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.
A wide pullback shape for any type J
can be written simply as Option J
.
Instances For
A wide pushout shape for any type J
can be written simply as Option J
.
Instances For
- id: {J : Type w} → (X : CategoryTheory.Limits.WidePullbackShape J) → CategoryTheory.Limits.WidePullbackShape.Hom X X
- term: {J : Type w} → (j : J) → CategoryTheory.Limits.WidePullbackShape.Hom (some j) none
The type of arrows for the shape indexing a wide pullback.
Instances For
An aesop tactic for bulk cases on morphisms in WidePushoutShape
Instances For
Construct a functor out of the wide pullback shape given a J-indexed collection of arrows to a fixed object.
Instances For
Every diagram is naturally isomorphic (actually, equal) to a wideCospan
Instances For
Construct a cone over a wide cospan.
Instances For
Wide pullback diagrams of equivalent index types are equivalent.
Instances For
Lifting universe and morphism levels preserves wide pullback diagrams.
Instances For
- id: {J : Type w} → (X : CategoryTheory.Limits.WidePushoutShape J) → CategoryTheory.Limits.WidePushoutShape.Hom X X
- init: {J : Type w} → (j : J) → CategoryTheory.Limits.WidePushoutShape.Hom none (some j)
The type of arrows for the shape indexing a wide pushout.
Instances For
An aesop tactic for bulk cases on morphisms in WidePushoutShape
Instances For
Construct a functor out of the wide pushout shape given a J-indexed collection of arrows from a fixed object.
Instances For
Every diagram is naturally isomorphic (actually, equal) to a wideSpan
Instances For
Construct a cocone over a wide span.
Instances For
Wide pushout diagrams of equivalent index types are equivalent.
Instances For
Lifting universe and morphism levels preserves wide pushout diagrams.
Instances For
HasWidePullbacks
represents a choice of wide pullback for every collection of morphisms
Instances For
HasWidePushouts
represents a choice of wide pushout for every collection of morphisms
Instances For
HasWidePullback B objs arrows
means that wideCospan B objs arrows
has a limit.
Instances For
HasWidePushout B objs arrows
means that wideSpan B objs arrows
has a colimit.
Instances For
A choice of wide pullback.
Instances For
A choice of wide pushout.
Instances For
The j
-th projection from the pullback.
Instances For
The unique map to the base from the pullback.
Instances For
Lift a collection of morphisms to a morphism to the pullback.
Instances For
The j
-th inclusion to the pushout.
Instances For
The unique map from the head to the pushout.
Instances For
Descend a collection of morphisms to a morphism from the pushout.
Instances For
The action on morphisms of the obvious functor
WidePullbackShape_op : WidePullbackShape J ⥤ (WidePushoutShape J)ᵒᵖ
Instances For
The obvious functor WidePullbackShape J ⥤ (WidePushoutShape J)ᵒᵖ
Instances For
The action on morphisms of the obvious functor
widePushoutShapeOp : WidePushoutShape J ⥤ (WidePullbackShape J)ᵒᵖ
Instances For
The obvious functor WidePushoutShape J ⥤ (WidePullbackShape J)ᵒᵖ
Instances For
The obvious functor (WidePullbackShape J)ᵒᵖ ⥤ WidePushoutShape J
Instances For
The obvious functor (WidePushoutShape J)ᵒᵖ ⥤ WidePullbackShape J
Instances For
The inverse of the unit isomorphism of the equivalence
widePushoutShapeOpEquiv : (WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J
Instances For
The counit isomorphism of the equivalence
widePullbackShapeOpEquiv : (WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J
Instances For
The inverse of the unit isomorphism of the equivalence
widePullbackShapeOpEquiv : (WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J
Instances For
The counit isomorphism of the equivalence
widePushoutShapeOpEquiv : (WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J
Instances For
The duality equivalence (WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J
Instances For
The duality equivalence (WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J
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.