Documentation

Mathlib.Tactic.CategoryTheory.BicategoricalComp

Bicategorical composition ⊗≫ (composition up to associators) #

We provide f ⊗≫ g, the bicategoricalComp operation, which automatically inserts associators and unitors as needed to make the target of f match the source of g.

source
🔶 coverage
class CategoryTheory.BicategoricalCoherence {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) :
Type w

A typeclass carrying a choice of bicategorical structural isomorphism between two objects. Used by the ⊗≫ bicategorical composition operator, and the coherence tactic.

  • iso : f ≅ g

    The chosen structural isomorphism between to 1-morphisms.

Instances
    source
    🔸 coverage
    def CategoryTheory.Bicategory.«term⊗𝟙» :
    Lean.ParserDescr

    Notation for identities up to unitors and associators.

    Instances For
      source
      🔸 coverage
      @[reducible, inline]
      abbrev CategoryTheory.bicategoricalIso {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) [BicategoricalCoherence f g] :
      f ≅ g

      Construct an isomorphism between two objects in a bicategorical category out of unitors and associators.

      Instances For
        source
        🔸 coverage
        def CategoryTheory.bicategoricalComp {B : Type u} [Bicategory B] {a b : B} {f g h i : a ⟶ b} [BicategoricalCoherence g h] (η : f ⟶ g) (θ : h ⟶ i) :
        f ⟶ i

        Compose two morphisms in a bicategorical category, inserting unitors and associators between as necessary.

        Instances For
          source
          🔸 coverage
          def CategoryTheory.Bicategory.«term_⊗≫_» :
          Lean.TrailingParserDescr

          Compose two morphisms in a bicategorical category, inserting unitors and associators between as necessary.

          Instances For
            source
            🔸 coverage
            def CategoryTheory.bicategoricalIsoComp {B : Type u} [Bicategory B] {a b : B} {f g h i : a ⟶ b} [BicategoricalCoherence g h] (η : f ≅ g) (θ : h ≅ i) :
            f ≅ i

            Compose two isomorphisms in a bicategorical category, inserting unitors and associators between as necessary.

            Instances For
              source
              🔸 coverage
              def CategoryTheory.Bicategory.«term_≪⊗≫_» :
              Lean.TrailingParserDescr

              Compose two isomorphisms in a bicategorical category, inserting unitors and associators between as necessary.

              Instances For
                source
                🔸 coverage
                @[implicit_reducible]
                instance CategoryTheory.BicategoricalCoherence.refl {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) :
                BicategoricalCoherence f f
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.BicategoricalCoherence.refl_iso {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) :
                iso = Iso.refl f
                source
                🔸 coverage
                @[implicit_reducible]
                instance CategoryTheory.BicategoricalCoherence.whiskerLeft {B : Type u} [Bicategory B] {a b c : B} (f : a ⟶ b) (g h : b ⟶ c) [BicategoricalCoherence g h] :
                BicategoricalCoherence (CategoryStruct.comp f g) (CategoryStruct.comp f h)
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.BicategoricalCoherence.whiskerLeft_iso {B : Type u} [Bicategory B] {a b c : B} (f : a ⟶ b) (g h : b ⟶ c) [BicategoricalCoherence g h] :
                iso = Bicategory.whiskerLeftIso f iso
                source
                🔸 coverage
                @[implicit_reducible]
                instance CategoryTheory.BicategoricalCoherence.whiskerRight {B : Type u} [Bicategory B] {a b c : B} (f g : a ⟶ b) (h : b ⟶ c) [BicategoricalCoherence f g] :
                BicategoricalCoherence (CategoryStruct.comp f h) (CategoryStruct.comp g h)
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.BicategoricalCoherence.whiskerRight_iso {B : Type u} [Bicategory B] {a b c : B} (f g : a ⟶ b) (h : b ⟶ c) [BicategoricalCoherence f g] :
                iso = Bicategory.whiskerRightIso iso h
                source
                🔸 coverage
                @[implicit_reducible]
                instance CategoryTheory.BicategoricalCoherence.tensorRight {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) (g : b ⟶ b) [BicategoricalCoherence (CategoryStruct.id b) g] :
                BicategoricalCoherence f (CategoryStruct.comp f g)
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.BicategoricalCoherence.tensorRight_iso {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) (g : b ⟶ b) [BicategoricalCoherence (CategoryStruct.id b) g] :
                iso = (Bicategory.rightUnitor f).symm ≪≫ Bicategory.whiskerLeftIso f iso
                source
                🔸 coverage
                @[implicit_reducible]
                instance CategoryTheory.BicategoricalCoherence.tensorRight' {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) (g : b ⟶ b) [BicategoricalCoherence g (CategoryStruct.id b)] :
                BicategoricalCoherence (CategoryStruct.comp f g) f
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.BicategoricalCoherence.tensorRight'_iso {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) (g : b ⟶ b) [BicategoricalCoherence g (CategoryStruct.id b)] :
                iso = Bicategory.whiskerLeftIso f iso ≪≫ Bicategory.rightUnitor f
                source
                🔸 coverage
                @[implicit_reducible]
                instance CategoryTheory.BicategoricalCoherence.left {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) [BicategoricalCoherence f g] :
                BicategoricalCoherence (CategoryStruct.comp (CategoryStruct.id a) f) g
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.BicategoricalCoherence.left_iso {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) [BicategoricalCoherence f g] :
                iso = Bicategory.leftUnitor f ≪≫ iso
                source
                🔸 coverage
                @[implicit_reducible]
                instance CategoryTheory.BicategoricalCoherence.left' {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) [BicategoricalCoherence f g] :
                BicategoricalCoherence f (CategoryStruct.comp (CategoryStruct.id a) g)
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.BicategoricalCoherence.left'_iso {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) [BicategoricalCoherence f g] :
                iso = iso ≪≫ (Bicategory.leftUnitor g).symm
                source
                🔸 coverage
                @[implicit_reducible]
                instance CategoryTheory.BicategoricalCoherence.right {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) [BicategoricalCoherence f g] :
                BicategoricalCoherence (CategoryStruct.comp f (CategoryStruct.id b)) g
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.BicategoricalCoherence.right_iso {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) [BicategoricalCoherence f g] :
                iso = Bicategory.rightUnitor f ≪≫ iso
                source
                🔸 coverage
                @[implicit_reducible]
                instance CategoryTheory.BicategoricalCoherence.right' {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) [BicategoricalCoherence f g] :
                BicategoricalCoherence f (CategoryStruct.comp g (CategoryStruct.id b))
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.BicategoricalCoherence.right'_iso {B : Type u} [Bicategory B] {a b : B} (f g : a ⟶ b) [BicategoricalCoherence f g] :
                iso = iso ≪≫ (Bicategory.rightUnitor g).symm
                source
                🔸 coverage
                @[implicit_reducible]
                instance CategoryTheory.BicategoricalCoherence.assoc {B : Type u} [Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : a ⟶ d) [BicategoricalCoherence (CategoryStruct.comp f (CategoryStruct.comp g h)) i] :
                BicategoricalCoherence (CategoryStruct.comp (CategoryStruct.comp f g) h) i
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.BicategoricalCoherence.assoc_iso {B : Type u} [Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : a ⟶ d) [BicategoricalCoherence (CategoryStruct.comp f (CategoryStruct.comp g h)) i] :
                iso = Bicategory.associator f g h ≪≫ iso
                source
                🔸 coverage
                @[implicit_reducible]
                instance CategoryTheory.BicategoricalCoherence.assoc' {B : Type u} [Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : a ⟶ d) [BicategoricalCoherence i (CategoryStruct.comp f (CategoryStruct.comp g h))] :
                BicategoricalCoherence i (CategoryStruct.comp (CategoryStruct.comp f g) h)
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.BicategoricalCoherence.assoc'_iso {B : Type u} [Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : a ⟶ d) [BicategoricalCoherence i (CategoryStruct.comp f (CategoryStruct.comp g h))] :
                iso = iso ≪≫ (Bicategory.associator f g h).symm
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.bicategoricalComp_refl {B : Type u} [Bicategory B] {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) :
                bicategoricalComp η θ = CategoryStruct.comp η θ