Associativity of pullbacks #
This file shows that pullbacks (and pushouts) are associative up to natural isomorphism.
noncomputable 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ā).
Instances For
noncomputable 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ā).
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ā)
noncomputable 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ā).
Instances For
noncomputable 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ā.
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ā).
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)
noncomputable 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ā).
Instances For
noncomputable 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ā).
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ā))
noncomputable 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ā).
Instances For
noncomputable 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ā.
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ā).
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)