Documentation

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

The pullback of an isomorphism #

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

source
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.

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
    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
    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
    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.

    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
      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.

      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
        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
        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
        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.

        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_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)
          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
          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.

          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
            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.

            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
              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.

              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
                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.

                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)