-
Notifications
You must be signed in to change notification settings - Fork 243
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(CategoryTheory): the monoidal category structure induced by a monoidal functor #12926
base: master
Are you sure you want to change the base?
Conversation
…d by a monoidal functor
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
noncomputable instance : MonoidalCategory (InducedCategory D F.obj) where | ||
tensor_id X Y := by | ||
dsimp [inducedCategoryMonoidal] | ||
erw [tensor_id] | ||
simp | ||
rfl | ||
tensor_comp := sorry | ||
tensorHom_def := sorry | ||
whiskerLeft_id X Y := by | ||
dsimp [inducedCategoryMonoidal] | ||
erw [whiskerLeft_id] | ||
simp | ||
rfl | ||
id_whiskerRight X Y := by | ||
dsimp [inducedCategoryMonoidal] | ||
erw [id_whiskerRight] | ||
simp | ||
rfl | ||
associator_naturality := sorry | ||
leftUnitor_naturality := sorry | ||
rightUnitor_naturality := sorry | ||
pentagon X Y Z T := by | ||
dsimp [inducedCategoryMonoidal, homMk] | ||
simp only [LaxMonoidalFunctor.μ_natural_left, MonoidalFunctor.μ_inv_hom_id_assoc, | ||
LaxMonoidalFunctor.μ_natural_right] | ||
erw [← F.map_comp, ← F.map_comp, ← F.map_comp] | ||
simp | ||
triangle X Y := by | ||
dsimp [inducedCategoryMonoidal, homMk] | ||
simp only [LaxMonoidalFunctor.μ_natural_right, MonoidalFunctor.μ_inv_hom_id_assoc, | ||
LaxMonoidalFunctor.μ_natural_left] | ||
erw [← F.map_comp] | ||
simp |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Isn't this
noncomputable instance : MonoidalCategory (InducedCategory D F.obj) :=
CategoryTheory.Monoidal.induced (inducedFunctor F.obj) {
μIso := fun X Y => F.μIso X Y
εIso := F.εIso
}
with some proof fields / extra simp
lemmas / explicit casts? (and import Mathlib.CategoryTheory.Monoidal.Transport
)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks very much indeed! I am sorry I had overlooked your remark: I was confused because of the two steps construction (first the MonoidalCategoryStruct
and then the verification of the axioms).
In this PR, given a monoidal functor
F : MonoidalFunctor C D
, we define a monoidal category structure on the categoryInducedCategory D F.obj
, which has the "same" objects asC
, but the morphisms betweenX
andY
identify toF.obj X ⟶ F.obj Y
.