feat(category_theory): monoidal natural transformations and discrete …

…monoidal categories (#4112)




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

src/algebra/group/hom.lean

@@ -81,6 +81,14 @@ lemma to_fun_eq_coe (f : M →* N) : f.to_fun = f := rfl
 @[simp, to_additive]
 lemma coe_mk (f : M → N) (h1 hmul) : ⇑(monoid_hom.mk f h1 hmul) = f := rfl
 
+@[to_additive]
+theorem congr_fun {f g : M →* N} (h : f = g) (x : M) : f x = g x :=
+congr_arg (λ h : M →* N, h x) h
+
+@[to_additive]
+theorem congr_arg (f : M →* N) {x y : M} (h : x = y) : f x = f y :=
+congr_arg (λ x : M, f x) h
+
 @[to_additive]
 lemma coe_inj ⦃f g : M →* N⦄ (h : (f : M → N) = g) : f = g :=
 by cases f; cases g; cases h; refl

src/algebra/group_with_zero.lean

@@ -958,7 +958,8 @@ begin
   rw [← f.map_mul, inv_mul_cancel h, f.map_one]
 end
 
-lemma map_div : f (a / b) = f a / f b := (f.map_mul _ _).trans $ congr_arg _ $ f.map_inv' h0 b
+lemma map_div : f (a / b) = f a / f b :=
+(f.map_mul _ _).trans $ _root_.congr_arg _ $ f.map_inv' h0 b
 
 omit h0
 

src/algebra/ring/basic.lean

@@ -227,6 +227,12 @@ lemma to_fun_eq_coe (f : α →+* β) : f.to_fun = f := rfl
 
 variables (f : α →+* β) {x y : α} {rα rβ}
 
+theorem congr_fun {f g : α →+* β} (h : f = g) (x : α) : f x = g x :=
+congr_arg (λ h : α →+* β, h x) h
+
+theorem congr_arg (f : α →+* β) {x y : α} (h : x = y) : f x = f y :=
+congr_arg (λ x : α, f x) h
+
 theorem coe_inj ⦃f g : α →+* β⦄ (h : (f : α → β) = g) : f = g :=
 by cases f; cases g; cases h; refl
 
@@ -237,10 +243,10 @@ theorem ext_iff {f g : α →+* β} : f = g ↔ ∀ x, f x = g x :=
 ⟨λ h x, h ▸ rfl, λ h, ext h⟩
 
 theorem coe_add_monoid_hom_injective : function.injective (coe : (α →+* β) → (α →+ β)) :=
-λ f g h, coe_inj $ show ((f : α →+ β) : α → β) = (g : α →+ β), from congr_arg coe_fn h
+λ f g h, ext (λ x, add_monoid_hom.congr_fun h x)
 
 theorem coe_monoid_hom_injective : function.injective (coe : (α →+* β) → (α →* β)) :=
-λ f g h, coe_inj $ show ((f : α →* β) : α → β) = (g : α →* β), from congr_arg coe_fn h
+λ f g h, ext (λ x, monoid_hom.congr_fun h x)
 
 /-- Ring homomorphisms map zero to zero. -/
 @[simp] lemma map_zero (f : α →+* β) : f 0 = 0 := f.map_zero'

src/category_theory/discrete_category.lean

@@ -38,10 +38,16 @@ by { dsimp [discrete], apply_instance }
 instance [subsingleton α] : subsingleton (discrete α) :=
 by { dsimp [discrete], apply_instance }
 
+/-- Extract the equation from a morphism in a discrete category. -/
+lemma eq_of_hom {X Y : discrete α} (i : X ⟶ Y) : X = Y := i.down.down
+
 @[simp] lemma id_def (X : discrete α) : ulift.up (plift.up (eq.refl X)) = 𝟙 X := rfl
 
 variables {C : Type u₂} [category.{v₂} C]
 
+instance {I : Type u₁} {i j : discrete I} (f : i ⟶ j) : is_iso f :=
+{ inv := eq_to_hom (eq_of_hom f).symm, }
+
 /--
 Any function `I → C` gives a functor `discrete I ⥤ C`.
 -/
@@ -117,8 +123,8 @@ def equivalence {I J : Type u₁} (e : I ≃ J) : discrete I ≌ discrete J :=
 def equiv_of_equivalence {α β : Type u₁} (h : discrete α ≌ discrete β) : α ≃ β :=
 { to_fun := h.functor.obj,
   inv_fun := h.inverse.obj,
-  left_inv := λ a, (h.unit_iso.app a).2.1.1,
-  right_inv := λ a, (h.counit_iso.app a).1.1.1 }
+  left_inv := λ a, eq_of_hom (h.unit_iso.app a).2,
+  right_inv := λ a, eq_of_hom (h.counit_iso.app a).1 }
 
 end discrete
 

