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} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.IsIso f] :

CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.IsIso f] :

(CategoryTheory.Limits.pullbackConeOfLeftIso f g).pt = Y

source

@[simp]

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

(CategoryTheory.Limits.pullbackConeOfLeftIso f g).fst = CategoryTheory.CategoryStruct.comp g (CategoryTheory.inv f)

source

@[simp]

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

(CategoryTheory.Limits.pullbackConeOfLeftIso f g).snd = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullbackConeOfLeftIso f g).pt

source

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

(CategoryTheory.Limits.pullbackConeOfLeftIso f g).π.app none = g

source

@[simp]

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

(CategoryTheory.Limits.pullbackConeOfLeftIso f g).π.app CategoryTheory.Limits.WalkingCospan.left = CategoryTheory.CategoryStruct.comp g (CategoryTheory.inv f)

source

@[simp]

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

(CategoryTheory.Limits.pullbackConeOfLeftIso f g).π.app CategoryTheory.Limits.WalkingCospan.right = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingCospan).obj (CategoryTheory.Limits.pullbackConeOfLeftIso f g).pt).obj CategoryTheory.Limits.WalkingCospan.right)

source

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

CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.IsIso f] :

CategoryTheory.Limits.HasPullback f g

source

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

CategoryTheory.IsIso (CategoryTheory.Limits.pullback.snd f g)

source

@[simp]

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

CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.pullback.snd f g)) (CategoryTheory.Limits.pullback.fst f g) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.inv f)

source

@[simp]

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

CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.pullback.snd f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) h)

source

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

CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.IsIso g] :

(CategoryTheory.Limits.pullbackConeOfRightIso f g).pt = X

source

@[simp]

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

(CategoryTheory.Limits.pullbackConeOfRightIso f g).fst = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullbackConeOfRightIso f g).pt

source

@[simp]

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

(CategoryTheory.Limits.pullbackConeOfRightIso f g).snd = CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv g)

source

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

(CategoryTheory.Limits.pullbackConeOfRightIso f g).π.app none = f

source

@[simp]

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

(CategoryTheory.Limits.pullbackConeOfRightIso f g).π.app CategoryTheory.Limits.WalkingCospan.left = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingCospan).obj (CategoryTheory.Limits.pullbackConeOfRightIso f g).pt).obj CategoryTheory.Limits.WalkingCospan.left)

source

@[simp]

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

(CategoryTheory.Limits.pullbackConeOfRightIso f g).π.app CategoryTheory.Limits.WalkingCospan.right = CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv g)

source

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

CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.IsIso g] :

CategoryTheory.Limits.HasPullback f g

source

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

CategoryTheory.IsIso (CategoryTheory.Limits.pullback.fst f g)

source

@[simp]

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

CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.Limits.pullback.snd f g) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv g)

source

@[simp]

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

CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) h)

source

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

CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.IsIso f] :

(CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).pt = Z

source

@[simp]

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

(CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).inl = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) g

source

@[simp]

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

(CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).inr = CategoryTheory.CategoryStruct.id Z

source

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

(CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).ι.app none = g

source

@[simp]

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

(CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).ι.app CategoryTheory.Limits.WalkingSpan.left = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) g

source

@[simp]

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

(CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).ι.app CategoryTheory.Limits.WalkingSpan.right = CategoryTheory.CategoryStruct.id ((CategoryTheory.Limits.span f g).obj CategoryTheory.Limits.WalkingSpan.right)

source

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

CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.IsIso f] :

CategoryTheory.Limits.HasPushout f g

source

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

CategoryTheory.IsIso (CategoryTheory.Limits.pushout.inr f g)

source

@[simp]

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

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) (CategoryTheory.inv (CategoryTheory.Limits.pushout.inr f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) g

source

@[simp]

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

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.pushout.inr f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) (CategoryTheory.CategoryStruct.comp g h)

source

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

CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.IsIso g] :

(CategoryTheory.Limits.pushoutCoconeOfRightIso f g).pt = Y

source

@[simp]

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

(CategoryTheory.Limits.pushoutCoconeOfRightIso f g).inl = CategoryTheory.CategoryStruct.id Y

source

@[simp]

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

(CategoryTheory.Limits.pushoutCoconeOfRightIso f g).inr = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) f

source

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

(CategoryTheory.Limits.pushoutCoconeOfRightIso f g).ι.app none = f

source

@[simp]

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

(CategoryTheory.Limits.pushoutCoconeOfRightIso f g).ι.app CategoryTheory.Limits.WalkingSpan.left = CategoryTheory.CategoryStruct.id ((CategoryTheory.Limits.span f g).obj CategoryTheory.Limits.WalkingSpan.left)

source

@[simp]

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

(CategoryTheory.Limits.pushoutCoconeOfRightIso f g).ι.app CategoryTheory.Limits.WalkingSpan.right = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) f

source

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

CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.IsIso g] :

CategoryTheory.Limits.HasPushout f g

source

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

CategoryTheory.IsIso (CategoryTheory.Limits.pushout.inl f g)

source

@[simp]

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

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) (CategoryTheory.inv (CategoryTheory.Limits.pushout.inl f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) f

source

@[simp]

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

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.pushout.inl f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) (CategoryTheory.CategoryStruct.comp f h)

Documentation

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

The pullback of an isomorphism #