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 #

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
    @[simp]
    theorem CategoryTheory.Bicategory.Adj.mk_obj {B : Type u} [Bicategory B] (b : Adj B) :
    { obj := b.obj } = b
    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
      Equations
      • One or more equations did not get rendered due to their size.
      @[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) :
      @[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) :
      @[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) :
      structure CategoryTheory.Bicategory.Adj.Hom₂ {B : Type u} [Bicategory B] {a b : Adj B} (α β : a b) :

      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
        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
        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
        Equations
        • One or more equations did not get rendered due to their size.
        @[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) :
        @[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) :
        @[simp]
        theorem CategoryTheory.Bicategory.Adj.Hom_def {B : Type u} [Bicategory B] {a b : Adj B} (α β : a b) :
        (α β) = Hom₂ α β
        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) :
        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) :
        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
        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
        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
          @[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
          @[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
          @[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
          @[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

          The associator in the bicategory Adj B.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[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) :
            @[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) :
            @[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) :
            @[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) :
            def CategoryTheory.Bicategory.Adj.Bicategory.whiskerLeft {B : Type u} [Bicategory B] {a b c : Adj B} (α : a b) {β β' : b c} (y : β β') :

            The left whiskering in the bicategory Adj B.

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

              The right whiskering in the bicategory Adj B.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem CategoryTheory.Bicategory.Adj.Bicategory.whiskerRight_τr {B : Type u} [Bicategory B] {a b c : Adj B} {α α' : a b} (x : α α') (β : b c) :
                @[simp]
                theorem CategoryTheory.Bicategory.Adj.Bicategory.whiskerRight_τl {B : Type u} [Bicategory B] {a b c : Adj B} {α α' : a b} (x : α α') (β : b c) :
                Equations
                • One or more equations did not get rendered due to their size.
                @[simp]
                theorem CategoryTheory.Bicategory.Adj.rightUnitor_inv_τr {B : Type u} [Bicategory B] {a✝ b✝ : Adj B} (α : a✝ b✝) :
                @[simp]
                theorem CategoryTheory.Bicategory.Adj.leftUnitor_hom_τl {B : Type u} [Bicategory B] {a✝ b✝ : Adj B} (α : a✝ b✝) :
                @[simp]
                theorem CategoryTheory.Bicategory.Adj.rightUnitor_hom_τl {B : Type u} [Bicategory B] {a✝ b✝ : Adj B} (α : a✝ b✝) :
                @[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✝) :
                @[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
                @[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
                @[simp]
                theorem CategoryTheory.Bicategory.Adj.leftUnitor_inv_τr {B : Type u} [Bicategory B] {a✝ b✝ : Adj B} (α : a✝ b✝) :
                @[simp]
                theorem CategoryTheory.Bicategory.Adj.whiskerLeft_τr {B : Type u} [Bicategory B] {a✝ b✝ c✝ : Adj B} (α : a✝ b✝) {β β' : b✝ c✝} (y : β β') :
                @[simp]
                theorem CategoryTheory.Bicategory.Adj.rightUnitor_inv_τl {B : Type u} [Bicategory B] {a✝ b✝ : Adj B} (α : a✝ b✝) :
                @[simp]
                theorem CategoryTheory.Bicategory.Adj.whiskerLeft_τl {B : Type u} [Bicategory B] {a✝ b✝ c✝ : Adj B} (α : a✝ b✝) {β β' : b✝ c✝} (y : β β') :
                @[simp]
                theorem CategoryTheory.Bicategory.Adj.leftUnitor_hom_τr {B : Type u} [Bicategory B] {a✝ b✝ : Adj B} (α : a✝ b✝) :
                @[simp]
                theorem CategoryTheory.Bicategory.Adj.leftUnitor_inv_τl {B : Type u} [Bicategory B] {a✝ b✝ : Adj B} (α : a✝ b✝) :
                @[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
                @[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
                @[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✝) :
                @[simp]
                theorem CategoryTheory.Bicategory.Adj.rightUnitor_hom_τr {B : Type u} [Bicategory B] {a✝ b✝ : Adj B} (α : a✝ b✝) :

                The forget pseudofunctor from Adj B to B.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem CategoryTheory.Bicategory.Adj.forget₁_toPrelaxFunctor_toPrelaxFunctorStruct_map₂ {B : Type u} [Bicategory B] {a✝ b✝ : Adj B} {f✝ g✝ : a✝ b✝} (α : f✝ g✝) :
                  @[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
                  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
                    @[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
                    @[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
                    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
                      @[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
                      @[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