Skip to content

Commit 34a002f

Browse files
mckoenmckoen
committed
feat(CategoryTheory/Monoidal/Arrow): define monoidal structure on arrow category (#33935)
defines a monoidal category structure on the arrow category of a cartesian closed category.
1 parent a8913b9 commit 34a002f

File tree

6 files changed

+659
-0
lines changed

6 files changed

+659
-0
lines changed

‎Mathlib.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2978,6 +2978,7 @@ public import Mathlib.CategoryTheory.Monoidal.Action.Basic
29782978
public import Mathlib.CategoryTheory.Monoidal.Action.End
29792979
public import Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
29802980
public import Mathlib.CategoryTheory.Monoidal.Action.Opposites
2981+
public import Mathlib.CategoryTheory.Monoidal.Arrow
29812982
public import Mathlib.CategoryTheory.Monoidal.Bimod
29822983
public import Mathlib.CategoryTheory.Monoidal.Bimon_
29832984
public import Mathlib.CategoryTheory.Monoidal.Braided.Basic
@@ -3001,6 +3002,7 @@ public import Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
30013002
public import Mathlib.CategoryTheory.Monoidal.Category
30023003
public import Mathlib.CategoryTheory.Monoidal.Center
30033004
public import Mathlib.CategoryTheory.Monoidal.Closed.Basic
3005+
public import Mathlib.CategoryTheory.Monoidal.Closed.Braided
30043006
public import Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
30053007
public import Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
30063008
public import Mathlib.CategoryTheory.Monoidal.Closed.Functor
@@ -3042,7 +3044,9 @@ public import Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp_
30423044
public import Mathlib.CategoryTheory.Monoidal.Limits.Basic
30433045
public import Mathlib.CategoryTheory.Monoidal.Limits.Cokernels
30443046
public import Mathlib.CategoryTheory.Monoidal.Limits.Colimits
3047+
public import Mathlib.CategoryTheory.Monoidal.Limits.HasLimits
30453048
public import Mathlib.CategoryTheory.Monoidal.Limits.Preserves
3049+
public import Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
30463050
public import Mathlib.CategoryTheory.Monoidal.Linear
30473051
public import Mathlib.CategoryTheory.Monoidal.Mod_
30483052
public import Mathlib.CategoryTheory.Monoidal.Mon_
@@ -3052,6 +3056,7 @@ public import Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
30523056
public import Mathlib.CategoryTheory.Monoidal.Opposite
30533057
public import Mathlib.CategoryTheory.Monoidal.Opposite.Mon_
30543058
public import Mathlib.CategoryTheory.Monoidal.Preadditive
3059+
public import Mathlib.CategoryTheory.Monoidal.PushoutProduct
30553060
public import Mathlib.CategoryTheory.Monoidal.Rigid.Basic
30563061
public import Mathlib.CategoryTheory.Monoidal.Rigid.Braided
30573062
public import Mathlib.CategoryTheory.Monoidal.Rigid.Functor

‎Mathlib/CategoryTheory/Monoidal/Arrow.lean‎

Lines changed: 158 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,158 @@
1+
/-
2+
Copyright (c) 2026 Jack McKoen. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Jack McKoen
5+
-/
6+
module
7+
8+
public import Mathlib.CategoryTheory.Monoidal.Closed.Braided
9+
public import Mathlib.CategoryTheory.Monoidal.Limits.HasLimits
10+
public import Mathlib.CategoryTheory.Monoidal.PushoutProduct
11+
12+
/-!
13+
# Monoidal structure on the arrow category of a cartesian closed category.
14+
15+
If `C` is a braided, cartesian closed category with pushouts and an initial object, then `Arrow C`
16+
has a symmetric monoidal category structure given by the pushout-product (the Leibniz construction
17+
given by the tensor product on `C`).
18+
19+
If `C` also has pullbacks, then `Arrow C` has a monoidal closed structure given by the pullback-hom
20+
(the Leibniz construction given by the internal hom on `C`).
21+
22+
-/
23+
24+
@[expose] public section
25+
26+
universe v u
27+
28+
namespace CategoryTheory
29+
30+
open Limits MonoidalCategory Functor PushoutObjObj
31+
32+
variable {C : Type u} [Category.{v} C]
33+
34+
attribute [local simp] PushoutObjObj.ι ofHasPushout_pt ofHasPushout_inl ofHasPushout_inr
35+
36+
namespace MonoidalCategory.Arrow.PushoutProduct
37+
38+
noncomputable section
39+
40+
/-- The monoidal category instance induced by the pushout-product. -/
41+
@[simps]
42+
scoped instance [HasPushouts C] [HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C]
43+
[BraidedCategory C] : MonoidalCategoryStruct (Arrow C) where
44+
tensorObj X Y := X □ Y
45+
whiskerLeft X _ _ f := (pushoutProduct.obj X).map f
46+
whiskerRight f X := (pushoutProduct.map f).app X
47+
tensorUnit := initial.to (𝟙_ C)
48+
associator _ _ _ := PushoutProduct.associator ..
49+
leftUnitor := PushoutProduct.leftUnitor
50+
rightUnitor := PushoutProduct.rightUnitor
51+
52+
variable [HasPushouts C] [HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C]
53+
[BraidedCategory C]
54+
55+
lemma tensorHom_comp_tensorHom {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Arrow C}
56+
(f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) :
57+
(f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = (f₁ ≫ g₁) ⊗ₘ (f₂ ≫ g₂) := by
58+
refine Arrow.hom_ext _ _ ?_ (by simp [whisker_exchange_assoc])
59+
apply pushout.hom_ext <;> simp [whisker_exchange_assoc]
60+
61+
set_option backward.isDefEq.respectTransparency false in
62+
lemma associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C}
63+
(f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
64+
((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ (f₂ ⊗ₘ f₃)) := by
65+
refine Arrow.hom_ext _ _ (pushout.hom_ext (by simp [whisker_exchange_assoc]) ?_) (by simp)
66+
apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
67+
· suffices _ ◁ _ ◁ f₃.right ≫ (α_ _ _ _).inv ≫ f₁.right ▷ _ ▷ _ ≫ (α_ _ _ _).hom ≫
68+
_ ◁ f₂.left ▷ _ ≫ _ ◁ pushout.inr _ _ = _ ◁ f₂.left ▷ _ ≫ _ ◁ _ ◁ f₃.right ≫
69+
_ ◁ pushout.inr _ _ ≫ f₁.right ▷ pushout (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom) by
70+
simp [← whisker_exchange_assoc, reassoc_of% this]
71+
rw [← MonoidalCategory.whiskerLeft_comp_assoc, whisker_exchange, whisker_exchange_assoc,
72+
← whisker_exchange, associator_inv_naturality_right_assoc, whisker_exchange_assoc,
73+
← associator_inv_naturality_left_assoc, associator_naturality_right_assoc,
74+
Iso.inv_hom_id_assoc, MonoidalCategory.whiskerLeft_comp_assoc]
75+
· suffices ((α_ _ _ _).hom ≫ _ ◁ _ ◁ f₃.right ≫ (α_ _ _ _).inv ≫ f₁.left ▷ _ ▷ _ ≫
76+
(α_ _ _ _).hom ≫ _ ◁ f₂.right ▷ _ = f₁.left ▷ _ ▷ _ ≫ (α_ _ _ _).hom ≫
77+
_ ◁ f₂.right ▷ _ ≫ _ ◁ _ ◁ f₃.right) by
78+
simp [← whisker_exchange_assoc, reassoc_of% this]
79+
cat_disch
80+
81+
set_option backward.isDefEq.respectTransparency false in
82+
lemma leftUnitor_naturality {X Y : Arrow C} (f : X ⟶ Y) :
83+
𝟙_ _ ◁ f ≫ (λ_ Y).hom = (λ_ X).hom ≫ f := by
84+
refine Arrow.hom_ext _ _ (pushout.hom_ext (by simp) ?_) (by simp)
85+
apply (initialIsInitial.ofIso (mulZero initialIsInitial).symm).hom_ext
86+
87+
set_option backward.isDefEq.respectTransparency false in
88+
lemma rightUnitor_naturality {X Y : Arrow C} (f : X ⟶ Y) :
89+
f ▷ 𝟙_ _ ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f := by
90+
refine Arrow.hom_ext _ _ (pushout.hom_ext ?_ (by simp)) (by simp)
91+
apply (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).hom_ext
92+
93+
set_option backward.isDefEq.respectTransparency false in
94+
lemma pentagon (W X Y Z : Arrow C) :
95+
(α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom =
96+
(α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom := by
97+
refine Arrow.hom_ext _ _ (pushout.hom_ext (by simp) ?_) (by simp)
98+
apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext (by simp)
99+
apply ((tensorRight _ ⋙ tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext <;>
100+
simp [associator_naturality_left_assoc]
101+
102+
set_option backward.isDefEq.respectTransparency false in
103+
lemma triangle (X Y : Arrow C) :
104+
(α_ X (𝟙_ _) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y := by
105+
refine Arrow.hom_ext _ _ (pushout.hom_ext (by simp) ?_) (by simp)
106+
apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
107+
· apply (initialIsInitial.ofIso ((initialIsoIsInitial ?_) ≪≫ (mulZero ?_).symm)).hom_ext <;>
108+
exact initialIsInitial.ofIso (zeroMul initialIsInitial).symm
109+
· simp [← comp_whiskerRight_assoc]
110+
111+
/-- The monoidal category instance induced by the pushout-product. -/
112+
scoped instance : MonoidalCategory (Arrow C) where
113+
tensorHom_comp_tensorHom := tensorHom_comp_tensorHom
114+
associator_naturality := associator_naturality
115+
leftUnitor_naturality := leftUnitor_naturality
116+
rightUnitor_naturality := rightUnitor_naturality
117+
pentagon := pentagon
118+
triangle := triangle
119+
120+
set_option backward.isDefEq.respectTransparency false in
121+
lemma hexagon_forward (X Y Z : Arrow C) :
122+
(α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom =
123+
((braiding X Y).hom ▷ Z) ≫ (α_ Y X Z).hom ≫ (Y ◁ (braiding X Z).hom) := by
124+
refine Arrow.hom_ext _ _ (pushout.hom_ext (by simp) ?_) (by simp)
125+
apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext <;> simp
126+
127+
set_option backward.isDefEq.respectTransparency false in
128+
lemma hexagon_reverse (X Y Z : Arrow C) :
129+
(α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv =
130+
(X ◁ (braiding Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((braiding X Z).hom ▷ Y) := by
131+
refine Arrow.hom_ext _ _ (pushout.hom_ext ?_ (by simp)) (by simp)
132+
apply ((tensorLeft _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext <;> simp
133+
134+
set_option backward.isDefEq.respectTransparency false in
135+
/-- The braided category instance induced by the pushout-product. -/
136+
@[simps -isSimp]
137+
scoped instance braidedCategory : BraidedCategory (Arrow C) where
138+
braiding := braiding
139+
hexagon_forward := hexagon_forward
140+
hexagon_reverse := hexagon_reverse
141+
142+
set_option backward.isDefEq.respectTransparency false in
143+
attribute [local simp] braidedCategory_braiding in
144+
/-- The symmetric category instance induced by the pushout-product. -/
145+
@[simps! -isSimp]
146+
scoped instance symmetricCategory : SymmetricCategory (Arrow C) where
147+
148+
/-- The monoidal closed instance induced by the pushout-product and pullback-hom. -/
149+
scoped instance [HasPullbacks C] : MonoidalClosed (Arrow C) where
150+
closed X := {
151+
rightAdj := pullbackHom.obj (Opposite.op X)
152+
adj := LeibnizAdjunction.adj _ _ (MonoidalClosed.internalHomAdjunction₂) X }
153+
154+
end
155+
156+
end MonoidalCategory.Arrow.PushoutProduct
157+
158+
end CategoryTheory

‎Mathlib/CategoryTheory/Monoidal/Closed/Braided.lean‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
/-
2+
Copyright (c) 2026 Jack McKoen. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Jack McKoen
5+
-/
6+
module
7+
8+
public import Mathlib.CategoryTheory.Monoidal.Braided.Basic
9+
public import Mathlib.CategoryTheory.Monoidal.Closed.Basic
10+
11+
/-!
12+
# Closed braided monoidal categories
13+
14+
Interactions between monoidal closed and braided category structures.
15+
16+
-/
17+
18+
@[expose] public section
19+
20+
universe v u u₂ v₂
21+
22+
namespace CategoryTheory
23+
24+
open Category MonoidalCategory
25+
26+
variable {C : Type u} [Category.{v} C] [MonoidalCategory C]
27+
28+
namespace ihom
29+
30+
instance [BraidedCategory C] (A : C) [Closed A] :
31+
(tensorRight A).IsLeftAdjoint :=
32+
Functor.isLeftAdjoint_of_iso (BraidedCategory.tensorLeftIsoTensorRight A)
33+
34+
end ihom
35+
36+
end CategoryTheory

‎Mathlib/CategoryTheory/Monoidal/Limits/HasLimits.lean‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
/-
2+
Copyright (c) 2026 Jack McKoen. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Jack McKoen
5+
-/
6+
module
7+
8+
public import Mathlib.CategoryTheory.Limits.HasLimits
9+
public import Mathlib.CategoryTheory.Monoidal.Category
10+
11+
/-!
12+
# Compatibility lemmas for limits and colimits in a monoidal category
13+
14+
For numerous simp lemmas of the form `f ≫ g = h`, we add accompanying simp lemmas of the form
15+
`Q ◁ f ≫ Q ◁ g = Q ◁ h` and `f ▷ Q ≫ g ▷ Q = h ▷ Q`. This file and
16+
`Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback` are needed to define a monoidal category
17+
structure in `Mathlib.CategoryTheory.Monoidal.Arrow`.
18+
19+
## TODO
20+
An attribute should be developed to automatically generate lemmas of this form.
21+
-/
22+
23+
@[expose] public section
24+
25+
universe v v₁ u u₁
26+
27+
namespace CategoryTheory.MonoidalCategory
28+
29+
open Limits MonoidalCategory
30+
31+
variable {C : Type u} [Category.{v} C] [MonoidalCategory C]
32+
33+
namespace Limits
34+
35+
section HasColimit
36+
37+
variable {J : Type u₁} [Category.{v₁} J]
38+
{F G : J ⥤ C} [HasColimit F] [HasColimit G]
39+
40+
@[reassoc (attr := simp)]
41+
lemma HasColimit.whiskerLeft_isoOfNatIso_ι_hom (w : F ≅ G) (j : J) {Q : C} :
42+
Q ◁ colimit.ι F j ≫ Q ◁ (HasColimit.isoOfNatIso w).hom =
43+
Q ◁ w.hom.app j ≫ Q ◁ colimit.ι G j := by
44+
simp [← MonoidalCategory.whiskerLeft_comp]
45+
46+
@[reassoc (attr := simp)]
47+
lemma HasColimit.isoOfNatIso_ι_hom_whiskerRight (w : F ≅ G) (j : J) {Q : C} :
48+
colimit.ι F j ▷ Q ≫ (HasColimit.isoOfNatIso w).hom ▷ Q =
49+
w.hom.app j ▷ Q ≫ colimit.ι G j ▷ Q := by
50+
simp [← MonoidalCategory.comp_whiskerRight]
51+
52+
@[reassoc (attr := simp)]
53+
lemma colimit.whiskerLeft_ι_desc (c : Cocone F) (j : J) {Q : C} :
54+
Q ◁ colimit.ι F j ≫ Q ◁ colimit.desc F c = Q ◁ c.ι.app j := by
55+
simp [← MonoidalCategory.whiskerLeft_comp]
56+
57+
@[reassoc (attr := simp)]
58+
lemma colimit.ι_desc_whiskerRight (c : Cocone F) (j : J) {Q : C} :
59+
colimit.ι F j ▷ Q ≫ colimit.desc F c ▷ Q = c.ι.app j ▷ Q := by
60+
simp [← comp_whiskerRight]
61+
62+
end HasColimit
63+
64+
end Limits
65+
66+
end CategoryTheory.MonoidalCategory

0 commit comments

Comments
 (0)
⚡