Associativity of pullbacks #
This file shows that pullbacks (and pushouts) are associative up to natural isomorphism.
def
CategoryTheory.Limits.pullbackPullbackLeftIsPullback
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback (CategoryStruct.comp (pullback.snd fā fā) fā) fā]
:
IsLimit
(PullbackCone.mk (pullback.fst (CategoryStruct.comp (pullback.snd fā fā) fā) fā)
(pullback.lift
(CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd fā fā) fā) fā) (pullback.snd fā fā))
(pullback.snd (CategoryStruct.comp (pullback.snd fā fā) fā) fā) āÆ)
āÆ)
(Xā Ć[Yā] Xā) Ć[Yā] Xā is the pullback (Xā Ć[Yā] Xā) Ć[Xā] (Xā Ć[Yā] Xā).
Equations
Instances For
def
CategoryTheory.Limits.pullbackAssocIsPullback
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback (CategoryStruct.comp (pullback.snd fā fā) fā) fā]
:
IsLimit
(PullbackCone.mk
(CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd fā fā) fā) fā) (pullback.fst fā fā))
(pullback.lift
(CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd fā fā) fā) fā) (pullback.snd fā fā))
(pullback.snd (CategoryStruct.comp (pullback.snd fā fā) fā) fā) āÆ)
āÆ)
(Xā Ć[Yā] Xā) Ć[Yā] Xā is the pullback Xā Ć[Yā] (Xā Ć[Yā] Xā).
Equations
Instances For
theorem
CategoryTheory.Limits.hasPullback_assoc
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback (CategoryStruct.comp (pullback.snd fā fā) fā) fā]
:
HasPullback fā (CategoryStruct.comp (pullback.fst fā fā) fā)
def
CategoryTheory.Limits.pullbackPullbackRightIsPullback
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback fā (CategoryStruct.comp (pullback.fst fā fā) fā)]
:
IsLimit
(PullbackCone.mk
(pullback.lift (pullback.fst fā (CategoryStruct.comp (pullback.fst fā fā) fā))
(CategoryStruct.comp (pullback.snd fā (CategoryStruct.comp (pullback.fst fā fā) fā)) (pullback.fst fā fā)) āÆ)
(pullback.snd fā (CategoryStruct.comp (pullback.fst fā fā) fā)) āÆ)
Xā Ć[Yā] (Xā Ć[Yā] Xā) is the pullback (Xā Ć[Yā] Xā) Ć[Xā] (Xā Ć[Yā] Xā).
Equations
Instances For
def
CategoryTheory.Limits.pullbackAssocSymmIsPullback
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback fā (CategoryStruct.comp (pullback.fst fā fā) fā)]
:
IsLimit
(PullbackCone.mk
(pullback.lift (pullback.fst fā (CategoryStruct.comp (pullback.fst fā fā) fā))
(CategoryStruct.comp (pullback.snd fā (CategoryStruct.comp (pullback.fst fā fā) fā)) (pullback.fst fā fā)) āÆ)
(CategoryStruct.comp (pullback.snd fā (CategoryStruct.comp (pullback.fst fā fā) fā)) (pullback.snd fā fā)) āÆ)
Xā Ć[Yā] (Xā Ć[Yā] Xā) is the pullback (Xā Ć[Yā] Xā) Ć[Yā] Xā.
Equations
Instances For
theorem
CategoryTheory.Limits.hasPullback_assoc_symm
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback fā (CategoryStruct.comp (pullback.fst fā fā) fā)]
:
HasPullback (CategoryStruct.comp (pullback.snd fā fā) fā) fā
noncomputable def
CategoryTheory.Limits.pullbackAssoc
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback (CategoryStruct.comp (pullback.snd fā fā) fā) fā]
[HasPullback fā (CategoryStruct.comp (pullback.fst fā fā) fā)]
:
pullback (CategoryStruct.comp (pullback.snd fā fā) fā) fā ā
pullback fā (CategoryStruct.comp (pullback.fst fā fā) fā)
The canonical isomorphism (Xā Ć[Yā] Xā) Ć[Yā] Xā ā
Xā Ć[Yā] (Xā Ć[Yā] Xā).
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_inv_fst_fst
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback (CategoryStruct.comp (pullback.snd fā fā) fā) fā]
[HasPullback fā (CategoryStruct.comp (pullback.fst fā fā) fā)]
:
CategoryStruct.comp (pullbackAssoc fā fā fā fā).inv
(CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd fā fā) fā) fā) (pullback.fst fā fā)) = pullback.fst fā (CategoryStruct.comp (pullback.fst fā fā) fā)
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_inv_fst_fst_assoc
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback (CategoryStruct.comp (pullback.snd fā fā) fā) fā]
[HasPullback fā (CategoryStruct.comp (pullback.fst fā fā) fā)]
{Z : C}
(h : Xā ā¶ Z)
:
CategoryStruct.comp (pullbackAssoc fā fā fā fā).inv
(CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd fā fā) fā) fā)
(CategoryStruct.comp (pullback.fst fā fā) h)) = CategoryStruct.comp (pullback.fst fā (CategoryStruct.comp (pullback.fst fā fā) fā)) h
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_hom_fst
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback (CategoryStruct.comp (pullback.snd fā fā) fā) fā]
[HasPullback fā (CategoryStruct.comp (pullback.fst fā fā) fā)]
:
CategoryStruct.comp (pullbackAssoc fā fā fā fā).hom (pullback.fst fā (CategoryStruct.comp (pullback.fst fā fā) fā)) = CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd fā fā) fā) fā) (pullback.fst fā fā)
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_hom_fst_assoc
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback (CategoryStruct.comp (pullback.snd fā fā) fā) fā]
[HasPullback fā (CategoryStruct.comp (pullback.fst fā fā) fā)]
{Z : C}
(h : Xā ā¶ Z)
:
CategoryStruct.comp (pullbackAssoc fā fā fā fā).hom
(CategoryStruct.comp (pullback.fst fā (CategoryStruct.comp (pullback.fst fā fā) fā)) h) = CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd fā fā) fā) fā)
(CategoryStruct.comp (pullback.fst fā fā) h)
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_hom_snd_fst
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback (CategoryStruct.comp (pullback.snd fā fā) fā) fā]
[HasPullback fā (CategoryStruct.comp (pullback.fst fā fā) fā)]
:
CategoryStruct.comp (pullbackAssoc fā fā fā fā).hom
(CategoryStruct.comp (pullback.snd fā (CategoryStruct.comp (pullback.fst fā fā) fā)) (pullback.fst fā fā)) = CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd fā fā) fā) fā) (pullback.snd fā fā)
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_hom_snd_fst_assoc
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback (CategoryStruct.comp (pullback.snd fā fā) fā) fā]
[HasPullback fā (CategoryStruct.comp (pullback.fst fā fā) fā)]
{Z : C}
(h : Xā ā¶ Z)
:
CategoryStruct.comp (pullbackAssoc fā fā fā fā).hom
(CategoryStruct.comp (pullback.snd fā (CategoryStruct.comp (pullback.fst fā fā) fā))
(CategoryStruct.comp (pullback.fst fā fā) h)) = CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd fā fā) fā) fā)
(CategoryStruct.comp (pullback.snd fā fā) h)
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_hom_snd_snd
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback (CategoryStruct.comp (pullback.snd fā fā) fā) fā]
[HasPullback fā (CategoryStruct.comp (pullback.fst fā fā) fā)]
:
CategoryStruct.comp (pullbackAssoc fā fā fā fā).hom
(CategoryStruct.comp (pullback.snd fā (CategoryStruct.comp (pullback.fst fā fā) fā)) (pullback.snd fā fā)) = pullback.snd (CategoryStruct.comp (pullback.snd fā fā) fā) fā
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_hom_snd_snd_assoc
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback (CategoryStruct.comp (pullback.snd fā fā) fā) fā]
[HasPullback fā (CategoryStruct.comp (pullback.fst fā fā) fā)]
{Z : C}
(h : Xā ā¶ Z)
:
CategoryStruct.comp (pullbackAssoc fā fā fā fā).hom
(CategoryStruct.comp (pullback.snd fā (CategoryStruct.comp (pullback.fst fā fā) fā))
(CategoryStruct.comp (pullback.snd fā fā) h)) = CategoryStruct.comp (pullback.snd (CategoryStruct.comp (pullback.snd fā fā) fā) fā) h
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_inv_fst_snd
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback (CategoryStruct.comp (pullback.snd fā fā) fā) fā]
[HasPullback fā (CategoryStruct.comp (pullback.fst fā fā) fā)]
:
CategoryStruct.comp (pullbackAssoc fā fā fā fā).inv
(CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd fā fā) fā) fā) (pullback.snd fā fā)) = CategoryStruct.comp (pullback.snd fā (CategoryStruct.comp (pullback.fst fā fā) fā)) (pullback.fst fā fā)
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_inv_fst_snd_assoc
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback (CategoryStruct.comp (pullback.snd fā fā) fā) fā]
[HasPullback fā (CategoryStruct.comp (pullback.fst fā fā) fā)]
{Z : C}
(h : Xā ā¶ Z)
:
CategoryStruct.comp (pullbackAssoc fā fā fā fā).inv
(CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd fā fā) fā) fā)
(CategoryStruct.comp (pullback.snd fā fā) h)) = CategoryStruct.comp (pullback.snd fā (CategoryStruct.comp (pullback.fst fā fā) fā))
(CategoryStruct.comp (pullback.fst fā fā) h)
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_inv_snd
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback (CategoryStruct.comp (pullback.snd fā fā) fā) fā]
[HasPullback fā (CategoryStruct.comp (pullback.fst fā fā) fā)]
:
CategoryStruct.comp (pullbackAssoc fā fā fā fā).inv (pullback.snd (CategoryStruct.comp (pullback.snd fā fā) fā) fā) = CategoryStruct.comp (pullback.snd fā (CategoryStruct.comp (pullback.fst fā fā) fā)) (pullback.snd fā fā)
@[simp]
theorem
CategoryTheory.Limits.pullbackAssoc_inv_snd_assoc
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Yā Yā : C}
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
(fā : Xā ā¶ Yā)
[HasPullback fā fā]
[HasPullback fā fā]
[HasPullback (CategoryStruct.comp (pullback.snd fā fā) fā) fā]
[HasPullback fā (CategoryStruct.comp (pullback.fst fā fā) fā)]
{Z : C}
(h : Xā ā¶ Z)
:
CategoryStruct.comp (pullbackAssoc fā fā fā fā).inv
(CategoryStruct.comp (pullback.snd (CategoryStruct.comp (pullback.snd fā fā) fā) fā) h) = CategoryStruct.comp (pullback.snd fā (CategoryStruct.comp (pullback.fst fā fā) fā))
(CategoryStruct.comp (pullback.snd fā fā) h)
def
CategoryTheory.Limits.pushoutPushoutLeftIsPushout
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā]
:
IsColimit
(PushoutCocone.mk (pushout.inl (CategoryStruct.comp gā (pushout.inr gā gā)) gā)
(pushout.desc
(CategoryStruct.comp (pushout.inr gā gā) (pushout.inl (CategoryStruct.comp gā (pushout.inr gā gā)) gā))
(pushout.inr (CategoryStruct.comp gā (pushout.inr gā gā)) gā) āÆ)
āÆ)
(Xā āØæ[Zā] Xā) āØæ[Zā] Xā is the pushout (Xā āØæ[Zā] Xā) Ć[Xā] (Xā āØæ[Zā] Xā).
Equations
Instances For
def
CategoryTheory.Limits.pushoutAssocIsPushout
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā]
:
IsColimit
(PushoutCocone.mk
(CategoryStruct.comp (pushout.inl gā gā) (pushout.inl (CategoryStruct.comp gā (pushout.inr gā gā)) gā))
(pushout.desc
(CategoryStruct.comp (pushout.inr gā gā) (pushout.inl (CategoryStruct.comp gā (pushout.inr gā gā)) gā))
(pushout.inr (CategoryStruct.comp gā (pushout.inr gā gā)) gā) āÆ)
āÆ)
(Xā āØæ[Zā] Xā) āØæ[Zā] Xā is the pushout Xā āØæ[Zā] (Xā āØæ[Zā] Xā).
Equations
Instances For
theorem
CategoryTheory.Limits.hasPushout_assoc
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā]
:
HasPushout gā (CategoryStruct.comp gā (pushout.inl gā gā))
def
CategoryTheory.Limits.pushoutPushoutRightIsPushout
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout gā (CategoryStruct.comp gā (pushout.inl gā gā))]
:
IsColimit
(PushoutCocone.mk
(pushout.desc (pushout.inl gā (CategoryStruct.comp gā (pushout.inl gā gā)))
(CategoryStruct.comp (pushout.inl gā gā) (pushout.inr gā (CategoryStruct.comp gā (pushout.inl gā gā)))) āÆ)
(pushout.inr gā (CategoryStruct.comp gā (pushout.inl gā gā))) āÆ)
Xā āØæ[Zā] (Xā āØæ[Zā] Xā) is the pushout (Xā āØæ[Zā] Xā) Ć[Xā] (Xā āØæ[Zā] Xā).
Equations
Instances For
def
CategoryTheory.Limits.pushoutAssocSymmIsPushout
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout gā (CategoryStruct.comp gā (pushout.inl gā gā))]
:
IsColimit
(PushoutCocone.mk
(pushout.desc (pushout.inl gā (CategoryStruct.comp gā (pushout.inl gā gā)))
(CategoryStruct.comp (pushout.inl gā gā) (pushout.inr gā (CategoryStruct.comp gā (pushout.inl gā gā)))) āÆ)
(CategoryStruct.comp (pushout.inr gā gā) (pushout.inr gā (CategoryStruct.comp gā (pushout.inl gā gā)))) āÆ)
Xā āØæ[Zā] (Xā āØæ[Zā] Xā) is the pushout (Xā āØæ[Zā] Xā) āØæ[Zā] Xā.
Equations
Instances For
theorem
CategoryTheory.Limits.hasPushout_assoc_symm
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout gā (CategoryStruct.comp gā (pushout.inl gā gā))]
:
HasPushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā
noncomputable def
CategoryTheory.Limits.pushoutAssoc
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā]
[HasPushout gā (CategoryStruct.comp gā (pushout.inl gā gā))]
:
pushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā ā
pushout gā (CategoryStruct.comp gā (pushout.inl gā gā))
The canonical isomorphism (Xā āØæ[Zā] Xā) āØæ[Zā] Xā ā
Xā āØæ[Zā] (Xā āØæ[Zā] Xā).
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.inl_inl_pushoutAssoc_hom
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā]
[HasPushout gā (CategoryStruct.comp gā (pushout.inl gā gā))]
:
CategoryStruct.comp (pushout.inl gā gā)
(CategoryStruct.comp (pushout.inl (CategoryStruct.comp gā (pushout.inr gā gā)) gā) (pushoutAssoc gā gā gā gā).hom) = pushout.inl gā (CategoryStruct.comp gā (pushout.inl gā gā))
@[simp]
theorem
CategoryTheory.Limits.inl_inl_pushoutAssoc_hom_assoc
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā]
[HasPushout gā (CategoryStruct.comp gā (pushout.inl gā gā))]
{Z : C}
(h : pushout gā (CategoryStruct.comp gā (pushout.inl gā gā)) ā¶ Z)
:
CategoryStruct.comp (pushout.inl gā gā)
(CategoryStruct.comp (pushout.inl (CategoryStruct.comp gā (pushout.inr gā gā)) gā)
(CategoryStruct.comp (pushoutAssoc gā gā gā gā).hom h)) = CategoryStruct.comp (pushout.inl gā (CategoryStruct.comp gā (pushout.inl gā gā))) h
@[simp]
theorem
CategoryTheory.Limits.inr_inl_pushoutAssoc_hom
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā]
[HasPushout gā (CategoryStruct.comp gā (pushout.inl gā gā))]
:
CategoryStruct.comp (pushout.inr gā gā)
(CategoryStruct.comp (pushout.inl (CategoryStruct.comp gā (pushout.inr gā gā)) gā) (pushoutAssoc gā gā gā gā).hom) = CategoryStruct.comp (pushout.inl gā gā) (pushout.inr gā (CategoryStruct.comp gā (pushout.inl gā gā)))
@[simp]
theorem
CategoryTheory.Limits.inr_inl_pushoutAssoc_hom_assoc
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā]
[HasPushout gā (CategoryStruct.comp gā (pushout.inl gā gā))]
{Z : C}
(h : pushout gā (CategoryStruct.comp gā (pushout.inl gā gā)) ā¶ Z)
:
CategoryStruct.comp (pushout.inr gā gā)
(CategoryStruct.comp (pushout.inl (CategoryStruct.comp gā (pushout.inr gā gā)) gā)
(CategoryStruct.comp (pushoutAssoc gā gā gā gā).hom h)) = CategoryStruct.comp (pushout.inl gā gā)
(CategoryStruct.comp (pushout.inr gā (CategoryStruct.comp gā (pushout.inl gā gā))) h)
@[simp]
theorem
CategoryTheory.Limits.inr_inr_pushoutAssoc_inv
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā]
[HasPushout gā (CategoryStruct.comp gā (pushout.inl gā gā))]
:
CategoryStruct.comp (pushout.inr gā gā)
(CategoryStruct.comp (pushout.inr gā (CategoryStruct.comp gā (pushout.inl gā gā))) (pushoutAssoc gā gā gā gā).inv) = pushout.inr (CategoryStruct.comp gā (pushout.inr gā gā)) gā
@[simp]
theorem
CategoryTheory.Limits.inr_inr_pushoutAssoc_inv_assoc
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā]
[HasPushout gā (CategoryStruct.comp gā (pushout.inl gā gā))]
{Z : C}
(h : pushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā ā¶ Z)
:
CategoryStruct.comp (pushout.inr gā gā)
(CategoryStruct.comp (pushout.inr gā (CategoryStruct.comp gā (pushout.inl gā gā)))
(CategoryStruct.comp (pushoutAssoc gā gā gā gā).inv h)) = CategoryStruct.comp (pushout.inr (CategoryStruct.comp gā (pushout.inr gā gā)) gā) h
@[simp]
theorem
CategoryTheory.Limits.inl_pushoutAssoc_inv
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā]
[HasPushout gā (CategoryStruct.comp gā (pushout.inl gā gā))]
:
CategoryStruct.comp (pushout.inl gā (CategoryStruct.comp gā (pushout.inl gā gā))) (pushoutAssoc gā gā gā gā).inv = CategoryStruct.comp (pushout.inl gā gā) (pushout.inl (CategoryStruct.comp gā (pushout.inr gā gā)) gā)
@[simp]
theorem
CategoryTheory.Limits.inl_pushoutAssoc_inv_assoc
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā]
[HasPushout gā (CategoryStruct.comp gā (pushout.inl gā gā))]
{Z : C}
(h : pushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā ā¶ Z)
:
CategoryStruct.comp (pushout.inl gā (CategoryStruct.comp gā (pushout.inl gā gā)))
(CategoryStruct.comp (pushoutAssoc gā gā gā gā).inv h) = CategoryStruct.comp (pushout.inl gā gā)
(CategoryStruct.comp (pushout.inl (CategoryStruct.comp gā (pushout.inr gā gā)) gā) h)
@[simp]
theorem
CategoryTheory.Limits.inl_inr_pushoutAssoc_inv
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā]
[HasPushout gā (CategoryStruct.comp gā (pushout.inl gā gā))]
:
CategoryStruct.comp (pushout.inl gā gā)
(CategoryStruct.comp (pushout.inr gā (CategoryStruct.comp gā (pushout.inl gā gā))) (pushoutAssoc gā gā gā gā).inv) = CategoryStruct.comp (pushout.inr gā gā) (pushout.inl (CategoryStruct.comp gā (pushout.inr gā gā)) gā)
@[simp]
theorem
CategoryTheory.Limits.inl_inr_pushoutAssoc_inv_assoc
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā]
[HasPushout gā (CategoryStruct.comp gā (pushout.inl gā gā))]
{Z : C}
(h : pushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā ā¶ Z)
:
CategoryStruct.comp (pushout.inl gā gā)
(CategoryStruct.comp (pushout.inr gā (CategoryStruct.comp gā (pushout.inl gā gā)))
(CategoryStruct.comp (pushoutAssoc gā gā gā gā).inv h)) = CategoryStruct.comp (pushout.inr gā gā)
(CategoryStruct.comp (pushout.inl (CategoryStruct.comp gā (pushout.inr gā gā)) gā) h)
@[simp]
theorem
CategoryTheory.Limits.inr_pushoutAssoc_hom
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā]
[HasPushout gā (CategoryStruct.comp gā (pushout.inl gā gā))]
:
CategoryStruct.comp (pushout.inr (CategoryStruct.comp gā (pushout.inr gā gā)) gā) (pushoutAssoc gā gā gā gā).hom = CategoryStruct.comp (pushout.inr gā gā) (pushout.inr gā (CategoryStruct.comp gā (pushout.inl gā gā)))
@[simp]
theorem
CategoryTheory.Limits.inr_pushoutAssoc_hom_assoc
{C : Type u}
[Category.{v, u} C]
{Xā Xā Xā Zā Zā : C}
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
(gā : Zā ā¶ Xā)
[HasPushout gā gā]
[HasPushout gā gā]
[HasPushout (CategoryStruct.comp gā (pushout.inr gā gā)) gā]
[HasPushout gā (CategoryStruct.comp gā (pushout.inl gā gā))]
{Z : C}
(h : pushout gā (CategoryStruct.comp gā (pushout.inl gā gā)) ā¶ Z)
:
CategoryStruct.comp (pushout.inr (CategoryStruct.comp gā (pushout.inr gā gā)) gā)
(CategoryStruct.comp (pushoutAssoc gā gā gā gā).hom h) = CategoryStruct.comp (pushout.inr gā gā)
(CategoryStruct.comp (pushout.inr gā (CategoryStruct.comp gā (pushout.inl gā gā))) h)