CategoryTheory.NatIso.isIso_of_isIso_app
theorem CategoryTheory.NatIso.isIso_of_isIso_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 ⟶ G)
[inst_2 : ∀ (X : C), CategoryTheory.IsIso (α.app X)], CategoryTheory.IsIso α
This theorem states that in the context of category theory, a natural transformation (denoted by `α`) between two functors `F` and `G` from category `C` to `D`, is an isomorphism if all of its components (i.e., the morphism `α.app X` for all `X` in `C`) are isomorphisms.
More concisely: A natural transformation between functors is an isomorphism if and only if all its components are isomorphisms.
|
CategoryTheory.NatIso.isIso_map_iff
theorem CategoryTheory.NatIso.isIso_map_iff :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F₁ F₂ : CategoryTheory.Functor C D},
(F₁ ≅ F₂) → ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIso (F₁.map f) ↔ CategoryTheory.IsIso (F₂.map f)
This theorem states that for any two categories `C` and `D`, and any two functors `F₁` and `F₂` from `C` to `D`, if `F₁` is naturally isomorphic to `F₂`, then for any morphism `f` from object `X` to `Y` in `C`, `F₁` mapping `f` is an isomorphism if and only if `F₂` mapping `f` is an isomorphism. In other words, the isomorphism property of a morphism is preserved under a natural isomorphism of functors.
More concisely: If functors $F\_1$ and $F\_2$ between categories $C$ and $D$ are naturally isomorphic, then for any isomorphism $f$ in $C$ between objects $X$ and $Y$, $F\_1(f)$ and $F\_2(f)$ are mutual inverses.
|
CategoryTheory.NatIso.naturality_2
theorem CategoryTheory.NatIso.naturality_2 :
∀ {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 : C} (α : F ≅ G)
(f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp (α.hom.app X) (CategoryTheory.CategoryStruct.comp (G.map f) (α.inv.app Y)) =
F.map f
This theorem, `CategoryTheory.NatIso.naturality_2`, states that for any two categories `C` and `D`, and any two functors `F` and `G` from `C` to `D`, if there is a natural isomorphism `α` between `F` and `G`, and a morphism `f` from `X` to `Y` in `C`, then the composition of the application of the homomorphism part of `α` at `X` with the composition of the mapping of `f` through `G` and the application of the inverse of the homomorphism part of `α` at `Y` is equal to the mapping of `f` through `F`. In other words, it asserts the naturality condition for a natural transformation in the context of category theory.
More concisely: Given categories `C`, `D`, functors `F` and `G` with a natural isomorphism `α: F ≅ G`, and a morphism `f: X ⟹ Y` in `C`, the following diagram commutes:
```
F(X) �� /******/ ⏥ ┓
╱ α_X ╲
G(X) ⏸───────────────┛
╵ α_Y ╮
Y G(f) F(f)
```
|
CategoryTheory.Iso.inv_hom_id_app
theorem CategoryTheory.Iso.inv_hom_id_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 ≅ G) (X : C),
CategoryTheory.CategoryStruct.comp (α.inv.app X) (α.hom.app X) = CategoryTheory.CategoryStruct.id (G.obj X)
This theorem states that for any two categories `C` and `D`, and any two functors `F` and `G` from `C` to `D` that are isomorphic with isomorphism `α`, for any object `X` in `C`, the composition of the inverse of `α` applied to `X` and `α` applied to `X` is the identity morphism on the object obtained by applying the functor `G` to `X`. In terms of category theory, it expresses the fundamental property of isomorphisms that the composition of an isomorphism and its inverse gives the identity, in the context of functors between categories.
More concisely: For any categories `C` and `D`, functors `F` and `G` from `C` to `D`, and isomorphism `α` between `F` and `G`, the composite of `α` and its inverse, when applied to any object `X` in `C`, results in the identity morphism on `G(X)`.
|
Mathlib.CategoryTheory.NatIso._auxLemma.2
theorem Mathlib.CategoryTheory.NatIso._auxLemma.2 :
∀ {α : Sort u} {r : α → α → Prop} [inst : IsRefl α r] (a : α), r a a = True
This theorem states that for any type 'α' and a binary relation 'r' over this type, where 'r' is reflexive (meaning that 'r a a' holds for all 'a' in 'α'), then the proposition 'r a a' is always true for any element 'a' of 'α'. Essentially, this theorem is affirming the reflexivity of the relation 'r' in terms of propositional logic by setting 'r a a' equal to 'True' for all 'a'.
More concisely: For any reflexive binary relation r on type α, we have r a a holds for all a in α.
|
CategoryTheory.Iso.hom_inv_id_app
theorem CategoryTheory.Iso.hom_inv_id_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 ≅ G) (X : C),
CategoryTheory.CategoryStruct.comp (α.hom.app X) (α.inv.app X) = CategoryTheory.CategoryStruct.id (F.obj X)
This theorem, `CategoryTheory.Iso.hom_inv_id_app`, states that for any two categories `C` and `D`, with `C` being of type `u₁` and `D` being of type `u₂`, and for any two functors `F` and `G` from `C` to `D`, if `α` is an isomorphism between `F` and `G`, then the composition of the morphism from `F` to `G` and the inverse of this morphism, when both are applied to an object `X` in `C`, is equal to the identity morphism on `F.obj X` in `D`. In mathematical terms, we have `(α.hom.app X) ∘ (α.inv.app X) = id(F.obj X)`, where `∘` denotes composition of morphisms, `id(F.obj X)` is the identity morphism on `F.obj X`, and `α.hom.app X` and `α.inv.app X` are the application of the morphism and its inverse to `X`, respectively.
More concisely: For any categories `C` and `D`, functors `F` and `G` between them, and isomorphism `α` between `F` and `G`, the composition of `α` and its inverse, when applied to any object `X` in `C`, equals the identity morphism on `F(X)` in `D`.
|
CategoryTheory.NatIso.naturality_1
theorem CategoryTheory.NatIso.naturality_1 :
∀ {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 : C} (α : F ≅ G)
(f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp (α.inv.app X) (CategoryTheory.CategoryStruct.comp (F.map f) (α.hom.app Y)) =
G.map f
This theorem states that for any two categories 'C' and 'D', and any two functors 'F' and 'G' from 'C' to 'D', if 'α' is a natural isomorphism between 'F' and 'G', then for any morphism 'f' from object 'X' to 'Y' in 'C', the composition of the inverse of the application of 'α' at 'X' with the composition of the mapping of 'f' by 'F' and the application of 'α' at 'Y', equals the mapping of 'f' by 'G'. In essence, this theorem encapsulates the naturality condition of a natural isomorphism in category theory.
More concisely: For any categories 'C' and 'D', functors 'F' and 'G' from 'C' to 'D', and natural isomorphism α between F and G: for all objects X and Y in C and morphism f from X to Y, α⁻¹∘F(f)∘α(Y) = G(f).
|
CategoryTheory.Iso.inv_hom_id_app_assoc
theorem CategoryTheory.Iso.inv_hom_id_app_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} (α : F ≅ G) (X : C) {Z : D}
(h : G.obj X ⟶ Z),
CategoryTheory.CategoryStruct.comp (α.inv.app X) (CategoryTheory.CategoryStruct.comp (α.hom.app X) h) = h
This theorem, titled `CategoryTheory.Iso.inv_hom_id_app_assoc`, states that for any categories `C` and `D` with functors `F` and `G` between them, if `α` is a natural isomorphism between `F` and `G` and `X` is an object of `C`, then for any morphism `h` from `G.obj X` to some object `Z` in `D`, the composition of the inverse of the component of `α` at `X` with the composition of the component of `α` at `X` and `h` is equal to `h`. In other words, it demonstrates that the inverse of a natural isomorphism, when composed with the original isomorphism, results in the identity, in accordance with the properties of an isomorphism in category theory.
More concisely: Given categories `C`, `D` with functors `F` and `G` between them, a natural isomorphism `α: F ≅ G`, and an object `X` in `C` and a morphism `h: G(X) → Z` in `D`, the composition of `h` with `α.inv (X)` and `α (X)` is equal to `h`.
|
CategoryTheory.Iso.hom_inv_id_app_assoc
theorem CategoryTheory.Iso.hom_inv_id_app_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} (α : F ≅ G) (X : C) {Z : D}
(h : F.obj X ⟶ Z),
CategoryTheory.CategoryStruct.comp (α.hom.app X) (CategoryTheory.CategoryStruct.comp (α.inv.app X) h) = h
The theorem `CategoryTheory.Iso.hom_inv_id_app_assoc` states that for any two functors `F` and `G` from a category `C` to another category `D`, given a natural isomorphism `α : F ≅ G`, and for any object `X` in `C`, and morphism `h : F.obj X ⟶ Z`, the composition of `α.hom.app X` and the composition of `α.inv.app X` with `h` is equal to `h`. In other words, the homomorphism of `α` for `X`, followed by the inverse of the homomorphism of `α` for `X` then `h`, is equal to `h`. This is an instance of the property that the composition of an isomorphism and its inverse acts as an identity.
More concisely: Given functors F and G between categories, a natural isomorphism α : F ≅ G, and an object X in the domain category and a morphism h : F X → Z, we have α.hom.app X * α.inv.app X * h = h.
|
CategoryTheory.NatIso.inv_inv_app
theorem CategoryTheory.NatIso.inv_inv_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} (e : F ≅ G) (X : C),
CategoryTheory.inv (e.inv.app X) = e.hom.app X
The theorem `CategoryTheory.NatIso.inv_inv_app` establishes that in any two categories `C` and `D`, for every natural isomorphism `e` between two functors `F` and `G` from `C` to `D`, and for every object `X` in `C`, the inverse of the application of the inverse natural transformation of `e` to `X` is equal to the application of the homomorphism part of `e` to `X`. Essentially, this theorem is stating that the inverse of the inverse of a natural transformation, when applied to an object, gives back the original natural transformation when applied to the same object.
More concisely: Given any two categories `C` and `D`, and a natural isomorphism `e` between functors `F` and `G` from `C` to `D`, for every object `X` in `C`, the inverse of the application of the inverse natural transformation of `e` to `X` equals the application of `e` to `X`.
|
Mathlib.CategoryTheory.NatIso._auxLemma.5
theorem Mathlib.CategoryTheory.NatIso._auxLemma.5 :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f]
{g h : Z ⟶ X}, (CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp h f) = (g = h)
The theorem `Mathlib.CategoryTheory.NatIso._auxLemma.5` asserts that for any Category `C` and objects `X`, `Y`, and `Z` within this Category, given a morphism `f` from `X` to `Y` that is monic (or injective), and two morphisms `g` and `h` from `Z` to `X`, the statement that the composition of `g` and `f` is equal to the composition of `h` and `f` implies that `g` is equal to `h`. This is a property related to the cancellation law for monic (or injective) morphisms in category theory.
More concisely: Given a category C, objects X, Y, Z, a monic morphism f : X -> Y, and morphisms g, h : Z -> X with g \* f = h \* f, then g = h.
|