CategoryTheory.Functorial.map_id'
theorem CategoryTheory.Functorial.map_id' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : C → D} [self : CategoryTheory.Functorial F] (X : C),
CategoryTheory.Functorial.map' (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (F X)
This theorem, `CategoryTheory.Functorial.map_id'`, states that for any category `C` and `D`, and any functorial map `F` from `C` to `D`, the functorial map preserves the identity morphism. In other words, if we apply the functorial map to the identity morphism of an object `X` in `C`, we get the identity morphism of the object `F X` in `D`. This is a fundamental property of functors in category theory, reflecting that they must respect the structure of categories.
More concisely: For any category `C`, any category `D`, and any functor `F` from `C` to `D`, the functor `F` preserves identity morphisms, i.e., `F(id X) = id (FX)` for all objects `X` in `C`.
|
CategoryTheory.Functorial.map_comp
theorem CategoryTheory.Functorial.map_comp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : C → D} [inst_2 : CategoryTheory.Functorial F] {X Y Z : C}
{f : X ⟶ Y} {g : Y ⟶ Z},
CategoryTheory.map F (CategoryTheory.CategoryStruct.comp f g) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.map F f) (CategoryTheory.map F g)
This theorem, `CategoryTheory.Functorial.map_comp`, states that for any categories `C` and `D`, and for any function `F` from `C` to `D` that is functorial, and for any three objects `X`, `Y`, `Z` of `C`, and any two morphisms `f` from `X` to `Y` and `g` from `Y` to `Z`, the functorial action of `F` on the composition of `f` and `g` (denoted `CategoryTheory.CategoryStruct.comp f g`) is equivalent to the composition of the functorial action of `F` on `f` and the functorial action of `F` on `g`.
In simpler terms, this theorem is asserting that mapping the composition of two morphisms under a functor is the same as first mapping the individual morphisms and then composing them - a property that is known as functor preservation of composition or simply functor composition law in category theory.
In mathematical notation, it could be expressed as `F(f ∘ g) = F(f) ∘ F(g)`, where `∘` denotes composition of morphisms and `F` is a functor.
More concisely: For any functor F between categories C and D, F(f ∘ g) = F(f) ∘ F(g) for all objects X, Y, Z in C and morphisms f : X → Y and g : Y → Z.
|
CategoryTheory.Functorial.map_id
theorem CategoryTheory.Functorial.map_id :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : C → D} [inst_2 : CategoryTheory.Functorial F] {X : C},
CategoryTheory.map F (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (F X)
The theorem `CategoryTheory.Functorial.map_id` states that for any category `C` of type `u₁` with a category structure `inst`, any category `D` of type `u₂` with a category structure `inst_1`, any function `F` from `C` to `D` that has a functorial structure `inst_2`, and an object `X` in `C`, the mapping of the identity morphism of `X` under `F` (denoted `CategoryTheory.map F (CategoryTheory.CategoryStruct.id X)`) is the identity morphism of the object `F X` in `D` (denoted `CategoryTheory.CategoryStruct.id (F X)`). This theorem is essentially asserting that the functor `F` preserves identity morphisms, a crucial property of functors in category theory.
More concisely: For any functors F from category C to category D, the identity morphism of an object X in C is mapped to the identity morphism of the object F(X) in D.
|
CategoryTheory.Functorial.map_comp'
theorem CategoryTheory.Functorial.map_comp' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : C → D} [self : CategoryTheory.Functorial F] {X Y Z : C}
(f : X ⟶ Y) (g : Y ⟶ Z),
CategoryTheory.Functorial.map' (CategoryTheory.CategoryStruct.comp f g) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Functorial.map' f) (CategoryTheory.Functorial.map' g)
This theorem, `CategoryTheory.Functorial.map_comp'`, states that for any two categories `C` and `D`, and a functor `F` from `C` to `D`, the functorial map preserves the composition of morphisms. More specifically, given any three objects `X`, `Y`, `Z` in `C`, and morphisms `f` from `X` to `Y` and `g` from `Y` to `Z`, the functorial map applied to the composition of `f` and `g` (denoted `CategoryTheory.CategoryStruct.comp f g`) is equal to the composition of the functorial map applied to `f` and the functorial map applied to `g`. This property is a key characteristic of functors in category theory.
More concisely: For any functor F from category C to category D, the composite of the functorial maps of two morphisms is equal to the functorial map of their composition.
|