feat(category_theory/monoidal): define the bicategory of algebras and…

… bimodules internal to some monoidal category (#14402)

We generalise the [well-known construction](https://ncatlab.org/nlab/show/bimodule#AsMorphismsInA2Category) of the 2-category of rings, bimodules, and intertwiners.  Given a monoidal category `C` that has coequalizers and in which left and right tensor products preserve colimits, we define a bicategory whose
- objects are monoids in C;
- 1-morphisms are bimodules;
- 2-morphisms are bimodule homomorphisms.

The composition of 1-morphisms is given by the tensor product of bimodules over the middle monoid.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/limits/preserves/shapes/equalizers.lean

@@ -183,6 +183,47 @@ begin
   apply_instance
 end
 
+instance map_π_epi : epi (G.map (coequalizer.π f g)) :=
+⟨λ W h k, by { rw ←ι_comp_coequalizer_comparison, apply (cancel_epi _).1, apply epi_comp }⟩
+
+@[reassoc]
+lemma map_π_preserves_coequalizer_inv :
+  G.map (coequalizer.π f g) ≫ (preserves_coequalizer.iso G f g).inv =
+  coequalizer.π (G.map f) (G.map g) :=
+begin
+  rw [←ι_comp_coequalizer_comparison_assoc, ←preserves_coequalizer.iso_hom,
+      iso.hom_inv_id, comp_id],
+end
+
+@[reassoc]
+lemma map_π_preserves_coequalizer_inv_desc
+  {W : D} (k : G.obj Y ⟶ W) (wk : G.map f ≫ k = G.map g ≫ k) :
+  G.map (coequalizer.π f g) ≫ (preserves_coequalizer.iso G f g).inv ≫ coequalizer.desc k wk = k :=
+by rw [←category.assoc, map_π_preserves_coequalizer_inv, coequalizer.π_desc]
+
+@[reassoc]
+lemma map_π_preserves_coequalizer_inv_colim_map
+  {X' Y' : D} (f' g' : X' ⟶ Y') [has_coequalizer f' g'] (p : G.obj X ⟶ X') (q : G.obj Y ⟶ Y')
+  (wf : (G.map f) ≫ q = p ≫ f') (wg : (G.map g) ≫ q = p ≫ g') :
+  G.map (coequalizer.π f g) ≫ (preserves_coequalizer.iso G f g).inv ≫
+  colim_map (parallel_pair_hom (G.map f) (G.map g) f' g' p q wf wg) =
+  q ≫ coequalizer.π f' g' :=
+by rw [←category.assoc, map_π_preserves_coequalizer_inv, ι_colim_map, parallel_pair_hom_app_one]
+
+@[reassoc]
+lemma map_π_preserves_coequalizer_inv_colim_map_desc
+  {X' Y' : D} (f' g' : X' ⟶ Y') [has_coequalizer f' g'] (p : G.obj X ⟶ X') (q : G.obj Y ⟶ Y')
+  (wf : (G.map f) ≫ q = p ≫ f') (wg : (G.map g) ≫ q = p ≫ g')
+  {Z' : D} (h : Y' ⟶ Z') (wh : f' ≫ h = g' ≫ h) :
+  G.map (coequalizer.π f g) ≫ (preserves_coequalizer.iso G f g).inv ≫
+  colim_map (parallel_pair_hom (G.map f) (G.map g) f' g' p q wf wg) ≫
+  coequalizer.desc h wh =
+  q ≫ h :=
+begin
+  slice_lhs 1 3 { rw map_π_preserves_coequalizer_inv_colim_map },
+  slice_lhs 2 3 { rw coequalizer.π_desc },
+end
+
 /-- Any functor preserves coequalizers of split pairs. -/
 @[priority 1]
 instance preserves_split_coequalizers (f g : X ⟶ Y) [has_split_coequalizer f g] :

src/category_theory/limits/shapes/equalizers.lean

@@ -751,6 +751,13 @@ lemma coequalizer.π_desc {W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) :
   coequalizer.π f g ≫ coequalizer.desc k h = k :=
 colimit.ι_desc _ _
 
+lemma coequalizer.π_colim_map_desc {X' Y' Z : C} (f' g' : X' ⟶ Y') [has_coequalizer f' g']
+  (p : X ⟶ X') (q : Y ⟶ Y') (wf : f ≫ q = p ≫ f') (wg : g ≫ q = p ≫ g')
+  (h : Y' ⟶ Z) (wh : f' ≫ h = g' ≫ h) :
+  coequalizer.π f g ≫ colim_map (parallel_pair_hom f g f' g' p q wf wg) ≫ coequalizer.desc h wh =
+  q ≫ h :=
+by rw [ι_colim_map_assoc, parallel_pair_hom_app_one, coequalizer.π_desc]
+
 /-- Any morphism `k : Y ⟶ W` satisfying `f ≫ k = g ≫ k` induces a morphism
     `l : coequalizer f g ⟶ W` satisfying `coequalizer.π ≫ g = l`. -/
 def coequalizer.desc' {W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) :