From 5e3058fbdc86b98636ecf24a870de887c194525d Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Tue, 21 Apr 2026 15:52:27 +0200 Subject: [PATCH 1/6] mul action objects --- .../Monoidal/Cartesian/MulAction.lean | 198 ++++++++++++++++++ 1 file changed, 198 insertions(+) create mode 100644 Mathlib/CategoryTheory/Monoidal/Cartesian/MulAction.lean diff --git a/Mathlib/CategoryTheory/Monoidal/Cartesian/MulAction.lean b/Mathlib/CategoryTheory/Monoidal/Cartesian/MulAction.lean new file mode 100644 index 00000000000000..83d2d1599fe63b --- /dev/null +++ b/Mathlib/CategoryTheory/Monoidal/Cartesian/MulAction.lean @@ -0,0 +1,198 @@ +/- +Copyright (c) 2026 Christian Merten. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Merten +-/ +module + +public import Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_ +public import Mathlib.GroupTheory.GroupAction.Hom + +/-! +# Action objects in cartesian monoidal categories + +Given a monoid object `M` in a cartesian monoidal category `C`, we define the notion of a +multiplicative action of `M` on an object `X` of `C`. + +## Main definitions + +- `CategoryTheory.MulActionObj`: A multiplicative action of a monoid object on an object. +- `CategoryTheory.IsMulActionHom`: Equivariant morphisms under monoid actions. +- `CategoryTheory.Hom.mulAction`: If `M` acts on `X`, morphisms into `M` act on morphism into `X`. +-/ + +@[expose] public section + +namespace CategoryTheory + +open MonoidalCategory CartesianMonoidalCategory MonObj AddMonObj + +variable {C : Type*} [Category* C] [CartesianMonoidalCategory C] + +/-- An additive action of an additive monoid object `M` on an object `X` +in a cartesian monoidal category. -/ +@[ext] +class AddActionObj (M : C) [AddMonObj M] (X : C) where + /-- The additive action morphism. -/ + vadd : M ⊗ X ⟶ X + /-- Acting by the zero element is the identity. -/ + zero_vadd (M X) : ζ ▷ X ≫ vadd = (λ_ X).hom := by cat_disch + /-- The action is compatible with addition. -/ + add_vadd (M X) : (σ ▷ X) ≫ vadd = (α_ _ _ _).hom ≫ (M ◁ vadd) ≫ vadd := by cat_disch + +/-- A multiplicative action of a monoid object `M` on an object `X` +in a cartesian monoidal category. -/ +@[to_additive (attr := ext)] +class MulActionObj (M : C) [MonObj M] (X : C) where + /-- The scalar multiplication morphism. -/ + smul : M ⊗ X ⟶ X + /-- Acting by the unit element is the identity. -/ + one_smul (M X) : η ▷ X ≫ smul = (λ_ X).hom := by cat_disch + /-- The action is compatible with multiplication. -/ + mul_smul (M X) : (μ ▷ X) ≫ smul = (α_ _ _ _).hom ≫ (M ◁ smul) ≫ smul := by cat_disch + +variable {M : C} [MonObj M] {X : C} [MulActionObj M X] + +namespace MulActionObj + +attribute [to_additive existing (attr := reassoc), simp] one_smul +attribute [to_additive existing (attr := simp)] one_smul_assoc +attribute [to_additive existing (attr := reassoc)] mul_smul +attribute [to_additive existing] mul_smul_assoc + +/-- Every monoid object acts on itself by left multiplication. -/ +@[to_additive /-- Every additive monoid object acts on itself by left addition. -/] +instance : MulActionObj M M where + smul := mul + +variable (M) in +/-- The trivial action of `M` on `X`, given by projection to the second factor. -/ +@[to_additive (attr := simps!, implicit_reducible) +/-- The trivial action of `M` on `X`, given by projection to the second factor. -/] +def trivial (X : C) : MulActionObj M X where + smul := snd _ _ + one_smul := by simp [leftUnitor_hom] + +/-- Transfer a `MulActionObj` along isomorphisms. -/ +@[to_additive (attr := implicit_reducible) + /-- Transfer an `AddActionObj` along isomorphisms. -/] +def ofIso {N : C} [MonObj N] (e₁ : M ≅ N) [IsMonHom e₁.hom] {Y : C} (e₂ : X ≅ Y) : + MulActionObj N Y where + smul := (e₁.inv ⊗ₘ e₂.inv) ≫ smul ≫ e₂.hom + one_smul := by + have : η ▷ Y ≫ (e₁.inv ⊗ₘ e₂.inv) = _ ◁ e₂.inv ≫ (η ≫ e₁.inv) ▷ X := by + rw [tensorHom_def', comp_whiskerRight, whisker_exchange_assoc] + simp [reassoc_of% this] + mul_smul := by + have : μ[N] ▷ Y ≫ (e₁.inv ⊗ₘ e₂.inv) = + ((e₁.inv ⊗ₘ e₁.inv) ⊗ₘ e₂.inv) ≫ μ[M] ▷ X := by + rw [tensorHom_def', whisker_exchange, ← comp_whiskerRight_assoc, IsMonHom.mul_hom, + comp_whiskerRight, Category.assoc, ← whisker_exchange] + nth_rw 2 [tensorHom_def', whisker_exchange] + simp + rw [reassoc_of% this] + have : (α_ N M X).inv ≫ e₁.inv ▷ M ▷ X ≫ (α_ M M X).hom ≫ M ◁ smul = + N ◁ smul ≫ e₁.inv ▷ X := by + rw [associator_naturality_left_assoc, whisker_exchange] + simp + simp [tensorHom_def', mul_smul_assoc, reassoc_of% this] + +variable (M) in +@[to_additive (attr := reassoc)] +theorem mul_smul_flip : + M ◁ smul ≫ smul = (α_ M M X).inv ≫ (μ ▷ X) ≫ smul := by + simp [MulActionObj.mul_smul] + +@[to_additive (attr := reassoc (attr := simp))] +theorem one_smul_hom {Z : C} (f : Z ⟶ X) : + (η[M] ⊗ₘ f) ≫ smul = (λ_ Z).hom ≫ f := by + rw [tensorHom_def'_assoc, one_smul, leftUnitor_naturality] + +end MulActionObj + +variable {N O : C} [MonObj N] [MonObj O] {Y Z : C} [MulActionObj N Y] [MulActionObj O Z] + +/-- If `φ : M ⟶ N` is a morphism of additive monoid objects and `X` and `Y` are equipped with +actions of `M` and `N`, a morphism `f : X ⟶ Y` is `φ`-equivariant if the actions commute with +`f` and `φ`. -/ +class IsAddActionHom {M : C} [AddMonObj M] {X : C} [AddActionObj M X] {N : C} [AddMonObj N] + {Y : C} [AddActionObj N Y] (φ : M ⟶ N) (f : X ⟶ Y) : Prop where + vadd_hom (f) : AddActionObj.vadd ≫ f = (φ ⊗ₘ f) ≫ AddActionObj.vadd + +/-- If `φ : M ⟶ N` is a morphism of monoid objects and `X` and `Y` are equipped with actions of +`M` and `N`, a morphism `f : X ⟶ Y` is `φ`-equivariant if the actions commute with `f` and `φ`. -/ +@[to_additive existing] +class IsMulActionHom (φ : M ⟶ N) (f : X ⟶ Y) : Prop where + smul_hom (φ f) : MulActionObj.smul ≫ f = (φ ⊗ₘ f) ≫ MulActionObj.smul := by cat_disch + +namespace IsMulActionHom + +-- `attribute [to_additive (attr := reassoc)] IsMulActionHom.smul_hom` is not sufficient +attribute [reassoc] IsMulActionHom.smul_hom +attribute [to_additive] IsMulActionHom.smul_hom_assoc + +variable [MulActionObj M Y] [MulActionObj M Z] in +@[to_additive (attr := reassoc (attr := simp))] +lemma smul_hom_id (f : X ⟶ Y) [IsMulActionHom (𝟙 M) f] : + MulActionObj.smul ≫ f = M ◁ f ≫ MulActionObj.smul := by + simp [smul_hom (𝟙 M)] + +-- Without this, the proof of `IsMulActionHom (𝟙 M) (f ≫ g)` breaks below. +set_option linter.existingAttributeWarning false in +attribute [to_additive existing] IsMulActionHom.smul_hom_id_assoc + +@[to_additive] +instance : IsMulActionHom (𝟙 M) (𝟙 X) where + +@[to_additive] +instance (φ : M ⟶ N) (ψ : N ⟶ O) (f : X ⟶ Y) (g : Y ⟶ Z) [IsMulActionHom φ f] [IsMulActionHom ψ g] : + IsMulActionHom (φ ≫ ψ) (f ≫ g) where + smul_hom := by simp [smul_hom_assoc φ, smul_hom ψ] + +variable [MulActionObj M Y] [MulActionObj M Z] in +@[to_additive] +instance (f : X ⟶ Y) (g : Y ⟶ Z) [IsMulActionHom (𝟙 M) f] [IsMulActionHom (𝟙 M) g] : + IsMulActionHom (𝟙 M) (f ≫ g) where + +end IsMulActionHom + +namespace Hom + +variable (M X) in +/-- Morphisms `Y ⟶ M` act on morphisms `Y ⟶ X` via the internal scalar multiplication. -/ +@[to_additive /-- Morphisms `Y ⟶ M` act on morphisms `Y ⟶ X` via the internal additive action. -/] +instance (Y : C) : SMul (Y ⟶ M) (Y ⟶ X) where + smul m x := lift m x ≫ MulActionObj.smul + +@[to_additive] +lemma smul_def {Y : C} (m : Y ⟶ M) (x : Y ⟶ X) : m • x = lift m x ≫ MulActionObj.smul := + rfl + +/-- If `M` is a monoid object acting on `X`, then morphisms into `M` act on +morphisms into `X`. -/ +@[to_additive /-- If `M` is an additive monoid object acting on `X`, then morphisms into `M` act on +morphisms into `X`. -/] +instance mulAction (Y : C) : MulAction (Y ⟶ M) (Y ⟶ X) where + smul m x := lift m x ≫ MulActionObj.smul + one_smul x := by + rw [one_def, smul_def, ← lift_whiskerRight, Category.assoc] + simp + mul_smul m n x := by + rw [mul_def, smul_def, ← lift_whiskerRight, Category.assoc] + simp [smul_def, MulActionObj.mul_smul] + +@[to_additive] +lemma map_smul (φ : M ⟶ N) (f : X ⟶ Y) [IsMulActionHom φ f] {Z : C} (m : Z ⟶ M) (x : Z ⟶ X) : + (m • x) ≫ f = m ≫ φ • x ≫ f := by + simp [smul_def, Category.assoc, IsMulActionHom.smul_hom φ] + +/-- A `φ`-equivariant morphism induces an equivariant morphism on hom types. -/ +@[to_additive /-- A `φ`-equivariant morphism induces an equivariant morphism on hom types. -/] +def mulActionHom (φ : M ⟶ N) (f : X ⟶ Y) [IsMulActionHom φ f] (Z : C) : + MulActionHom (· ≫ φ : (Z ⟶ M) → _) (Z ⟶ X) (Z ⟶ Y) where + toFun := (· ≫ f) + map_smul' := map_smul φ f + +end Hom + +end CategoryTheory From 71adca95e9468aefd4418b2b2621c125d31b071f Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Tue, 21 Apr 2026 15:53:41 +0200 Subject: [PATCH 2/6] mk_all --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index 1d25f1feb37561..cbadeb12ef0490 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3006,6 +3006,7 @@ public import Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_ public import Mathlib.CategoryTheory.Monoidal.Cartesian.InfSemilattice public import Mathlib.CategoryTheory.Monoidal.Cartesian.Mod_ public import Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_ +public import Mathlib.CategoryTheory.Monoidal.Cartesian.MulAction public import Mathlib.CategoryTheory.Monoidal.Cartesian.Over public import Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda public import Mathlib.CategoryTheory.Monoidal.Category From 965951af7569eba969221f2d87fb0de9c3272385 Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Wed, 6 May 2026 21:16:17 +0200 Subject: [PATCH 3/6] fix --- .../Monoidal/Cartesian/Basic.lean | 8 ++ .../Monoidal/Cartesian/Mod.lean | 102 +++++++++++++++++- .../Monoidal/Cartesian/MulAction.lean | 2 +- Mathlib/CategoryTheory/Monoidal/Mod.lean | 48 +++++++++ 4 files changed, 157 insertions(+), 3 deletions(-) diff --git a/Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean index ce52f087b80a25..17ccfca4bd9521 100644 --- a/Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean +++ b/Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean @@ -277,6 +277,14 @@ lemma lift_comp_fst_snd {X Y Z : C} (f : X ⟶ Y ⊗ Z) : lift (f ≫ fst _ _) (f ≫ snd _ _) = f := by cat_disch +/-- The universal property of a cartesian `⊗` as an equivalence. -/ +@[simps] +def liftEquiv {T X Y : C} : (T ⟶ X) × (T ⟶ Y) ≃ (T ⟶ X ⊗ Y) where + toFun f := lift f.1 f.2 + invFun f := ⟨f ≫ fst _ _, f ≫ snd _ _⟩ + left_inv := by cat_disch + right_inv := by cat_disch + @[reassoc (attr := simp)] lemma whiskerLeft_fst (X : C) {Y Z : C} (f : Y ⟶ Z) : X ◁ f ≫ fst _ _ = fst _ _ := by simp [fst_def, ← whiskerLeft_comp_assoc] diff --git a/Mathlib/CategoryTheory/Monoidal/Cartesian/Mod.lean b/Mathlib/CategoryTheory/Monoidal/Cartesian/Mod.lean index f566933d0f1771..67608b3e4bab1d 100644 --- a/Mathlib/CategoryTheory/Monoidal/Cartesian/Mod.lean +++ b/Mathlib/CategoryTheory/Monoidal/Cartesian/Mod.lean @@ -5,11 +5,18 @@ Authors: Paul Lezeau -/ module -public import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic +public import Mathlib.CategoryTheory.Monoidal.Cartesian.Mon public import Mathlib.CategoryTheory.Monoidal.Mod +public import Mathlib.GroupTheory.GroupAction.Hom /-! -# Additional results about module objects in Cartesian monoidal categories +# Module objects in cartesian monoidal categories + +In this file we study module objects in a cartesian monoidal category `C` action on +itself by `⊗`. + +In particular, for a monoid object `M : C` action on `X : C`, we equip `Z ⟶ X` with a `M ⟶ X` action +for every `Z : C`. -/ @[expose] public section @@ -20,6 +27,8 @@ namespace CategoryTheory universe v u variable {C : Type u} [Category.{v} C] [CartesianMonoidalCategory C] +open scoped MonObj + attribute [local simp] leftUnitor_hom /-- Every object is a module over a monoid object via the trivial action. -/ @@ -36,4 +45,93 @@ def Mod.trivialAction (M : Mon C) (X : C) : Mod C M.X where @[deprecated (since := "2026-04-21")] alias Mod_.trivialAction := Mod.trivialAction +variable {M : C} [MonObj M] {X : C} [ModObj M X] + +namespace Hom + +/-- Morphisms `Y ⟶ M` act on morphisms `Y ⟶ X` via the internal scalar multiplication. -/ +@[to_additive (attr := simps! -isSimp) +/-- Morphisms `Y ⟶ M` act on morphisms `Y ⟶ X` via the internal additive action. -/] +instance (Y : C) : SMul (Y ⟶ M) (Y ⟶ X) where + smul m x := lift m x ≫ γ[M, X] + +/-- If `M` is a monoid object acting on `X`, then morphisms into `M` act on +morphisms into `X`. -/ +@[to_additive /-- If `M` is an additive monoid object acting on `X`, then morphisms into `M` act on +morphisms into `X`. -/] +instance mulAction (Z : C) : MulAction (Z ⟶ M) (Z ⟶ X) where + one_smul x := by + rw [one_def, smul_def, ← lift_whiskerRight, Category.assoc] + simp + mul_smul m n x := by + rw [mul_def, smul_def, ← lift_whiskerRight, Category.assoc] + simp [smul_def] + +end Hom + +variable {Y : C} [ModObj M Y] + +lemma ModObj.comp_smul {Z Z' : C} (g : Z' ⟶ Z) (m : Z ⟶ M) (x : Z ⟶ X) : + g ≫ (m • x) = (g ≫ m) • (g ≫ x) := by + rw [Hom.smul_def, Hom.smul_def, comp_lift_assoc] + +@[to_additive (attr := reassoc (attr := simp))] +lemma IsModHom.map_smul (f : X ⟶ Y) [IsModHom M f] {Z : C} (m : Z ⟶ M) (x : Z ⟶ X) : + (m • x) ≫ f = m • x ≫ f := by + simp [Hom.smul_def, Category.assoc, IsModHom.smul_hom] + +/-- An `M`-equivariant morphism induces an equivariant function on hom types. -/ +@[to_additive (attr := simps) +/-- A `φ`-equivariant morphism induces an equivariant morphism on hom types. -/] +def IsModHom.mulActionHom (f : X ⟶ Y) [IsModHom M f] (Z : C) : + MulActionHom (id (α := Z ⟶ M)) (Z ⟶ X) (Z ⟶ Y) where + toFun := (· ≫ f) + map_smul' := map_smul f + +namespace ModObj + +variable (M X) in +/-- The morphism `(m, x) ↦ (m • x, x)`. -/ +def leftSMul : M ⊗ X ⟶ X ⊗ X := + lift γ[M, X] (snd _ _) + +@[reassoc (attr := simp)] +lemma leftSMul_fst : leftSMul M X ≫ fst _ _ = γ[M, X] := by + simp [leftSMul] + +@[reassoc (attr := simp)] +lemma leftSMul_snd : leftSMul M X ≫ snd _ _ = snd _ _ := by + simp [leftSMul] + +@[reassoc] +lemma lift_leftSMul (Z : C) (x : Z ⟶ X) (m : Z ⟶ M) : lift m x ≫ leftSMul M X = lift (m • x) x := by + ext <;> simp [Hom.smul_def] + +lemma lift_leftSMul_eq_lift_iff (Z : C) (x y : Z ⟶ X) (m : Z ⟶ M) : + lift m x ≫ leftSMul M X = lift y x ↔ m • x = y := by + simp [Hom.smul_def, leftSMul, CartesianMonoidalCategory.hom_ext_iff] + +open CartesianMonoidalCategory in +/-- The morphism `(m, x) ↦ (m • x, x)` is an isomorphism if and only if the induced +action is pointwise simply transitive. -/ +lemma isIso_leftSMul_iff : + IsIso (leftSMul M X) ↔ ∀ (Z : C) (x y : Z ⟶ X), ∃! (m : Z ⟶ M), m • x = y := by + have H (Z : C) (x : Z ⟶ X) (m : Z ⟶ M) : + lift m x ≫ leftSMul M X = lift (m • x) x := by + ext <;> simp [Hom.smul_def] + have h (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X) : + lift m x ≫ leftSMul M X = lift f g ↔ x = g ∧ m • x = f := by + simp [← lift_leftSMul_eq_lift_iff, CartesianMonoidalCategory.hom_ext_iff] + grind + rw [isIso_iff_yoneda_map_bijective] + congr! with Z + rw [← Function.Bijective.of_comp_iff _ liftEquiv.bijective, Function.bijective_iff_existsUnique] + simp only [liftEquiv.surjective.forall, liftEquiv_apply, Prod.forall, Function.comp_apply, h] + rw [forall_comm] + congr! 2 with f g + exact Equiv.existsUnique_subtype_congr ⟨fun a ↦ ⟨a.val.fst, by grind⟩, + fun a ↦ ⟨⟨a.val, f⟩, by grind⟩, by cat_disch, by cat_disch⟩ + +end ModObj + end CategoryTheory diff --git a/Mathlib/CategoryTheory/Monoidal/Cartesian/MulAction.lean b/Mathlib/CategoryTheory/Monoidal/Cartesian/MulAction.lean index 83d2d1599fe63b..ba0bbd91357591 100644 --- a/Mathlib/CategoryTheory/Monoidal/Cartesian/MulAction.lean +++ b/Mathlib/CategoryTheory/Monoidal/Cartesian/MulAction.lean @@ -5,7 +5,7 @@ Authors: Christian Merten -/ module -public import Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_ +public import Mathlib.CategoryTheory.Monoidal.Cartesian.Mon public import Mathlib.GroupTheory.GroupAction.Hom /-! diff --git a/Mathlib/CategoryTheory/Monoidal/Mod.lean b/Mathlib/CategoryTheory/Monoidal/Mod.lean index a23ee55949bdd7..596b42541d34a6 100644 --- a/Mathlib/CategoryTheory/Monoidal/Mod.lean +++ b/Mathlib/CategoryTheory/Monoidal/Mod.lean @@ -66,6 +66,9 @@ class ModObj (X : D) where attribute [to_additive existing (attr := reassoc (attr := simp))] ModObj.mul_smul ModObj.one_smul +set_option linter.existingAttributeWarning false in +attribute [to_additive existing] ModObj.one_smul_assoc ModObj.mul_smul_assoc + namespace AddModObj @[inherit_doc] scoped[CategoryTheory.AddMonObj] notation "δ" => AddModObj.vadd @@ -118,6 +121,51 @@ theorem ext {X : C} (h₁ h₂ : ModObj M X) (H : h₁.smul = h₂.smul) : subst H rfl +open MonoidalLeftAction in +/-- Transfer a `MulActionObj` along isomorphisms. -/ +@[to_additive (attr := simps! -isSimp, implicit_reducible) +/-- Transfer an `AddActionObj` along isomorphisms. -/] +def ofIso {X : D} {N : C} [MonObj N] (e₁ : M ≅ N) [IsMonHom e₁.hom] + {Y : D} (e₂ : X ≅ Y) [ModObj M X] : + ModObj N Y where + smul := (e₁.inv ⊙ₗₘ e₂.inv) ≫ γ ≫ e₂.hom + one_smul := by + have : η ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) = _ ⊴ₗ e₂.inv ≫ (η ≫ e₁.inv) ⊵ₗ X := by + rw [actionHom_def', comp_actionHomLeft, action_exchange_assoc] + simp [reassoc_of% this] + mul_smul := by + have : μ[N] ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) = + ((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ[M] ⊵ₗ X := by + rw [actionHom_def', action_exchange, ← comp_actionHomLeft_assoc, IsMonHom.mul_hom, + comp_actionHomLeft, Category.assoc, ← action_exchange, actionHom_def'] + nth_rw 2 [action_exchange] + rw [Category.assoc] + rw [reassoc_of% this] + have : (αₗ N M X).inv ≫ (e₁.inv ▷ M) ⊵ₗ X ≫ (αₗ M M X).hom ≫ M ⊴ₗ smul = + N ⊴ₗ γ ≫ e₁.inv ⊵ₗ X := by + rw [← actionHomLeft_action_assoc, action_exchange] + simp [tensorHom_def', actionHom_def', mul_smul_assoc, reassoc_of% this] + +section SelfAction + +variable (X : C) [ModObj M X] + +@[to_additive (attr := reassoc (attr := simp))] +lemma one_smul_self (M : C) [MonObj M] (X : C) [ModObj M X] : + η ▷ X ≫ γ[M, X] = (λ_ X).hom := + ModObj.one_smul (M := M) X + +@[to_additive (attr := reassoc (attr := simp))] +lemma mul_smul_self (M : C) [MonObj M] (X : C) [ModObj M X] : + (μ ▷ X) ≫ γ[M, X] = (α_ _ _ _).hom ≫ (M ◁ γ[M, X]) ≫ γ[M, X] := + ModObj.mul_smul (M := M) X + +@[to_additive (attr := reassoc)] +theorem mul_smul_self_flip : M ◁ γ[M, X] ≫ γ[M, X] = (α_ M M X).inv ≫ (μ ▷ X) ≫ γ[M, X] := by + simp + +end SelfAction + end ModObj end ModObj From 07a79ebc245b8dd65591a38d151ee50ad6b240ba Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Wed, 6 May 2026 21:17:13 +0200 Subject: [PATCH 4/6] fix --- Mathlib.lean | 1 - .../Monoidal/Cartesian/MulAction.lean | 198 ------------------ 2 files changed, 199 deletions(-) delete mode 100644 Mathlib/CategoryTheory/Monoidal/Cartesian/MulAction.lean diff --git a/Mathlib.lean b/Mathlib.lean index 1ba7ae3009f7d9..2b3f5d847b6449 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3031,7 +3031,6 @@ public import Mathlib.CategoryTheory.Monoidal.Cartesian.Mod public import Mathlib.CategoryTheory.Monoidal.Cartesian.Mod_ public import Mathlib.CategoryTheory.Monoidal.Cartesian.Mon public import Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_ -public import Mathlib.CategoryTheory.Monoidal.Cartesian.MulAction public import Mathlib.CategoryTheory.Monoidal.Cartesian.Over public import Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda public import Mathlib.CategoryTheory.Monoidal.Category diff --git a/Mathlib/CategoryTheory/Monoidal/Cartesian/MulAction.lean b/Mathlib/CategoryTheory/Monoidal/Cartesian/MulAction.lean deleted file mode 100644 index ba0bbd91357591..00000000000000 --- a/Mathlib/CategoryTheory/Monoidal/Cartesian/MulAction.lean +++ /dev/null @@ -1,198 +0,0 @@ -/- -Copyright (c) 2026 Christian Merten. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Christian Merten --/ -module - -public import Mathlib.CategoryTheory.Monoidal.Cartesian.Mon -public import Mathlib.GroupTheory.GroupAction.Hom - -/-! -# Action objects in cartesian monoidal categories - -Given a monoid object `M` in a cartesian monoidal category `C`, we define the notion of a -multiplicative action of `M` on an object `X` of `C`. - -## Main definitions - -- `CategoryTheory.MulActionObj`: A multiplicative action of a monoid object on an object. -- `CategoryTheory.IsMulActionHom`: Equivariant morphisms under monoid actions. -- `CategoryTheory.Hom.mulAction`: If `M` acts on `X`, morphisms into `M` act on morphism into `X`. --/ - -@[expose] public section - -namespace CategoryTheory - -open MonoidalCategory CartesianMonoidalCategory MonObj AddMonObj - -variable {C : Type*} [Category* C] [CartesianMonoidalCategory C] - -/-- An additive action of an additive monoid object `M` on an object `X` -in a cartesian monoidal category. -/ -@[ext] -class AddActionObj (M : C) [AddMonObj M] (X : C) where - /-- The additive action morphism. -/ - vadd : M ⊗ X ⟶ X - /-- Acting by the zero element is the identity. -/ - zero_vadd (M X) : ζ ▷ X ≫ vadd = (λ_ X).hom := by cat_disch - /-- The action is compatible with addition. -/ - add_vadd (M X) : (σ ▷ X) ≫ vadd = (α_ _ _ _).hom ≫ (M ◁ vadd) ≫ vadd := by cat_disch - -/-- A multiplicative action of a monoid object `M` on an object `X` -in a cartesian monoidal category. -/ -@[to_additive (attr := ext)] -class MulActionObj (M : C) [MonObj M] (X : C) where - /-- The scalar multiplication morphism. -/ - smul : M ⊗ X ⟶ X - /-- Acting by the unit element is the identity. -/ - one_smul (M X) : η ▷ X ≫ smul = (λ_ X).hom := by cat_disch - /-- The action is compatible with multiplication. -/ - mul_smul (M X) : (μ ▷ X) ≫ smul = (α_ _ _ _).hom ≫ (M ◁ smul) ≫ smul := by cat_disch - -variable {M : C} [MonObj M] {X : C} [MulActionObj M X] - -namespace MulActionObj - -attribute [to_additive existing (attr := reassoc), simp] one_smul -attribute [to_additive existing (attr := simp)] one_smul_assoc -attribute [to_additive existing (attr := reassoc)] mul_smul -attribute [to_additive existing] mul_smul_assoc - -/-- Every monoid object acts on itself by left multiplication. -/ -@[to_additive /-- Every additive monoid object acts on itself by left addition. -/] -instance : MulActionObj M M where - smul := mul - -variable (M) in -/-- The trivial action of `M` on `X`, given by projection to the second factor. -/ -@[to_additive (attr := simps!, implicit_reducible) -/-- The trivial action of `M` on `X`, given by projection to the second factor. -/] -def trivial (X : C) : MulActionObj M X where - smul := snd _ _ - one_smul := by simp [leftUnitor_hom] - -/-- Transfer a `MulActionObj` along isomorphisms. -/ -@[to_additive (attr := implicit_reducible) - /-- Transfer an `AddActionObj` along isomorphisms. -/] -def ofIso {N : C} [MonObj N] (e₁ : M ≅ N) [IsMonHom e₁.hom] {Y : C} (e₂ : X ≅ Y) : - MulActionObj N Y where - smul := (e₁.inv ⊗ₘ e₂.inv) ≫ smul ≫ e₂.hom - one_smul := by - have : η ▷ Y ≫ (e₁.inv ⊗ₘ e₂.inv) = _ ◁ e₂.inv ≫ (η ≫ e₁.inv) ▷ X := by - rw [tensorHom_def', comp_whiskerRight, whisker_exchange_assoc] - simp [reassoc_of% this] - mul_smul := by - have : μ[N] ▷ Y ≫ (e₁.inv ⊗ₘ e₂.inv) = - ((e₁.inv ⊗ₘ e₁.inv) ⊗ₘ e₂.inv) ≫ μ[M] ▷ X := by - rw [tensorHom_def', whisker_exchange, ← comp_whiskerRight_assoc, IsMonHom.mul_hom, - comp_whiskerRight, Category.assoc, ← whisker_exchange] - nth_rw 2 [tensorHom_def', whisker_exchange] - simp - rw [reassoc_of% this] - have : (α_ N M X).inv ≫ e₁.inv ▷ M ▷ X ≫ (α_ M M X).hom ≫ M ◁ smul = - N ◁ smul ≫ e₁.inv ▷ X := by - rw [associator_naturality_left_assoc, whisker_exchange] - simp - simp [tensorHom_def', mul_smul_assoc, reassoc_of% this] - -variable (M) in -@[to_additive (attr := reassoc)] -theorem mul_smul_flip : - M ◁ smul ≫ smul = (α_ M M X).inv ≫ (μ ▷ X) ≫ smul := by - simp [MulActionObj.mul_smul] - -@[to_additive (attr := reassoc (attr := simp))] -theorem one_smul_hom {Z : C} (f : Z ⟶ X) : - (η[M] ⊗ₘ f) ≫ smul = (λ_ Z).hom ≫ f := by - rw [tensorHom_def'_assoc, one_smul, leftUnitor_naturality] - -end MulActionObj - -variable {N O : C} [MonObj N] [MonObj O] {Y Z : C} [MulActionObj N Y] [MulActionObj O Z] - -/-- If `φ : M ⟶ N` is a morphism of additive monoid objects and `X` and `Y` are equipped with -actions of `M` and `N`, a morphism `f : X ⟶ Y` is `φ`-equivariant if the actions commute with -`f` and `φ`. -/ -class IsAddActionHom {M : C} [AddMonObj M] {X : C} [AddActionObj M X] {N : C} [AddMonObj N] - {Y : C} [AddActionObj N Y] (φ : M ⟶ N) (f : X ⟶ Y) : Prop where - vadd_hom (f) : AddActionObj.vadd ≫ f = (φ ⊗ₘ f) ≫ AddActionObj.vadd - -/-- If `φ : M ⟶ N` is a morphism of monoid objects and `X` and `Y` are equipped with actions of -`M` and `N`, a morphism `f : X ⟶ Y` is `φ`-equivariant if the actions commute with `f` and `φ`. -/ -@[to_additive existing] -class IsMulActionHom (φ : M ⟶ N) (f : X ⟶ Y) : Prop where - smul_hom (φ f) : MulActionObj.smul ≫ f = (φ ⊗ₘ f) ≫ MulActionObj.smul := by cat_disch - -namespace IsMulActionHom - --- `attribute [to_additive (attr := reassoc)] IsMulActionHom.smul_hom` is not sufficient -attribute [reassoc] IsMulActionHom.smul_hom -attribute [to_additive] IsMulActionHom.smul_hom_assoc - -variable [MulActionObj M Y] [MulActionObj M Z] in -@[to_additive (attr := reassoc (attr := simp))] -lemma smul_hom_id (f : X ⟶ Y) [IsMulActionHom (𝟙 M) f] : - MulActionObj.smul ≫ f = M ◁ f ≫ MulActionObj.smul := by - simp [smul_hom (𝟙 M)] - --- Without this, the proof of `IsMulActionHom (𝟙 M) (f ≫ g)` breaks below. -set_option linter.existingAttributeWarning false in -attribute [to_additive existing] IsMulActionHom.smul_hom_id_assoc - -@[to_additive] -instance : IsMulActionHom (𝟙 M) (𝟙 X) where - -@[to_additive] -instance (φ : M ⟶ N) (ψ : N ⟶ O) (f : X ⟶ Y) (g : Y ⟶ Z) [IsMulActionHom φ f] [IsMulActionHom ψ g] : - IsMulActionHom (φ ≫ ψ) (f ≫ g) where - smul_hom := by simp [smul_hom_assoc φ, smul_hom ψ] - -variable [MulActionObj M Y] [MulActionObj M Z] in -@[to_additive] -instance (f : X ⟶ Y) (g : Y ⟶ Z) [IsMulActionHom (𝟙 M) f] [IsMulActionHom (𝟙 M) g] : - IsMulActionHom (𝟙 M) (f ≫ g) where - -end IsMulActionHom - -namespace Hom - -variable (M X) in -/-- Morphisms `Y ⟶ M` act on morphisms `Y ⟶ X` via the internal scalar multiplication. -/ -@[to_additive /-- Morphisms `Y ⟶ M` act on morphisms `Y ⟶ X` via the internal additive action. -/] -instance (Y : C) : SMul (Y ⟶ M) (Y ⟶ X) where - smul m x := lift m x ≫ MulActionObj.smul - -@[to_additive] -lemma smul_def {Y : C} (m : Y ⟶ M) (x : Y ⟶ X) : m • x = lift m x ≫ MulActionObj.smul := - rfl - -/-- If `M` is a monoid object acting on `X`, then morphisms into `M` act on -morphisms into `X`. -/ -@[to_additive /-- If `M` is an additive monoid object acting on `X`, then morphisms into `M` act on -morphisms into `X`. -/] -instance mulAction (Y : C) : MulAction (Y ⟶ M) (Y ⟶ X) where - smul m x := lift m x ≫ MulActionObj.smul - one_smul x := by - rw [one_def, smul_def, ← lift_whiskerRight, Category.assoc] - simp - mul_smul m n x := by - rw [mul_def, smul_def, ← lift_whiskerRight, Category.assoc] - simp [smul_def, MulActionObj.mul_smul] - -@[to_additive] -lemma map_smul (φ : M ⟶ N) (f : X ⟶ Y) [IsMulActionHom φ f] {Z : C} (m : Z ⟶ M) (x : Z ⟶ X) : - (m • x) ≫ f = m ≫ φ • x ≫ f := by - simp [smul_def, Category.assoc, IsMulActionHom.smul_hom φ] - -/-- A `φ`-equivariant morphism induces an equivariant morphism on hom types. -/ -@[to_additive /-- A `φ`-equivariant morphism induces an equivariant morphism on hom types. -/] -def mulActionHom (φ : M ⟶ N) (f : X ⟶ Y) [IsMulActionHom φ f] (Z : C) : - MulActionHom (· ≫ φ : (Z ⟶ M) → _) (Z ⟶ X) (Z ⟶ Y) where - toFun := (· ≫ f) - map_smul' := map_smul φ f - -end Hom - -end CategoryTheory From ef7b4965e3d21a8992aee81fc8a8343786dfdabf Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Wed, 6 May 2026 21:18:22 +0200 Subject: [PATCH 5/6] add name --- Mathlib/CategoryTheory/Monoidal/Cartesian/Mod.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Monoidal/Cartesian/Mod.lean b/Mathlib/CategoryTheory/Monoidal/Cartesian/Mod.lean index 67608b3e4bab1d..8a0e6d1c041545 100644 --- a/Mathlib/CategoryTheory/Monoidal/Cartesian/Mod.lean +++ b/Mathlib/CategoryTheory/Monoidal/Cartesian/Mod.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2025 Paul Lezeau. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Paul Lezeau +Authors: Paul Lezeau, Christian Merten -/ module From 2fe48471325709972a1a73ab48584a9249c2a87b Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Thu, 7 May 2026 23:32:47 +0200 Subject: [PATCH 6/6] Update Mathlib/CategoryTheory/Monoidal/Cartesian/Mod.lean Co-authored-by: Dagur Asgeirsson --- Mathlib/CategoryTheory/Monoidal/Cartesian/Mod.lean | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/Mathlib/CategoryTheory/Monoidal/Cartesian/Mod.lean b/Mathlib/CategoryTheory/Monoidal/Cartesian/Mod.lean index 8a0e6d1c041545..4f01d4b744f8fd 100644 --- a/Mathlib/CategoryTheory/Monoidal/Cartesian/Mod.lean +++ b/Mathlib/CategoryTheory/Monoidal/Cartesian/Mod.lean @@ -60,12 +60,8 @@ morphisms into `X`. -/ @[to_additive /-- If `M` is an additive monoid object acting on `X`, then morphisms into `M` act on morphisms into `X`. -/] instance mulAction (Z : C) : MulAction (Z ⟶ M) (Z ⟶ X) where - one_smul x := by - rw [one_def, smul_def, ← lift_whiskerRight, Category.assoc] - simp - mul_smul m n x := by - rw [mul_def, smul_def, ← lift_whiskerRight, Category.assoc] - simp [smul_def] + one_smul x := by simp [one_def, smul_def, ← lift_whiskerRight] + mul_smul m n x := by simp [mul_def, smul_def, ← lift_whiskerRight] end Hom