Skip to content
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

[Merged by Bors] - feat: port CategoryTheory.Monoidal.Functorial #2504

Closed
wants to merge 6 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -274,6 +274,7 @@ import Mathlib.CategoryTheory.Limits.Cones
import Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
import Mathlib.CategoryTheory.Monoidal.Category
import Mathlib.CategoryTheory.Monoidal.Functor
import Mathlib.CategoryTheory.Monoidal.Functorial
import Mathlib.CategoryTheory.NatIso
import Mathlib.CategoryTheory.NatTrans
import Mathlib.CategoryTheory.Opposites
Expand Down
117 changes: 117 additions & 0 deletions Mathlib/CategoryTheory/Monoidal/Functorial.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,117 @@
/-
Copyright (c) 2019 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison

! This file was ported from Lean 3 source module category_theory.monoidal.functorial
! leanprover-community/mathlib commit 73dd4b5411ec8fafb18a9d77c9c826907730af80
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.CategoryTheory.Monoidal.Functor
import Mathlib.CategoryTheory.Functor.Functorial

/-!
# Unbundled lax monoidal functors

## Design considerations
The essential problem I've encountered that requires unbundled functors is
having an existing (non-monoidal) functor `F : C ⥤ D` between monoidal categories,
and wanting to assert that it has an extension to a lax monoidal functor.

The two options seem to be
1. Construct a separate `F' : LaxMonoidalFunctor C D`,
and assert `F'.toFunctor ≅ F`.
2. Introduce unbundled functors and unbundled lax monoidal functors,
and construct `LaxMonoidal F.obj`, then construct `F' := LaxMonoidalFunctor.of F.obj`.

Both have costs, but as for option 2. the cost is in library design,
while in option 1. the cost is users having to carry around additional isomorphisms forever,
I wanted to introduce unbundled functors.

TODO:
later, we may want to do this for strong monoidal functors as well,
but the immediate application, for enriched categories, only requires this notion.
-/


open CategoryTheory

universe v₁ v₂ v₃ u₁ u₂ u₃

open CategoryTheory.Category

open CategoryTheory.Functor

namespace CategoryTheory

open MonoidalCategory

variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C] {D : Type u₂} [Category.{v₂} D]
[MonoidalCategory.{v₂} D]

-- Perhaps in the future we'll redefine `LaxMonoidalFunctor` in terms of this,
-- but that isn't the immediate plan.
/-- An unbundled description of lax monoidal functors. -/
class LaxMonoidal (F : C → D) [Functorial.{v₁, v₂} F] where
/-- unit morphism -/
ε : 𝟙_ D ⟶ F (𝟙_ C)
/-- tensorator -/
μ : ∀ X Y : C, F X ⊗ F Y ⟶ F (X ⊗ Y)
/-- natuality -/
μ_natural :
∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
(map F f ⊗ map F g) ≫ μ Y Y' = μ X X' ≫ map F (f ⊗ g) := by
aesop_cat
/-- associativity of the tensorator -/
associativity :
∀ X Y Z : C,
(μ X Y ⊗ 𝟙 (F Z)) ≫ μ (X ⊗ Y) Z ≫ map F (α_ X Y Z).hom =
(α_ (F X) (F Y) (F Z)).hom ≫ (𝟙 (F X) ⊗ μ Y Z) ≫ μ X (Y ⊗ Z) := by
aesop_cat
/-- left unitality -/
left_unitality : ∀ X : C, (λ_ (F X)).hom = (ε ⊗ 𝟙 (F X)) ≫ μ (𝟙_ C) X ≫ map F (λ_ X).hom := by
aesop_cat
/-- right unitality -/
right_unitality : ∀ X : C, (ρ_ (F X)).hom = (𝟙 (F X) ⊗ ε) ≫ μ X (𝟙_ C) ≫ map F (ρ_ X).hom := by
aesop_cat
#align category_theory.lax_monoidal CategoryTheory.LaxMonoidal

attribute [simp] LaxMonoidal.μ_natural

attribute [simp] LaxMonoidal.μ_natural

-- The unitality axioms cannot be used as simp lemmas because they require
-- higher-order matching to figure out the `F` and `X` from `F X`.

attribute [simp] LaxMonoidal.associativity

namespace LaxMonoidalFunctor

/-- Construct a bundled `LaxMonoidalFunctor` from the object level function
and `Functorial` and `LaxMonoidal` typeclasses.
-/
@[simps]
def of (F : C → D) [I₁ : Functorial.{v₁, v₂} F] [I₂ : LaxMonoidal.{v₁, v₂} F] :
LaxMonoidalFunctor.{v₁, v₂} C D :=
{ I₁, I₂ with obj := F }
#align category_theory.lax_monoidal_functor.of CategoryTheory.LaxMonoidalFunctor.of

end LaxMonoidalFunctor

instance (F : LaxMonoidalFunctor.{v₁, v₂} C D) : LaxMonoidal.{v₁, v₂} F.obj :=
{ F with }

section

instance laxMonoidalId : LaxMonoidal.{v₁, v₁} (id : C → C)
where
ε := 𝟙 _
μ X Y := 𝟙 _
#align category_theory.lax_monoidal_id CategoryTheory.laxMonoidalId

end

-- TODO instances for composition, as required
-- TODO `StrongMonoidal`, as well as `LaxMonoidal`
end CategoryTheory