Action.hom_ext
theorem Action.hom_ext :
∀ {V : Type (u + 1)} [inst : CategoryTheory.LargeCategory V] {G : MonCat} {M N : Action V G} (φ₁ φ₂ : M ⟶ N),
φ₁.hom = φ₂.hom → φ₁ = φ₂
The theorem `Action.hom_ext` states that for any large category `V`, any monoid `G` in the category of monoids `MonCat`, and any two action objects `M` and `N` in the category of actions over `V` and `G`, if two morphisms `φ₁` and `φ₂` from `M` to `N` have the same underlying function (i.e., `φ₁.hom = φ₂.hom`), then `φ₁` and `φ₂` are the same morphism. This is a property of extensionality for morphisms in the category of actions.
More concisely: In the category of actions over a large category and a monoid, morphisms with equal underlying functions are equal.
|
Action.ρ_one
theorem Action.ρ_one :
∀ {V : Type (u + 1)} [inst : CategoryTheory.LargeCategory V] {G : MonCat} (A : Action V G),
A.ρ 1 = CategoryTheory.CategoryStruct.id A.V
The theorem `Action.ρ_one` states that for any Large Category `V`, any Monoid Category `G`, and any action `A` of `G` on `V`, the right action of the identity element `1` of the monoid on any element of `V` is the identity morphism in the category `V`. In other words, the action of the identity does not change the element of the category `V`, just as you would expect from an identity.
More concisely: For any Monoid Category `G` action `A` on a Large Category `V`, the right action of the identity element of `G` on any object in `V` is the identity morphism in `V`.
|
Action.Hom.ext
theorem Action.Hom.ext :
∀ {V : Type (u + 1)} {inst : CategoryTheory.LargeCategory V} {G : MonCat} {M N : Action V G} (x y : M.Hom N),
x.hom = y.hom → x = y
This theorem states that for any large category `V` and any monoid `G` in the category of monoids (`MonCat`), given two actions `M` and `N` of `G` on objects in `V`, if we have two morphisms (`Action.Hom`) `x` and `y` from `M` to `N`, then if the `hom` component of `x` and `y` (the actual function maps of `x` and `y`) are the same, it implies that `x` and `y` are the same. Essentially, it guarantees uniqueness of morphisms in this context based on their function maps.
More concisely: In any large category `V` and for any monoid `G` in `MonCat`, if two `G`-actions `M` and `N` on objects of `V` have homomorphisms `x: M -> N` and `y: M -> N` with equal function components, then `x = y`.
|