src/category_theory/limits/lattice.lean

@@ -21,8 +21,8 @@ instance has_finite_limits_of_semilattice_inf_top [semilattice_inf_top α] :
   { has_limit := λ F, has_limit.mk
     { cone :=
       { X := finset.univ.inf F.obj,
-        π := { app := λ j, ⟨⟨finset.inf_le (fintype.complete _)⟩⟩ } },
-      is_limit := { lift := λ s, ⟨⟨finset.le_inf (λ j _, (s.π.app j).down.down)⟩⟩ } } }
+        π := { app := λ j, hom_of_le (finset.inf_le (fintype.complete _)) } },
+      is_limit := { lift := λ s, hom_of_le (finset.le_inf (λ j _, (s.π.app j).down.down)) } } }
 
 @[priority 100] -- see Note [lower instance priority]
 instance has_finite_colimits_of_semilattice_sup_bot [semilattice_sup_bot α] :
@@ -31,8 +31,8 @@ instance has_finite_colimits_of_semilattice_sup_bot [semilattice_sup_bot α] :
   { has_colimit := λ F, has_colimit.mk
     { cocone :=
       { X := finset.univ.sup F.obj,
-        ι := { app := λ i, ⟨⟨finset.le_sup (fintype.complete _)⟩⟩ } },
-      is_colimit := { desc := λ s, ⟨⟨finset.sup_le (λ j _, (s.ι.app j).down.down)⟩⟩ } } }
+        ι := { app := λ i, hom_of_le (finset.le_sup (fintype.complete _)) } },
+      is_colimit := { desc := λ s, hom_of_le (finset.sup_le (λ j _, (s.ι.app j).down.down)) } } }
 
 -- It would be nice to only use the `Inf` half of the complete lattice, but
 -- this seems not to have been described separately.
@@ -43,10 +43,10 @@ instance has_limits_of_complete_lattice [complete_lattice α] : has_limits α :=
     { cone :=
       { X := Inf (set.range F.obj),
         π :=
-        { app := λ j, ⟨⟨complete_lattice.Inf_le _ _ (set.mem_range_self _)⟩⟩ } },
+        { app := λ j, hom_of_le (complete_lattice.Inf_le _ _ (set.mem_range_self _)) } },
       is_limit :=
-      { lift := λ s, ⟨⟨complete_lattice.le_Inf _ _
-        begin rintros _ ⟨j, rfl⟩, exact le_of_hom (s.π.app j), end⟩⟩ } } } }
+      { lift := λ s, hom_of_le (complete_lattice.le_Inf _ _
+        begin rintros _ ⟨j, rfl⟩, exact le_of_hom (s.π.app j), end) } } } }
 
 @[priority 100] -- see Note [lower instance priority]
 instance has_colimits_of_complete_lattice [complete_lattice α] : has_colimits α :=
@@ -55,9 +55,9 @@ instance has_colimits_of_complete_lattice [complete_lattice α] : has_colimits 
     { cocone :=
       { X := Sup (set.range F.obj),
         ι :=
-        { app := λ j, ⟨⟨complete_lattice.le_Sup _ _ (set.mem_range_self _)⟩⟩ } },
+        { app := λ j, hom_of_le (complete_lattice.le_Sup _ _ (set.mem_range_self _)) } },
       is_colimit :=
-      { desc := λ s, ⟨⟨complete_lattice.Sup_le _ _
-        begin rintros _ ⟨j, rfl⟩, exact le_of_hom (s.ι.app j), end⟩⟩ } } } }
+      { desc := λ s, hom_of_le (complete_lattice.Sup_le _ _
+        begin rintros _ ⟨j, rfl⟩, exact le_of_hom (s.ι.app j), end) } } } }
 
 end category_theory.limits

