The pullback of an isomorphism #

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

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.

Equations

CategoryTheory.Limits.pullbackConeOfLeftIso f g = CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.CategoryStruct.comp g (CategoryTheory.inv f)) (CategoryTheory.CategoryStruct.id Y) ⋯

Instances For

source

@[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

source

@[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)

source

@[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

source

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

source

@[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)

source

@[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)

source

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.

Equations

CategoryTheory.Limits.pullbackConeOfLeftIsoIsLimit f g = (CategoryTheory.Limits.pullbackConeOfLeftIso f g).isLimitAux' fun (s : CategoryTheory.Limits.PullbackCone f g) => ⟨s.snd, ⋯⟩

Instances For

source

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

source

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)

source

@[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)

source

@[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)

source

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.

Equations

CategoryTheory.Limits.pullbackConeOfRightIso f g = CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv g)) ⋯

Instances For

source

@[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

source

@[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

source

@[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)

source

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

source

@[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)

source

@[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)

source

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.

Equations

CategoryTheory.Limits.pullbackConeOfRightIsoIsLimit f g = (CategoryTheory.Limits.pullbackConeOfRightIso f g).isLimitAux' fun (s : CategoryTheory.Limits.PullbackCone f g) => ⟨s.fst, ⋯⟩

Instances For

source

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

source

instance CategoryTheory.Limits.pullback_snd_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)

source

@[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)

source

@[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)

source

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.

Equations

CategoryTheory.Limits.pushoutCoconeOfLeftIso f g = CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) g) (CategoryTheory.CategoryStruct.id Z) ⋯

Instances For

source

@[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

source

@[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

source

@[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

source

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

source

@[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

source

@[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)

source

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.

Equations

CategoryTheory.Limits.pushoutCoconeOfLeftIsoIsLimit f g = (CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).isColimitAux' fun (s : CategoryTheory.Limits.PushoutCocone f g) => ⟨s.inr, ⋯⟩

Instances For

source

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

source

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)

source

@[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

source

@[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)

source

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.

Equations

CategoryTheory.Limits.pushoutCoconeOfRightIso f g = CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) f) ⋯

Instances For

source

@[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

source

@[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

source

@[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

source

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

source

@[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)

source

@[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

source

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.

Equations

CategoryTheory.Limits.pushoutCoconeOfRightIsoIsLimit f g = (CategoryTheory.Limits.pushoutCoconeOfRightIso f g).isColimitAux' fun (s : CategoryTheory.Limits.PushoutCocone f g) => ⟨s.inl, ⋯⟩

Instances For

source

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

source

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)

source

@[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

source

@[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)

Documentation

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

The pullback of an isomorphism #