CategoryTheory.Functor.id_map
theorem CategoryTheory.Functor.id_map :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] {X Y : C} (f : X ā¶ Y),
(CategoryTheory.Functor.id C).map f = f
The theorem `CategoryTheory.Functor.id_map` states that for any category `C` and any morphism `f` from object `X` to object `Y` in `C`, the map function of the identity functor on `C` applied to `f` is equivalent to `f` itself. In other words, the identity functor leaves every morphism in the category unchanged when it is applied.
More concisely: For any category C and morphism f in C, the identity functor's map application to f is equal to f itself.
|
CategoryTheory.Functor.map_id
theorem CategoryTheory.Functor.map_id :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] {D : Type uā}
[inst_1 : CategoryTheory.Category.{vā, uā} D] (self : CategoryTheory.Functor C D) (X : C),
self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)
The theorem `CategoryTheory.Functor.map_id` states that for any categories `C` and `D`, and any functor `F` from `C` to `D`, the functor preserves identity morphisms. This means that if `X` is an object in category `C`, then the result of applying the functor `F` to the identity morphism on `X` in category `C` is the same as the identity morphism on the object `F(X)` in category `D`. In mathematical terms, this can be written as `F(id_X) = id_{F(X)}`. This is a key property of functors in category theory.
More concisely: For any functor F between categories C and D, F preserves identities, that is, for any object X in C, F(id X) = id(FX).
|
CategoryTheory.Functor.comp_obj
theorem CategoryTheory.Functor.comp_obj :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] {D : Type uā}
[inst_1 : CategoryTheory.Category.{vā, uā} D] {E : Type uā} [inst_2 : CategoryTheory.Category.{vā, uā} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : C), (F.comp G).obj X = G.obj (F.obj X)
This theorem states that for any three categories `C`, `D`, and `E`, and any two functors `F` from `C` to `D` and `G` from `D` to `E`, the object `X` in `C` under the composition of the two functors `F` and `G` is the same as the object `X` under functor `F` then under functor `G`. In other words, functor composition respects the mapping of objects.
More concisely: For any functors F : C -> D and G : D -> E, the composition Functor(G) ā Functor(F) equals Functor(F) ā Object(X) for any object X in category C.
|
CategoryTheory.Functor.comp_map
theorem CategoryTheory.Functor.comp_map :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] {D : Type uā}
[inst_1 : CategoryTheory.Category.{vā, uā} D] {E : Type uā} [inst_2 : CategoryTheory.Category.{vā, uā} E]
(F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) {X Y : C} (f : X ā¶ Y),
(F.comp G).map f = G.map (F.map f)
This theorem states that, in category theory, given two categories `C` and `D` and a third category `E`, together with functors `F` from `C` to `D` and `G` from `D` to `E`, the composition of the functors `F` and `G` applied to a morphism `f` from `C` is equal to the functor `G` applied to the result of the functor `F` applied to `f`. This embodies the concept of functor composition, which is a central concept in category theory, and is analogous to the composition of functions in set theory.
More concisely: Given functors F from category C to D and G from category D to E, the composition Functor(G ā F) equals Functor(G) ā Morphism(F), where Morphism(F) denotes the image of morphisms under F.
|
CategoryTheory.Functor.map_comp_assoc
theorem CategoryTheory.Functor.map_comp_assoc :
ā {C : Type uā} [inst : CategoryTheory.Category.{u_1, uā} C] {D : Type uā}
[inst_1 : CategoryTheory.Category.{u_2, uā} D] (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ā¶ Y)
(g : Y ā¶ Z) {W : D} (h : F.obj Z ā¶ W),
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp f g)) h =
CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) h)
The theorem `CategoryTheory.Functor.map_comp_assoc` states that for any categories `C` and `D`, any functor `F` from `C` to `D`, any three objects `X`, `Y`, and `Z` in `C`, a morphism `f` from `X` to `Y`, a morphism `g` from `Y` to `Z`, and a morphism `h` from `F.obj Z` to any object `W` in `D`, the composition of the mapped composition of `f` and `g` with `h` is equal to the composition of the mapped `f` with the composition of the mapped `g` and `h`. In mathematical terms, this theorem expresses the associativity of the composition of morphisms after applying a functor, i.e., `F(f ā« g) ā« h = F(f) ā« (F(g) ā« h)`.
More concisely: For any categories C, D and functor F, for any objects X, Y, Z in C and morphisms f: X ā Y, g: Y ā Z, and h: F(Z) ā W in D, the diagram F(f) ā F(Y) ā F(Z) ā F(W) commutes with F(g) ā F(Z) ā F(W), that is, F(f ā« g) = F(f) ā« F(g).
|
CategoryTheory.Functor.map_dite
theorem CategoryTheory.Functor.map_dite :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] {D : Type uā}
[inst_1 : CategoryTheory.Category.{vā, uā} D] (F : CategoryTheory.Functor C D) {X Y : C} {P : Prop}
[inst_2 : Decidable P] (f : P ā (X ā¶ Y)) (g : Ā¬P ā (X ā¶ Y)),
F.map (if h : P then f h else g h) = if h : P then F.map (f h) else F.map (g h)
This is a theorem in category theory which states that, given any two categories `C` and `D`, along with a functor `F` from `C` to `D`, and two morphisms `f` and `g` from object `X` to `Y` in `C` that depend on a proposition `P`, the map of `F` applied to the disjunction `f` or `g` (depending on `P`) is equal to the disjunction of the map of `F` applied to `f` or `g` (again, depending on `P`). In simpler terms, it says that the functor `F` preserves the logical disjunction operation on morphisms.
More concisely: Given any functor F between categories C and D, and objects X, Y in C, morphisms f, g : X ā Y, and proposition P, the diagram F(f ā g) ā
F(f) ā F(g) commutes, where ā denotes disjunction.
|
CategoryTheory.Functor.map_comp
theorem CategoryTheory.Functor.map_comp :
ā {C : Type uā} [inst : CategoryTheory.Category.{vā, uā} C] {D : Type uā}
[inst_1 : CategoryTheory.Category.{vā, uā} D] (self : CategoryTheory.Functor C D) {X Y Z : C} (f : X ā¶ Y)
(g : Y ā¶ Z),
self.map (CategoryTheory.CategoryStruct.comp f g) =
CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
The theorem `CategoryTheory.Functor.map_comp` states that for any types `C` and `D` that are instances of the category theory, and for any functor `self` from `C` to `D`, given three objects `X`, `Y`, and `Z` in `C` and morphisms `f` from `X` to `Y` and `g` from `Y` to `Z`, the functor `self` preserves the composition of morphisms. In other words, the map of the composition of `f` and `g` under the functor `self` is equal to the composition of the maps of `f` and `g` under the functor `self`. This is expressed formally in Lean 4 as `self.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)`.
More concisely: Given any functor `self` between categories `C` and `D`, and morphisms `f: X ā Y` and `g: Y ā Z` in `C`, the diagram `self.map(f ā g) = self.map(f) ā self.map(g)` commutes in `D`.
|