CategoryTheory.congr_app
theorem CategoryTheory.congr_app :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} {α β : F.NatTrans G},
α = β → ∀ (X : C), α.app X = β.app X
The theorem `CategoryTheory.congr_app` states that given two categories `C` and `D`, and two functors `F` and `G` from `C` to `D`, if we have two natural transformations `α` and `β` from `F` to `G`, and `α` equals to `β`, then for any object `X` in category `C`, the application of `α` to `X` is equal to the application of `β` to `X`. In simpler terms, it says that if two natural transformations between the same functors are equal, then they act identically on every object in the source category.
More concisely: If two natural transformations between functors are equal, then they induce the same function on objects in the source category.
|
CategoryTheory.NatTrans.naturality_assoc
theorem CategoryTheory.NatTrans.naturality_assoc :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (self : F.NatTrans G) ⦃X Y : C⦄
(f : X ⟶ Y) {Z : D} (h : G.obj Y ⟶ Z),
CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (self.app Y) h) =
CategoryTheory.CategoryStruct.comp (self.app X) (CategoryTheory.CategoryStruct.comp (G.map f) h)
In natural language, this theorem states that for any two categories `C` and `D`, with functors `F` and `G` from `C` to `D` and a natural transformation `self` from `F` to `G`, the naturality condition holds. This means that for any objects `X` and `Y` in `C` and any morphism `f` from `X` to `Y`, and a morphism `h` from `G.obj Y` to any object `Z` in `D`, the composition of the transformation of `f` under `F` and the composition of the application of `self` at `Y` with `h` is the same as the composition of the application of `self` at `X` and the composition of the transformation of `f` under `G` with `h`.
This can be stated in the language of category theory as follows: `(F.map f) ≫ (self.app Y ≫ h) = (self.app X) ≫ (G.map f ≫ h)`. This is a fundamental property of natural transformations between functors in category theory, ensuring the commutativity of the diagram associated with the natural transformation.
More concisely: Given functors F and G from category C to category D, and a natural transformation self from F to G, the naturality condition holds, that is, for any object X in C and morphism f : X -> Y, and any morphism h : G(Y) -> Z in D, (F.map f) . (self.app Y . h) = (self.app X) . (G.map f) . h.
|
CategoryTheory.NatTrans.naturality
theorem CategoryTheory.NatTrans.naturality :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (self : F.NatTrans G) ⦃X Y : C⦄
(f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp (F.map f) (self.app Y) =
CategoryTheory.CategoryStruct.comp (self.app X) (G.map f)
This theorem, known as the "naturality square" condition in category theory, states that for any two categories `C` and `D`, given any two functors `F` and `G` from `C` to `D` and a natural transformation `self` from `F` to `G`, for every pair of objects `X` and `Y` in `C` and any morphism `f` from `X` to `Y` in `C`, the composition of the function `F` applied to the morphism `f` with the application of the natural transformation `self` at `Y` is equal to the composition of the application of the natural transformation `self` at `X` with the function `G` applied to the morphism `f`. In simpler terms, it states that transforming before mapping is the same as mapping before transforming.
This can be represented as a commutative diagram:
```math
X --(F.map f)--> F(Y) --(self.app Y)--> G(Y)
| |
(self.app X) (G.map f)
| |
v v
G(X) <---(G.map f)--- G(Y)
```
where all paths from top-left to bottom-right are equal.
More concisely: Given any two functors F and G between categories C and D, and a natural transformation self from F to G, for all objects X and Y in C and morphism f from X to Y, the diagram commutes: F(f) ∘ self.app Y = self.app X ∘ G(f).
|
CategoryTheory.NatTrans.ext
theorem CategoryTheory.NatTrans.ext :
∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂}
{inst_1 : CategoryTheory.Category.{v₂, u₂} D} {F G : CategoryTheory.Functor C D} (x y : F.NatTrans G),
x.app = y.app → x = y
This theorem states that for any two categories `C` and `D` (of certain types `u₁` and `u₂`, and with Category structures `inst` and `inst_1`, respectively), and for any two functors `F` and `G` from `C` to `D`, if two natural transformations `x` and `y` from `F` to `G` have the same application function (`app`), then `x` and `y` are indeed the same natural transformation. In other words, a natural transformation between two functors is completely determined by its application function.
More concisely: If two natural transformations between functors have the same application function, then they are equal.
|