feat(category_theory/monoidal/internal): Mon_ (Module R) ≌ Algebra R (#3695)

The category of internal monoid objects in `Module R`
is equivalent to the category of "native" bundled `R`-algebras.

Moreover, this equivalence is compatible with the forgetful functors to `Module R`.



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

Author: kim-em

src/algebra/category/Module/monoidal.lean

@@ -135,17 +135,21 @@ instance : comm_ring ((𝟙_ (Module R) : Module R) : Type u) := (by apply_insta
 namespace monoidal_category
 
 @[simp]
-lemma left_unitor_hom {M : Module R} (r : R) (m : M) :
+lemma hom_apply {K L M N : Module R} (f : K ⟶ L) (g : M ⟶ N) (k : K) (m : M) :
+  (f ⊗ g) (k ⊗ₜ m) = f k ⊗ₜ g m := rfl
+
+@[simp]
+lemma left_unitor_hom_apply {M : Module R} (r : R) (m : M) :
   ((λ_ M).hom : 𝟙_ (Module R) ⊗ M ⟶ M) (r ⊗ₜ[R] m) = r • m :=
 tensor_product.lid_tmul m r
 
 @[simp]
-lemma right_unitor_hom {M : Module R} (m : M) (r : R) :
+lemma right_unitor_hom_apply {M : Module R} (m : M) (r : R) :
   ((ρ_ M).hom : M ⊗ 𝟙_ (Module R) ⟶ M) (m ⊗ₜ r) = r • m :=
 tensor_product.rid_tmul m r
 
 @[simp]
-lemma associator_hom {M N K : Module R} (m : M) (n : N) (k : K) :
+lemma associator_hom_apply {M N K : Module R} (m : M) (n : N) (k : K) :
   ((α_ M N K).hom : (M ⊗ N) ⊗ K ⟶ M ⊗ (N ⊗ K)) ((m ⊗ₜ n) ⊗ₜ k) = (m ⊗ₜ (n ⊗ₜ k)) := rfl
 
 end monoidal_category

src/algebra/module/basic.lean

@@ -295,6 +295,10 @@ lemma coe_fn_congr : Π {x x' : M}, x = x' → f x = f x'
 theorem ext_iff : f = g ↔ ∀ x, f x = g x :=
 ⟨by { rintro rfl x, refl } , ext⟩
 
+/-- If two linear maps are equal, they are equal at each point. -/
+lemma lcongr_fun (h : f = g) (m : M) : f m = g m :=
+congr_fun (congr_arg linear_map.to_fun h) m
+
 variables (f g)
 
 @[simp] lemma map_add (x y : M) : f (x + y) = f x + f y := f.map_add' x y

src/category_theory/monoidal/internal/Module.lean

@@ -0,0 +1,176 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import algebra.category.Module.monoidal
+import algebra.category.Algebra.basic
+import category_theory.monoidal.internal
+
+
+/-!
+# `Mon_ (Module R) ≌ Algebra R`
+
+The category of internal monoid objects in `Module R`
+is equivalent to the category of "native" bundled `R`-algebras.
+
+Moreover, this equivalence is compatible with the forgetful functors to `Module R`.
+-/
+
+universes v u
+
+open category_theory
+open linear_map
+
+open_locale tensor_product
+
+namespace Module
+
+variables {R : Type u} [comm_ring R]
+
+namespace Mon_Module_equivalence_Algebra
+
+@[simps]
+instance (A : Mon_ (Module R)) : ring A.X :=
+{ one := A.one (1 : R),
+  mul := λ x y, A.mul (x ⊗ₜ y),
+  one_mul := λ x, by { convert lcongr_fun A.one_mul ((1 : R) ⊗ₜ x), simp, },
+  mul_one := λ x, by { convert lcongr_fun A.mul_one (x ⊗ₜ (1 : R)), simp, },
+  mul_assoc := λ x y z, by convert lcongr_fun A.mul_assoc ((x ⊗ₜ y) ⊗ₜ z),
+  left_distrib := λ x y z,
+  begin
+    convert A.mul.map_add (x ⊗ₜ y) (x ⊗ₜ z),
+    rw ←tensor_product.tmul_add,
+    refl,
+  end,
+  right_distrib := λ x y z,
+  begin
+    convert A.mul.map_add (x ⊗ₜ z) (y ⊗ₜ z),
+    rw ←tensor_product.add_tmul,
+    refl,
+  end,
+  ..(by apply_instance : add_comm_group A.X) }
+
+instance (A : Mon_ (Module R)) : algebra R A.X :=
+{ map_zero' := A.one.map_zero,
+  map_one' := rfl,
+  map_mul' := λ x y,
+  begin
+    have h := lcongr_fun A.one_mul.symm (x ⊗ₜ (A.one y)),
+    rwa [monoidal_category.left_unitor_hom_apply, ←A.one.map_smul] at h,
+  end,
+  commutes' := λ r a,
+  begin dsimp,
+    have h₁ := lcongr_fun A.one_mul (r ⊗ₜ a),
+    have h₂ := lcongr_fun A.mul_one (a ⊗ₜ r),
+    exact h₁.trans h₂.symm,
+  end,
+  smul_def' := λ r a, by { convert (lcongr_fun A.one_mul (r ⊗ₜ a)).symm, simp, },
+  ..A.one }
+
+@[simp] lemma algebra_map (A : Mon_ (Module R)) (r : R) : algebra_map R A.X r = A.one r := rfl
+
+/--
+Converting a monoid object in `Module R` to a bundled algebra.
+-/
+@[simps]
+def functor : Mon_ (Module R) ⥤ Algebra R :=
+{ obj := λ A, Algebra.of R A.X,
+  map := λ A B f,
+  { to_fun := f.hom,
+    map_one' := lcongr_fun f.one_hom (1 : R),
+    map_mul' := λ x y, lcongr_fun f.mul_hom (x ⊗ₜ y),
+    commutes' := λ r, lcongr_fun f.one_hom r,
+    ..(f.hom.to_add_monoid_hom) }, }.
+
+/--
+Converting a bundled algebra to a monoid object in `Module R`.
+-/
+@[simps]
+def inverse_obj (A : Algebra.{u} R) : Mon_ (Module.{u} R) :=
+{ X := Module.of R A,
+  one := algebra.linear_map R A,
+  mul := algebra.lmul' R A,
+  one_mul' :=
+  begin
+    ext x,
+    dsimp,
+    rw [algebra.lmul'_apply, monoidal_category.left_unitor_hom_apply, algebra.smul_def],
+    refl,
+  end,
+  mul_one' :=
+  begin
+    ext x,
+    dsimp,
+    rw [algebra.lmul'_apply, monoidal_category.right_unitor_hom_apply,
+      ←algebra.commutes, algebra.smul_def],
+    refl,
+  end,
+  mul_assoc' :=
+  begin
+    ext xy z,
+    dsimp,
+    apply tensor_product.induction_on xy,
+    { simp only [linear_map.map_zero, tensor_product.zero_tmul], },
+    { intros x y, dsimp, simp [mul_assoc], },
+    { intros x y hx hy, dsimp, simp [tensor_product.add_tmul, hx, hy], },
+  end }
+
+/--
+Converting a bundled algebra to a monoid object in `Module R`.
+-/
+@[simps]
+def inverse : Algebra.{u} R ⥤ Mon_ (Module.{u} R) :=
+{ obj := inverse_obj,
+  map := λ A B f,
+  { hom := f.to_linear_map, }, }.
+
+end Mon_Module_equivalence_Algebra
+
+open Mon_Module_equivalence_Algebra
+
+/--
+The category of internal monoid objects in `Module R`
+is equivalent to the category of "native" bundled `R`-algebras.
+-/
+def Mon_Module_equivalence_Algebra : Mon_ (Module R) ≌ Algebra R :=
+{ functor := functor,
+  inverse := inverse,
+  unit_iso := nat_iso.of_components
+    (λ A,
+    { hom := { hom := { to_fun := id, map_add' := λ x y, rfl, map_smul' := λ r a, rfl, } },
+      inv := { hom := { to_fun := id, map_add' := λ x y, rfl, map_smul' := λ r a, rfl, } } })
+    (by tidy),
+  counit_iso := nat_iso.of_components (λ A,
+  { hom :=
+    { to_fun := id,
+      map_zero' := rfl,
+      map_add' := λ x y, rfl,
+      map_one' := (algebra_map R A).map_one,
+      map_mul' := λ x y, algebra.lmul'_apply,
+      commutes' := λ r, rfl, },
+    inv :=
+    { to_fun := id,
+      map_zero' := rfl,
+      map_add' := λ x y, rfl,
+      map_one' := (algebra_map R A).map_one.symm,
+      map_mul' := λ x y, algebra.lmul'_apply.symm,
+      commutes' := λ r, rfl } }) (by tidy), }.
+
+/--
+The equivalence `Mon_ (Module R) ≌ Algebra R`
+is naturally compatible with the forgetful functors to `Module R`.
+-/
+def Mon_Module_equivalence_Algebra_forget :
+  Mon_Module_equivalence_Algebra.functor ⋙ forget₂ (Algebra R) (Module R) ≅ Mon_.forget :=
+nat_iso.of_components (λ A,
+{ hom :=
+  { to_fun := id,
+    map_add' := λ x y, rfl,
+    map_smul' := λ c x, rfl },
+  inv :=
+  { to_fun := id,
+    map_add' := λ x y, rfl,
+    map_smul' := λ c x, rfl }, }) (by tidy)
+
+end Module

src/category_theory/monoidal/types.lean

@@ -7,6 +7,10 @@ import category_theory.monoidal.of_has_finite_products
 import category_theory.limits.shapes.finite_products
 import category_theory.limits.shapes.types
 
+/-!
+# The category of types is a symmetric monoidal category
+-/
+
 open category_theory
 open category_theory.limits
 open tactic

src/ring_theory/algebra.lean

@@ -151,9 +151,22 @@ by rw [smul_def, smul_def, left_comm]
   (r • x) * y = r • (x * y) :=
 by rw [smul_def, smul_def, mul_assoc]
 
-variables (R)
+variables (R A)
+
+/--
+The canonical ring homomorphism `algebra_map R A : R →* A` for any `R`-algebra `A`,
+packaged as an `R`-linear map.
+-/
+protected def linear_map : R →ₗ[R] A :=
+{ map_smul' := λ x y, begin dsimp, simp [algebra.smul_def], end,
+  ..algebra_map R A }
+
+@[simp]
+lemma linear_map_apply (r : R) : algebra.linear_map R A r = algebra_map R A r := rfl
+
 instance id : algebra R R := (ring_hom.id R).to_algebra
-variables {R}
+
+variables {R A}
 
 namespace id
 
@@ -208,6 +221,10 @@ def lmul_right (r : A) : A →ₗ A :=
 def lmul_left_right (vw: A × A) : A →ₗ[R] A :=
 (lmul_right R A vw.2).comp (lmul_left R A vw.1)
 
+/-- The multiplication map on an algebra, as an `R`-linear map from `A ⊗[R] A` to `A`. -/
+def lmul' : A ⊗[R] A →ₗ[R] A :=
+tensor_product.lift (algebra.lmul R A)
+
 variables {R A}
 
 @[simp] lemma lmul_apply (p q : A) : lmul R A p q = p * q := rfl
@@ -216,6 +233,12 @@ variables {R A}
 @[simp] lemma lmul_left_right_apply (vw : A × A) (p : A) :
   lmul_left_right R A vw p = vw.1 * p * vw.2 := rfl
 
+@[simp] lemma lmul'_apply {x y} : algebra.lmul' R A (x ⊗ₜ y) = x * y :=
+begin
+  dsimp [algebra.lmul'],
+  simp,
+end
+
 end semiring
 
 end algebra
@@ -1122,6 +1145,7 @@ variable {I : Type u}     -- The indexing type
 variable {f : I → Type v} -- The family of types already equipped with instances
 variables (x y : Π i, f i) (i : I)
 variables (I f)
+
 instance algebra (α) {r : comm_semiring α}
   [s : ∀ i, semiring (f i)] [∀ i, algebra α (f i)] :
   algebra α (Π i : I, f i) :=