The pullback of an isomorphism

This file provides some basic results about the pullback (and pushout) of an isomorphism.

noncomputable def CategoryTheory.Limits.pullbackConeOfLeftIso {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso f] : PullbackCone f g

If f : X ⟶ Z is iso, then X ×[Z] Y ≅ Y. This is the explicit limit cone.

@[simp]

theorem CategoryTheory.Limits.pullbackConeOfLeftIso_x {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso f] : (pullbackConeOfLeftIso f g).pt = Y

@[simp]

theorem CategoryTheory.Limits.pullbackConeOfLeftIso_fst {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso f] : (pullbackConeOfLeftIso f g).fst = CategoryStruct.comp g (inv f)

@[simp]

theorem CategoryTheory.Limits.pullbackConeOfLeftIso_snd {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso f] : (pullbackConeOfLeftIso f g).snd = CategoryStruct.id (pullbackConeOfLeftIso f g).pt

theorem CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_none {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso f] : (pullbackConeOfLeftIso f g).π.app none = g

@[simp]

theorem CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_left {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso f] : (pullbackConeOfLeftIso f g).π.app WalkingCospan.left = CategoryStruct.comp g (inv f)

@[simp]

theorem CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_right {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso f] : (pullbackConeOfLeftIso f g).π.app WalkingCospan.right = CategoryStruct.id (((Functor.const WalkingCospan).obj (pullbackConeOfLeftIso f g).pt).obj WalkingCospan.right)

noncomputable def CategoryTheory.Limits.pullbackConeOfLeftIsoIsLimit {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso f] : IsLimit (pullbackConeOfLeftIso f g)

Verify that the constructed limit cone is indeed a limit.

theorem CategoryTheory.Limits.hasPullback_of_left_iso {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso f] : HasPullback f g

instance CategoryTheory.Limits.pullback_snd_iso_of_left_iso {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso f] : IsIso (pullback.snd f g)

@[simp]

theorem CategoryTheory.Limits.pullback_inv_snd_fst_of_left_isIso {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso f] : CategoryStruct.comp (inv (pullback.snd f g)) (pullback.fst f g) = CategoryStruct.comp g (inv f)

@[simp]

theorem CategoryTheory.Limits.pullback_inv_snd_fst_of_left_isIso_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso f] {Z✝ : C} (h : X ⟶ Z✝) : CategoryStruct.comp (inv (pullback.snd f g)) (CategoryStruct.comp (pullback.fst f g) h) = CategoryStruct.comp g (CategoryStruct.comp (inv f) h)

noncomputable def CategoryTheory.Limits.pullbackConeOfRightIso {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso g] : PullbackCone f g

If g : Y ⟶ Z is iso, then X ×[Z] Y ≅ X. This is the explicit limit cone.

@[simp]

theorem CategoryTheory.Limits.pullbackConeOfRightIso_x {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso g] : (pullbackConeOfRightIso f g).pt = X

@[simp]

theorem CategoryTheory.Limits.pullbackConeOfRightIso_fst {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso g] : (pullbackConeOfRightIso f g).fst = CategoryStruct.id (pullbackConeOfRightIso f g).pt

@[simp]

theorem CategoryTheory.Limits.pullbackConeOfRightIso_snd {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso g] : (pullbackConeOfRightIso f g).snd = CategoryStruct.comp f (inv g)

theorem CategoryTheory.Limits.pullbackConeOfRightIso_π_app_none {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso g] : (pullbackConeOfRightIso f g).π.app none = f

@[simp]

theorem CategoryTheory.Limits.pullbackConeOfRightIso_π_app_left {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso g] : (pullbackConeOfRightIso f g).π.app WalkingCospan.left = CategoryStruct.id (((Functor.const WalkingCospan).obj (pullbackConeOfRightIso f g).pt).obj WalkingCospan.left)

@[simp]

theorem CategoryTheory.Limits.pullbackConeOfRightIso_π_app_right {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso g] : (pullbackConeOfRightIso f g).π.app WalkingCospan.right = CategoryStruct.comp f (inv g)

noncomputable def CategoryTheory.Limits.pullbackConeOfRightIsoIsLimit {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso g] : IsLimit (pullbackConeOfRightIso f g)

Verify that the constructed limit cone is indeed a limit.

theorem CategoryTheory.Limits.hasPullback_of_right_iso {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso g] : HasPullback f g

instance CategoryTheory.Limits.pullback_fst_iso_of_right_iso {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso g] : IsIso (pullback.fst f g)

@[simp]

