Documentation

Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

The bicategory of adjunctions in a bicategory #

Given a bicategory B, we construct a bicategory Adj B that has essentially the same objects as B but whose 1-morphisms are adjunctions (in the same direction as the left adjoints), and 2-morphisms are tuples of mate maps between the left and right adjoints (where the map between right adjoints is in the opposite direction).

Certain pseudofunctors to the bicategory Adj Cat are analogous to bifibered categories: in various contexts, this may be used in order to formalize the properties of both pullback and pushforward functors.

References #

source
structure CategoryTheory.Bicategory.Adj (B : Type u) [Bicategory B] :
Type u

The bicategory that has the same objects as a bicategory B, in which 1-morphisms are adjunctions (in the same direction as the left adjoints), and 2-morphisms are tuples of mate maps between the left and right adjoints (where the map between right adjoints is in the opposite direction).

  • obj : B

    If a : Adj B, a.obj : B is the underlying object of the bicategory B.

Instances For
    source
    @[simp]
    theorem CategoryTheory.Bicategory.Adj.mk_obj {B : Type u} [Bicategory B] (b : Adj B) :
    { obj := b.obj } = b
    source
    structure CategoryTheory.Bicategory.Adj.Hom {B : Type u} [Bicategory B] (a b : B) :
    Type (max v w)

    Given two objects a and b in a bicategory, this is the type of adjunctions between a and b.

    • l : a ⟶ b

      the left adjoint

    • r : b ⟶ a

      the right adjoint

    • adj : Adjunction self.l self.r

      the adjunction

    Instances For
      source
      instance CategoryTheory.Bicategory.Adj.instCategoryStruct {B : Type u} [Bicategory B] :
      CategoryStruct.{max v w, u} (Adj B)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[simp]
      theorem CategoryTheory.Bicategory.Adj.comp_r {B : Type u} [Bicategory B] {X✝ Y✝ Z✝ : Adj B} (f : Hom X✝.obj Y✝.obj) (g : Hom Y✝.obj Z✝.obj) :
      (CategoryStruct.comp f g).r = CategoryStruct.comp g.r f.r
      source
      @[simp]
      theorem CategoryTheory.Bicategory.Adj.id_adj {B : Type u} [Bicategory B] (a : Adj B) :
      (CategoryStruct.id a).adj = Adjunction.id a.obj
      source
      @[simp]
      theorem CategoryTheory.Bicategory.Adj.comp_adj {B : Type u} [Bicategory B] {X✝ Y✝ Z✝ : Adj B} (f : Hom X✝.obj Y✝.obj) (g : Hom Y✝.obj Z✝.obj) :
      (CategoryStruct.comp f g).adj = f.adj.comp g.adj
      source
      @[simp]
      theorem CategoryTheory.Bicategory.Adj.comp_l {B : Type u} [Bicategory B] {X✝ Y✝ Z✝ : Adj B} (f : Hom X✝.obj Y✝.obj) (g : Hom Y✝.obj Z✝.obj) :
      (CategoryStruct.comp f g).l = CategoryStruct.comp f.l g.l
      source
      @[simp]
      theorem CategoryTheory.Bicategory.Adj.id_l {B : Type u} [Bicategory B] (a : Adj B) :
      (CategoryStruct.id a).l = CategoryStruct.id a.obj
      source
      @[simp]
      theorem CategoryTheory.Bicategory.Adj.id_r {B : Type u} [Bicategory B] (a : Adj B) :
      (CategoryStruct.id a).r = CategoryStruct.id a.obj
      source
      structure CategoryTheory.Bicategory.Adj.Hom₂ {B : Type u} [Bicategory B] {a b : Adj B} (α β : a ⟶ b) :
      Type w

      A morphism between two adjunctions consists of a tuple of mate maps.

      • τl : α.l ⟶ β.l

        the morphism between left adjoints

      • τr : β.r ⟶ α.r

        the morphism in the opposite direction between right adjoints

      • conjugateEquiv_τl : (conjugateEquiv β.adj α.adj) self.τl = self.τr
      Instances For
        source
        theorem CategoryTheory.Bicategory.Adj.Hom₂.ext {B : Type u} {inst✝ : Bicategory B} {a b : Adj B} {α β : a ⟶ b} {x y : Hom₂ α β} (τl : x.τl = y.τl) (τr : x.τr = y.τr) :
        x = y
        source
        theorem CategoryTheory.Bicategory.Adj.Hom₂.ext_iff {B : Type u} {inst✝ : Bicategory B} {a b : Adj B} {α β : a ⟶ b} {x y : Hom₂ α β} :
        x = y ↔ x.τl = y.τl ∧ x.τr = y.τr
        source
        theorem CategoryTheory.Bicategory.Adj.Hom₂.conjugateEquiv_symm_τr {B : Type u} [Bicategory B] {a b : Adj B} {α β : a ⟶ b} (p : Hom₂ α β) :
        (conjugateEquiv β.adj α.adj).symm p.τr = p.τl
        source
        instance CategoryTheory.Bicategory.Adj.instCategoryStructHom {B : Type u} [Bicategory B] {a b : Adj B} :
        CategoryStruct.{w, max v w} (a ⟶ b)
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[simp]
        theorem CategoryTheory.Bicategory.Adj.comp_τl {B : Type u} [Bicategory B] {a b : Adj B} {a✝ b✝ c : a ⟶ b} (x : Hom₂ a✝ b✝) (y : Hom₂ b✝ c) :
        (CategoryStruct.comp x y).τl = CategoryStruct.comp x.τl y.τl
        source
        @[simp]
        theorem CategoryTheory.Bicategory.Adj.id_τr {B : Type u} [Bicategory B] {a b : Adj B} (α : a ⟶ b) :
        (CategoryStruct.id α).τr = CategoryStruct.id α.r
        source
        @[simp]
        theorem CategoryTheory.Bicategory.Adj.comp_τr {B : Type u} [Bicategory B] {a b : Adj B} {a✝ b✝ c : a ⟶ b} (x : Hom₂ a✝ b✝) (y : Hom₂ b✝ c) :
        (CategoryStruct.comp x y).τr = CategoryStruct.comp y.τr x.τr
        source
        @[simp]
        theorem CategoryTheory.Bicategory.Adj.id_τl {B : Type u} [Bicategory B] {a b : Adj B} (α : a ⟶ b) :
        (CategoryStruct.id α).τl = CategoryStruct.id α.l
        source
        @[simp]
        theorem CategoryTheory.Bicategory.Adj.Hom_def {B : Type u} [Bicategory B] {a b : Adj B} (α β : a ⟶ b) :
        (α ⟶ β) = Hom₂ α β
        source
        theorem CategoryTheory.Bicategory.Adj.comp_τl_assoc {B : Type u} [Bicategory B] {a b : Adj B} {a✝ b✝ c : a ⟶ b} (x : Hom₂ a✝ b✝) (y : Hom₂ b✝ c) {Z : a.obj ⟶ b.obj} (h : c.l ⟶ Z) :
        CategoryStruct.comp (CategoryStruct.comp x y).τl h = CategoryStruct.comp x.τl (CategoryStruct.comp y.τl h)
        source
        theorem CategoryTheory.Bicategory.Adj.comp_τr_assoc {B : Type u} [Bicategory B] {a b : Adj B} {a✝ b✝ c : a ⟶ b} (x : Hom₂ a✝ b✝) (y : Hom₂ b✝ c) {Z : b.obj ⟶ a.obj} (h : a✝.r ⟶ Z) :
        CategoryStruct.comp (CategoryStruct.comp x y).τr h = CategoryStruct.comp y.τr (CategoryStruct.comp x.τr h)
        source
        theorem CategoryTheory.Bicategory.Adj.hom₂_ext {B : Type u} [Bicategory B] {a b : Adj B} {α β : a ⟶ b} {x y : α ⟶ β} (hl : x.τl = y.τl) :
        x = y
        source
        theorem CategoryTheory.Bicategory.Adj.hom₂_ext_iff {B : Type u} [Bicategory B] {a b : Adj B} {α β : a ⟶ b} {x y : α ⟶ β} :
        x = y ↔ x.τl = y.τl
        source
        instance CategoryTheory.Bicategory.Adj.instCategoryHom {B : Type u} [Bicategory B] {a b : Adj B} :
        Category.{w, max v w} (a ⟶ b)
        Equations
        source
        def CategoryTheory.Bicategory.Adj.iso₂Mk {B : Type u} [Bicategory B] {a b : Adj B} {α β : a ⟶ b} (el : α.l ≅ β.l) (er : β.r ≅ α.r) (h : (conjugateEquiv β.adj α.adj) el.hom = er.hom) :
        α ≅ β

        Constructor for isomorphisms between 1-morphisms in the bicategory Adj B.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Bicategory.Adj.iso₂Mk_hom_τr {B : Type u} [Bicategory B] {a b : Adj B} {α β : a ⟶ b} (el : α.l ≅ β.l) (er : β.r ≅ α.r) (h : (conjugateEquiv β.adj α.adj) el.hom = er.hom) :
          (iso₂Mk el er h).hom.τr = er.hom
          source
          @[simp]
          theorem CategoryTheory.Bicategory.Adj.iso₂Mk_inv_τl {B : Type u} [Bicategory B] {a b : Adj B} {α β : a ⟶ b} (el : α.l ≅ β.l) (er : β.r ≅ α.r) (h : (conjugateEquiv β.adj α.adj) el.hom = er.hom) :
          (iso₂Mk el er h).inv.τl = el.inv
          source
          @[simp]
          theorem CategoryTheory.Bicategory.Adj.iso₂Mk_inv_τr {B : Type u} [Bicategory B] {a b : Adj B} {α β : a ⟶ b} (el : α.l ≅ β.l) (er : β.r ≅ α.r) (h : (conjugateEquiv β.adj α.adj) el.hom = er.hom) :
          (iso₂Mk el er h).inv.τr = er.inv
          source
          @[simp]
          theorem CategoryTheory.Bicategory.Adj.iso₂Mk_hom_τl {B : Type u} [Bicategory B] {a b : Adj B} {α β : a ⟶ b} (el : α.l ≅ β.l) (er : β.r ≅ α.r) (h : (conjugateEquiv β.adj α.adj) el.hom = er.hom) :
          (iso₂Mk el er h).hom.τl = el.hom
          source
          def CategoryTheory.Bicategory.Adj.Bicategory.associator {B : Type u} [Bicategory B] {a b c d : Adj B} (α : a ⟶ b) (β : b ⟶ c) (γ : c ⟶ d) :
          CategoryStruct.comp (CategoryStruct.comp α β) γ ≅ CategoryStruct.comp α (CategoryStruct.comp β γ)

          The associator in the bicategory Adj B.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Bicategory.Adj.Bicategory.associator_hom_τl {B : Type u} [Bicategory B] {a b c d : Adj B} (α : a ⟶ b) (β : b ⟶ c) (γ : c ⟶ d) :
            (associator α β γ).hom.τl = (CategoryTheory.Bicategory.associator α.l β.l γ.l).hom
            source
            @[simp]
            theorem CategoryTheory.Bicategory.Adj.Bicategory.associator_hom_τr {B : Type u} [Bicategory B] {a b c d : Adj B} (α : a ⟶ b) (β : b ⟶ c) (γ : c ⟶ d) :
            (associator α β γ).hom.τr = (CategoryTheory.Bicategory.associator γ.r β.r α.r).hom
            source
            @[simp]
            theorem CategoryTheory.Bicategory.Adj.Bicategory.associator_inv_τl {B : Type u} [Bicategory B] {a b c d : Adj B} (α : a ⟶ b) (β : b ⟶ c) (γ : c ⟶ d) :
            (associator α β γ).inv.τl = (CategoryTheory.Bicategory.associator α.l β.l γ.l).inv
            source
            @[simp]
            theorem CategoryTheory.Bicategory.Adj.Bicategory.associator_inv_τr {B : Type u} [Bicategory B] {a b c d : Adj B} (α : a ⟶ b) (β : b ⟶ c) (γ : c ⟶ d) :
            (associator α β γ).inv.τr = (CategoryTheory.Bicategory.associator γ.r β.r α.r).inv
            source
            def CategoryTheory.Bicategory.Adj.Bicategory.leftUnitor {B : Type u} [Bicategory B] {a b : Adj B} (α : a ⟶ b) :
            CategoryStruct.comp (CategoryStruct.id a) α ≅ α

            The left unitor in the bicategory Adj B.

            Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Bicategory.Adj.Bicategory.leftUnitor_hom_τr {B : Type u} [Bicategory B] {a b : Adj B} (α : a ⟶ b) :
              (leftUnitor α).hom.τr = (CategoryTheory.Bicategory.rightUnitor α.r).inv
              source
              @[simp]
              theorem CategoryTheory.Bicategory.Adj.Bicategory.leftUnitor_hom_τl {B : Type u} [Bicategory B] {a b : Adj B} (α : a ⟶ b) :
              (leftUnitor α).hom.τl = (CategoryTheory.Bicategory.leftUnitor α.l).hom
              source
              @[simp]
              theorem CategoryTheory.Bicategory.Adj.Bicategory.leftUnitor_inv_τr {B : Type u} [Bicategory B] {a b : Adj B} (α : a ⟶ b) :
              (leftUnitor α).inv.τr = (CategoryTheory.Bicategory.rightUnitor α.r).hom
              source
              @[simp]
              theorem CategoryTheory.Bicategory.Adj.Bicategory.leftUnitor_inv_τl {B : Type u} [Bicategory B] {a b : Adj B} (α : a ⟶ b) :
              (leftUnitor α).inv.τl = (CategoryTheory.Bicategory.leftUnitor α.l).inv
              source
              def CategoryTheory.Bicategory.Adj.Bicategory.rightUnitor {B : Type u} [Bicategory B] {a b : Adj B} (α : a ⟶ b) :
              CategoryStruct.comp α (CategoryStruct.id b) ≅ α

              The right unitor in the bicategory Adj B.

              Equations
              Instances For
                source
                @[simp]
                theorem CategoryTheory.Bicategory.Adj.Bicategory.rightUnitor_inv_τl {B : Type u} [Bicategory B] {a b : Adj B} (α : a ⟶ b) :
                (rightUnitor α).inv.τl = (CategoryTheory.Bicategory.rightUnitor α.l).inv
                source
                @[simp]
                theorem CategoryTheory.Bicategory.Adj.Bicategory.rightUnitor_inv_τr {B : Type u} [Bicategory B] {a b : Adj B} (α : a ⟶ b) :
                (rightUnitor α).inv.τr = (CategoryTheory.Bicategory.leftUnitor α.r).hom
                source
                @[simp]
                theorem CategoryTheory.Bicategory.Adj.Bicategory.rightUnitor_hom_τr {B : Type u} [Bicategory B] {a b : Adj B} (α : a ⟶ b) :
                (rightUnitor α).hom.τr = (CategoryTheory.Bicategory.leftUnitor α.r).inv
                source
                @[simp]
                theorem CategoryTheory.Bicategory.Adj.Bicategory.rightUnitor_hom_τl {B : Type u} [Bicategory B] {a b : Adj B} (α : a ⟶ b) :
                (rightUnitor α).hom.τl = (CategoryTheory.Bicategory.rightUnitor α.l).hom
                source
                def CategoryTheory.Bicategory.Adj.Bicategory.whiskerLeft {B : Type u} [Bicategory B] {a b c : Adj B} (α : a ⟶ b) {β β' : b ⟶ c} (y : β ⟶ β') :
                CategoryStruct.comp α β ⟶ CategoryStruct.comp α β'

                The left whiskering in the bicategory Adj B.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.Adj.Bicategory.whiskerLeft_τl {B : Type u} [Bicategory B] {a b c : Adj B} (α : a ⟶ b) {β β' : b ⟶ c} (y : β ⟶ β') :
                  (whiskerLeft α y).τl = CategoryTheory.Bicategory.whiskerLeft α.l y.τl
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.Adj.Bicategory.whiskerLeft_τr {B : Type u} [Bicategory B] {a b c : Adj B} (α : a ⟶ b) {β β' : b ⟶ c} (y : β ⟶ β') :
                  (whiskerLeft α y).τr = CategoryTheory.Bicategory.whiskerRight y.τr α.r
                  source
                  def CategoryTheory.Bicategory.Adj.Bicategory.whiskerRight {B : Type u} [Bicategory B] {a b c : Adj B} {α α' : a ⟶ b} (x : α ⟶ α') (β : b ⟶ c) :
                  CategoryStruct.comp α β ⟶ CategoryStruct.comp α' β

                  The right whiskering in the bicategory Adj B.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.Adj.Bicategory.whiskerRight_τl {B : Type u} [Bicategory B] {a b c : Adj B} {α α' : a ⟶ b} (x : α ⟶ α') (β : b ⟶ c) :
                    (whiskerRight x β).τl = CategoryTheory.Bicategory.whiskerRight x.τl β.l
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.Adj.Bicategory.whiskerRight_τr {B : Type u} [Bicategory B] {a b c : Adj B} {α α' : a ⟶ b} (x : α ⟶ α') (β : b ⟶ c) :
                    (whiskerRight x β).τr = CategoryTheory.Bicategory.whiskerLeft β.r x.τr
                    source
                    instance CategoryTheory.Bicategory.Adj.inst {B : Type u} [Bicategory B] :
                    Bicategory (Adj B)
                    Equations
                    • One or more equations did not get rendered due to their size.
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.Adj.leftUnitor_hom_τr {B : Type u} [Bicategory B] {a✝ b✝ : Adj B} (α : a✝ ⟶ b✝) :
                    (leftUnitor α).hom.τr = (rightUnitor α.r).inv
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.Adj.leftUnitor_inv_τl {B : Type u} [Bicategory B] {a✝ b✝ : Adj B} (α : a✝ ⟶ b✝) :
                    (leftUnitor α).inv.τl = (leftUnitor α.l).inv
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.Adj.leftUnitor_hom_τl {B : Type u} [Bicategory B] {a✝ b✝ : Adj B} (α : a✝ ⟶ b✝) :
                    (leftUnitor α).hom.τl = (leftUnitor α.l).hom
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.Adj.rightUnitor_inv_τr {B : Type u} [Bicategory B] {a✝ b✝ : Adj B} (α : a✝ ⟶ b✝) :
                    (rightUnitor α).inv.τr = (leftUnitor α.r).hom
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.Adj.leftUnitor_inv_τr {B : Type u} [Bicategory B] {a✝ b✝ : Adj B} (α : a✝ ⟶ b✝) :
                    (leftUnitor α).inv.τr = (rightUnitor α.r).hom
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.Adj.rightUnitor_hom_τr {B : Type u} [Bicategory B] {a✝ b✝ : Adj B} (α : a✝ ⟶ b✝) :
                    (rightUnitor α).hom.τr = (leftUnitor α.r).inv
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.Adj.associator_hom_τr {B : Type u} [Bicategory B] {a✝ b✝ c✝ d✝ : Adj B} (α : a✝ ⟶ b✝) (β : b✝ ⟶ c✝) (γ : c✝ ⟶ d✝) :
                    (associator α β γ).hom.τr = (associator γ.r β.r α.r).hom
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.Adj.whiskerLeft_τr {B : Type u} [Bicategory B] {a✝ b✝ c✝ : Adj B} (α : a✝ ⟶ b✝) {β β' : b✝ ⟶ c✝} (y : β ⟶ β') :
                    (whiskerLeft α y).τr = whiskerRight y.τr α.r
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.Adj.associator_inv_τr {B : Type u} [Bicategory B] {a✝ b✝ c✝ d✝ : Adj B} (α : a✝ ⟶ b✝) (β : b✝ ⟶ c✝) (γ : c✝ ⟶ d✝) :
                    (associator α β γ).inv.τr = (associator γ.r β.r α.r).inv
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.Adj.whiskerLeft_τl {B : Type u} [Bicategory B] {a✝ b✝ c✝ : Adj B} (α : a✝ ⟶ b✝) {β β' : b✝ ⟶ c✝} (y : β ⟶ β') :
                    (whiskerLeft α y).τl = whiskerLeft α.l y.τl
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.Adj.whiskerRight_τl {B : Type u} [Bicategory B] {a✝ b✝ c✝ : Adj B} {f✝ g✝ : a✝ ⟶ b✝} (x : f✝ ⟶ g✝) (β : b✝ ⟶ c✝) :
                    (whiskerRight x β).τl = whiskerRight x.τl β.l
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.Adj.whiskerRight_τr {B : Type u} [Bicategory B] {a✝ b✝ c✝ : Adj B} {f✝ g✝ : a✝ ⟶ b✝} (x : f✝ ⟶ g✝) (β : b✝ ⟶ c✝) :
                    (whiskerRight x β).τr = whiskerLeft β.r x.τr
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.Adj.rightUnitor_hom_τl {B : Type u} [Bicategory B] {a✝ b✝ : Adj B} (α : a✝ ⟶ b✝) :
                    (rightUnitor α).hom.τl = (rightUnitor α.l).hom
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.Adj.rightUnitor_inv_τl {B : Type u} [Bicategory B] {a✝ b✝ : Adj B} (α : a✝ ⟶ b✝) :
                    (rightUnitor α).inv.τl = (rightUnitor α.l).inv
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.Adj.associator_inv_τl {B : Type u} [Bicategory B] {a✝ b✝ c✝ d✝ : Adj B} (α : a✝ ⟶ b✝) (β : b✝ ⟶ c✝) (γ : c✝ ⟶ d✝) :
                    (associator α β γ).inv.τl = (associator α.l β.l γ.l).inv
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.Adj.associator_hom_τl {B : Type u} [Bicategory B] {a✝ b✝ c✝ d✝ : Adj B} (α : a✝ ⟶ b✝) (β : b✝ ⟶ c✝) (γ : c✝ ⟶ d✝) :
                    (associator α β γ).hom.τl = (associator α.l β.l γ.l).hom
                    source
                    def CategoryTheory.Bicategory.Adj.forget₁ {B : Type u} [Bicategory B] :
                    Pseudofunctor (Adj B) B

                    The forget pseudofunctor from Adj B to B.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.Bicategory.Adj.forget₁_mapComp {B : Type u} [Bicategory B] {a✝ b✝ c✝ : Adj B} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) :
                      forget₁.mapComp x✝ x✝¹ = Iso.refl (CategoryStruct.comp x✝ x✝¹).l
                      source
                      @[simp]
                      theorem CategoryTheory.Bicategory.Adj.forget₁_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map {B : Type u} [Bicategory B] {X✝ Y✝ : Adj B} (x : X✝ ⟶ Y✝) :
                      forget₁.map x = x.l
                      source
                      @[simp]
                      theorem CategoryTheory.Bicategory.Adj.forget₁_mapId {B : Type u} [Bicategory B] (x✝ : Adj B) :
                      forget₁.mapId x✝ = Iso.refl (CategoryStruct.id x✝).l
                      source
                      @[simp]
                      theorem CategoryTheory.Bicategory.Adj.forget₁_toPrelaxFunctor_toPrelaxFunctorStruct_map₂ {B : Type u} [Bicategory B] {a✝ b✝ : Adj B} {f✝ g✝ : a✝ ⟶ b✝} (α : f✝ ⟶ g✝) :
                      forget₁.map₂ α = α.τl
                      source
                      @[simp]
                      theorem CategoryTheory.Bicategory.Adj.forget₁_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj {B : Type u} [Bicategory B] (a : Adj B) :
                      forget₁.obj a = a.obj
                      source
                      def CategoryTheory.Bicategory.Adj.lIso {B : Type u} [Bicategory B] {a b : Adj B} {adj₁ adj₂ : a ⟶ b} (e : adj₁ ≅ adj₂) :
                      adj₁.l ≅ adj₂.l

                      Given an isomorphism between two 1-morphisms in Adj B, this is the underlying isomorphisms between the left adjoints.

                      Equations
                      Instances For
                        source
                        @[simp]
                        theorem CategoryTheory.Bicategory.Adj.lIso_hom {B : Type u} [Bicategory B] {a b : Adj B} {adj₁ adj₂ : a ⟶ b} (e : adj₁ ≅ adj₂) :
                        (lIso e).hom = e.hom.τl
                        source
                        @[simp]
                        theorem CategoryTheory.Bicategory.Adj.lIso_inv {B : Type u} [Bicategory B] {a b : Adj B} {adj₁ adj₂ : a ⟶ b} (e : adj₁ ≅ adj₂) :
                        (lIso e).inv = e.inv.τl
                        source
                        def CategoryTheory.Bicategory.Adj.rIso {B : Type u} [Bicategory B] {a b : Adj B} {adj₁ adj₂ : a ⟶ b} (e : adj₁ ≅ adj₂) :
                        adj₁.r ≅ adj₂.r

                        Given an isomorphism between two 1-morphisms in Adj B, this is the underlying isomorphisms between the right adjoints.

                        Equations
                        Instances For
                          source
                          @[simp]
                          theorem CategoryTheory.Bicategory.Adj.rIso_inv {B : Type u} [Bicategory B] {a b : Adj B} {adj₁ adj₂ : a ⟶ b} (e : adj₁ ≅ adj₂) :
                          (rIso e).inv = e.hom.τr
                          source
                          @[simp]
                          theorem CategoryTheory.Bicategory.Adj.rIso_hom {B : Type u} [Bicategory B] {a b : Adj B} {adj₁ adj₂ : a ⟶ b} (e : adj₁ ≅ adj₂) :
                          (rIso e).hom = e.inv.τr