chore(category_theory/monoidal): monoidal_category doesn't extend cat…

…egory (#1338)

* chore(category_theory/monoidal): monoidal_category doesn't extend category

* remove _aux file, simplifying

* make notations global, and add doc-strings

src/category_theory/monoidal/category.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Michael Jendrusch. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Jendrusch, Scott Morrison
 -/
-import category_theory.monoidal.category_aux
+import category_theory.products
 import category_theory.natural_isomorphism
 import tactic.basic
 import tactic.slice
@@ -18,13 +18,20 @@ open category_theory.iso
 
 namespace category_theory
 
-class monoidal_category (C : Type u) extends category.{v} C :=
+/--
+In a monoidal category, we can take the tensor product of objects, `X ⊗ Y` and of morphisms `f ⊗ g`.
+Tensor product does not need to be strictly associative on objects, but there is a
+specified associator, `α_ X Y Z : (X ⊗ Y) ⊗ Z ≅ X ⊗ (Y ⊗ Z)`. There is a tensor unit `𝟙_ C`,
+with specified left and right unitor isomorphisms `λ_ X : 𝟙_ C ⊗ X ≅ X` and `ρ_ X : X ⊗ 𝟙_ C ≅ X`.
+These associators and unitors satisfy the pentagon and triangle equations.
+-/
+class monoidal_category (C : Type u) [𝒞 : category.{v} C] :=
 -- curried tensor product of objects:
 (tensor_obj               : C → C → C)
 (infixr ` ⊗ `:70          := tensor_obj) -- This notation is only temporary
 -- curried tensor product of morphisms:
 (tensor_hom               :
-  Π {X₁ Y₁ X₂ Y₂ : C}, hom X₁ Y₁ → hom X₂ Y₂ → hom (X₁ ⊗ X₂) (Y₁ ⊗ Y₂))
+  Π {X₁ Y₁ X₂ Y₂ : C}, (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → ((X₁ ⊗ X₂) ⟶ (Y₁ ⊗ Y₂)))
 (infixr ` ⊗' `:69         := tensor_hom) -- This notation is only temporary
 -- tensor product laws:
 (tensor_id'               :
@@ -34,24 +41,31 @@ class monoidal_category (C : Type u) extends category.{v} C :=
   (f₁ ≫ g₁) ⊗' (f₂ ≫ g₂) = (f₁ ⊗' f₂) ≫ (g₁ ⊗' g₂) . obviously)
 -- tensor unit:
 (tensor_unit              : C)
+(notation `𝟙_`            := tensor_unit)
 -- associator:
 (associator               :
   Π X Y Z : C, (X ⊗ Y) ⊗ Z ≅ X ⊗ (Y ⊗ Z))
+(notation `α_`            := associator)
 (associator_naturality'   :
-  assoc_natural tensor_obj @tensor_hom associator . obviously)
+  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
+  ((f₁ ⊗' f₂) ⊗' f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗' (f₂ ⊗' f₃)) . obviously)
 -- left unitor:
-(left_unitor              : Π X : C, tensor_unit ⊗ X ≅ X)
+(left_unitor              : Π X : C, 𝟙_ ⊗ X ≅ X)
+(notation `λ_`            := left_unitor)
 (left_unitor_naturality'  :
-  left_unitor_natural tensor_obj @tensor_hom tensor_unit left_unitor . obviously)
+  ∀ {X Y : C} (f : X ⟶ Y), ((𝟙 𝟙_) ⊗' f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f . obviously)
 -- right unitor:
-(right_unitor             : Π X : C, X ⊗ tensor_unit ≅ X)
+(right_unitor             : Π X : C, X ⊗ 𝟙_ ≅ X)
+(notation `ρ_`            := right_unitor)
 (right_unitor_naturality' :
-  right_unitor_natural tensor_obj @tensor_hom tensor_unit right_unitor . obviously)
+  ∀ {X Y : C} (f : X ⟶ Y), (f ⊗' (𝟙 𝟙_)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f . obviously)
 -- pentagon identity:
-(pentagon'                : pentagon @tensor_hom associator . obviously)
+(pentagon'                : ∀ W X Y Z : C,
+  ((α_ W X Y).hom ⊗' (𝟙 Z)) ≫ (α_ W (X ⊗ Y) Z).hom ≫ ((𝟙 W) ⊗' (α_ X Y Z).hom)
+  = (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom . obviously)
 -- triangle identity:
 (triangle'                :
-  triangle @tensor_hom left_unitor right_unitor associator . obviously)
+  ∀ X Y : C, (α_ X 𝟙_ Y).hom ≫ ((𝟙 X) ⊗' (λ_ Y).hom) = (ρ_ X).hom ⊗' (𝟙 Y) . obviously)
 
 restate_axiom monoidal_category.tensor_id'
 attribute [simp] monoidal_category.tensor_id
@@ -69,12 +83,13 @@ open monoidal_category
 infixr ` ⊗ `:70 := tensor_obj
 infixr ` ⊗ `:70 := tensor_hom
 
-local notation `𝟙_` := tensor_unit
-local notation `α_` := associator
-local notation `λ_` := left_unitor
-local notation `ρ_` := right_unitor
+notation `𝟙_` := tensor_unit
+notation `α_` := associator
+notation `λ_` := left_unitor
+notation `ρ_` := right_unitor
 
-def tensor_iso {C : Type u} {X Y X' Y' : C} [monoidal_category.{v} C] (f : X ≅ Y) (g : X' ≅ Y') :
+/-- The tensor product of two isomorphisms is an isomorphism. -/
+def tensor_iso {C : Type u} {X Y X' Y' : C} [category.{v} C] [monoidal_category.{v} C] (f : X ≅ Y) (g : X' ≅ Y') :
     X ⊗ X' ≅ Y ⊗ Y' :=
 { hom := f.hom ⊗ g.hom,
   inv := f.inv ⊗ g.inv,
@@ -87,7 +102,7 @@ namespace monoidal_category
 
 section
 
-variables {C : Type u} [𝒞 : monoidal_category.{v} C]
+variables {C : Type u} [category.{v} C] [𝒞 : monoidal_category.{v} C]
 include 𝒞
 
 instance tensor_is_iso {W X Y Z : C} (f : W ⟶ X) [is_iso f] (g : Y ⟶ Z) [is_iso g] : is_iso (f ⊗ g) :=
@@ -329,13 +344,15 @@ section
 -- In order to be able to describe the tensor product as a functor, we
 -- need to be up in at least `Type 0` for both objects and morphisms,
 -- so that we can construct products.
-variables (C : Type u) [𝒞 : monoidal_category.{v+1} C]
+variables (C : Type u) [category.{v+1} C] [𝒞 : monoidal_category.{v+1} C]
 include 𝒞
 
+/-- The tensor product expressed as a functor. -/
 def tensor : (C × C) ⥤ C :=
-{ obj := λ X, tensor_obj X.1 X.2,
-  map := λ {X Y : C × C} (f : X ⟶ Y), tensor_hom f.1 f.2 }
+{ obj := λ X, X.1 ⊗ X.2,
+  map := λ {X Y : C × C} (f : X ⟶ Y), f.1 ⊗ f.2 }
 
+/-- The left-associated triple tensor product as a functor. -/
 def left_assoc_tensor : (C × C × C) ⥤ C :=
 { obj := λ X, (X.1 ⊗ X.2.1) ⊗ X.2.2,
   map := λ {X Y : C × C × C} (f : X ⟶ Y), (f.1 ⊗ f.2.1) ⊗ f.2.2 }
@@ -345,6 +362,7 @@ def left_assoc_tensor : (C × C × C) ⥤ C :=
 @[simp] lemma left_assoc_tensor_map {X Y} (f : X ⟶ Y) :
   (left_assoc_tensor C).map f = (f.1 ⊗ f.2.1) ⊗ f.2.2 := rfl
 
+/-- The right-associated triple tensor product as a functor. -/
 def right_assoc_tensor : (C × C × C) ⥤ C :=
 { obj := λ X, X.1 ⊗ (X.2.1 ⊗ X.2.2),
   map := λ {X Y : C × C × C} (f : X ⟶ Y), f.1 ⊗ (f.2.1 ⊗ f.2.2) }
@@ -354,28 +372,33 @@ def right_assoc_tensor : (C × C × C) ⥤ C :=
 @[simp] lemma right_assoc_tensor_map {X Y} (f : X ⟶ Y) :
   (right_assoc_tensor C).map f = f.1 ⊗ (f.2.1 ⊗ f.2.2) := rfl
 
+/-- The functor `λ X, 𝟙_ C ⊗ X`. -/
 def tensor_unit_left : C ⥤ C :=
 { obj := λ X, 𝟙_ C ⊗ X,
   map := λ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ C)) ⊗ f }
+/-- The functor `λ X, X ⊗ 𝟙_ C`. -/
 def tensor_unit_right : C ⥤ C :=
 { obj := λ X, X ⊗ 𝟙_ C,
   map := λ {X Y : C} (f : X ⟶ Y), f ⊗ (𝟙 (𝟙_ C)) }
 
 -- We can express the associator and the unitors, given componentwise above,
 -- as natural isomorphisms.
 
+/-- The associator as a natural isomorphism. -/
 def associator_nat_iso :
   left_assoc_tensor C ≅ right_assoc_tensor C :=
 nat_iso.of_components
   (by { intros, apply monoidal_category.associator })
   (by { intros, apply monoidal_category.associator_naturality })
 
+/-- The left unitor as a natural isomorphism. -/
 def left_unitor_nat_iso :
   tensor_unit_left C ≅ functor.id C :=
 nat_iso.of_components
   (by { intros, apply monoidal_category.left_unitor })
   (by { intros, apply monoidal_category.left_unitor_naturality })
 
+/-- The right unitor as a natural isomorphism. -/
 def right_unitor_nat_iso :
   tensor_unit_right C ≅ functor.id C :=
 nat_iso.of_components

src/category_theory/monoidal/functor.lean

@@ -18,13 +18,16 @@ section
 
 open monoidal_category
 
-variables (C : Type u₁) [𝒞 : monoidal_category.{v₁} C]
-          (D : Type u₂) [𝒟 : monoidal_category.{v₂} D]
+variables (C : Type u₁) [category.{v₁} C] [𝒞 : monoidal_category.{v₁} C]
+          (D : Type u₂) [category.{v₂} D] [𝒟 : monoidal_category.{v₂} D]
 include 𝒞 𝒟
 
+/-- A lax monoidal functor is a functor `F : C ⥤ D` between monoidal categories, equipped with morphisms
+    `ε : 𝟙 _D ⟶ F.obj (𝟙_ C)` and `μ X Y : F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)`, satisfying the
+    the appropriate coherences. -/
 structure lax_monoidal_functor extends C ⥤ D :=
 -- unit morphism
-(ε               : tensor_unit D ⟶ obj (tensor_unit C))
+(ε               : 𝟙_ D ⟶ obj (𝟙_ C))
 -- tensorator
 (μ                : Π X Y : C, (obj X) ⊗ (obj Y) ⟶ obj (X ⊗ Y))
 (μ_natural'       : ∀ {X Y X' Y' : C}
@@ -33,17 +36,17 @@ structure lax_monoidal_functor extends C ⥤ D :=
   . obviously)
 -- associativity of the tensorator
 (associativity'   : ∀ (X Y Z : C),
-    (μ X Y ⊗ 𝟙 (obj Z)) ≫ μ (X ⊗ Y) Z ≫ map (associator X Y Z).hom
-  = (associator (obj X) (obj Y) (obj Z)).hom ≫ (𝟙 (obj X) ⊗ μ Y Z) ≫ μ X (Y ⊗ Z)
+    (μ X Y ⊗ 𝟙 (obj Z)) ≫ μ (X ⊗ Y) Z ≫ map (α_ X Y Z).hom
+  = (α_ (obj X) (obj Y) (obj Z)).hom ≫ (𝟙 (obj X) ⊗ μ Y Z) ≫ μ X (Y ⊗ Z)
   . obviously)
 -- unitality
 (left_unitality'  : ∀ X : C,
-    (left_unitor (obj X)).hom
-  = (ε ⊗ 𝟙 (obj X)) ≫ μ (tensor_unit C) X ≫ map (left_unitor X).hom
+    (λ_ (obj X)).hom
+  = (ε ⊗ 𝟙 (obj X)) ≫ μ (𝟙_ C) X ≫ map (λ_ X).hom
   . obviously)
 (right_unitality' : ∀ X : C,
-    (right_unitor (obj X)).hom
-  = (𝟙 (obj X) ⊗ ε) ≫ μ X (tensor_unit C) ≫ map (right_unitor X).hom
+    (ρ_ (obj X)).hom
+  = (𝟙 (obj X) ⊗ ε) ≫ μ X (𝟙_ C) ≫ map (ρ_ X).hom
   . obviously)
 
 restate_axiom lax_monoidal_functor.μ_natural'
@@ -59,6 +62,7 @@ attribute [simp] lax_monoidal_functor.associativity
 -- lax_monoidal_functor.μ_natural lax_monoidal_functor.left_unitality
 -- lax_monoidal_functor.right_unitality lax_monoidal_functor.associativity
 
+/-- A monoidal functor is a lax monoidal functor for which the tensorator and unitor as isomorphisms. -/
 structure monoidal_functor
 extends lax_monoidal_functor.{v₁ v₂} C D :=
 (ε_is_iso            : is_iso ε . obviously)
@@ -84,10 +88,11 @@ namespace monoidal_functor
 section
 -- In order to express the tensorator as a natural isomorphism,
 -- we need to be in at least `Type 0`, so we have products.
-variables {C : Type u₁} [𝒞 : monoidal_category.{v₁+1} C]
-variables {D : Type u₂} [𝒟 : monoidal_category.{v₂+1} D]
+variables {C : Type u₁} [category.{v₁+1} C] [𝒞 : monoidal_category.{v₁+1} C]
+variables {D : Type u₂} [category.{v₂+1} D] [𝒟 : monoidal_category.{v₂+1} D]
 include 𝒞 𝒟
 
+/-- The tensorator as a natural isomorphism. -/
 def μ_nat_iso (F : monoidal_functor.{v₁+1 v₂+1} C D) :
   (functor.prod F.to_functor F.to_functor) ⋙ (tensor D) ≅ (tensor C) ⋙ F.to_functor :=
 nat_iso.of_components
@@ -96,9 +101,10 @@ nat_iso.of_components
 end
 
 section
-variables (C : Type u₁) [𝒞 : monoidal_category.{v₁} C]
+variables (C : Type u₁) [category.{v₁} C] [𝒞 : monoidal_category.{v₁} C]
 include 𝒞
 
+/-- The identity monoidal functor. -/
 def id : monoidal_functor.{v₁ v₁} C C :=
 { ε := 𝟙 _,
   μ := λ X Y, 𝟙 _,
@@ -113,16 +119,17 @@ end
 
 end monoidal_functor
 
-variables {C : Type u₁} [𝒞 : monoidal_category.{v₁} C]
-variables {D : Type u₂} [𝒟 : monoidal_category.{v₂} D]
-variables {E : Type u₃} [ℰ : monoidal_category.{v₃} E]
+variables {C : Type u₁} [category.{v₁} C] [𝒞 : monoidal_category.{v₁} C]
+variables {D : Type u₂} [category.{v₂} D] [𝒟 : monoidal_category.{v₂} D]
+variables {E : Type u₃} [category.{v₃} E] [ℰ : monoidal_category.{v₃} E]
 
 include 𝒞 𝒟 ℰ
 
 namespace lax_monoidal_functor
 variables (F : lax_monoidal_functor.{v₁ v₂} C D) (G : lax_monoidal_functor.{v₂ v₃} D E)
 
 -- The proofs here are horrendous; rewrite_search helps a lot.
+/-- The composition of two lax monoidal functors is again lax monoidal. -/
 def comp : lax_monoidal_functor.{v₁ v₃} C E :=
 { ε                := G.ε ≫ (G.map F.ε),
   μ                := λ X Y, G.μ (F.obj X) (F.obj Y) ≫ G.map (F.μ X Y),
@@ -174,9 +181,10 @@ namespace monoidal_functor
 
 variables (F : monoidal_functor.{v₁ v₂} C D) (G : monoidal_functor.{v₂ v₃} D E)
 
+/-- The composition of two monoidal functors is again monoidal. -/
 def comp : monoidal_functor.{v₁ v₃} C E :=
-{ ε_is_iso := by { dsimp, apply_instance }, -- TODO tidy would get this if we deferred ext
-  μ_is_iso := by { dsimp, apply_instance }, -- TODO as above
+{ ε_is_iso := by { dsimp, apply_instance },
+  μ_is_iso := by { dsimp, apply_instance },
   .. (F.to_lax_monoidal_functor).comp (G.to_lax_monoidal_functor) }.
 
 end monoidal_functor