Monoids as discrete monoidal categories #
The discrete category on a monoid is a monoidal category. Multiplicative morphisms induced monoidal functors.
theorem
CategoryTheory.Discrete.addMonoidal.proof_6
(M : Type u_1)
[AddMonoid M]
(X : CategoryTheory.Discrete M)
:
theorem
CategoryTheory.Discrete.addMonoidal.proof_1
(M : Type u_1)
[AddMonoid M]
(X : CategoryTheory.Discrete M)
:
∀ (x x_1 : CategoryTheory.Discrete M),
(x ⟶ x_1) →
(fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X x = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X x_1
theorem
CategoryTheory.Discrete.addMonoidal.proof_9
(M : Type u_1)
[AddMonoid M]
{X₁ : CategoryTheory.Discrete M}
{Y₁ : CategoryTheory.Discrete M}
{Z₁ : CategoryTheory.Discrete M}
{X₂ : CategoryTheory.Discrete M}
{Y₂ : CategoryTheory.Discrete M}
{Z₂ : CategoryTheory.Discrete M}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₂)
(g₁ : Y₁ ⟶ Z₁)
(g₂ : Y₂ ⟶ Z₂)
:
theorem
CategoryTheory.Discrete.addMonoidal.proof_15
(M : Type u_1)
[AddMonoid M]
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
:
theorem
CategoryTheory.Discrete.addMonoidal.proof_5
(M : Type u_1)
[AddMonoid M]
(X : CategoryTheory.Discrete M)
:
theorem
CategoryTheory.Discrete.addMonoidal.proof_8
(M : Type u_1)
[AddMonoid M]
(X₁ : CategoryTheory.Discrete M)
(X₂ : CategoryTheory.Discrete M)
:
CategoryTheory.CategoryStruct.id { as := X₁.as + X₂.as } = CategoryTheory.CategoryStruct.id { as := X₁.as + X₂.as }
theorem
CategoryTheory.Discrete.addMonoidal.proof_3
(M : Type u_1)
[AddMonoid M]
:
∀ {X₁ Y₁ X₂ Y₂ : CategoryTheory.Discrete M},
(X₁ ⟶ Y₁) →
(X₂ ⟶ Y₂) →
(fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X₁ X₂ = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) Y₁ Y₂
theorem
CategoryTheory.Discrete.addMonoidal.proof_14
(M : Type u_1)
[AddMonoid M]
(W : CategoryTheory.Discrete M)
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
(Z : CategoryTheory.Discrete M)
:
theorem
CategoryTheory.Discrete.addMonoidal.proof_11
(M : Type u_1)
[AddMonoid M]
{X₁ : CategoryTheory.Discrete M}
{X₂ : CategoryTheory.Discrete M}
{X₃ : CategoryTheory.Discrete M}
{Y₁ : CategoryTheory.Discrete M}
{Y₂ : CategoryTheory.Discrete M}
{Y₃ : CategoryTheory.Discrete M}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₂)
(f₃ : X₃ ⟶ Y₃)
:
theorem
CategoryTheory.Discrete.addMonoidal.proof_12
(M : Type u_1)
[AddMonoid M]
{X : CategoryTheory.Discrete M}
{Y : CategoryTheory.Discrete M}
(f : X ⟶ Y)
:
theorem
CategoryTheory.Discrete.addMonoidal.proof_2
(M : Type u_1)
[AddMonoid M]
:
∀ {X₁ X₂ : CategoryTheory.Discrete M},
(X₁ ⟶ X₂) →
∀ (X : CategoryTheory.Discrete M),
(fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X₁ X = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X₂ X
theorem
CategoryTheory.Discrete.addMonoidal.proof_13
(M : Type u_1)
[AddMonoid M]
{X : CategoryTheory.Discrete M}
{Y : CategoryTheory.Discrete M}
(f : X ⟶ Y)
:
theorem
CategoryTheory.Discrete.addMonoidal.proof_10
(M : Type u_1)
[AddMonoid M]
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
:
CategoryTheory.CategoryStruct.id { as := X.as + Y.as } = CategoryTheory.CategoryStruct.id { as := X.as + Y.as }
theorem
CategoryTheory.Discrete.addMonoidal.proof_7
(M : Type u_1)
[AddMonoid M]
{X₁ : CategoryTheory.Discrete M}
{Y₁ : CategoryTheory.Discrete M}
{X₂ : CategoryTheory.Discrete M}
{Y₂ : CategoryTheory.Discrete M}
(f : X₁ ⟶ Y₁)
(g : X₂ ⟶ Y₂)
:
Equations
- CategoryTheory.Discrete.addMonoidal M = CategoryTheory.MonoidalCategory.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
theorem
CategoryTheory.Discrete.addMonoidal.proof_4
(M : Type u_1)
[AddMonoid M]
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
(Z : CategoryTheory.Discrete M)
:
@[simp]
theorem
CategoryTheory.Discrete.monoidal_leftUnitor
(M : Type u)
[Monoid M]
(X : CategoryTheory.Discrete M)
:
@[simp]
@[simp]
theorem
CategoryTheory.Discrete.monoidal_associator
(M : Type u)
[Monoid M]
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
(Z : CategoryTheory.Discrete M)
:
@[simp]
theorem
CategoryTheory.Discrete.monoidal_tensorObj_as
(M : Type u)
[Monoid M]
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
:
(CategoryTheory.MonoidalCategory.tensorObj X Y).as = X.as * Y.as
@[simp]
theorem
CategoryTheory.Discrete.monoidal_rightUnitor
(M : Type u)
[Monoid M]
(X : CategoryTheory.Discrete M)
:
@[simp]
theorem
CategoryTheory.Discrete.addMonoidal_associator
(M : Type u)
[AddMonoid M]
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
(Z : CategoryTheory.Discrete M)
:
@[simp]
theorem
CategoryTheory.Discrete.addMonoidal_leftUnitor
(M : Type u)
[AddMonoid M]
(X : CategoryTheory.Discrete M)
:
@[simp]
theorem
CategoryTheory.Discrete.addMonoidal_tensorObj_as
(M : Type u)
[AddMonoid M]
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
:
(CategoryTheory.MonoidalCategory.tensorObj X Y).as = X.as + Y.as
Equations
- CategoryTheory.Discrete.monoidal M = CategoryTheory.MonoidalCategory.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
@[simp]
theorem
CategoryTheory.Discrete.addMonoidal_tensorUnit_as
(M : Type u)
[AddMonoid M]
:
(𝟙_ (CategoryTheory.Discrete M)).as = 0
@[simp]
theorem
CategoryTheory.Discrete.monoidal_tensorUnit_as
(M : Type u)
[Monoid M]
:
(𝟙_ (CategoryTheory.Discrete M)).as = 1
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_5
{M : Type u_2}
[AddMonoid M]
{N : Type u_1}
[AddMonoid N]
(F : M →+ N)
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
:
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_2
{M : Type u_1}
[AddMonoid M]
{N : Type u_2}
[AddMonoid N]
(F : M →+ N)
(X : CategoryTheory.Discrete M)
:
CategoryTheory.CategoryStruct.id { as := F X.as } = CategoryTheory.CategoryStruct.id { as := F X.as }
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_10
{M : Type u_1}
[AddMonoid M]
{N : Type u_2}
[AddMonoid N]
(F : M →+ N)
(X : CategoryTheory.Discrete M)
:
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_7
{M : Type u_1}
[AddMonoid M]
{N : Type u_2}
[AddMonoid N]
(F : M →+ N)
{X : CategoryTheory.Discrete M}
{Y : CategoryTheory.Discrete M}
(X' : CategoryTheory.Discrete M)
(f : X ⟶ Y)
:
def
CategoryTheory.Discrete.addMonoidalFunctor
{M : Type u}
[AddMonoid M]
{N : Type u'}
[AddMonoid N]
(F : M →+ N)
:
An additive morphism between add_monoids gives a monoidal functor between the corresponding discrete monoidal categories.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_12
{M : Type u_1}
[AddMonoid M]
{N : Type u_2}
[AddMonoid N]
(F : M →+ N)
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
:
CategoryTheory.IsIso
({ obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as },
map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom ⋯, map_id := ⋯,
map_comp := ⋯, ε := CategoryTheory.Discrete.eqToHom ⋯,
μ := fun (X Y : CategoryTheory.Discrete M) => CategoryTheory.Discrete.eqToHom ⋯, μ_natural_left := ⋯,
μ_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯, right_unitality := ⋯ }.μ
X Y)
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_6
{M : Type u_1}
[AddMonoid M]
{N : Type u_2}
[AddMonoid N]
(F : M →+ N)
{X : CategoryTheory.Discrete M}
{Y : CategoryTheory.Discrete M}
(f : X ⟶ Y)
(X' : CategoryTheory.Discrete M)
:
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_8
{M : Type u_1}
[AddMonoid M]
{N : Type u_2}
[AddMonoid N]
(F : M →+ N)
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
(Z : CategoryTheory.Discrete M)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.eqToHom ⋯) { as := F Z.as })
(CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerLeft { as := F X.as } (CategoryTheory.eqToHom ⋯))
(CategoryTheory.Discrete.eqToHom ⋯))
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_3
{M : Type u_1}
[AddMonoid M]
{N : Type u_2}
[AddMonoid N]
(F : M →+ N)
{X : CategoryTheory.Discrete M}
{Y : CategoryTheory.Discrete M}
{Z : CategoryTheory.Discrete M}
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_11
{M : Type u_2}
[AddMonoid M]
{N : Type u_1}
[AddMonoid N]
(F : M →+ N)
:
CategoryTheory.IsIso
{ obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as },
map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom ⋯, map_id := ⋯,
map_comp := ⋯, ε := CategoryTheory.Discrete.eqToHom ⋯,
μ := fun (X Y : CategoryTheory.Discrete M) => CategoryTheory.Discrete.eqToHom ⋯, μ_natural_left := ⋯,
μ_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯, right_unitality := ⋯ }.ε
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_9
{M : Type u_1}
[AddMonoid M]
{N : Type u_2}
[AddMonoid N]
(F : M →+ N)
(X : CategoryTheory.Discrete M)
:
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_1
{M : Type u_2}
[AddMonoid M]
{N : Type u_1}
[AddMonoid N]
(F : M →+ N)
:
∀ {X Y : CategoryTheory.Discrete M}, (X ⟶ Y) → F X.as = F Y.as
@[simp]
theorem
CategoryTheory.Discrete.addMonoidalFunctor_toLaxMonoidalFunctor_toFunctor_obj_as
{M : Type u}
[AddMonoid M]
{N : Type u'}
[AddMonoid N]
(F : M →+ N)
(X : CategoryTheory.Discrete M)
:
((CategoryTheory.Discrete.addMonoidalFunctor F).obj X).as = F X.as
@[simp]
theorem
CategoryTheory.Discrete.addMonoidalFunctor_toLaxMonoidalFunctor_toFunctor_map
{M : Type u}
[AddMonoid M]
{N : Type u'}
[AddMonoid N]
(F : M →+ N)
:
∀ {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y),
(CategoryTheory.Discrete.addMonoidalFunctor F).map f = CategoryTheory.Discrete.eqToHom ⋯
@[simp]
theorem
CategoryTheory.Discrete.monoidalFunctor_toLaxMonoidalFunctor_toFunctor_obj_as
{M : Type u}
[Monoid M]
{N : Type u'}
[Monoid N]
(F : M →* N)
(X : CategoryTheory.Discrete M)
:
((CategoryTheory.Discrete.monoidalFunctor F).obj X).as = F X.as
@[simp]
theorem
CategoryTheory.Discrete.monoidalFunctor_toLaxMonoidalFunctor_toFunctor_map
{M : Type u}
[Monoid M]
{N : Type u'}
[Monoid N]
(F : M →* N)
:
∀ {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y),
(CategoryTheory.Discrete.monoidalFunctor F).map f = CategoryTheory.Discrete.eqToHom ⋯
@[simp]
theorem
CategoryTheory.Discrete.addMonoidalFunctor_toLaxMonoidalFunctor_μ
{M : Type u}
[AddMonoid M]
{N : Type u'}
[AddMonoid N]
(F : M →+ N)
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
:
@[simp]
theorem
CategoryTheory.Discrete.monoidalFunctor_toLaxMonoidalFunctor_μ
{M : Type u}
[Monoid M]
{N : Type u'}
[Monoid N]
(F : M →* N)
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
:
def
CategoryTheory.Discrete.monoidalFunctor
{M : Type u}
[Monoid M]
{N : Type u'}
[Monoid N]
(F : M →* N)
:
A multiplicative morphism between monoids gives a monoidal functor between the corresponding discrete monoidal categories.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Discrete.addMonoidalFunctorComp.proof_7
{M : Type u_1}
[AddMonoid M]
{N : Type u_2}
[AddMonoid N]
{K : Type u_1}
[AddMonoid K]
(F : M →+ N)
(G : N →+ K)
:
CategoryTheory.CategoryStruct.comp
{
app := fun (X : CategoryTheory.Discrete M) =>
CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor F ⊗⋙ CategoryTheory.Discrete.addMonoidalFunctor G).obj X),
naturality := ⋯, unit := ⋯, tensor := ⋯ }
{
app := fun (X : CategoryTheory.Discrete M) =>
CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (G.comp F)).obj X),
naturality := ⋯, unit := ⋯, tensor := ⋯ } = CategoryTheory.CategoryStruct.id
(CategoryTheory.Discrete.addMonoidalFunctor F ⊗⋙ CategoryTheory.Discrete.addMonoidalFunctor G)
theorem
CategoryTheory.Discrete.addMonoidalFunctorComp.proof_2
{M : Type u_1}
[AddMonoid M]
{N : Type u_2}
[AddMonoid N]
{K : Type u_1}
[AddMonoid K]
(F : M →+ N)
(G : N →+ K)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯))
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor G).obj
((CategoryTheory.Discrete.addMonoidalFunctor F).obj (𝟙_ (CategoryTheory.Discrete M))))) = CategoryTheory.Discrete.eqToHom ⋯
theorem
CategoryTheory.Discrete.addMonoidalFunctorComp.proof_8
{M : Type u_1}
[AddMonoid M]
{N : Type u_2}
[AddMonoid N]
{K : Type u_1}
[AddMonoid K]
(F : M →+ N)
(G : N →+ K)
:
CategoryTheory.CategoryStruct.comp
{
app := fun (X : CategoryTheory.Discrete M) =>
CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (G.comp F)).obj X),
naturality := ⋯, unit := ⋯, tensor := ⋯ }
{
app := fun (X : CategoryTheory.Discrete M) =>
CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor F ⊗⋙ CategoryTheory.Discrete.addMonoidalFunctor G).obj X),
naturality := ⋯, unit := ⋯, tensor := ⋯ } = CategoryTheory.CategoryStruct.id (CategoryTheory.Discrete.addMonoidalFunctor (G.comp F))
theorem
CategoryTheory.Discrete.addMonoidalFunctorComp.proof_4
{M : Type u_1}
[AddMonoid M]
{N : Type u_2}
[AddMonoid N]
{K : Type u_1}
[AddMonoid K]
(F : M →+ N)
(G : N →+ K)
⦃X : CategoryTheory.Discrete M⦄
⦃Y : CategoryTheory.Discrete M⦄
(f : X ⟶ Y)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Discrete.eqToHom ⋯)
(CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (G.comp F)).obj Y)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (G.comp F)).obj X))
(CategoryTheory.Discrete.eqToHom ⋯)
theorem
CategoryTheory.Discrete.addMonoidalFunctorComp.proof_3
{M : Type u_1}
[AddMonoid M]
{N : Type u_2}
[AddMonoid N]
{K : Type u_1}
[AddMonoid K]
(F : M →+ N)
(G : N →+ K)
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯))
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor G).obj
((CategoryTheory.Discrete.addMonoidalFunctor F).obj (CategoryTheory.MonoidalCategory.tensorObj X Y)))) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor G).obj ((CategoryTheory.Discrete.addMonoidalFunctor F).obj X)))
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor G).obj ((CategoryTheory.Discrete.addMonoidalFunctor F).obj Y))))
(CategoryTheory.Discrete.eqToHom ⋯)
theorem
CategoryTheory.Discrete.addMonoidalFunctorComp.proof_6
{M : Type u_1}
[AddMonoid M]
{N : Type u_2}
[AddMonoid N]
{K : Type u_1}
[AddMonoid K]
(F : M →+ N)
(G : N →+ K)
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Discrete.eqToHom ⋯)
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor (G.comp F)).obj (CategoryTheory.MonoidalCategory.tensorObj X Y))) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom
(CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (G.comp F)).obj X))
(CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (G.comp F)).obj Y)))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯))
def
CategoryTheory.Discrete.addMonoidalFunctorComp
{M : Type u}
[AddMonoid M]
{N : Type u'}
[AddMonoid N]
{K : Type u}
[AddMonoid K]
(F : M →+ N)
(G : N →+ K)
:
The monoidal natural isomorphism corresponding to composing two additive morphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Discrete.addMonoidalFunctorComp.proof_1
{M : Type u_1}
[AddMonoid M]
{N : Type u_2}
[AddMonoid N]
{K : Type u_1}
[AddMonoid K]
(F : M →+ N)
(G : N →+ K)
⦃X : CategoryTheory.Discrete M⦄
⦃Y : CategoryTheory.Discrete M⦄
(f : X ⟶ Y)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Discrete.eqToHom ⋯)
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor G).obj ((CategoryTheory.Discrete.addMonoidalFunctor F).obj Y))) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor G).obj ((CategoryTheory.Discrete.addMonoidalFunctor F).obj X)))
(CategoryTheory.Discrete.eqToHom ⋯)
def
CategoryTheory.Discrete.monoidalFunctorComp
{M : Type u}
[Monoid M]
{N : Type u'}
[Monoid N]
{K : Type u}
[Monoid K]
(F : M →* N)
(G : N →* K)
:
The monoidal natural isomorphism corresponding to composing two multiplicative morphisms.
Equations
- One or more equations did not get rendered due to their size.