CategoryTheory.Discrete.addMonoidalFunctor.proof_1
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_1 :
∀ {M : Type u_2} [inst : AddMonoid M] {N : Type u_1} [inst_1 : AddMonoid N] (F : M →+ N)
{X Y : CategoryTheory.Discrete M}, (X ⟶ Y) → F X.as = F Y.as
This theorem states that for any two objects `X` and `Y` in a discrete category whose objects are elements of an additive monoid `M`, and any additive monoid homomorphism `F` from `M` to another additive monoid `N`, the action of `F` on the objects `X` and `Y` is the same if there exists a morphism from `X` to `Y`. In other words, every morphism in the discrete category induces an equation between the results of applying `F` to the source and target of the morphism.
More concisely: For any additive monoid homomorphism F between additive monoids M and N, and any objects X and Y in the discrete category of M with a morphism f : X -> Y, we have F(X) = F(Y).
|
CategoryTheory.Discrete.monoidalFunctor.proof_1
theorem CategoryTheory.Discrete.monoidalFunctor.proof_1 :
∀ {M : Type u_2} [inst : Monoid M] {N : Type u_1} [inst_1 : Monoid N] (F : M →* N)
{X Y : CategoryTheory.Discrete M}, (X ⟶ Y) → F X.as = F Y.as
This theorem states that for any two objects `X` and `Y` in the discrete category of a monoid `M`, and a monoid homomorphism `F` from `M` to another monoid `N`, the image of the `as` (the underlying element of the monoid) of `X` under `F` is equal to the image of the `as` of `Y` under `F`, provided that there exists a morphism from `X` to `Y` in the discrete category. In simpler terms, this theorem says that any morphism in the discrete category essentially maps elements in `M` to their corresponding images in `N` under the homomorphism `F`.
More concisely: Given any monoid homomorphism `F` from monoid `M` to monoid `N`, objects `X` and `Y` in the discrete category of `M`, and a morphism from `X` to `Y`, the image of the underlying element of `X` under `F` is equal to the image of the underlying element of `Y` under `F`.
|