src/category_theory/monoidal/discrete.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import category_theory.monoidal.natural_transformation
+import category_theory.discrete_category
+import algebra.group.hom
+
+/-!
+# Monoids as discrete monoidal categories
+
+The discrete category on a monoid is a monoidal category.
+Multiplicative morphisms induced monoidal functors.
+-/
+
+universes u
+
+open category_theory
+open category_theory.discrete
+
+variables (M : Type u) [monoid M]
+
+namespace category_theory
+
+instance monoid_discrete : monoid (discrete M) := by { dsimp [discrete], apply_instance }
+
+instance : monoidal_category (discrete M) :=
+{ tensor_unit := 1,
+  tensor_obj := λ X Y, X * Y,
+  tensor_hom := λ W X Y Z f g, eq_to_hom (by rw [eq_of_hom f, eq_of_hom g]),
+  left_unitor := λ X, eq_to_iso (one_mul X),
+  right_unitor := λ X, eq_to_iso (mul_one X),
+  associator := λ X Y Z, eq_to_iso (mul_assoc _ _ _), }
+
+variables {M} {N : Type u} [monoid N]
+
+/--
+A multiplicative morphism between monoids gives a monoidal functor between the corresponding
+discrete monoidal categories.
+-/
+def discrete.monoidal_functor (F : M →* N) : monoidal_functor (discrete M) (discrete N) :=
+{ obj := F,
+  map := λ X Y f, eq_to_hom (F.congr_arg (eq_of_hom f)),
+  ε := eq_to_hom F.map_one.symm,
+  μ := λ X Y, eq_to_hom (F.map_mul X Y).symm, }
+
+variables {K : Type u} [monoid K]
+
+/--
+The monoidal natural isomorphism corresponding to composing two multiplicative morphisms.
+-/
+def discrete.monoidal_functor_comp (F : M →* N) (G : N →* K) :
+  discrete.monoidal_functor F ⊗⋙ discrete.monoidal_functor G ≅
+  discrete.monoidal_functor (G.comp F) :=
+{ hom := { app := λ X, 𝟙 _, },
+  inv := { app := λ X, 𝟙 _, }, }
+
+end category_theory

src/category_theory/monoidal/functor.lean

@@ -68,8 +68,8 @@ See https://stacks.math.columbia.edu/tag/0FFL.
 -/
 structure monoidal_functor
 extends lax_monoidal_functor.{v₁ v₂} C D :=
-(ε_is_iso            : is_iso ε . obviously)
-(μ_is_iso            : Π X Y : C, is_iso (μ X Y) . obviously)
+(ε_is_iso            : is_iso ε . tactic.apply_instance)
+(μ_is_iso            : Π X Y : C, is_iso (μ X Y) . tactic.apply_instance)
 
 attribute [instance] monoidal_functor.ε_is_iso monoidal_functor.μ_is_iso
 
@@ -181,6 +181,8 @@ variables (F : lax_monoidal_functor.{v₁ v₂} C D) (G : lax_monoidal_functor.{
   end,
   .. (F.to_functor) ⋙ (G.to_functor) }.
 
+infixr ` ⊗⋙ `:80 := comp
+
 end lax_monoidal_functor
 
 namespace monoidal_functor
@@ -194,6 +196,8 @@ def comp : monoidal_functor.{v₁ v₃} C E :=
   μ_is_iso := by { dsimp, apply_instance },
   .. (F.to_lax_monoidal_functor).comp (G.to_lax_monoidal_functor) }.
 
+infixr ` ⊗⋙ `:80 := comp -- We overload notation; potentially dangerous, but it seems to work.
+
 end monoidal_functor
 
 end category_theory

src/category_theory/monoidal/internal.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import category_theory.monoidal.functor
+import category_theory.monoidal.natural_transformation
 import category_theory.monoidal.unitors
 import category_theory.limits.shapes.terminal
 
@@ -150,7 +150,6 @@ A lax monoidal functor takes monoid objects to monoid objects.
 
 That is, a lax monoidal functor `F : C ⥤ D` induces a functor `Mon_ C ⥤ Mon_ D`.
 -/
--- TODO: This is functorial in `F`. (In fact, `Mon_` is a 2-functor.)
 -- TODO: map_Mod F A : Mod A ⥤ Mod (F.map_Mon A)
 @[simps]
 def map_Mon (F : lax_monoidal_functor C D) : Mon_ C ⥤ Mon_ D :=
@@ -199,6 +198,13 @@ def map_Mon (F : lax_monoidal_functor C D) : Mon_ C ⥤ Mon_ D :=
   map_id' := λ A, by { ext, simp, },
   map_comp' := λ A B C f g, by { ext, simp, }, }
 
+/-- `map_Mon` is functorial in the lax monoidal functor. -/
+def map_Mon_functor : (lax_monoidal_functor C D) ⥤ (Mon_ C ⥤ Mon_ D) :=
+{ obj := map_Mon,
+  map := λ F G α,
+  { app := λ A,
+    { hom := α.app A.X, } } }
+
 end category_theory.lax_monoidal_functor
 
 variables {C}

