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_13
(M : Type u_1)
[AddMonoid M]
{X : CategoryTheory.Discrete M}
{Y : CategoryTheory.Discrete M}
(f : X ⟶ Y)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom
(_ : (fun X Y => { as := X.as + Y.as }) X { as := 0 } = (fun X Y => { as := X.as + Y.as }) Y { as := 0 }))
(CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) Y { as := 0 } = Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) X { as := 0 } = X))
f
theorem
CategoryTheory.Discrete.addMonoidal.proof_7
(M : Type u_1)
[AddMonoid M]
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
(Z : CategoryTheory.Discrete M)
:
theorem
CategoryTheory.Discrete.addMonoidal.proof_8
(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_11
(M : Type u_1)
[AddMonoid M]
{X : CategoryTheory.Discrete M}
{Y : CategoryTheory.Discrete M}
(f : X ⟶ Y)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom
(_ : (fun X Y => { as := X.as + Y.as }) { as := 0 } X = (fun X Y => { as := X.as + Y.as }) { as := 0 } Y))
(CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) { as := 0 } Y = Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) { as := 0 } X = X))
f
theorem
CategoryTheory.Discrete.addMonoidal.proof_4
(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₂)
:
CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) X₁ X₂ = (fun X Y => { as := X.as + Y.as }) Y₁ Y₂) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) X₁ X₂ = (fun X Y => { as := X.as + Y.as }) Y₁ X₂))
(CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) Y₁ X₂ = (fun X Y => { 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)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom
(_ :
(fun X Y => { as := X.as + Y.as })
((fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) W X) Y) Z = (fun X Y => { as := X.as + Y.as })
((fun X Y => { as := X.as + Y.as }) W ((fun X Y => { as := X.as + Y.as }) X Y)) Z))
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom
(_ :
(fun X Y => { as := X.as + Y.as })
((fun X Y => { as := X.as + Y.as }) W ((fun X Y => { as := X.as + Y.as }) X Y)) Z = (fun X Y => { as := X.as + Y.as }) W
((fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) X Y) Z)))
(CategoryTheory.eqToHom
(_ :
(fun X Y => { as := X.as + Y.as }) W
((fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) X Y) Z) = (fun X Y => { as := X.as + Y.as }) W
((fun X Y => { as := X.as + Y.as }) X ((fun X Y => { as := X.as + Y.as }) Y Z))))) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom
(_ :
(fun X Y => { as := X.as + Y.as })
((fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) W X) Y) Z = (fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) W X)
((fun X Y => { as := X.as + Y.as }) Y Z)))
(CategoryTheory.eqToHom
(_ :
(fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) W X)
((fun X Y => { as := X.as + Y.as }) Y Z) = (fun X Y => { as := X.as + Y.as }) W
((fun X Y => { as := X.as + Y.as }) X ((fun X Y => { as := X.as + Y.as }) Y Z))))
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 => { as := X.as + Y.as }) X₁ X = (fun X Y => { as := X.as + Y.as }) X₂ X
theorem
CategoryTheory.Discrete.addMonoidal.proof_10
(M : Type u_1)
[AddMonoid M]
(X : CategoryTheory.Discrete M)
:
theorem
CategoryTheory.Discrete.addMonoidal.proof_9
(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₃)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom
(_ :
(fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) X₁ X₂) X₃ = (fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) Y₁ Y₂) Y₃))
(CategoryTheory.eqToHom
(_ :
(fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) Y₁ Y₂) Y₃ = (fun X Y => { as := X.as + Y.as }) Y₁ ((fun X Y => { as := X.as + Y.as }) Y₂ Y₃))) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom
(_ :
(fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) X₁ X₂) X₃ = (fun X Y => { as := X.as + Y.as }) X₁ ((fun X Y => { as := X.as + Y.as }) X₂ X₃)))
(CategoryTheory.eqToHom
(_ :
(fun X Y => { as := X.as + Y.as }) X₁ ((fun X Y => { as := X.as + Y.as }) X₂ X₃) = (fun X Y => { as := X.as + Y.as }) Y₁ ((fun X Y => { as := X.as + Y.as }) Y₂ Y₃)))
theorem
CategoryTheory.Discrete.addMonoidal.proof_12
(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 => { as := X.as + Y.as }) X x = (fun X Y => { as := X.as + Y.as }) X x_1
theorem
CategoryTheory.Discrete.addMonoidal.proof_15
(M : Type u_1)
[AddMonoid M]
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom
(_ :
(fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) X { as := 0 }) Y = (fun X Y => { as := X.as + Y.as }) X ((fun X Y => { as := X.as + Y.as }) { as := 0 } Y)))
(CategoryTheory.eqToHom
(_ :
(fun X Y => { as := X.as + Y.as }) X ((fun X Y => { as := X.as + Y.as }) { as := 0 } Y) = (fun X Y => { as := X.as + Y.as }) X Y)) = CategoryTheory.eqToHom
(_ :
(fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) X { as := 0 }) Y = (fun X Y => { as := X.as + Y.as }) X Y)
theorem
CategoryTheory.Discrete.addMonoidal.proof_6
(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₂)
:
CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) X₁ X₂ = (fun X Y => { as := X.as + Y.as }) Z₁ Z₂) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) X₁ X₂ = (fun X Y => { as := X.as + Y.as }) Y₁ Y₂))
(CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) Y₁ Y₂ = (fun X Y => { as := X.as + Y.as }) Z₁ Z₂))
theorem
CategoryTheory.Discrete.addMonoidal.proof_5
(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 }
@[simp]
theorem
CategoryTheory.Discrete.addMonoidal_rightUnitor
(M : Type u)
[AddMonoid M]
(X : CategoryTheory.Discrete M)
:
CategoryTheory.MonoidalCategory.rightUnitor X = CategoryTheory.Discrete.eqToIso (_ : X.as + 0 = X.as)
@[simp]
theorem
CategoryTheory.Discrete.addMonoidal_leftUnitor
(M : Type u)
[AddMonoid M]
(X : CategoryTheory.Discrete M)
:
CategoryTheory.MonoidalCategory.leftUnitor X = CategoryTheory.Discrete.eqToIso (_ : 0 + X.as = X.as)
@[simp]
theorem
CategoryTheory.Discrete.monoidal_rightUnitor
(M : Type u)
[Monoid M]
(X : CategoryTheory.Discrete M)
:
CategoryTheory.MonoidalCategory.rightUnitor X = CategoryTheory.Discrete.eqToIso (_ : X.as * 1 = X.as)
@[simp]
theorem
CategoryTheory.Discrete.monoidal_associator
(M : Type u)
[Monoid M]
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
(Z : CategoryTheory.Discrete M)
:
CategoryTheory.MonoidalCategory.associator X Y Z = CategoryTheory.Discrete.eqToIso (_ : X.as * Y.as * Z.as = X.as * (Y.as * Z.as))
@[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
@[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_leftUnitor
(M : Type u)
[Monoid M]
(X : CategoryTheory.Discrete M)
:
CategoryTheory.MonoidalCategory.leftUnitor X = CategoryTheory.Discrete.eqToIso (_ : 1 * X.as = X.as)
@[simp]
theorem
CategoryTheory.Discrete.addMonoidal_associator
(M : Type u)
[AddMonoid M]
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
(Z : CategoryTheory.Discrete M)
:
CategoryTheory.MonoidalCategory.associator X Y Z = CategoryTheory.Discrete.eqToIso (_ : X.as + Y.as + Z.as = X.as + (Y.as + Z.as))
@[simp]
@[simp]
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_11
{M : Type u_1}
[AddMonoid M]
{N : Type u_1}
[AddMonoid N]
(F : M →+ N)
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
:
CategoryTheory.IsIso
(CategoryTheory.LaxMonoidalFunctor.μ
(CategoryTheory.LaxMonoidalFunctor.mk
(CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑F X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Y.as) })
(CategoryTheory.Discrete.eqToHom (_ : 0 = ↑F 0)) fun X Y =>
CategoryTheory.Discrete.eqToHom (_ : ↑F X.as + ↑F Y.as = ↑F (X.as + Y.as)))
X Y)
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_8
{M : Type u_1}
[AddMonoid M]
{N : Type u_1}
[AddMonoid N]
(F : M →+ N)
(X : CategoryTheory.Discrete M)
:
CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) { as := 0 } { as := ↑F X.as } = { as := ↑F X.as }) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Discrete.eqToHom (_ : 0 = ↑F 0))
(CategoryTheory.CategoryStruct.id { as := ↑F X.as }))
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom
(_ :
CategoryTheory.MonoidalCategory.tensorObj
((CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑F X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Y.as) }).obj
(CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete M)))
((CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑F X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Y.as) }).obj
X) = (CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑F X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Y.as) }).obj
(CategoryTheory.MonoidalCategory.tensorObj
(CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete M)) X)))
(CategoryTheory.eqToHom
(_ :
(fun X => { as := ↑F X.as })
(CategoryTheory.MonoidalCategory.tensorObj
(CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete M)) X) = (fun X => { as := ↑F X.as }) X)))
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_2
{M : Type u_1}
[AddMonoid M]
{N : Type u_1}
[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_9
{M : Type u_1}
[AddMonoid M]
{N : Type u_1}
[AddMonoid N]
(F : M →+ N)
(X : CategoryTheory.Discrete M)
:
CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) { as := ↑F X.as } { as := 0 } = { as := ↑F X.as }) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id { as := ↑F X.as })
(CategoryTheory.Discrete.eqToHom (_ : 0 = ↑F 0)))
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom
(_ :
CategoryTheory.MonoidalCategory.tensorObj
((CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑F X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Y.as) }).obj
X)
((CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑F X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Y.as) }).obj
(CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete M))) = (CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑F X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Y.as) }).obj
(CategoryTheory.MonoidalCategory.tensorObj X
(CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete M)))))
(CategoryTheory.eqToHom
(_ :
(fun X => { as := ↑F X.as })
(CategoryTheory.MonoidalCategory.tensorObj X
(CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete M))) = (fun X => { as := ↑F X.as }) X)))
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_1
{M : Type u_1}
[AddMonoid M]
{N : Type u_1}
[AddMonoid N]
(F : M →+ N)
:
∀ {X Y : CategoryTheory.Discrete M}, (X ⟶ Y) → ↑F X.as = ↑F Y.as
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_3
{M : Type u_1}
[AddMonoid M]
{N : Type u_1}
[AddMonoid N]
(F : M →+ N)
{X : CategoryTheory.Discrete M}
{Y : CategoryTheory.Discrete M}
{Z : CategoryTheory.Discrete M}
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Z.as) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom (_ : (fun X => { as := ↑F X.as }) X = (fun X => { as := ↑F X.as }) Y))
(CategoryTheory.eqToHom (_ : (fun X => { as := ↑F X.as }) Y = (fun X => { as := ↑F X.as }) Z))
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_6
{M : Type u_1}
[AddMonoid M]
{N : Type u_1}
[AddMonoid N]
(F : M →+ N)
{X : CategoryTheory.Discrete M}
{Y : CategoryTheory.Discrete M}
{X' : CategoryTheory.Discrete M}
{Y' : CategoryTheory.Discrete M}
(f : X ⟶ Y)
(g : X' ⟶ Y')
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Y.as))
(CategoryTheory.Discrete.eqToHom (_ : ↑F X'.as = ↑F Y'.as)))
(CategoryTheory.Discrete.eqToHom (_ : ↑F Y.as + ↑F Y'.as = ↑F (Y.as + Y'.as))) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom
(_ :
CategoryTheory.MonoidalCategory.tensorObj
((CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑F X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Y.as) }).obj
X)
((CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑F X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Y.as) }).obj
X') = (CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑F X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Y.as) }).obj
(CategoryTheory.MonoidalCategory.tensorObj X X')))
(CategoryTheory.eqToHom
(_ :
(fun X => { as := ↑F X.as }) (CategoryTheory.MonoidalCategory.tensorObj X X') = (fun X => { as := ↑F X.as }) (CategoryTheory.MonoidalCategory.tensorObj Y Y')))
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_5
{M : Type u_1}
[AddMonoid M]
{N : Type u_1}
[AddMonoid N]
(F : M →+ N)
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
:
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_7
{M : Type u_1}
[AddMonoid M]
{N : Type u_1}
[AddMonoid N]
(F : M →+ N)
(X : CategoryTheory.Discrete M)
(Y : CategoryTheory.Discrete M)
(Z : CategoryTheory.Discrete M)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom
(CategoryTheory.Discrete.eqToHom (_ : ↑F X.as + ↑F Y.as = ↑F (X.as + Y.as)))
(CategoryTheory.CategoryStruct.id { as := ↑F Z.as }))
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom
(_ :
CategoryTheory.MonoidalCategory.tensorObj
((CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑F X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Y.as) }).obj
(CategoryTheory.MonoidalCategory.tensorObj X Y))
((CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑F X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Y.as) }).obj
Z) = (CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑F X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Y.as) }).obj
(CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z)))
(CategoryTheory.eqToHom
(_ :
(fun X => { as := ↑F X.as })
(CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) = (fun X => { as := ↑F X.as })
(CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z))))) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom
(_ :
(fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) { as := ↑F X.as } { as := ↑F Y.as })
{ as := ↑F Z.as } = (fun X Y => { as := X.as + Y.as }) { as := ↑F X.as }
((fun X Y => { as := X.as + Y.as }) { as := ↑F Y.as } { as := ↑F Z.as })))
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id { as := ↑F X.as })
(CategoryTheory.Discrete.eqToHom (_ : ↑F Y.as + ↑F Z.as = ↑F (Y.as + Z.as))))
(CategoryTheory.Discrete.eqToHom
(_ :
↑F X.as + ↑F (CategoryTheory.MonoidalCategory.tensorObj Y Z).as = ↑F (X.as + (CategoryTheory.MonoidalCategory.tensorObj Y Z).as))))
theorem
CategoryTheory.Discrete.addMonoidalFunctor.proof_10
{M : Type u_1}
[AddMonoid M]
{N : Type u_1}
[AddMonoid N]
(F : M →+ N)
:
CategoryTheory.IsIso
(CategoryTheory.LaxMonoidalFunctor.mk
(CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑F X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Y.as) })
(CategoryTheory.Discrete.eqToHom (_ : 0 = ↑F 0)) fun X Y =>
CategoryTheory.Discrete.eqToHom (_ : ↑F X.as + ↑F Y.as = ↑F (X.as + 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).toLaxMonoidalFunctor.toFunctor.obj X).as = ↑F X.as
@[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)
:
CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.Discrete.monoidalFunctor F).toLaxMonoidalFunctor X Y = CategoryTheory.Discrete.eqToHom (_ : ↑F X.as * ↑F Y.as = ↑F (X.as * Y.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).toLaxMonoidalFunctor.toFunctor.map f = CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Y.as)
@[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).toLaxMonoidalFunctor.toFunctor.obj X).as = ↑F X.as
@[simp]
theorem
CategoryTheory.Discrete.addMonoidalFunctor_toLaxMonoidalFunctor_ε
{M : Type u}
[AddMonoid M]
{N : Type u}
[AddMonoid N]
(F : M →+ N)
:
(CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.ε = CategoryTheory.Discrete.eqToHom (_ : 0 = ↑F 0)
@[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).toLaxMonoidalFunctor.toFunctor.map f = CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Y.as)
@[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)
:
CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor X Y = CategoryTheory.Discrete.eqToHom (_ : ↑F X.as + ↑F Y.as = ↑F (X.as + Y.as))
@[simp]
theorem
CategoryTheory.Discrete.monoidalFunctor_toLaxMonoidalFunctor_ε
{M : Type u}
[Monoid M]
{N : Type u}
[Monoid N]
(F : M →* N)
:
(CategoryTheory.Discrete.monoidalFunctor F).toLaxMonoidalFunctor.ε = CategoryTheory.Discrete.eqToHom (_ : 1 = ↑F 1)
theorem
CategoryTheory.Discrete.addMonoidalFunctorComp.proof_6
{M : Type u_1}
[AddMonoid M]
{N : Type u_1}
[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
(_ : ↑(AddMonoidHom.comp G F) X.as + ↑(AddMonoidHom.comp G F) Y.as = ↑(AddMonoidHom.comp G F) (X.as + Y.as)))
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.obj
(CategoryTheory.MonoidalCategory.tensorObj X Y))) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.obj X))
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.obj Y)))
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom
(_ :
CategoryTheory.MonoidalCategory.tensorObj
((CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑G X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑G X.as = ↑G Y.as) }).obj
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj X))
((CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑G X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑G X.as = ↑G Y.as) }).obj
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj Y)) = (CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑G X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑G X.as = ↑G Y.as) }).obj
(CategoryTheory.MonoidalCategory.tensorObj
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj X)
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj Y))))
(CategoryTheory.eqToHom
(_ :
(fun X => { as := ↑G X.as })
(CategoryTheory.MonoidalCategory.tensorObj
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj X)
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj Y)) = (fun X => { as := ↑G X.as })
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj
(CategoryTheory.MonoidalCategory.tensorObj X Y)))))
theorem
CategoryTheory.Discrete.addMonoidalFunctorComp.proof_1
{M : Type u_1}
[AddMonoid M]
{N : Type u_1}
[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
(_ :
↑G ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj X).as = ↑G ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj Y).as))
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.obj
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj Y))) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.obj
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj X)))
(CategoryTheory.Discrete.eqToHom (_ : ↑(AddMonoidHom.comp G F) X.as = ↑(AddMonoidHom.comp G F) Y.as))
theorem
CategoryTheory.Discrete.addMonoidalFunctorComp.proof_8
{M : Type u_1}
[AddMonoid M]
{N : Type u_1}
[AddMonoid N]
{K : Type u_1}
[AddMonoid K]
(F : M →+ N)
(G : N →+ K)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalNatTrans.mk
(CategoryTheory.NatTrans.mk fun X =>
CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.obj X)))
(CategoryTheory.MonoidalNatTrans.mk
(CategoryTheory.NatTrans.mk fun X =>
CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor F ⊗⋙ CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.obj
X))) = CategoryTheory.CategoryStruct.id (CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F))
theorem
CategoryTheory.Discrete.addMonoidalFunctorComp.proof_4
{M : Type u_1}
[AddMonoid M]
{N : Type u_1}
[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 (_ : ↑(AddMonoidHom.comp G F) X.as = ↑(AddMonoidHom.comp G F) Y.as))
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.obj Y)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.obj X))
(CategoryTheory.Discrete.eqToHom
(_ :
↑G ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj X).as = ↑G ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj Y).as))
theorem
CategoryTheory.Discrete.addMonoidalFunctorComp.proof_2
{M : Type u_1}
[AddMonoid M]
{N : Type u_1}
[AddMonoid N]
{K : Type u_1}
[AddMonoid K]
(F : M →+ N)
(G : N →+ K)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom
(_ :
CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete K) = (CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑G X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑G X.as = ↑G Y.as) }).obj
(CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete N))))
(CategoryTheory.eqToHom
(_ :
(fun X => { as := ↑G X.as }) (CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete N)) = (fun X => { as := ↑G X.as })
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj
(CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete M))))))
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.obj
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj
(CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete M))))) = CategoryTheory.Discrete.eqToHom (_ : 0 = ↑(AddMonoidHom.comp G F) 0)
theorem
CategoryTheory.Discrete.addMonoidalFunctorComp.proof_7
{M : Type u_1}
[AddMonoid M]
{N : Type u_1}
[AddMonoid N]
{K : Type u_1}
[AddMonoid K]
(F : M →+ N)
(G : N →+ K)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalNatTrans.mk
(CategoryTheory.NatTrans.mk fun X =>
CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor F ⊗⋙ CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.obj
X)))
(CategoryTheory.MonoidalNatTrans.mk
(CategoryTheory.NatTrans.mk fun X =>
CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.obj
X))) = CategoryTheory.CategoryStruct.id
(CategoryTheory.Discrete.addMonoidalFunctor F ⊗⋙ CategoryTheory.Discrete.addMonoidalFunctor G)
theorem
CategoryTheory.Discrete.addMonoidalFunctorComp.proof_3
{M : Type u_1}
[AddMonoid M]
{N : Type u_1}
[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.MonoidalCategory.tensorObj
((CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑G X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑G X.as = ↑G Y.as) }).obj
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj X))
((CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑G X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑G X.as = ↑G Y.as) }).obj
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj Y)) = (CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑G X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑G X.as = ↑G Y.as) }).obj
(CategoryTheory.MonoidalCategory.tensorObj
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj X)
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj Y))))
(CategoryTheory.eqToHom
(_ :
(fun X => { as := ↑G X.as })
(CategoryTheory.MonoidalCategory.tensorObj
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj X)
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj Y)) = (fun X => { as := ↑G X.as })
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj
(CategoryTheory.MonoidalCategory.tensorObj X Y)))))
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.obj
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj
(CategoryTheory.MonoidalCategory.tensorObj X Y)))) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.obj
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj X)))
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.obj
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj Y))))
(CategoryTheory.Discrete.eqToHom
(_ : ↑(AddMonoidHom.comp G F) X.as + ↑(AddMonoidHom.comp G F) Y.as = ↑(AddMonoidHom.comp G F) (X.as + Y.as)))
theorem
CategoryTheory.Discrete.addMonoidalFunctorComp.proof_5
{M : Type u_1}
[AddMonoid M]
{N : Type u_1}
[AddMonoid N]
{K : Type u_1}
[AddMonoid K]
(F : M →+ N)
(G : N →+ K)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Discrete.eqToHom (_ : 0 = ↑(AddMonoidHom.comp G F) 0))
(CategoryTheory.CategoryStruct.id
((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.obj
(CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete M)))) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.eqToHom
(_ :
CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete K) = (CategoryTheory.Functor.mk
{ obj := fun X => { as := ↑G X.as },
map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑G X.as = ↑G Y.as) }).obj
(CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete N))))
(CategoryTheory.eqToHom
(_ :
(fun X => { as := ↑G X.as }) (CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete N)) = (fun X => { as := ↑G X.as })
((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj
(CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete M)))))