CategoryTheory.Discrete.eqToHom.proof_1
theorem CategoryTheory.Discrete.eqToHom.proof_1 :
∀ {α : Type u_1} {X Y : CategoryTheory.Discrete α}, X.as = Y.as → X = Y
This theorem states that for any type `α`, and for any two objects `X` and `Y` in the category `CategoryTheory.Discrete α`, if the underlying objects of `X` and `Y` (accessed via the `.as` function) are equal, then `X` and `Y` themselves are also equal. In other words, two elements of a discrete category are identical if and only if their underlying objects are identical. This implies that the discrete category is fully determined by its underlying set of objects.
More concisely: In the discrete category of type `α`, two objects are equal if and only if their underlying elements are equal.
|
CategoryTheory.Discrete.eq_of_hom
theorem CategoryTheory.Discrete.eq_of_hom : ∀ {α : Type u₁} {X Y : CategoryTheory.Discrete α}, (X ⟶ Y) → X.as = Y.as
The theorem `CategoryTheory.Discrete.eq_of_hom` states that for any type `α` and any two objects `X` and `Y` in a discrete category of `α`, if there exists a morphism from `X` to `Y`, then `X.as` must be equal to `Y.as`. In other words, in a discrete category, if there's a morphism between two objects, those objects must be the same.
More concisely: In a discrete category, if there exists a morphism between objects X and Y, then X = Y.
|
CategoryTheory.Discrete.mk_as
theorem CategoryTheory.Discrete.mk_as : ∀ {α : Type u₁} (X : CategoryTheory.Discrete α), { as := X.as } = X
This theorem states that for any type `α` and any object `X` of the category `CategoryTheory.Discrete α`, constructing a new object with `as` field equal to `X.as` results in the original object `X`. In other words, the `as` field completely determines an object in the `CategoryTheory.Discrete α` category.
More concisely: For any type `α` and object `X` in `CategoryTheory.Discrete α`, `X` and the object with `as` field equal to `X.as` are equal.
|
CategoryTheory.Discrete.ext
theorem CategoryTheory.Discrete.ext : ∀ {α : Type u₁} (x y : CategoryTheory.Discrete α), x.as = y.as → x = y
This theorem, called `CategoryTheory.Discrete.ext`, states that for any type `α`, if we have two objects `x` and `y` of the discrete category over `α` (i.e., `CategoryTheory.Discrete α`), and if the underlying objects of `x` and `y` in `α` are the same (i.e., `x.as = y.as`), then `x` and `y` themselves are the same (i.e., `x = y`). This reinforces the idea that objects in a discrete category are just the underlying objects of the type they are based on.
More concisely: In the discrete category over a type `α`, two objects `x` and `y` are equal if and only if their underlying objects in `α` are equal.
|
CategoryTheory.Discrete.eqToIso.proof_1
theorem CategoryTheory.Discrete.eqToIso.proof_1 :
∀ {α : Type u_1} {X Y : CategoryTheory.Discrete α}, X.as = Y.as → X = Y
This theorem states that for any type `α` and for any two objects `X` and `Y` in the Discrete category of `α`, if the `as` (identity) of `X` is equal to the `as` (identity) of `Y`, then `X` and `Y` are indeed the same object. Simply put, in a Discrete category, two objects are the same if and only if their identities are the same.
More concisely: In the Discrete category, two objects are equal if and only if their identities are equal.
|
CategoryTheory.Discrete.functor_map_id
theorem CategoryTheory.Discrete.functor_map_id :
∀ {J : Type v₁} {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C]
(F : CategoryTheory.Functor (CategoryTheory.Discrete J) C) {j : CategoryTheory.Discrete J} (f : j ⟶ j),
F.map f = CategoryTheory.CategoryStruct.id (F.obj j)
The theorem `CategoryTheory.Discrete.functor_map_id` states that for any given type `J`, type `C` which forms a category, and a functor `F` from the discrete category on `J` to `C`, any morphism `f` from an object `j` to itself in the discrete category gets mapped to the identity morphism on the object `F.obj j` in category `C`. In other words, this theorem ensures that the functor `F` preserves the identity morphisms of the discrete category.
More concisely: Given a functor F from the discrete category on J to category C, for all objects j in J and their identity morphisms id\_j, F(id\_j) = id\_{F.obj j} in C.
|