src/category_theory/monoidal/natural_transformation.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import category_theory.monoidal.functor
+import category_theory.full_subcategory
+
+/-!
+# Monoidal natural transformations
+
+Natural transformations between (lax) monoidal functors must satisfy
+an additional compatibility relation with the tensorators:
+`F.μ X Y ≫ app (X ⊗ Y) = (app X ⊗ app Y) ≫ G.μ X Y`.
+
+(Lax) monoidal functors between a fixed pair of monoidal categories
+themselves form a category.
+-/
+
+open category_theory
+
+universes v₁ v₂ v₃ u₁ u₂ u₃
+
+open category_theory.category
+open category_theory.functor
+
+namespace category_theory
+
+open monoidal_category
+
+variables {C : Type u₁} [category.{v₁} C] [monoidal_category.{v₁} C]
+          {D : Type u₂} [category.{v₂} D] [monoidal_category.{v₂} D]
+
+/--
+A monoidal natural transformation is a natural transformation between (lax) monoidal functors
+additionally satisfying:
+`F.μ X Y ≫ app (X ⊗ Y) = (app X ⊗ app Y) ≫ G.μ X Y`
+-/
+@[ext]
+structure monoidal_nat_trans (F G : lax_monoidal_functor C D)
+  extends nat_trans F.to_functor G.to_functor :=
+(unit' : F.ε ≫ app (𝟙_ C) = G.ε . obviously)
+(tensor' : ∀ X Y, F.μ _ _ ≫ app (X ⊗ Y) = (app X ⊗ app Y) ≫ G.μ _ _ . obviously)
+
+restate_axiom monoidal_nat_trans.tensor'
+attribute [simp, reassoc] monoidal_nat_trans.tensor
+restate_axiom monoidal_nat_trans.unit'
+attribute [simp, reassoc] monoidal_nat_trans.unit
+
+namespace monoidal_nat_trans
+
+/--
+The identity monoidal natural transformation.
+-/
+@[simps]
+def id (F : lax_monoidal_functor C D) : monoidal_nat_trans F F :=
+{ ..(𝟙 F.to_functor) }
+
+instance (F : lax_monoidal_functor C D) : inhabited (monoidal_nat_trans F F) := ⟨id F⟩
+
+/--
+Vertical composition of monoidal natural transformations.
+-/
+@[simps]
+def vcomp {F G H : lax_monoidal_functor C D}
+  (α : monoidal_nat_trans F G) (β : monoidal_nat_trans G H) : monoidal_nat_trans F H :=
+{ ..(nat_trans.vcomp α.to_nat_trans β.to_nat_trans) }
+
+instance category_lax_monoidal_functor : category (lax_monoidal_functor C D) :=
+{ hom := monoidal_nat_trans,
+  id := id,
+  comp := λ F G H α β, vcomp α β, }
+
+instance category_monoidal_functor : category (monoidal_functor C D) :=
+induced_category.category monoidal_functor.to_lax_monoidal_functor
+
+variables {E : Type u₃} [category.{v₃} E] [monoidal_category.{v₃} E]
+
+/--
+Horizontal composition of monoidal natural transformations.
+-/
+@[simps]
+def hcomp {F G : lax_monoidal_functor C D} {H K : lax_monoidal_functor D E}
+  (α : monoidal_nat_trans F G) (β : monoidal_nat_trans H K) :
+  monoidal_nat_trans (F ⊗⋙ H) (G ⊗⋙ K) :=
+{ unit' :=
+  begin
+    dsimp, simp,
+    conv_lhs { rw [←K.to_functor.map_comp, α.unit], },
+  end,
+  tensor' := λ X Y,
+  begin
+    dsimp, simp,
+    conv_lhs { rw [←K.to_functor.map_comp, α.tensor, K.to_functor.map_comp], },
+  end,
+  ..(nat_trans.hcomp α.to_nat_trans β.to_nat_trans) }
+
+end monoidal_nat_trans
+
+end category_theory

src/topology/instances/real_vector_space.lean

@@ -22,7 +22,7 @@ namespace add_monoid_hom
 /-- A continuous additive map between two vector spaces over `ℝ` is `ℝ`-linear. -/
 lemma map_real_smul (f : E →+ F) (hf : continuous f) (c : ℝ) (x : E) :
   f (c • x) = c • f x :=
-suffices (λ c : ℝ, f (c • x)) = λ c : ℝ, c • f x, from congr_fun this c,
+suffices (λ c : ℝ, f (c • x)) = λ c : ℝ, c • f x, from _root_.congr_fun this c,
 dense_embedding_of_rat.dense.equalizer
   (hf.comp $ continuous_id.smul continuous_const)
   (continuous_id.smul continuous_const)