From 3683cd05bdfd69791f8e4c80f6571fc5d1197dea Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 18 Jun 2024 14:43:56 +0000 Subject: [PATCH] chore(CategoryTheory/Monoidal/Mon_): cleanup (#13310) Co-authored-by: Scott Morrison --- Mathlib/CategoryTheory/Monoidal/Mon_.lean | 63 +++++++------------ .../Monoidal/NaturalTransformation.lean | 8 ++- 2 files changed, 26 insertions(+), 45 deletions(-) diff --git a/Mathlib/CategoryTheory/Monoidal/Mon_.lean b/Mathlib/CategoryTheory/Monoidal/Mon_.lean index bac37afc4b68a..03bba6f31ab8a 100644 --- a/Mathlib/CategoryTheory/Monoidal/Mon_.lean +++ b/Mathlib/CategoryTheory/Monoidal/Mon_.lean @@ -81,9 +81,9 @@ theorem mul_one_hom {Z : C} (f : Z ⟶ M.X) : (f ⊗ M.one) ≫ M.mul = (ρ_ Z). rw [tensorHom_def_assoc, M.mul_one, rightUnitor_naturality] #align Mon_.mul_one_hom Mon_.mul_one_hom -theorem assoc_flip : +theorem mul_assoc_flip : (M.X ◁ M.mul) ≫ M.mul = (α_ M.X M.X M.X).inv ≫ (M.mul ▷ M.X) ≫ M.mul := by simp -#align Mon_.assoc_flip Mon_.assoc_flip +#align Mon_.assoc_flip Mon_.mul_assoc_flip /-- A morphism of monoid objects. -/ @[ext] @@ -153,12 +153,7 @@ instance {A B : Mon_ C} (f : A ⟶ B) [e : IsIso ((forget C).map f)] : IsIso f.h /-- The forgetful functor from monoid objects to the ambient category reflects isomorphisms. -/ instance : (forget C).ReflectsIsomorphisms where - reflects f e := - ⟨⟨{ hom := inv f.hom - mul_hom := by - simp only [IsIso.comp_inv_eq, Hom.mul_hom, Category.assoc, ← tensor_comp_assoc, - IsIso.inv_hom_id, tensor_id, Category.id_comp] }, - by aesop_cat⟩⟩ + reflects f e := ⟨⟨{ hom := inv f.hom }, by aesop_cat⟩⟩ /-- Construct an isomorphism of monoids by giving an isomorphism between the underlying objects and checking compatibility with unit and multiplication only in the forward direction. @@ -166,26 +161,23 @@ and checking compatibility with unit and multiplication only in the forward dire @[simps] def mkIso {M N : Mon_ C} (f : M.X ≅ N.X) (one_f : M.one ≫ f.hom = N.one := by aesop_cat) (mul_f : M.mul ≫ f.hom = (f.hom ⊗ f.hom) ≫ N.mul := by aesop_cat) : M ≅ N where - hom := - { hom := f.hom - one_hom := one_f - mul_hom := mul_f } + hom := { hom := f.hom } inv := - { hom := f.inv - one_hom := by rw [← one_f]; simp - mul_hom := by - rw [← cancel_mono f.hom] - slice_rhs 2 3 => rw [mul_f] - simp } + { hom := f.inv + one_hom := by rw [← one_f]; simp + mul_hom := by + rw [← cancel_mono f.hom] + slice_rhs 2 3 => rw [mul_f] + simp } #align Mon_.iso_of_iso Mon_.mkIso instance uniqueHomFromTrivial (A : Mon_ C) : Unique (trivial C ⟶ A) where default := - { hom := A.one - one_hom := by dsimp; simp - mul_hom := by dsimp; simp [A.one_mul, unitors_equal] } + { hom := A.one + mul_hom := by dsimp; simp [A.one_mul, unitors_equal] } uniq f := by - ext; simp + ext + simp only [trivial_X] rw [← Category.id_comp f.hom] erw [f.one_hom] #align Mon_.unique_hom_from_trivial Mon_.uniqueHomFromTrivial @@ -231,8 +223,6 @@ def mapMon (F : LaxMonoidalFunctor C D) : Mon_ C ⥤ Mon_ D where dsimp rw [Category.assoc, F.μ_natural_assoc, ← F.toFunctor.map_comp, ← F.toFunctor.map_comp, f.mul_hom] } - map_id A := by ext; simp - map_comp f g := by ext; simp #align category_theory.lax_monoidal_functor.map_Mon CategoryTheory.LaxMonoidalFunctor.mapMon variable (C D) @@ -263,17 +253,12 @@ def laxMonoidalToMon : LaxMonoidalFunctor (Discrete PUnit.{u + 1}) C ⥤ Mon_ C @[simps] def monToLaxMonoidal : Mon_ C ⥤ LaxMonoidalFunctor (Discrete PUnit.{u + 1}) C where obj A := - { obj := fun _ => A.X - map := fun _ => 𝟙 _ - ε := A.one - μ := fun _ _ => A.mul - map_id := fun _ => rfl - map_comp := fun _ _ => (Category.id_comp (𝟙 A.X)).symm } + { obj := fun _ => A.X + map := fun _ => 𝟙 _ + ε := A.one + μ := fun _ _ => A.mul } map f := - { app := fun _ => f.hom - naturality := fun _ _ _ => by dsimp; rw [Category.id_comp, Category.comp_id] - unit := f.one_hom - tensor := fun _ _ => f.mul_hom } + { app := fun _ => f.hom } #align Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal attribute [local aesop safe tactic (rule_sets := [CategoryTheory])] @@ -287,19 +272,13 @@ def unitIso : 𝟭 (LaxMonoidalFunctor (Discrete PUnit.{u + 1}) C) ≅ laxMonoidalToMon C ⋙ monToLaxMonoidal C := NatIso.ofComponents (fun F => - MonoidalNatIso.ofComponents (fun _ => F.toFunctor.mapIso (eqToIso (by ext))) (by aesop_cat) - (by aesop_cat) (by aesop_cat)) - (by aesop_cat) + MonoidalNatIso.ofComponents (fun _ => F.toFunctor.mapIso (eqToIso (by ext)))) #align Mon_.equiv_lax_monoidal_functor_punit.unit_iso Mon_.EquivLaxMonoidalFunctorPUnit.unitIso /-- Implementation of `Mon_.equivLaxMonoidalFunctorPUnit`. -/ @[simps!] def counitIso : monToLaxMonoidal C ⋙ laxMonoidalToMon C ≅ 𝟭 (Mon_ C) := - NatIso.ofComponents - (fun F => - { hom := { hom := 𝟙 _ } - inv := { hom := 𝟙 _ } }) - (by aesop_cat) + NatIso.ofComponents (fun F => { hom := { hom := 𝟙 _ }, inv := { hom := 𝟙 _ } }) #align Mon_.equiv_lax_monoidal_functor_punit.counit_iso Mon_.EquivLaxMonoidalFunctorPUnit.counitIso end EquivLaxMonoidalFunctorPUnit diff --git a/Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean b/Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean index 9316fb4850e18..3f53b47f5a69b 100644 --- a/Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean +++ b/Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean @@ -142,9 +142,11 @@ variable {F G : LaxMonoidalFunctor C D} /-- Construct a monoidal natural isomorphism from object level isomorphisms, and the monoidal naturality in the forward direction. -/ def ofComponents (app : ∀ X : C, F.obj X ≅ G.obj X) - (naturality' : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f) - (unit' : F.ε ≫ (app (𝟙_ C)).hom = G.ε) - (tensor' : ∀ X Y, F.μ X Y ≫ (app (X ⊗ Y)).hom = ((app X).hom ⊗ (app Y).hom) ≫ G.μ X Y) : + (naturality' : + ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f := by aesop_cat) + (unit' : F.ε ≫ (app (𝟙_ C)).hom = G.ε := by aesop_cat) + (tensor' : + ∀ X Y, F.μ X Y ≫ (app (X ⊗ Y)).hom = ((app X).hom ⊗ (app Y).hom) ≫ G.μ X Y := by aesop_cat) : F ≅ G where hom := { app := fun X => (app X).hom } inv := {