Documentation

Mathlib.CategoryTheory.WithTerminal.Cone

Relations between Cone, WithTerminal and Over #

Given categories C and J, an object X : C and a functor K : J ⥤ Over X, it has an obvious lift liftFromOver K : WithTerminal J ⥤ C, namely, send the terminal object to X. These two functors have equivalent categories of cones (coneEquiv). As a corollary, the limit of K is the limit of liftFromOver K, and viceversa.

source
def CategoryTheory.WithTerminal.commaFromOver {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} :
Functor (Functor J (Over X)) (Comma (Functor.id (Functor J C)) (Functor.const J))

The category of functors J ⥤ Over X can be seen as part of a comma category, namely the comma category constructed from the identity of the category of functors J ⥤ C and the functor that maps X : C to the constant functor J ⥤ C.

Given a functor K : J ⥤ Over X, it is mapped to a natural transformation from the obvious functor J ⥤ C to the constant functor X.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.WithTerminal.commaFromOver_obj_right {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} (K : Functor J (Over X)) :
    (commaFromOver.obj K).right = X
    source
    @[simp]
    theorem CategoryTheory.WithTerminal.commaFromOver_map_left {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {X✝ Y✝ : Functor J (Over X)} (f : X✝ ⟶ Y✝) :
    (commaFromOver.map f).left = whiskerRight f (Over.forget X)
    source
    @[simp]
    theorem CategoryTheory.WithTerminal.commaFromOver_obj_left {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} (K : Functor J (Over X)) :
    (commaFromOver.obj K).left = K.comp (Over.forget X)
    source
    @[simp]
    theorem CategoryTheory.WithTerminal.commaFromOver_map_right {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {X✝ Y✝ : Functor J (Over X)} (f : X✝ ⟶ Y✝) :
    (commaFromOver.map f).right = CategoryStruct.id X
    source
    @[simp]
    theorem CategoryTheory.WithTerminal.commaFromOver_obj_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} (K : Functor J (Over X)) (a : J) :
    (commaFromOver.obj K).hom.app a = (K.obj a).hom
    source
    def CategoryTheory.WithTerminal.liftFromOver {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} :
    Functor (Functor J (Over X)) (Functor (WithTerminal J) C)

    For any functor K : J ⥤ Over X, there is a canonical extension WithTerminal J ⥤ C, that sends star to X.

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.WithTerminal.liftFromOver_obj_obj {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} (X✝ : Functor J (Over X)) (X✝ : WithTerminal J) :
      (liftFromOver.obj X✝).obj X✝ = match X✝ with | of x => (X✝.obj x).left | star => X
      source
      @[simp]
      theorem CategoryTheory.WithTerminal.liftFromOver_map_app {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {X✝ Y✝ : Functor J (Over X)} (f : X✝ ⟶ Y✝) (x : WithTerminal J) :
      (liftFromOver.map f).app x = match x with | of x => (f.app x).left | star => CategoryStruct.id X
      source
      @[simp]
      theorem CategoryTheory.WithTerminal.liftFromOver_obj_map {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} (X✝ : Functor J (Over X)) {X✝ Y : WithTerminal J} (f : X✝ ⟶ Y) :
      (liftFromOver.obj X✝).map f = match X✝, Y, f with | of a, of a_1, f => (X✝.map (down f)).left | of x, star, x_1 => (X✝.obj x).hom | star, star, x => CategoryStruct.id X
      source
      def CategoryTheory.WithTerminal.liftFromOverComp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} {F : Functor C D} :
      liftFromOver.obj (K.comp (Over.post F)) ≅ (liftFromOver.obj K).comp F

      The extension of a functor to over categories behaves well with compositions.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.WithTerminal.liftFromOverComp_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} {F : Functor C D} (x✝ : WithTerminal J) :
        liftFromOverComp.inv.app x✝ = match x✝ with | star => CategoryStruct.id (((liftFromOver.obj K).comp F).obj star) | of a => CategoryStruct.id (((liftFromOver.obj K).comp F).obj (of a))
        source
        @[simp]
        theorem CategoryTheory.WithTerminal.liftFromOverComp_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} {F : Functor C D} (x✝ : WithTerminal J) :
        liftFromOverComp.hom.app x✝ = match x✝ with | star => CategoryStruct.id ((liftFromOver.obj (K.comp (Over.post F))).obj star) | of a => CategoryStruct.id ((liftFromOver.obj (K.comp (Over.post F))).obj (of a))
        source
        def CategoryTheory.WithTerminal.coneEquiv {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} :
        Limits.Cone K ≌ Limits.Cone (liftFromOver.obj K)

        Given a functor K : J ⥤ Over X and its extension liftFromOver K : WithTerminal J ⥤ C, there is an obvious equivalence between cones of these two functors. A cone of K is an object of Over X, so it has the form t ⟶ X. Equivalently, a cone of WithTerminal K is an object t : C, and we can recover the structure morphism as π.app X : t ⟶ X.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.WithTerminal.coneEquiv_inverse_map_hom_left {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} {t₁ t₂ : Limits.Cone (liftFromOver.obj K)} {f : t₁ ⟶ t₂} :
          (coneEquiv.inverse.map f).hom.left = f.hom
          source
          @[simp]
          theorem CategoryTheory.WithTerminal.coneEquiv_functor_obj_pt {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} (t : Limits.Cone K) :
          (coneEquiv.functor.obj t).pt = t.pt.left
          source
          @[simp]
          theorem CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_hom {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} (t : Limits.Cone (liftFromOver.obj K)) :
          (coneEquiv.inverse.obj t).pt.hom = t.π.app star
          source
          @[simp]
          theorem CategoryTheory.WithTerminal.coneEquiv_inverse_obj_π_app_left {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} (t : Limits.Cone (liftFromOver.obj K)) (a : J) :
          ((coneEquiv.inverse.obj t).π.app a).left = t.π.app (of a)
          source
          @[simp]
          theorem CategoryTheory.WithTerminal.coneEquiv_counitIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} (X✝ : Limits.Cone (liftFromOver.obj K)) :
          (coneEquiv.counitIso.hom.app X✝).hom = CategoryStruct.id X✝.pt
          source
          @[simp]
          theorem CategoryTheory.WithTerminal.coneEquiv_unitIso_hom_app_hom_left {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} (X✝ : Limits.Cone K) :
          (coneEquiv.unitIso.hom.app X✝).hom.left = CategoryStruct.id X✝.pt.left
          source
          @[simp]
          theorem CategoryTheory.WithTerminal.coneEquiv_counitIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} (X✝ : Limits.Cone (liftFromOver.obj K)) :
          (coneEquiv.counitIso.inv.app X✝).hom = CategoryStruct.id X✝.pt
          source
          @[simp]
          theorem CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_right_as {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} (t : Limits.Cone (liftFromOver.obj K)) :
          (coneEquiv.inverse.obj t).pt.right.as = PUnit.unit
          source
          @[simp]
          theorem CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_left {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} (t : Limits.Cone (liftFromOver.obj K)) :
          (coneEquiv.inverse.obj t).pt.left = t.pt
          source
          @[simp]
          theorem CategoryTheory.WithTerminal.coneEquiv_functor_map_hom {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} {t₁ t₂ : Limits.Cone K} (f : t₁ ⟶ t₂) :
          (coneEquiv.functor.map f).hom = f.hom.left
          source
          @[simp]
          theorem CategoryTheory.WithTerminal.coneEquiv_unitIso_inv_app_hom_left {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} (X✝ : Limits.Cone K) :
          (coneEquiv.unitIso.inv.app X✝).hom.left = CategoryStruct.id X✝.pt.left
          source
          @[simp]
          theorem CategoryTheory.WithTerminal.coneEquiv_functor_obj_π_app_star {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} {t : Limits.Cone K} :
          (coneEquiv.functor.obj t).π.app star = t.pt.hom
          source
          @[simp]
          theorem CategoryTheory.WithTerminal.coneEquiv_functor_obj_π_app_of {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} {t : Limits.Cone K} (Y : J) :
          (coneEquiv.functor.obj t).π.app (of Y) = (t.π.app Y).left
          source
          def CategoryTheory.WithTerminal.isLimitEquiv {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} {t : Limits.Cone K} :
          Limits.IsLimit (coneEquiv.functor.obj t) ≃ Limits.IsLimit t

          A cone t of K : J ⥤ Over X is a limit if and only if the corresponding cone coneLift t of liftFromOver.obj K : WithTerminal K ⥤ C is a limit.

          Equations
          Instances For
            source
            @[simp]
            theorem CategoryTheory.WithTerminal.isLimitEquiv_symm_apply_lift {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} {t : Limits.Cone K} (t✝ : Limits.IsLimit t) (s : Limits.Cone (liftFromOver.obj K)) :
            (isLimitEquiv.symm t✝).lift s = ((coneEquiv.symm.toAdjunction.homEquiv s t) (t✝.liftConeMorphism (coneEquiv.inverse.obj s))).hom
            source
            @[simp]
            theorem CategoryTheory.WithTerminal.isLimitEquiv_apply_lift_left {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Over X)} {t : Limits.Cone K} (P : Limits.IsLimit (coneEquiv.functor.obj t)) (s : Limits.Cone K) :
            ((isLimitEquiv P).lift s).left = ((Limits.IsLimit.ofRightAdjoint coneEquiv.toAdjunction P).lift s).left
            source
            def CategoryTheory.WithInitial.commaFromUnder {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} :
            Functor (Functor J (Under X)) (Comma (Functor.const J) (Functor.id (Functor J C)))

            The category of functors J ⥤ Under X can be seen as part of a comma category, namely the comma category constructed from the identity of the category of functors J ⥤ C and the functor that maps X : C to the constant functor J ⥤ C.

            Given a functor K : J ⥤ Under X, it is mapped to a natural transformation to the obvious functor J ⥤ C from the constant functor X.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.WithInitial.commaFromUnder_map_left {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {X✝ Y✝ : Functor J (Under X)} (f : X✝ ⟶ Y✝) :
              (commaFromUnder.map f).left = CategoryStruct.id X
              source
              @[simp]
              theorem CategoryTheory.WithInitial.commaFromUnder_obj_left {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} (K : Functor J (Under X)) :
              (commaFromUnder.obj K).left = X
              source
              @[simp]
              theorem CategoryTheory.WithInitial.commaFromUnder_obj_right {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} (K : Functor J (Under X)) :
              (commaFromUnder.obj K).right = K.comp (Under.forget X)
              source
              @[simp]
              theorem CategoryTheory.WithInitial.commaFromUnder_map_right {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {X✝ Y✝ : Functor J (Under X)} (f : X✝ ⟶ Y✝) :
              (commaFromUnder.map f).right = whiskerRight f (Under.forget X)
              source
              @[simp]
              theorem CategoryTheory.WithInitial.commaFromUnder_obj_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} (K : Functor J (Under X)) (a : J) :
              (commaFromUnder.obj K).hom.app a = (K.obj a).hom
              source
              def CategoryTheory.WithInitial.liftFromUnder {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} :
              Functor (Functor J (Under X)) (Functor (WithInitial J) C)

              For any functor K : J ⥤ Under X, there is a canonical extension WithInitial J ⥤ C, that sends star to X.

              Equations
              Instances For
                source
                @[simp]
                theorem CategoryTheory.WithInitial.liftFromUnder_obj_obj {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} (X✝ : Functor J (Under X)) (X✝ : WithInitial J) :
                (liftFromUnder.obj X✝).obj X✝ = match X✝ with | of x => (X✝.obj x).right | star => X
                source
                @[simp]
                theorem CategoryTheory.WithInitial.liftFromUnder_map_app {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {X✝ Y✝ : Functor J (Under X)} (f : X✝ ⟶ Y✝) (x : WithInitial J) :
                (liftFromUnder.map f).app x = match x with | of x => (f.app x).right | star => CategoryStruct.id X
                source
                @[simp]
                theorem CategoryTheory.WithInitial.liftFromUnder_obj_map {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} (X✝ : Functor J (Under X)) {X✝ Y : WithInitial J} (f : X✝ ⟶ Y) :
                (liftFromUnder.obj X✝).map f = match X✝, Y, f with | of a, of a_1, f => (X✝.map (down f)).right | star, of a, x => (X✝.obj a).hom | star, star, x => CategoryStruct.id X
                source
                def CategoryTheory.WithInitial.liftFromUnderComp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} {F : Functor C D} :
                liftFromUnder.obj (K.comp (Under.post F)) ≅ (liftFromUnder.obj K).comp F

                The extension of a functor to under categories behaves well with compositions.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.WithInitial.liftFromUnderComp_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} {F : Functor C D} (x✝ : WithInitial J) :
                  liftFromUnderComp.hom.app x✝ = match x✝ with | star => CategoryStruct.id ((liftFromUnder.obj (K.comp (Under.post F))).obj star) | of a => CategoryStruct.id ((liftFromUnder.obj (K.comp (Under.post F))).obj (of a))
                  source
                  @[simp]
                  theorem CategoryTheory.WithInitial.liftFromUnderComp_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} {F : Functor C D} (x✝ : WithInitial J) :
                  liftFromUnderComp.inv.app x✝ = match x✝ with | star => CategoryStruct.id (((liftFromUnder.obj K).comp F).obj star) | of a => CategoryStruct.id (((liftFromUnder.obj K).comp F).obj (of a))
                  source
                  def CategoryTheory.WithInitial.coconeEquiv {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} :
                  Limits.Cocone K ≌ Limits.Cocone (liftFromUnder.obj K)

                  Given a functor K : J ⥤ Under X and its extension liftFromUnder K : WithInitial J ⥤ C, there is an obvious equivalence between cocones of these two functors. A cocone of K is an object of Under X, so it has the form X ⟶ t. Equivalently, a cocone of WithInitial K is an object t : C, and we can recover the structure morphism as ι.app X : X ⟶ t.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem CategoryTheory.WithInitial.coconeEquiv_inverse_obj_ι_app_right {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} (t : Limits.Cocone (liftFromUnder.obj K)) (a : J) :
                    ((coconeEquiv.inverse.obj t).ι.app a).right = t.ι.app (of a)
                    source
                    @[simp]
                    theorem CategoryTheory.WithInitial.coconeEquiv_inverse_map_hom_right {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} {t₁ t₂ : Limits.Cocone (liftFromUnder.obj K)} {f : t₁ ⟶ t₂} :
                    (coconeEquiv.inverse.map f).hom.right = f.hom
                    source
                    @[simp]
                    theorem CategoryTheory.WithInitial.coconeEquiv_counitIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} (X✝ : Limits.Cocone (liftFromUnder.obj K)) :
                    (coconeEquiv.counitIso.inv.app X✝).hom = CategoryStruct.id X✝.pt
                    source
                    @[simp]
                    theorem CategoryTheory.WithInitial.coconeEquiv_unitIso_inv_app_hom_right {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} (X✝ : Limits.Cocone K) :
                    (coconeEquiv.unitIso.inv.app X✝).hom.right = CategoryStruct.id X✝.pt.right
                    source
                    @[simp]
                    theorem CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_left_as {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} (t : Limits.Cocone (liftFromUnder.obj K)) :
                    (coconeEquiv.inverse.obj t).pt.left.as = PUnit.unit
                    source
                    @[simp]
                    theorem CategoryTheory.WithInitial.coconeEquiv_functor_map_hom {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} {t₁ t₂ : Limits.Cocone K} (f : t₁ ⟶ t₂) :
                    (coconeEquiv.functor.map f).hom = f.hom.right
                    source
                    @[simp]
                    theorem CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_right {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} (t : Limits.Cocone (liftFromUnder.obj K)) :
                    (coconeEquiv.inverse.obj t).pt.right = t.pt
                    source
                    @[simp]
                    theorem CategoryTheory.WithInitial.coconeEquiv_unitIso_hom_app_hom_right {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} (X✝ : Limits.Cocone K) :
                    (coconeEquiv.unitIso.hom.app X✝).hom.right = CategoryStruct.id X✝.pt.right
                    source
                    @[simp]
                    theorem CategoryTheory.WithInitial.coconeEquiv_functor_obj_pt {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} (t : Limits.Cocone K) :
                    (coconeEquiv.functor.obj t).pt = t.pt.right
                    source
                    @[simp]
                    theorem CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_hom {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} (t : Limits.Cocone (liftFromUnder.obj K)) :
                    (coconeEquiv.inverse.obj t).pt.hom = t.ι.app star
                    source
                    @[simp]
                    theorem CategoryTheory.WithInitial.coconeEquiv_counitIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} (X✝ : Limits.Cocone (liftFromUnder.obj K)) :
                    (coconeEquiv.counitIso.hom.app X✝).hom = CategoryStruct.id X✝.pt
                    source
                    @[simp]
                    theorem CategoryTheory.WithInitial.coconeEquiv_functor_obj_ι_app_star {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} {t : Limits.Cocone K} :
                    (coconeEquiv.functor.obj t).ι.app star = t.pt.hom
                    source
                    @[simp]
                    theorem CategoryTheory.WithInitial.coconeEquiv_functor_obj_ι_app_of {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} {t : Limits.Cocone K} (Y : J) :
                    (coconeEquiv.functor.obj t).ι.app (of Y) = (t.ι.app Y).right
                    source
                    def CategoryTheory.WithInitial.isColimitEquiv {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} {t : Limits.Cocone K} :
                    Limits.IsColimit (coconeEquiv.functor.obj t) ≃ Limits.IsColimit t

                    A cocone t of K : J ⥤ Under X is a colimit if and only if the corresponding cocone coconeLift t of liftFromUnder.obj K : WithInitial K ⥤ C is a colimit.

                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.WithInitial.isColimitEquiv_apply_desc_right {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} {t : Limits.Cocone K} (P : Limits.IsColimit (coconeEquiv.functor.obj t)) (s : Limits.Cocone K) :
                      ((isColimitEquiv P).desc s).right = ((Limits.IsColimit.ofLeftAdjoint coconeEquiv.symm.toAdjunction P).desc s).right
                      source
                      @[simp]
                      theorem CategoryTheory.WithInitial.isColimitEquiv_symm_apply_desc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {X : C} {K : Functor J (Under X)} {t : Limits.Cocone K} (t✝ : Limits.IsColimit t) (s : Limits.Cocone (liftFromUnder.obj K)) :
                      (isColimitEquiv.symm t✝).desc s = ((coconeEquiv.toAdjunction.homEquiv t s).symm (t✝.descCoconeMorphism (coconeEquiv.inverse.obj s))).hom