CategoryTheory.Monad.assoc
theorem CategoryTheory.Monad.assoc :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C),
CategoryTheory.CategoryStruct.comp (T.map (T.μ.app X)) (T.μ.app X) =
CategoryTheory.CategoryStruct.comp (T.μ.app (T.obj X)) (T.μ.app X)
This theorem states that for any category `C` and any monad `T` on `C`, and for any object `X` in `C`, the composition of the multiplication of the monad `T`, first applied to the image of `X` under `T` and then to `X`, is equal to the composition of the multiplication of `T` applied to `T(X)` and then to `X`.
In mathematical terms, we can express this as a form of associativity for the multiplication of the monad: μ(T(X)) ∘ μ(X) = μ(T(T(X))) ∘ μ(X) for all `X` in `C`, where μ denotes the multiplication of the monad `T`, and the ∘ symbol denotes the morphism composition in the category `C`.
More concisely: For any monad `T` in a category `C` and object `X` in `C`, the commutativity of multiplications holds: `μ(T(X)) ∘ μ(X) = μ(T(T(X))) ∘ μ(X)`.
|
CategoryTheory.Monad.left_unit
theorem CategoryTheory.Monad.left_unit :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C),
CategoryTheory.CategoryStruct.comp (T.η.app (T.obj X)) (T.μ.app X) = CategoryTheory.CategoryStruct.id (T.obj X)
This theorem, `CategoryTheory.Monad.left_unit`, states that for any category `C`, and for any monad `T` on `C`, and for any object `X` in `C`, the composition of the unit of the monad `T` applied to the object `T.obj X` and the multiplication of the monad `T` applied to the object `X` is equal to the identity morphism on the object `T.obj X`. This theorem is essentially expressing the left unit law for a monad in the category theory context. The left unit law is one of the three conditions in the definition of a monad, along with the right unit law and the associativity law.
More concisely: For any monad T on a category C and object X in C, the unit of T at X multiplied by the multiplication of T at X equals the identity morphism on T.obj X. (Expressed in Lean as `T.unit X ∘ T.bind X = id _`)
|
CategoryTheory.Monad.right_unit
theorem CategoryTheory.Monad.right_unit :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C),
CategoryTheory.CategoryStruct.comp (T.map (T.η.app X)) (T.μ.app X) = CategoryTheory.CategoryStruct.id (T.obj X)
This theorem states that for any category `C` and any monad `T` on `C`, for any object `X` in `C`, the composition of the morphism obtained by applying the unit of the monad `T` to `X` and then mapping that via `T` and the multiplication of the monad `T` applied to `X` is equal to the identity on the object `T.obj X`. This is essentially the statement of the right unit law for monads in category theory. In mathematical notation, it corresponds to the equation `T(η_X) ∘ μ_X = id_(T(X))`, where `η` is the unit of the monad, `μ` is the multiplication of the monad, and `id` denotes the identity morphism.
More concisely: For any category `C` and monad `T` on `C`, the composition of `T(η\_X)` and `μ\_X` equals the identity `id(T(X))` for any object `X` in `C`. (This is the right unit law for monads in category theory.)
|