From d3c565d48cea0d98b5a6c2b98e98eb55e9e14cc5 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Sat, 1 May 2021 18:03:22 +0000 Subject: [PATCH] feat(category_theory/monoidal): the monoidal coherence theorem (#7324) This PR contains a proof of the monoidal coherence theorem, stated in the following way: if `C` is any type, then the free monoidal category over `C` is a preorder. This should immediately imply the statement needed in the `coherence` branch. --- docs/references.bib | 59 ++-- src/category_theory/monoidal/category.lean | 6 +- src/category_theory/monoidal/free/basic.lean | 239 +++++++++++++++ .../monoidal/free/coherence.lean | 271 ++++++++++++++++++ 4 files changed, 555 insertions(+), 20 deletions(-) create mode 100644 src/category_theory/monoidal/free/basic.lean create mode 100644 src/category_theory/monoidal/free/coherence.lean diff --git a/docs/references.bib b/docs/references.bib index 500a23ebb60c0..69e9cddb9116e 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -85,16 +85,39 @@ @Book{ beals2004 title = {Analysis. An introduction}, publisher = {Cambridge University Press}, isbn = {0521600472}, - year = {2004}, + year = {2004} } -@article{ bernstein1912, +@Article{ bernstein1912, author = {Bernstein, S.}, year = {1912}, - title = {Démonstration du théorème de Weierstrass fondée sur le calcul des probabilités}, + title = {Démonstration du théorème de Weierstrass fondée sur le + calcul des probabilités}, journal = {Comm. Kharkov Math. Soc.}, volume = {13}, - number = {1–2}, + number = {1–2} +} + +@InProceedings{ beylin1996, + author = "Beylin, Ilya and Dybjer, Peter", + editor = "Berardi, Stefano and Coppo, Mario", + title = "Extracting a proof of coherence for monoidal categories + from a proof of normalization for monoids", + booktitle = "Types for Proofs and Programs", + year = "1996", + publisher = "Springer Berlin Heidelberg", + address = "Berlin, Heidelberg", + pages = "47--61", + abstract = "This paper studies the problem of coherence in category + theory from a type-theoretic viewpoint. We first show how a + Curry-Howard interpretation of a formal proof of + normalization for monoids almost directly yields a + coherence proof for monoidal categories. Then we formalize + this coherence proof in intensional intuitionistic type + theory and show how it relies on explicit reasoning about + proof objects for intensional equality. This formalization + has been checked in the proof assistant ALF.", + isbn = "978-3-540-70722-6" } @Book{ borceux-vol1, @@ -241,7 +264,8 @@ @Book{ conway2001 @Article{ dyckhoff_1992, author = {Dyckhoff, Roy}, - title = {Contraction-free sequent calculi for intuitionistic logic}, + title = {Contraction-free sequent calculi for intuitionistic + logic}, journal = {Journal of Symbolic Logic}, number = {3}, year = {1992}, @@ -321,7 +345,7 @@ @InProceedings{ fuerer-lochbihler-schneider-traytel2020 bibsource = {dblp computer science bibliography, https://dblp.org} } -@Inproceedings{ Gallier2011Notes, +@InProceedings{ Gallier2011Notes, title = {Notes on Differential Geometry and Lie Groups}, author = {J. Gallier and J. Quaintance}, year = {2011}, @@ -365,7 +389,7 @@ @Book{ Gratzer2011 pages = {xxx+614}, isbn = {978-3-0348-0018-1}, doi = {10.1007/978-3-0348-0018-1}, - mrnumber = {2768581}, + mrnumber = {2768581} } @Article{ Gusakov2021, @@ -809,6 +833,17 @@ @Book{ soare1987 doi = {10.1007/978-3-662-02460-7} } +@Article{ Stone1935, + author = {Stone, M. H.}, + year = {1935}, + title = {Postulates for Boolean Algebras and Generalized Boolean + Algebras}, + journal = {American Journal of Mathematics}, + volume = {57}, + issue = {4}, + doi = {10.2307/2371008} +} + @Article{ Stone1979, author = {Stone, A. H.}, journal = {General Topology Appl.}, @@ -825,16 +860,6 @@ @Article{ Stone1979 mrreviewer = {J. Segal} } -@Article{ Stone1935, - author = {Stone, M. H.}, - year = {1935}, - title = {Postulates for Boolean Algebras and Generalized Boolean Algebras}, - journal = {American Journal of Mathematics}, - volume = {57}, - issue = {4}, - doi = {10.2307/2371008} -} - @Book{ tao2010, author = {Tao, Terence}, title = {An Epsilon of Room, I: Real Analysis: Pages from Year diff --git a/src/category_theory/monoidal/category.lean b/src/category_theory/monoidal/category.lean index 2dff4b6c8fcdb..0380ffb3e39e8 100644 --- a/src/category_theory/monoidal/category.lean +++ b/src/category_theory/monoidal/category.lean @@ -291,11 +291,11 @@ lemma triangle_assoc_comp_left (X Y : C) : (α_ X (𝟙_ C) Y).hom ≫ ((𝟙 X) ⊗ (λ_ Y).hom) = (ρ_ X).hom ⊗ 𝟙 Y := monoidal_category.triangle X Y -@[simp] lemma triangle_assoc_comp_right (X Y : C) : +@[simp, reassoc] lemma triangle_assoc_comp_right (X Y : C) : (α_ X (𝟙_ C) Y).inv ≫ ((ρ_ X).hom ⊗ 𝟙 Y) = ((𝟙 X) ⊗ (λ_ Y).hom) := by rw [←triangle_assoc_comp_left, iso.inv_hom_id_assoc] -@[simp] lemma triangle_assoc_comp_right_inv (X Y : C) : +@[simp, reassoc] lemma triangle_assoc_comp_right_inv (X Y : C) : ((ρ_ X).inv ⊗ 𝟙 Y) ≫ (α_ X (𝟙_ C) Y).hom = ((𝟙 X) ⊗ (λ_ Y).inv) := begin apply (cancel_mono (𝟙 X ⊗ (λ_ Y).hom)).1, @@ -303,7 +303,7 @@ begin rw [←comp_tensor_id, iso.inv_hom_id, ←id_tensor_comp, iso.inv_hom_id] end -@[simp] lemma triangle_assoc_comp_left_inv (X Y : C) : +@[simp, reassoc] lemma triangle_assoc_comp_left_inv (X Y : C) : ((𝟙 X) ⊗ (λ_ Y).inv) ≫ (α_ X (𝟙_ C) Y).inv = ((ρ_ X).inv ⊗ 𝟙 Y) := begin apply (cancel_mono ((ρ_ X).hom ⊗ 𝟙 Y)).1, diff --git a/src/category_theory/monoidal/free/basic.lean b/src/category_theory/monoidal/free/basic.lean new file mode 100644 index 0000000000000..fa7c60e20c4cb --- /dev/null +++ b/src/category_theory/monoidal/free/basic.lean @@ -0,0 +1,239 @@ +/- +Copyright (c) 2021 Markus Himmel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import category_theory.monoidal.functor +import category_theory.groupoid + +/-! +# The free monoidal category over a type + +Given a type `C`, the free monoidal category over `C` has as objects formal expressions built from +(formal) tensor products of terms of `C` and a formal unit. Its morphisms are compositions and +tensor products of identities, unitors and associators. + +In this file, we construct the free monoidal category and prove that it is a monoidal category. If +`D` is a monoidal category, we construct the functor `free_monoidal_category C ⥤ D` associated to +a function `C → D`. + +The free monoidal category has two important properties: it is a groupoid and it is thin. The former +is obvious from the construction, and the latter is what is commonly known as the monoidal coherence +theorem. Both of these properties are proved in the file `coherence.lean`. + +-/ + +universes v' u u' + +namespace category_theory +open monoidal_category + +variables {C : Type u} + +section +variables (C) + +/-- +Given a type `C`, the free monoidal category over `C` has as objects formal expressions built from +(formal) tensor products of terms of `C` and a formal unit. Its morphisms are compositions and +tensor products of identities, unitors and associators. +-/ +@[derive inhabited] +inductive free_monoidal_category : Type u +| of : C → free_monoidal_category +| unit : free_monoidal_category +| tensor : free_monoidal_category → free_monoidal_category → free_monoidal_category + +end + +local notation `F` := free_monoidal_category + +namespace free_monoidal_category + +/-- Formal compositions and tensor products of identities, unitors and associators. The morphisms + of the free monoidal category are obtained as a quotient of these formal morphisms by the + relations defining a monoidal category. -/ +@[nolint has_inhabited_instance] +inductive hom : F C → F C → Type u +| id (X) : hom X X +| α_hom (X Y Z : F C) : hom ((X.tensor Y).tensor Z) (X.tensor (Y.tensor Z)) +| α_inv (X Y Z : F C) : hom (X.tensor (Y.tensor Z)) ((X.tensor Y).tensor Z) +| l_hom (X) : hom (unit.tensor X) X +| l_inv (X) : hom X (unit.tensor X) +| ρ_hom (X : F C) : hom (X.tensor unit) X +| ρ_inv (X : F C) : hom X (X.tensor unit) +| comp {X Y Z} (f : hom X Y) (g : hom Y Z) : hom X Z +| tensor {W X Y Z} (f : hom W Y) (g : hom X Z) : hom (W.tensor X) (Y.tensor Z) + +local infixr ` ⟶ᵐ `:10 := hom + +/-- The morphisms of the free monoidal category satisfy 21 relations ensuring that the resulting + category is in fact a category and that it is monoidal. -/ +inductive hom_equiv : Π {X Y : F C}, (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop +| refl {X Y} (f : X ⟶ᵐ Y) : hom_equiv f f +| symm {X Y} (f g : X ⟶ᵐ Y) : hom_equiv f g → hom_equiv g f +| trans {X Y} {f g h : X ⟶ᵐ Y} : hom_equiv f g → hom_equiv g h → hom_equiv f h +| comp {X Y Z} {f f' : X ⟶ᵐ Y} {g g' : Y ⟶ᵐ Z} : + hom_equiv f f' → hom_equiv g g' → hom_equiv (f.comp g) (f'.comp g') +| tensor {W X Y Z} {f f' : W ⟶ᵐ X} {g g' : Y ⟶ᵐ Z} : + hom_equiv f f' → hom_equiv g g' → hom_equiv (f.tensor g) (f'.tensor g') +| comp_id {X Y} (f : X ⟶ᵐ Y) : hom_equiv (f.comp (hom.id _)) f +| id_comp {X Y} (f : X ⟶ᵐ Y) : hom_equiv ((hom.id _).comp f) f +| assoc {X Y U V : F C} (f : X ⟶ᵐ U) (g : U ⟶ᵐ V) (h : V ⟶ᵐ Y) : + hom_equiv ((f.comp g).comp h) (f.comp (g.comp h)) +| tensor_id {X Y} : hom_equiv ((hom.id X).tensor (hom.id Y)) (hom.id _) +| tensor_comp {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : F C} + (f₁ : X₁ ⟶ᵐ Y₁) (f₂ : X₂ ⟶ᵐ Y₂) (g₁ : Y₁ ⟶ᵐ Z₁) (g₂ : Y₂ ⟶ᵐ Z₂) : + hom_equiv ((f₁.comp g₁).tensor (f₂.comp g₂)) ((f₁.tensor f₂).comp (g₁.tensor g₂)) +| α_hom_inv {X Y Z} : hom_equiv ((hom.α_hom X Y Z).comp (hom.α_inv X Y Z)) (hom.id _) +| α_inv_hom {X Y Z} : hom_equiv ((hom.α_inv X Y Z).comp (hom.α_hom X Y Z)) (hom.id _) +| associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃} (f₁ : X₁ ⟶ᵐ Y₁) (f₂ : X₂ ⟶ᵐ Y₂) (f₃ : X₃ ⟶ᵐ Y₃) : + hom_equiv (((f₁.tensor f₂).tensor f₃).comp (hom.α_hom Y₁ Y₂ Y₃)) + ((hom.α_hom X₁ X₂ X₃).comp (f₁.tensor (f₂.tensor f₃))) +| ρ_hom_inv {X} : hom_equiv ((hom.ρ_hom X).comp (hom.ρ_inv X)) (hom.id _) +| ρ_inv_hom {X} : hom_equiv ((hom.ρ_inv X).comp (hom.ρ_hom X)) (hom.id _) +| ρ_naturality {X Y} (f : X ⟶ᵐ Y) : hom_equiv + ((f.tensor (hom.id unit)).comp (hom.ρ_hom Y)) ((hom.ρ_hom X).comp f) +| l_hom_inv {X} : hom_equiv ((hom.l_hom X).comp (hom.l_inv X)) (hom.id _) +| l_inv_hom {X} : hom_equiv ((hom.l_inv X).comp (hom.l_hom X)) (hom.id _) +| l_naturality {X Y} (f : X ⟶ᵐ Y) : hom_equiv + (((hom.id unit).tensor f).comp (hom.l_hom Y)) ((hom.l_hom X).comp f) +| pentagon {W X Y Z} : hom_equiv + (((hom.α_hom W X Y).tensor (hom.id Z)).comp + ((hom.α_hom W (X.tensor Y) Z).comp ((hom.id W).tensor (hom.α_hom X Y Z)))) + ((hom.α_hom (W.tensor X) Y Z).comp (hom.α_hom W X (Y.tensor Z))) +| triangle {X Y} : hom_equiv ((hom.α_hom X unit Y).comp ((hom.id X).tensor (hom.l_hom Y))) + ((hom.ρ_hom X).tensor (hom.id Y)) + +/-- We say that two formal morphisms in the free monoidal category are equivalent if they become + equal if we apply the relations that are true in a monoidal category. Note that we will prove + that there is only one equivalence class -- this is the monoidal coherence theorem. -/ +def setoid_hom (X Y : F C) : setoid (X ⟶ᵐ Y) := +⟨hom_equiv, + ⟨λ f, hom_equiv.refl f, λ f g, hom_equiv.symm f g, λ f g h hfg hgh, hom_equiv.trans hfg hgh⟩⟩ + +attribute [instance] setoid_hom + +section +open free_monoidal_category.hom_equiv + +instance category_free_monoidal_category : category.{u} (F C) := +{ hom := λ X Y, quotient (free_monoidal_category.setoid_hom X Y), + id := λ X, ⟦free_monoidal_category.hom.id _⟧, + comp := λ X Y Z f g, quotient.map₂ hom.comp (by { intros f f' hf g g' hg, exact comp hf hg }) f g, + id_comp' := by { rintro X Y ⟨f⟩, exact quotient.sound (id_comp f) }, + comp_id' := by { rintro X Y ⟨f⟩, exact quotient.sound (comp_id f) }, + assoc' := by { rintro W X Y Z ⟨f⟩ ⟨g⟩ ⟨h⟩, exact quotient.sound (assoc f g h) } } + +instance : monoidal_category (F C) := +{ tensor_obj := λ X Y, free_monoidal_category.tensor X Y, + tensor_hom := λ X₁ Y₁ X₂ Y₂, quotient.map₂ hom.tensor $ + by { intros _ _ h _ _ h', exact hom_equiv.tensor h h'}, + tensor_id' := λ X Y, quotient.sound tensor_id, + tensor_comp' := λ X₁ Y₁ Z₁ X₂ Y₂ Z₂, + by { rintros ⟨f₁⟩ ⟨f₂⟩ ⟨g₁⟩ ⟨g₂⟩, exact quotient.sound (tensor_comp _ _ _ _) }, + tensor_unit := free_monoidal_category.unit, + associator := λ X Y Z, + ⟨⟦hom.α_hom X Y Z⟧, ⟦hom.α_inv X Y Z⟧, quotient.sound α_hom_inv, quotient.sound α_inv_hom⟩, + associator_naturality' := λ X₁ X₂ X₃ Y₁ Y₂ Y₃, + by { rintros ⟨f₁⟩ ⟨f₂⟩ ⟨f₃⟩, exact quotient.sound (associator_naturality _ _ _) }, + left_unitor := λ X, + ⟨⟦hom.l_hom X⟧, ⟦hom.l_inv X⟧, quotient.sound l_hom_inv, quotient.sound l_inv_hom⟩, + left_unitor_naturality' := λ X Y, by { rintro ⟨f⟩, exact quotient.sound (l_naturality _) }, + right_unitor := λ X, + ⟨⟦hom.ρ_hom X⟧, ⟦hom.ρ_inv X⟧, quotient.sound ρ_hom_inv, quotient.sound ρ_inv_hom⟩, + right_unitor_naturality' := λ X Y, by { rintro ⟨f⟩, exact quotient.sound (ρ_naturality _) }, + pentagon' := λ W X Y Z, quotient.sound pentagon, + triangle' := λ X Y, quotient.sound triangle } + +@[simp] lemma mk_comp {X Y Z : F C} (f : X ⟶ᵐ Y) (g : Y ⟶ᵐ Z) : + ⟦f.comp g⟧ = @category_struct.comp (F C) _ _ _ _ ⟦f⟧ ⟦g⟧ := +rfl + +@[simp] lemma mk_tensor {X₁ Y₁ X₂ Y₂ : F C} (f : X₁ ⟶ᵐ Y₁) (g : X₂ ⟶ᵐ Y₂) : + ⟦f.tensor g⟧ = @monoidal_category.tensor_hom (F C) _ _ _ _ _ _ ⟦f⟧ ⟦g⟧ := +rfl + +@[simp] lemma mk_id {X : F C} : ⟦hom.id X⟧ = 𝟙 X := rfl +@[simp] lemma mk_α_hom {X Y Z : F C} : ⟦hom.α_hom X Y Z⟧ = (α_ X Y Z).hom := rfl +@[simp] lemma mk_α_inv {X Y Z : F C} : ⟦hom.α_inv X Y Z⟧ = (α_ X Y Z).inv := rfl +@[simp] lemma mk_ρ_hom {X : F C} : ⟦hom.ρ_hom X⟧ = (ρ_ X).hom := rfl +@[simp] lemma mk_ρ_inv {X : F C} : ⟦hom.ρ_inv X⟧ = (ρ_ X).inv := rfl +@[simp] lemma mk_l_hom {X : F C} : ⟦hom.l_hom X⟧ = (λ_ X).hom := rfl +@[simp] lemma mk_l_inv {X : F C} : ⟦hom.l_inv X⟧ = (λ_ X).inv := rfl +@[simp] lemma tensor_eq_tensor {X Y : F C} : X.tensor Y = X ⊗ Y := rfl +@[simp] lemma unit_eq_unit : free_monoidal_category.unit = 𝟙_ (F C) := rfl + +section functor +variables {D : Type u'} [category.{v'} D] [monoidal_category D] (f : C → D) + +/-- Auxiliary definition for `free_monoidal_category.project`. -/ +def project_obj : F C → D +| (free_monoidal_category.of X) := f X +| free_monoidal_category.unit := 𝟙_ D +| (free_monoidal_category.tensor X Y) := project_obj X ⊗ project_obj Y + +section +open hom + +/-- Auxiliary definition for `free_monoidal_category.project`. -/ +@[simp] def project_map_aux : Π {X Y : F C}, (X ⟶ᵐ Y) → (project_obj f X ⟶ project_obj f Y) +| _ _ (id _) := 𝟙 _ +| _ _ (α_hom _ _ _) := (α_ _ _ _).hom +| _ _ (α_inv _ _ _) := (α_ _ _ _).inv +| _ _ (l_hom _) := (λ_ _).hom +| _ _ (l_inv _) := (λ_ _).inv +| _ _ (ρ_hom _) := (ρ_ _).hom +| _ _ (ρ_inv _) := (ρ_ _).inv +| _ _ (comp f g) := project_map_aux f ≫ project_map_aux g +| _ _ (hom.tensor f g) := project_map_aux f ⊗ project_map_aux g + +/-- Auxiliary definition for `free_monoidal_category.project`. -/ +def project_map (X Y : F C) : (X ⟶ Y) → (project_obj f X ⟶ project_obj f Y) := +quotient.lift (project_map_aux f) +begin + intros f g h, + induction h with X Y f X Y f g hfg hfg' X Y f g h _ _ hfg hgh X Y Z f f' g g' _ _ hf hg + W X Y Z f g f' g' _ _ hfg hfg', + { refl }, + { exact hfg'.symm }, + { exact hfg.trans hgh }, + { simp only [project_map_aux, hf, hg] }, + { simp only [project_map_aux, hfg, hfg'] }, + { simp only [project_map_aux, category.comp_id] }, + { simp only [project_map_aux, category.id_comp] }, + { simp only [project_map_aux, category.assoc ] }, + { simp only [project_map_aux, monoidal_category.tensor_id], refl }, + { simp only [project_map_aux, monoidal_category.tensor_comp] }, + { simp only [project_map_aux, iso.hom_inv_id] }, + { simp only [project_map_aux, iso.inv_hom_id] }, + { simp only [project_map_aux, monoidal_category.associator_naturality] }, + { simp only [project_map_aux, iso.hom_inv_id] }, + { simp only [project_map_aux, iso.inv_hom_id] }, + { simp only [project_map_aux], dsimp [project_obj], + exact monoidal_category.right_unitor_naturality _ }, + { simp only [project_map_aux, iso.hom_inv_id] }, + { simp only [project_map_aux, iso.inv_hom_id] }, + { simp only [project_map_aux], dsimp [project_obj], + exact monoidal_category.left_unitor_naturality _ }, + { simp only [project_map_aux], exact monoidal_category.pentagon _ _ _ _ }, + { simp only [project_map_aux], exact monoidal_category.triangle _ _ } +end + +end + +/-- If `D` is a monoidal category and we have a function `C → D`, then we have a functor from the + free monoidal category over `C` to the category `D`. -/ +def project : monoidal_functor (F C) D := +{ obj := project_obj f, + map := project_map f, + ε := 𝟙 _, + μ := λ X Y, 𝟙 _ } + +end functor + +end + +end free_monoidal_category + +end category_theory diff --git a/src/category_theory/monoidal/free/coherence.lean b/src/category_theory/monoidal/free/coherence.lean new file mode 100644 index 0000000000000..d7064e2d870d8 --- /dev/null +++ b/src/category_theory/monoidal/free/coherence.lean @@ -0,0 +1,271 @@ +/- +Copyright (c) 2021 Markus Himmel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import category_theory.monoidal.free.basic +import category_theory.discrete_category + +/-! +# The monoidal coherence theorem + +In this file, we prove the monoidal coherence theorem, stated in the following form: the free +monoidal category over any type `C` is thin. + +We follow a proof described by Ilya Beylin and Peter Dybjer, which has been previously formalized +in the proof assistant ALF. The idea is to declare a normal form (with regard to association and +adding units) on objects of the free monoidal category and consider the discrete subcategory of +objects that are in normal form. A normalization procedure is then just a functor +`full_normalize : free_monoidal_category C ⥤ discrete (normal_monoidal_object C)`, where +functoriality says that two objects which are related by associators and unitors have the +same normal form. Another desirable property of a normalization procedure is that an object is +isomorphic (i.e., related via associators and unitors) to its normal form. In the case of the +specific normalization procedure we use we not only get these isomorphismns, but also that they +assemble into a natural isomorphism `𝟭 (free_monoidal_category C) ≅ full_normalize ⋙ inclusion`. +But this means that any two parallel morphisms in the free monoidal category factor through a +discrete category in the same way, so they must be equal, and hence the free monoidal category +is thin. + +## References + +* [Ilya Beylin and Peter Dybjer, Extracting a proof of coherence for monoidal categories from a + proof of normalization for monoids][beylin1996] + +-/ + +universe u + +namespace category_theory +open monoidal_category + +namespace free_monoidal_category + + +variables {C : Type u} + +section +variables (C) + +/-- We say an object in the free monoidal category is in normal form if it is of the form + `(((𝟙_ C) ⊗ X₁) ⊗ X₂) ⊗ ⋯`. -/ +@[nolint has_inhabited_instance] +inductive normal_monoidal_object : Type u +| unit : normal_monoidal_object +| tensor : normal_monoidal_object → C → normal_monoidal_object + +end + +local notation `F` := free_monoidal_category +local notation `N` := discrete ∘ normal_monoidal_object +local infixr ` ⟶ᵐ `:10 := hom + +/-- Auxiliary definition for `inclusion`. -/ +@[simp] def inclusion_obj : normal_monoidal_object C → F C +| normal_monoidal_object.unit := unit +| (normal_monoidal_object.tensor n a) := tensor (inclusion_obj n) (of a) + +/-- The discrete subcategory of objects in normal form includes into the free monoidal category. -/ +@[simp] def inclusion : N C ⥤ F C := +discrete.functor inclusion_obj + +/-- Auxiliary definition for `normalize`. -/ +@[simp] def normalize_obj : F C → normal_monoidal_object C → normal_monoidal_object C +| unit n := n +| (of X) n := normal_monoidal_object.tensor n X +| (tensor X Y) n := normalize_obj Y (normalize_obj X n) + +@[simp] lemma normalize_obj_unitor (n : N C) : normalize_obj (𝟙_ (F C)) n = n := +rfl + +@[simp] lemma normalize_obj_tensor (X Y : F C) (n : N C) : + normalize_obj (X ⊗ Y) n = normalize_obj Y (normalize_obj X n) := +rfl + +section +open hom + +/-- Auxiliary definition for `normalize`. Here we prove that objects that are related by + associators and unitors map to the same normal form. -/ +@[simp] def normalize_map_aux : Π {X Y : F C}, + (X ⟶ᵐ Y) → + ((discrete.functor (normalize_obj X) : _ ⥤ N C) ⟶ discrete.functor (normalize_obj Y)) +| _ _ (id _) := 𝟙 _ +| _ _ (α_hom _ _ _) := ⟨λ X, 𝟙 _⟩ +| _ _ (α_inv _ _ _) := ⟨λ X, 𝟙 _⟩ +| _ _ (l_hom _) := ⟨λ X, 𝟙 _⟩ +| _ _ (l_inv _) := ⟨λ X, 𝟙 _⟩ +| _ _ (ρ_hom _) := ⟨λ X, 𝟙 _⟩ +| _ _ (ρ_inv _) := ⟨λ X, 𝟙 _⟩ +| X Y (@comp _ U V W f g) := normalize_map_aux f ≫ normalize_map_aux g +| X Y (@hom.tensor _ T U V W f g) := + ⟨λ X, (normalize_map_aux g).app (normalize_obj T X) ≫ + (discrete.functor (normalize_obj W) : _ ⥤ N C).map ((normalize_map_aux f).app X), by tidy⟩ + +end + +section +variables (C) + +/-- Our normalization procedure works by first defining a functor `F C ⥤ (N C ⥤ N C)` (which turns + out to be very easy), and then obtain a functor `F C ⥤ N C` by plugging in the normal object + `𝟙_ C`. -/ +@[simp] def normalize : F C ⥤ N C ⥤ N C := +{ obj := λ X, discrete.functor (normalize_obj X), + map := λ X Y, quotient.lift normalize_map_aux (by tidy) } + +/-- A variant of the normalization functor where we consider the result as an object in the free + monoidal category (rather than an object of the discrete subcategory of objects in normal + form). -/ +@[simp] def normalize' : F C ⥤ N C ⥤ F C := +normalize C ⋙ (whiskering_right _ _ _).obj inclusion + +/-- The normalization functor for the free monoidal category over `C`. -/ +def full_normalize : F C ⥤ N C := +{ obj := λ X, ((normalize C).obj X).obj normal_monoidal_object.unit, + map := λ X Y f, ((normalize C).map f).app normal_monoidal_object.unit } + +/-- Given an object `X` of the free monoidal category and an object `n` in normal form, taking + the tensor product `n ⊗ X` in the free monoidal category is functorial in both `X` and `n`. -/ +@[simp] def tensor_func : F C ⥤ N C ⥤ F C := +{ obj := λ X, discrete.functor (λ n, (inclusion.obj n) ⊗ X), + map := λ X Y f, ⟨λ n, 𝟙 _ ⊗ f, by tidy⟩ } + +lemma tensor_func_map_app {X Y : F C} (f : X ⟶ Y) (n) : ((tensor_func C).map f).app n = + 𝟙 _ ⊗ f := +rfl + +lemma tensor_func_obj_map (Z : F C) {n n' : N C} (f : n ⟶ n') : + ((tensor_func C).obj Z).map f = inclusion.map f ⊗ 𝟙 Z := +by tidy + +/-- Auxiliary definition for `normalize_iso`. Here we construct the isomorphism between + `n ⊗ X` and `normalize X n`. -/ +@[simp] def normalize_iso_app : + Π (X : F C) (n : N C), ((tensor_func C).obj X).obj n ≅ ((normalize' C).obj X).obj n +| (of X) n := iso.refl _ +| unit n := ρ_ _ +| (tensor X Y) n := + (α_ _ _ _).symm ≪≫ tensor_iso (normalize_iso_app X n) (iso.refl _) ≪≫ normalize_iso_app _ _ + +@[simp] lemma normalize_iso_app_tensor (X Y : F C) (n : N C) : + normalize_iso_app C (X ⊗ Y) n = + (α_ _ _ _).symm ≪≫ tensor_iso (normalize_iso_app C X n) (iso.refl _) ≪≫ + normalize_iso_app _ _ _ := +rfl + +@[simp] lemma normalize_iso_app_unitor (n : N C) : normalize_iso_app C (𝟙_ (F C)) n = ρ_ _ := +rfl + +/-- Auxiliary definition for `normalize_iso`. -/ +@[simp] def normalize_iso_aux (X : F C) : (tensor_func C).obj X ≅ (normalize' C).obj X := +nat_iso.of_components (normalize_iso_app C X) (by tidy) + +/-- The isomorphism between `n ⊗ X` and `normalize X n` is natural (in both `X` and `n`, but + naturality in `n` is trivial and was "proved" in `normalize_iso_aux`). This is the real heart + of our proof of the coherence theorem. -/ +def normalize_iso : tensor_func C ≅ normalize' C := +nat_iso.of_components (normalize_iso_aux C) +begin + rintros X Y f, + apply quotient.induction_on f, + intro f, + ext n, + induction f generalizing n, + { simp only [mk_id, functor.map_id, category.id_comp, category.comp_id] }, + { dsimp, + simp only [id_tensor_associator_inv_naturality_assoc, ←pentagon_inv_assoc, + tensor_hom_inv_id_assoc, tensor_id, category.id_comp, discrete.functor_map_id, comp_tensor_id, + iso.cancel_iso_inv_left, category.assoc], + dsimp, simp only [category.comp_id] }, + { dsimp, + simp only [discrete.functor_map_id, comp_tensor_id, category.assoc, pentagon_inv_assoc, + ←associator_inv_naturality_assoc, tensor_id, iso.cancel_iso_inv_left], + dsimp, simp only [category.comp_id],}, + { dsimp, + rw triangle_assoc_comp_right_assoc, + simp only [discrete.functor_map_id, category.assoc], + dsimp, simp only [category.comp_id] }, + { dsimp, + simp only [triangle_assoc_comp_left_inv_assoc, inv_hom_id_tensor_assoc, tensor_id, + category.id_comp, discrete.functor_map_id], + dsimp, simp only [category.comp_id] }, + { dsimp, + rw [←(iso.inv_comp_eq _).2 (right_unitor_tensor _ _), category.assoc, ←right_unitor_naturality], + simp only [discrete.functor_map_id, iso.cancel_iso_inv_left, category.assoc], + dsimp, simp only [category.comp_id] }, + { dsimp, + simp only [←(iso.eq_comp_inv _).1 (right_unitor_tensor_inv _ _), iso.hom_inv_id_assoc, + right_unitor_conjugation, discrete.functor_map_id, category.assoc], + dsimp, simp only [category.comp_id], }, + { dsimp at *, + rw [id_tensor_comp, category.assoc, f_ih_g ⟦f_g⟧, ←category.assoc, f_ih_f ⟦f_f⟧, category.assoc, + ←functor.map_comp], + congr' 2 }, + { dsimp at *, + rw associator_inv_naturality_assoc, + slice_lhs 2 3 { rw [←tensor_comp, f_ih_f ⟦f_f⟧] }, + conv_lhs { rw [←@category.id_comp (F C) _ _ _ ⟦f_g⟧] }, + simp only [category.comp_id, tensor_comp, category.assoc], + congr' 2, + rw [←mk_tensor, quotient.lift_mk], + dsimp, + rw [functor.map_comp, ←category.assoc, ←f_ih_g ⟦f_g⟧, ←@category.comp_id (F C) _ _ _ ⟦f_g⟧, + ←category.id_comp ((discrete.functor inclusion_obj).map _), tensor_comp], + dsimp, + simp only [category.assoc, category.comp_id], + congr' 1, + convert (normalize_iso_aux C f_Z).hom.naturality ((normalize_map_aux f_f).app n), + exact (tensor_func_obj_map _ _ _).symm } +end + +/-- The isomorphism between an object and its normal form is natural. -/ +def full_normalize_iso : 𝟭 (F C) ≅ full_normalize C ⋙ inclusion := +nat_iso.of_components + (λ X, (λ_ X).symm ≪≫ ((normalize_iso C).app X).app normal_monoidal_object.unit) + begin + intros X Y f, + dsimp, + rw [left_unitor_inv_naturality_assoc, category.assoc, iso.cancel_iso_inv_left], + exact congr_arg (λ f, nat_trans.app f normal_monoidal_object.unit) + ((normalize_iso.{u} C).hom.naturality f), + end + +end + +/-- The monoidal coherence theorem. -/ +instance subsingleton_hom {X Y : F C} : subsingleton (X ⟶ Y) := +⟨λ f g, have (full_normalize C).map f = (full_normalize C).map g, from subsingleton.elim _ _, + begin + rw [←functor.id_map f, ←functor.id_map g], + simp [←nat_iso.naturality_2 (full_normalize_iso.{u} C), this] + end⟩ + +section groupoid + +section +open hom + +/-- Auxiliary construction for showing that the free monoidal category is a groupoid. Do not use + this, use `is_iso.inv` instead. -/ +def inverse_aux : Π {X Y : F C}, (X ⟶ᵐ Y) → (Y ⟶ᵐ X) +| _ _ (id X) := id X +| _ _ (α_hom _ _ _) := α_inv _ _ _ +| _ _ (α_inv _ _ _) := α_hom _ _ _ +| _ _ (ρ_hom _) := ρ_inv _ +| _ _ (ρ_inv _) := ρ_hom _ +| _ _ (l_hom _) := l_inv _ +| _ _ (l_inv _) := l_hom _ +| _ _ (comp f g) := (inverse_aux g).comp (inverse_aux f) +| _ _ (hom.tensor f g) := (inverse_aux f).tensor (inverse_aux g) + +end + +instance : groupoid.{u} (F C) := +{ inv := λ X Y, quotient.lift (λ f, ⟦inverse_aux f⟧) (by tidy), + ..(infer_instance : category (F C)) } + +end groupoid + +end free_monoidal_category + +end category_theory