theorem CategoryTheory.Limits.pullback_inv_fst_snd_of_right_isIso {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso g] : CategoryStruct.comp (inv (pullback.fst f g)) (pullback.snd f g) = CategoryStruct.comp f (inv g)

@[simp]

theorem CategoryTheory.Limits.pullback_inv_fst_snd_of_right_isIso_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso g] {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (inv (pullback.fst f g)) (CategoryStruct.comp (pullback.snd f g) h) = CategoryStruct.comp f (CategoryStruct.comp (inv g) h)

noncomputable def CategoryTheory.Limits.pushoutCoconeOfLeftIso {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso f] : PushoutCocone f g

If f : X ⟶ Y is iso, then Y ⨿[X] Z ≅ Z. This is the explicit colimit cocone.

@[simp]

theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_x {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso f] : (pushoutCoconeOfLeftIso f g).pt = Z

@[simp]

theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_inl {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso f] : (pushoutCoconeOfLeftIso f g).inl = CategoryStruct.comp (inv f) g

@[simp]

theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_inr {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso f] : (pushoutCoconeOfLeftIso f g).inr = CategoryStruct.id Z

theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_none {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso f] : (pushoutCoconeOfLeftIso f g).ι.app none = g

@[simp]

theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_left {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso f] : (pushoutCoconeOfLeftIso f g).ι.app WalkingSpan.left = CategoryStruct.comp (inv f) g

@[simp]

theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_right {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso f] : (pushoutCoconeOfLeftIso f g).ι.app WalkingSpan.right = CategoryStruct.id ((span f g).obj WalkingSpan.right)

noncomputable def CategoryTheory.Limits.pushoutCoconeOfLeftIsoIsLimit {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso f] : IsColimit (pushoutCoconeOfLeftIso f g)

Verify that the constructed cocone is indeed a colimit.

theorem CategoryTheory.Limits.hasPushout_of_left_iso {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso f] : HasPushout f g

instance CategoryTheory.Limits.pushout_inr_iso_of_left_iso {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso f] : IsIso (pushout.inr f g)

@[simp]

theorem CategoryTheory.Limits.pushout_inl_inv_inr_of_right_isIso {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso f] : CategoryStruct.comp (pushout.inl f g) (inv (pushout.inr f g)) = CategoryStruct.comp (inv f) g

@[simp]

theorem CategoryTheory.Limits.pushout_inl_inv_inr_of_right_isIso_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso f] {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp (pushout.inl f g) (CategoryStruct.comp (inv (pushout.inr f g)) h) = CategoryStruct.comp (inv f) (CategoryStruct.comp g h)

noncomputable def CategoryTheory.Limits.pushoutCoconeOfRightIso {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso g] : PushoutCocone f g

If f : X ⟶ Z is iso, then Y ⨿[X] Z ≅ Y. This is the explicit colimit cocone.

@[simp]

theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_x {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso g] : (pushoutCoconeOfRightIso f g).pt = Y

@[simp]

theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_inl {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso g] : (pushoutCoconeOfRightIso f g).inl = CategoryStruct.id Y

@[simp]

theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_inr {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso g] : (pushoutCoconeOfRightIso f g).inr = CategoryStruct.comp (inv g) f

theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_none {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso g] : (pushoutCoconeOfRightIso f g).ι.app none = f

@[simp]

theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_left {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso g] : (pushoutCoconeOfRightIso f g).ι.app WalkingSpan.left = CategoryStruct.id ((span f g).obj WalkingSpan.left)

@[simp]

theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_right {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso g] : (pushoutCoconeOfRightIso f g).ι.app WalkingSpan.right = CategoryStruct.comp (inv g) f

noncomputable def CategoryTheory.Limits.pushoutCoconeOfRightIsoIsLimit {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso g] : IsColimit (pushoutCoconeOfRightIso f g)

Verify that the constructed cocone is indeed a colimit.

theorem CategoryTheory.Limits.hasPushout_of_right_iso {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso g] : HasPushout f g

instance CategoryTheory.Limits.pushout_inl_iso_of_right_iso {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso g] : IsIso (pushout.inl f g)

@[simp]

theorem CategoryTheory.Limits.pushout_inr_inv_inl_of_right_isIso {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso g] : CategoryStruct.comp (pushout.inr f g) (inv (pushout.inl f g)) = CategoryStruct.comp (inv g) f

@[simp]

theorem CategoryTheory.Limits.pushout_inr_inv_inl_of_right_isIso_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [IsIso g] {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (pushout.inr f g) (CategoryStruct.comp (inv (pushout.inl f g)) h) = CategoryStruct.comp (inv g) (CategoryStruct.comp f h)