CategoryTheory.IsIso.inv_comp
theorem CategoryTheory.IsIso.inv_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {h : Y ⟶ Z}
[inst_1 : CategoryTheory.IsIso f] [inst_2 : CategoryTheory.IsIso h],
CategoryTheory.inv (CategoryTheory.CategoryStruct.comp f h) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.inv h) (CategoryTheory.inv f)
This theorem, named `CategoryTheory.IsIso.inv_comp`, states that in any category `C`, for any three objects `X`, `Y`, and `Z` in this category, and for any two morphisms `f` from `X` to `Y` and `h` from `Y` to `Z` which are both isomorphisms, the inverse of the composition of `f` and `h` is equal to the composition of the inverse of `h` and the inverse of `f`. In mathematical terms, if both `f` and `h` are isomorphisms (invertible morphisms), then the inverse of `f` composed with `h` is the same as the composition of the inverse of `h` and the inverse of `f`.
More concisely: In any category, if two isomorphisms compose, their inverses are inverse to each other.
|
Mathlib.CategoryTheory.Iso._auxLemma.5
theorem Mathlib.CategoryTheory.Iso._auxLemma.5 :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ⟶ Y) [inst_1 : CategoryTheory.IsIso α]
{f : Z ⟶ Y} {g : Z ⟶ X},
(CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv α) = g) =
(f = CategoryTheory.CategoryStruct.comp g α)
This theorem states that in a category 'C', for any objects 'X', 'Y', and 'Z' and given a morphism 'α' from 'X' to 'Y' which is an isomorphism, for any morphisms 'f' from 'Z' to 'Y' and 'g' from 'Z' to 'X', the composition of 'f' and the inverse of 'α' is equal to 'g' if and only if 'f' is equal to the composition of 'g' and 'α'.
Here, the symbol '⟶' denotes a morphism between objects in the category, while 'CategoryTheory.CategoryStruct.comp' represents the composition of two morphisms and 'CategoryTheory.inv' represents the inverse of a morphism.
More concisely: In a category C, given an isomorphism α : X ⟶ Y and morphisms f : Z ⟶ Y and g : Z ⟶ X, f ∘ α⁻¹ = g if and only if f = g ∘ α.
|
CategoryTheory.Iso.trans_assoc
theorem CategoryTheory.Iso.trans_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z Z' : C} (α : X ≅ Y) (β : Y ≅ Z) (γ : Z ≅ Z'),
(α.trans β).trans γ = α.trans (β.trans γ)
This theorem states that in any category `C`, for any objects `X`, `Y`, `Z`, and `Z'` in `C`, and for any isomorphisms `α` from `X` to `Y`, `β` from `Y` to `Z`, and `γ` from `Z` to `Z'`, the composition of the composed isomorphism `(α ≪≫ β)` and `γ` is equal to the composition of `α` and the composed isomorphism `β ≪≫ γ`. This is the associativity law for isomorphism composition in category theory, analogous to the associativity law for multiplication in algebra.
More concisely: In any category, the composition of two isomorphisms is independent of the order: `(α ≪≫ β) = α ≪≫ γ <=> β ≪≫ γ = γ ≪≫ α`, where `α: X ⟹ Y`, `β: Y ⟹ Z`, and `γ: Z ⟹ Z'` are isomorphisms.
|
CategoryTheory.IsIso.Iso.inv_inv
theorem CategoryTheory.IsIso.Iso.inv_inv :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ≅ Y), CategoryTheory.inv f.inv = f.hom
This theorem states that, given a category with objects of type `C`, and for any two objects `X` and `Y` in `C`, if `f` is an isomorphism from `X` to `Y`, then the inverse of the inverse of `f` is the original morphism `f`. In other words, this theorem is asserting the property that the double inversion of an isomorphism yields the original isomorphism in the context of category theory.
More concisely: Given an isomorphism `f` between objects `X` and `Y` in a category, the inverse of `f`'s inverse is equal to `f`.
|
CategoryTheory.Iso.hom_inv_id_assoc
theorem CategoryTheory.Iso.hom_inv_id_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y) {Z : C} (h : X ⟶ Z),
CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp self.inv h) = h
This theorem states that in any category `C`, for any objects `X`, `Y`, and `Z` in `C`, and for any isomorphism `self` from `X` to `Y`, and any morphism `h` from `X` to `Z`, the composition of `self.hom` and `CategoryTheory.CategoryStruct.comp self.inv h`, or in other words the composition of the morphism of the isomorphism and the composition of the inverse of the isomorphism with the morphism `h`, is equal to `h`. In simpler terms, it asserts that if we follow an isomorphism and then its inverse, and then continue with some morphism, it's as if we did nothing before continuing with that morphism. This is akin to saying that an isomorphism and its inverse form an identity when composed, meaning it doesn't produce any effective change when applied before other morphisms.
More concisely: In any category, composing an isomorphism with its inverse and then with a morphism is equal to composing the morphism with the isomorphism.
|
CategoryTheory.IsIso.comp_inv_eq
theorem CategoryTheory.IsIso.comp_inv_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ⟶ Y) [inst_1 : CategoryTheory.IsIso α]
{f : Z ⟶ Y} {g : Z ⟶ X},
CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv α) = g ↔ f = CategoryTheory.CategoryStruct.comp g α
This theorem is a statement about the composition of morphisms in a category theory framework. Given a category `C` and objects `X`, `Y`, and `Z` in `C`, if `α` is an isomorphism from `X` to `Y`, the theorem states that for any morphisms `f : Z ⟶ Y` and `g : Z ⟶ X`, the composition of `f` and the inverse of `α` is equal to `g` if and only if `f` is equal to the composition of `g` and `α`. In less formal terms, this theorem is a condition for the exchange of a morphism and its inverse in a composition of morphisms.
More concisely: In a category `C`, given objects `X`, `Y`, `Z`, an isomorphism `α : X ≈ Y`, morphisms `f : Z ⟶ Y`, and `g : Z ⟶ X`, `f ∘ α⁻¹ = g` if and only if `f = g ∘ α`.
|
CategoryTheory.Iso.comp_inv_eq
theorem CategoryTheory.Iso.comp_inv_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X},
CategoryTheory.CategoryStruct.comp f α.inv = g ↔ f = CategoryTheory.CategoryStruct.comp g α.hom
This theorem states that for any category `C` with objects `X`, `Y`, and `Z`, and given an isomorphism `α` from `X` to `Y`, and morphisms `f` from `Z` to `Y` and `g` from `Z` to `X`, the composition of `f` with the inverse of `α` is equal to `g` if and only if `f` is equal to the composition of `g` with `α`. In other words, it asserts that in a category, pre-composing with an isomorphism's inverse and post-composing with the isomorphism are inverse operations to each other.
More concisely: For any category `C` and isomorphism `α: X ↔ Y` between objects `X` and `Y`, morphisms `f: Z → Y` and `g: Z → X`, the conditions `f ∘ α⁻¹ = g` and `g ∘ α = f` are equivalent.
|
CategoryTheory.Functor.map_inv
theorem CategoryTheory.Functor.map_inv :
∀ {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} (f : X ⟶ Y) [inst_2 : CategoryTheory.IsIso f],
F.map (CategoryTheory.inv f) = CategoryTheory.inv (F.map f)
The theorem `CategoryTheory.Functor.map_inv` states that for any category `C` and `D`, and any functor `F` from `C` to `D`, if `f` is an isomorphism in the category `C` from `X` to `Y`, then the image of the inverse of `f` under the functor `F` is equal to the inverse of the image of `f` under `F`. In other words, a functor preserves the inverse of isomorphisms.
More concisely: If `f: X → Y` is an isomorphism in a category `C` and `F: C → D` is a functor, then `F(f)^-1 = F(f^-1)`.
|
CategoryTheory.Iso.refl_trans
theorem CategoryTheory.Iso.refl_trans :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y),
(CategoryTheory.Iso.refl X).trans α = α
This theorem states that for any category `C` and any two objects `X` and `Y` in `C`, if there is an isomorphism `α` between `X` and `Y`, then the composition of the identity isomorphism on `X` and `α` is equal to `α`. This identity isomorphism is defined such that its forward and backward morphisms are simply the identity on `X`. In other words, pre-composing the isomorphism `α` with the identity mapping on `X` doesn't change `α`.
More concisely: Given any category C, isomorphism α between objects X and Y in C implies identity on X ∘ α = α.
|
CategoryTheory.IsIso.hom_inv_id
theorem CategoryTheory.IsIso.hom_inv_id :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f],
CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv f) = CategoryTheory.CategoryStruct.id X
This theorem states that for any category `C` and any objects `X` and `Y` in `C`, if a morphism `f` from `X` to `Y` is an isomorphism (i.e., has an inverse), then the composition of `f` and its inverse is the identity morphism on `X`. In mathematical terms, if we have an isomorphism `f: X ⟶ Y`, then `f ∘ f⁻¹ = id_X`, where `f⁻¹` is the inverse of `f` and `id_X` is the identity morphism on `X`.
More concisely: For any category `C` and objects `X`, `Y` in `C`, if `f : X ⟶ Y` is an isomorphism, then `f ∘ f⁻¹ = id_X`.
|
CategoryTheory.Functor.mapIso_refl
theorem CategoryTheory.Functor.mapIso_refl :
∀ {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 : C),
F.mapIso (CategoryTheory.Iso.refl X) = CategoryTheory.Iso.refl (F.obj X)
This theorem states that for any category `C` and `D`, and any functor `F` from `C` to `D`, the mapping of the identity isomorphism on an object `X` of `C` under the functor `F` is equal to the identity isomorphism on the image of `X` under the functor `F`. More formally, for any object `X` in `C`, `F.mapIso` applied to the identity isomorphism on `X` will yield the identity isomorphism on `F.obj X`. This exhibits that functors preserve identity isomorphisms.
More concisely: For any functor F from category C to category D and any object X in C, the image under F of the identity isomorphism on X is equal to the identity isomorphism on F(X).
|
CategoryTheory.Iso.ext
theorem CategoryTheory.Iso.ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} ⦃α β : X ≅ Y⦄, α.hom = β.hom → α = β
This theorem states that in any category `C`, for any two objects `X` and `Y` in `C`, if `α` and `β` are two isomorphisms from `X` to `Y`, then if the `hom` (the morphism part of the isomorphism) of `α` is equal to the `hom` of `β`, then the isomorphisms `α` and `β` are equal. In other words, in a category theory context, two isomorphisms are considered the same if they have the same morphism component.
More concisely: In any category, two isomorphisms between objects have equal morphism components if and only if they are equal as isomorphisms.
|
Mathlib.CategoryTheory.Iso._auxLemma.10
theorem Mathlib.CategoryTheory.Iso._auxLemma.10 :
∀ {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)
This theorem states that in any category `C`, for any objects `X`, `Y`, `Z` in `C`, and a monomorphism `f` from `X` to `Y`, if `g` and `h` are morphisms from `Z` to `X`, then the composition of `g` and `f` is equal to the composition of `h` and `f` if and only if `g` is equal to `h`. The condition of `f` being a monomorphism, in category theory, means that `f` is left-cancellable, i.e., for any pair of morphisms `g` and `h`, if the composition of `g` and `f` equals the composition of `h` and `f`, then `g` must equal `h`.
More concisely: In any category, if a morphism is a monomorphism and given objects X, Y, Z with morphisms g and h from Z to X, then g = h if and only if the composition of g and f equals the composition of h and f.
|
Mathlib.CategoryTheory.Iso._auxLemma.8
theorem Mathlib.CategoryTheory.Iso._auxLemma.8 :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ≅ Y) (g g' : Y ⟶ Z),
(CategoryTheory.CategoryStruct.comp f.hom g = CategoryTheory.CategoryStruct.comp f.hom g') = (g = g')
This theorem, "Mathlib.CategoryTheory.Iso._auxLemma.8", asserts that in any mathematical category 'C', for any three objects 'X', 'Y', and 'Z', and for any isomorphism 'f' from 'X' to 'Y' and any two morphisms 'g' and 'g'' from 'Y' to 'Z', the composition of the isomorphism 'f' with the morphisms 'g' and 'g'' are equal if and only if the two morphisms 'g' and 'g'' are themselves equal. This condition essentially says that the isomorphism 'f' preserves the equality of morphisms from 'Y' to 'Z'.
More concisely: In any category, if two morphisms from an object to another have equal compositions with an isomorphism, then they are equal.
|
CategoryTheory.IsIso.inv_comp_eq
theorem CategoryTheory.IsIso.inv_comp_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ⟶ Y) [inst_1 : CategoryTheory.IsIso α]
{f : X ⟶ Z} {g : Y ⟶ Z},
CategoryTheory.CategoryStruct.comp (CategoryTheory.inv α) f = g ↔ f = CategoryTheory.CategoryStruct.comp α g
The theorem `CategoryTheory.IsIso.inv_comp_eq` states that in any category `C`, for any objects `X`, `Y`, and `Z` in `C` and any isomorphism `α` from `X` to `Y`, and any morphisms `f` from `X` to `Z` and `g` from `Y` to `Z`, the composition of the inverse of `α` and `f` equals `g` if and only if `f` equals the composition of `α` and `g`. In other words, it provides a condition under which two morphisms are equal in terms of the composition of an isomorphism and another morphism.
More concisely: For any category C, given objects X, Y, Z, an isomorphism α from X to Y, and morphisms f from X to Z and g from Y to Z, if and only if the composition of the inverse of α and f equals g, then f equals the composition of α and g.
|
CategoryTheory.IsIso.Iso.inv_hom
theorem CategoryTheory.IsIso.Iso.inv_hom :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ≅ Y), CategoryTheory.inv f.hom = f.inv
This theorem, `CategoryTheory.IsIso.Iso.inv_hom`, states that for any category `C`, and any two objects `X` and `Y` in that category, if we have an isomorphism `f` from `X` to `Y`, then the inverse of the morphism `f.hom` as computed by the function `CategoryTheory.inv` is equal to `f.inv`. In other words, the inverse of the morphism given by an isomorphism, as defined by the `CategoryTheory.inv` function, is the same as the inverse morphism in the isomorphism itself.
More concisely: For any category C and isomorphism f : X ≈ Y in C, the inverse morphisms f^-1 and CategoryTheory.inv f agree: f^-1 = CategoryTheory.inv f.hom.
|
CategoryTheory.Iso.inv_ext'
theorem CategoryTheory.Iso.inv_ext' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ≅ Y} {g : Y ⟶ X},
CategoryTheory.CategoryStruct.comp f.hom g = CategoryTheory.CategoryStruct.id X → g = f.inv
This theorem, `CategoryTheory.Iso.inv_ext'`, states that for any category `C` and any two objects `X` and `Y` in `C`, if `f` is an isomorphism from `X` to `Y` and `g` is a morphism from `Y` to `X`, then if the composition of `f` and `g` equals the identity morphism on `X`, it follows that `g` equals the inverse of `f`. In simpler terms, if applying `f` then `g` leaves an object unchanged, then `g` undoes exactly what `f` does.
More concisely: If `f: X ➝ Y` is an isomorphism in a category `C` and `g: Y ➝ X` is a morphism such that `g ∘ f = id_X`, then `g = f^(-1)`.
|
CategoryTheory.Iso.symm_hom
theorem CategoryTheory.Iso.symm_hom :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y), α.symm.hom = α.inv
This theorem states that in any category `C`, for all objects `X` and `Y` in `C`, if there exists an isomorphism `α` between `X` and `Y`, then the morphism from `Y` to `X` in the inverse of `α` (denoted as `α.symm.hom`) is equal to the inverse of `α` (denoted as `α.inv`). In simpler terms, it asserts that the morphism of the inverse of an isomorphism is the inverse of the original isomorphism itself, in the context of category theory.
More concisely: In any category, the inverse of an isomorphism is equal to its symmetric morphism (i.e., the morphism induced by composing the isomorphism with its inverse).
|
CategoryTheory.Iso.eq_inv_comp
theorem CategoryTheory.Iso.eq_inv_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z},
g = CategoryTheory.CategoryStruct.comp α.inv f ↔ CategoryTheory.CategoryStruct.comp α.hom g = f
This theorem from category theory, `CategoryTheory.Iso.eq_inv_comp`, states that for any category `C` with objects `X`, `Y` and `Z`, and an isomorphism `α` from `X` to `Y`, the morphism `g` from `Y` to `Z` is equal to the composition of the inverse of `α` and `f` if and only if the composition of `α` and `g` is equal to `f`. In other words, the theorem describes a property of the composition of morphisms in a category involving an isomorphism.
More concisely: For any category C, an isomorphism α from X to Y in C makes morphisms f : X → Z and g : Y → Z equal if and only if g = f ∘ α^(-1).
|
Mathlib.CategoryTheory.Iso._auxLemma.2
theorem Mathlib.CategoryTheory.Iso._auxLemma.2 :
∀ {obj : Type u} [self : CategoryTheory.Category.{v, u} obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z),
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h
This theorem states that in any category, given four objects W, X, Y, Z and three morphisms f: W → X, g: X → Y, and h: Y → Z, the composition of f with the composition of g and h is equal to the composition of the composition of f and g with h. In other words, this theorem is asserting the associativity of the composition of morphisms in a category, an essential property in category theory.
More concisely: In any category, the composition of morphisms is associative: (f \*. g) \*. h = f \*. (g \*. h) for morphisms f: W → X, g: X → Y, and h: Y → Z.
|
CategoryTheory.eq_of_inv_eq_inv
theorem CategoryTheory.eq_of_inv_eq_inv :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [inst_1 : CategoryTheory.IsIso f]
[inst_2 : CategoryTheory.IsIso g], CategoryTheory.inv f = CategoryTheory.inv g → f = g
This theorem states that in any category `C`, for any objects `X` and `Y` in `C`, if `f` and `g` are morphisms from `X` to `Y` and both `f` and `g` are isomorphisms, then if the inverse of `f` is equal to the inverse of `g`, it follows that `f` is equal to `g`. In essence, it asserts the uniqueness of inverses in a category.
More concisely: In any category, if two morphisms between objects have equal sources and targets and are mutually inverse to isomorphic morphisms, then they are equal.
|
CategoryTheory.IsIso.inv_inv
theorem CategoryTheory.IsIso.inv_inv :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [inst_1 : CategoryTheory.IsIso f],
CategoryTheory.inv (CategoryTheory.inv f) = f
The theorem `CategoryTheory.IsIso.inv_inv` states that for any category `C` and any two objects `X` and `Y` in `C`, if `f` is an isomorphism (as indicated by `CategoryTheory.IsIso f`) from `X` to `Y`, then the inverse of the inverse of `f` is equal to `f` itself. In other words, this theorem ensures the "double inversion" property in the category theory context: applying the inverse operation twice on an isomorphism results in the original isomorphism.
More concisely: For any category `C` and objects `X` and `Y` with an isomorphism `f : X ↔ Y`, the inverse of `f` is the inverse of its own inverse, i.e., `(fun inv_f => inv_f ∘ inv_f) f = f`.
|
CategoryTheory.IsIso.hom_inv_id_assoc
theorem CategoryTheory.IsIso.hom_inv_id_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f] {Z : C}
(g : X ⟶ Z),
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) g) = g
The theorem `CategoryTheory.IsIso.hom_inv_id_assoc` states that for any objects `X`, `Y`, and `Z` in a category `C`, and for any morphism `f` from `X` to `Y` that is an isomorphism, composing `f` with the composition of the inverse of `f` and another morphism `g` from `X` to `Z` is equal to `g`. In other words, (f ⋅ (f⁻¹ ⋅ g)) = g. This can be seen as a generalization of the cancellation property in group theory to the setting of categories.
More concisely: For any objects X, Y, Z in a category C and isomorphism f from X to Y, f ⋅ (f⁻¹ ⋅ g) = g holds for any morphism g from X to Z.
|
CategoryTheory.Iso.self_symm_id
theorem CategoryTheory.Iso.self_symm_id :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y),
α.trans α.symm = CategoryTheory.Iso.refl X
This theorem states that for any category `C` and any objects `X` and `Y` in `C`, if there exists an isomorphism `α` from `X` to `Y`, then the composition of `α` and its inverse (`α.symm`) is the identity isomorphism on `X`. In other words, an isomorphism followed by its inverse will have no effect on `X`, demonstrating a fundamental feature of isomorphisms in category theory, which is their reversibility.
More concisely: In any category, for any objects X and Y with an isomorphism α from X to Y, α \* α.symm = id\_(X) holds. (Here, \* denotes composition, id\_(X) is the identity isomorphism on X, and symm denotes the symmetric inverse of α.)
|
CategoryTheory.Functor.mapIso_inv
theorem CategoryTheory.Functor.mapIso_inv :
∀ {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} (i : X ≅ Y), (F.mapIso i).inv = F.map i.inv
This theorem states that for any category `C`, its corresponding category `D`, and a functor `F` that maps from `C` to `D`, if `X` and `Y` are objects in `C` that are isomorphic (denoted by `X ≅ Y`), then the inverse of the functor's map applied to the isomorphism (`(F.mapIso i).inv`) is equal to the functor's map applied to the inverse isomorphism (`F.map i.inv`). This means that the functor preserves the isomorphism structure between objects in the underlying categories.
More concisely: Given any category `C`, functor `F` from `C` to another category `D`, and isomorphisms `i : X ≅ Y` in `C`, the inverse of `F.mapIso i` is equal to `F.map (i.inv)`.
|
CategoryTheory.IsIso.eq_inv_of_hom_inv_id
theorem CategoryTheory.IsIso.eq_inv_of_hom_inv_id :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [inst_1 : CategoryTheory.IsIso f]
{g : Y ⟶ X},
CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X → g = CategoryTheory.inv f
This theorem, `CategoryTheory.IsIso.eq_inv_of_hom_inv_id`, asserts that for any given category `C` which contains objects `X` and `Y`, if there exists an isomorphism `f : X ⟶ Y` and a morphism `g : Y ⟶ X` such that the composition of `f` and `g` is the identity on `X`, then `g` must be the inverse of `f`. In other words, if for an isomorphism `f` we have `f ≫ g = id_X`, then `g` is the inverse of `f`, or `g = f⁻¹` in notations.
More concisely: If in a category `C` there exists an isomorphism `f : X ⟶ Y` with `id_X = f ∘ g` for some morphism `g : Y ⟶ X`, then `g` is the inverse of `f`.
|
CategoryTheory.IsIso.inv_id
theorem CategoryTheory.IsIso.inv_id :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
CategoryTheory.inv (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id X
This theorem states that in any category `C`, for any object `X` in `C`, the inverse of the identity morphism on `X` is the identity morphism on `X` itself. In the language of category theory, this theorem asserts that the identity morphism is its own inverse.
More concisely: In any category, the identity morphism is equal to its own inverse for every object.
|
Mathlib.CategoryTheory.Iso._auxLemma.4
theorem Mathlib.CategoryTheory.Iso._auxLemma.4 :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ⟶ Y) [inst_1 : CategoryTheory.IsIso α]
{f : X ⟶ Z} {g : Y ⟶ Z},
(g = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv α) f) =
(CategoryTheory.CategoryStruct.comp α g = f)
This theorem states that for any category `C` and objects `X`, `Y`, `Z` in `C`, given an isomorphism `α` from `X` to `Y`, and morphisms `f` from `X` to `Z` and `g` from `Y` to `Z`, the equality `g = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv α) f` is equivalent to `CategoryTheory.CategoryStruct.comp α g = f`. In simpler terms, this theorem states that if you compose the inverse of isomorphism `α` with the morphism `f` and get `g`, it is same as composing `α` with `g` to get `f`. This captures a fundamental property of isomorphisms in category theory: they can be "undone" or "reversed" using their inverse.
More concisely: For any category `C` and isomorphisms `α:` `X ↔ Y` in `C`, morphisms `f:` `X → Z`, and `g:` `Y → Z`, the equality `g = α⁻¹ ∘ f` is equivalent to `α ∘ g = f`.
|
CategoryTheory.Iso.symm_self_id
theorem CategoryTheory.Iso.symm_self_id :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y),
α.symm.trans α = CategoryTheory.Iso.refl Y
This theorem states that for any category `C` and any objects `X` and `Y` in `C`, given an isomorphism `α` between `X` and `Y`, the composition of the inverse of `α` and `α` itself results in the identity isomorphism on `Y`. In other words, the inverse of an isomorphism followed by the isomorphism gives you back the identity. This is similar to the principle in mathematics where the inverse of a function followed by the function itself yields the identity function.
More concisely: For any isomorphism α between objects X and Y in a category C, α⁻¹ ∘ α = idY, where idY is the identity isomorphism on Y.
|
CategoryTheory.Iso.hom_inv_id
theorem CategoryTheory.Iso.hom_inv_id :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y),
CategoryTheory.CategoryStruct.comp self.hom self.inv = CategoryTheory.CategoryStruct.id X
This theorem states that, given any category `C`, objects `X` and `Y` in `C`, and an isomorphism `self` from `X` to `Y`, the composition of the morphism `self.hom` from `X` to `Y` and the inverse morphism `self.inv` from `Y` to `X` is equal to the identity morphism on `X`. In other words, if you go from `X` to `Y` and then come back to `X`, you get the same object `X` as before. This theorem is a fundamental property of isomorphisms in category theory, which can be thought of as a generalization of the notion of reversible processes in mathematics.
More concisely: Given any category `C`, for any isomorphism `self : X ↔ Y` in `C`, the composition `self.hom * self.symm` equals the identity morphism on `X`. (Here, `self.hom` is the morphism from `X` to `Y`, `self.symm` is the inverse morphism, and `*` denotes composition of morphisms.)
|
CategoryTheory.IsIso.of_isIso_comp_right
theorem CategoryTheory.IsIso.of_isIso_comp_right :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
[inst_1 : CategoryTheory.IsIso g] [inst_2 : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f g)],
CategoryTheory.IsIso f
The theorem `CategoryTheory.IsIso.of_isIso_comp_right` states that for any category `C`, and any three objects `X`, `Y`, and `Z` in `C`, if there exists a morphism `f` from `X` to `Y` and a morphism `g` from `Y` to `Z`, such that `g` is an isomorphism and the composition of `f` and `g` is also an isomorphism, then `f` itself must be an isomorphism. In other words, if `g` and `f ≫ g` are isomorphisms, then `f` is an isomorphism as well.
More concisely: If `f: X ⟶ Y` and `g: Y ⟶ Z` are morphisms in a category `C` with `g` an isomorphism and `f ∘ g` also an isomorphism, then `f` is an isomorphism.
|
CategoryTheory.IsIso.inv_hom_id_assoc
theorem CategoryTheory.IsIso.inv_hom_id_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f] {Z : C}
(g : Y ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) (CategoryTheory.CategoryStruct.comp f g) = g
The theorem `CategoryTheory.IsIso.inv_hom_id_assoc` states that for any category `C`, and for any objects `X`, `Y`, and `Z` in `C`, given a morphism `f` from `X` to `Y` that is an isomorphism, and another morphism `g` from `Y` to `Z`, the composition of the inverse of `f` with the composition of `f` and `g` is equal to `g`. This is a property of the categories where the composition of a morphism with its inverse behaves like an identity in the context of composition.
More concisely: For any category `C`, given isomorphisms `f : X ⟶ Y` and `g : Y ⟶ Z` in `C`, the composition `g ∘ f⁻¹` is equal to the identity morphism `id_Z : Z ⟶ Z`.
|
CategoryTheory.Iso.eq_comp_inv
theorem CategoryTheory.Iso.eq_comp_inv :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X},
g = CategoryTheory.CategoryStruct.comp f α.inv ↔ CategoryTheory.CategoryStruct.comp g α.hom = f
This theorem states that in any category `C`, for any objects `X`, `Y`, and `Z` in `C`, and any isomorphism `α` between `X` and `Y`, a morphism `g` from `Z` to `X` equals the composition of a morphism `f` from `Z` to `Y` and the inverse of `α` if and only if the composition of `g` and the isomorphism `α` equals `f`. In other words, this theorem presents a condition of equality for morphisms in terms of composition with an isomorphism and its inverse.
More concisely: In any category, given objects X, Y, Z, an isomorphism α : X ↔ Y, and morphisms g : Z → X and f : Z → Y, the conditions g = f α and α . g = f hold if and only if g = f.
|
CategoryTheory.IsIso.eq_inv_comp
theorem CategoryTheory.IsIso.eq_inv_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ⟶ Y) [inst_1 : CategoryTheory.IsIso α]
{f : X ⟶ Z} {g : Y ⟶ Z},
g = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv α) f ↔ CategoryTheory.CategoryStruct.comp α g = f
The theorem `CategoryTheory.IsIso.eq_inv_comp` states that in any category 'C' with object types 'X', 'Y', and 'Z', and given a morphism 'α' from 'X' to 'Y' which is an isomorphism (i.e., has an inverse), and arbitrary morphisms 'f' from 'X' to 'Z' and 'g' from 'Y' to 'Z', then 'g' is equal to the composition of the inverse of 'α' and 'f' if and only if the composition of 'α' and 'g' is equal to 'f'. In other words, we can swap between pre-composing with the inverse of 'α' and post-composing with 'α' itself when we are working with isomorphisms.
More concisely: Given a category 'C' with object types 'X', 'Y', and 'Z', an isomorphism α : X ↔ Y, and arbitrary morphisms f : X → Z and g : Y → Z, the following are equivalent: g = α⁻¹ ∘ f if and only if f = α ∘ g.
|
CategoryTheory.IsIso.inv_eq_of_hom_inv_id
theorem CategoryTheory.IsIso.inv_eq_of_hom_inv_id :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [inst_1 : CategoryTheory.IsIso f]
{g : Y ⟶ X},
CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X → CategoryTheory.inv f = g
The theorem `CategoryTheory.IsIso.inv_eq_of_hom_inv_id` states that for any category `C` and objects `X` and `Y` within `C`, if there is an isomorphism `f` from `X` to `Y` and another morphism `g` from `Y` to `X`, such that the composition of `f` and `g` equals the identity on `X`, then `g` is the inverse of `f`. In other words, if composing `f` with `g` results in the identity morphism (doing nothing), then `g` undoes exactly what `f` does and so `g` is the inverse of `f`.
More concisely: If in a category, the composition of an isomorphism with its right inverse equals the identity morphism, then they are inverses of each other.
|
CategoryTheory.Iso.trans_refl
theorem CategoryTheory.Iso.trans_refl :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y),
α.trans (CategoryTheory.Iso.refl Y) = α
This theorem states that in any category `C`, for any objects `X` and `Y` in `C`, and for any isomorphism `α` from `X` to `Y`, the composition of `α` with the identity isomorphism on `Y` is just `α`. In other words, when you follow the isomorphism `α` by doing nothing (applying the identity), you have effectively just applied `α`. This reflects the identity property of composition with the identity isomorphism in category theory.
More concisely: In any category, the composition of an isomorphism with the identity isomorphism is equal to the isomorphism itself.
|
CategoryTheory.Functor.mapIso_trans
theorem CategoryTheory.Functor.mapIso_trans :
∀ {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 Z : C} (i : X ≅ Y) (j : Y ≅ Z),
F.mapIso (i.trans j) = (F.mapIso i).trans (F.mapIso j)
In the context of category theory, this theorem states that for any category `C` and `D`, and any functor `F` mapping `C` to `D`, if we have isomorphisms `i` and `j` for objects `X`, `Y`, and `Z` in `C` such that `X ≅ Y` and `Y ≅ Z`, then the isomorphism induced by the functor `F` on the composition of the isomorphisms `i` and `j` is the same as the composition of the isomorphisms induced by `F` on `i` and `j` individually. In other words, functor preserves the transitivity of isomorphisms.
More concisely: For any functor F between categories C and D, if X iso Y and Y iso Z in C imply F(X) iso F(Y) iso F(Z) in D, then F preserves the transitivity of isomorphisms.
|
CategoryTheory.IsIso.inv_eq_of_inv_hom_id
theorem CategoryTheory.IsIso.inv_eq_of_inv_hom_id :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [inst_1 : CategoryTheory.IsIso f]
{g : Y ⟶ X},
CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id Y → CategoryTheory.inv f = g
The theorem `CategoryTheory.IsIso.inv_eq_of_inv_hom_id` states that for any category `C`, any two objects `X` and `Y` within this category, and a morphism `f` from `X` to `Y` that is an isomorphism, if there exists another morphism `g` from `Y` to `X` such that the composition of `g` and `f` is the identity on `Y` (denoted as `CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id Y`), then `g` is the inverse of `f` (denoted as `CategoryTheory.inv f = g`). In other words, if `g` composed with `f` results in the identity morphism, then `g` is the inverse of `f` according to the category theory.
More concisely: If in a category, the composition of the inverse morphism and a given isomorphism equals the identity on the domain of the isomorphism, then the inverse morphism is indeed the opposite isomorphism.
|
CategoryTheory.IsIso.of_isIso_comp_left
theorem CategoryTheory.IsIso.of_isIso_comp_left :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
[inst_1 : CategoryTheory.IsIso f] [inst_2 : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f g)],
CategoryTheory.IsIso g
The theorem `CategoryTheory.IsIso.of_isIso_comp_left` states that for any category `C` and any three objects `X`, `Y`, and `Z` in `C`, if the morphism `f` from `X` to `Y` is an isomorphism and the composition of `f` and `g` (where `g` is a morphism from `Y` to `Z`) is also an isomorphism, then `g` itself is an isomorphism. In other words, in the context of category theory, if a morphism and its composition with another morphism are both invertible, then the second morphism is also invertible.
More concisely: If `f: X ➝ Y` is an isomorphism in a category `C` and the composition `f ∘ g: Y ➝ Z` is an isomorphism for any `g: Y ➝ Z`, then `g` is an isomorphism.
|
CategoryTheory.Iso.comp_hom_eq_id
theorem CategoryTheory.Iso.comp_hom_eq_id :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {f : Y ⟶ X},
CategoryTheory.CategoryStruct.comp f α.hom = CategoryTheory.CategoryStruct.id Y ↔ f = α.inv
This theorem is about categories in category theory. It states that for any category 'C' and for any objects 'X' and 'Y' in 'C', given an isomorphism 'α' between 'X' and 'Y' and a morphism 'f' from 'Y' to 'X', the composition of the morphism 'f' with the homomorphism part of the isomorphism 'α' is equal to the identity morphism on 'Y' if and only if 'f' is equal to the inverse of the isomorphism 'α'. This is often a key property used in proofs involving isomorphisms in categories.
More concisely: For any category 'C', object 'X' and 'Y' in 'C', isomorphism 'α' : X ↔ Y, and morphism 'f' : Y → X, the condition f ∘ α.rightInv = idY if and only if f = α.inv holds.
|
CategoryTheory.Iso.inv_eq_inv
theorem CategoryTheory.Iso.inv_eq_inv :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ≅ Y), f.inv = g.inv ↔ f.hom = g.hom
This theorem states that in any category `C`, for any two objects `X` and `Y` in `C`, and any two isomorphisms `f` and `g` from `X` to `Y`, the inverse of `f` is equal to the inverse of `g` if and only if the morphism represented by `f` is equal to the morphism represented by `g`. This theorem thus provides a condition for the equality of two isomorphisms in a category, in terms of the equality of their inverses.
More concisely: In any category, two isomorphisms from one object to another have equal inverses if and only if they represent the same morphism.
|
CategoryTheory.Iso.inv_hom_id
theorem CategoryTheory.Iso.inv_hom_id :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y),
CategoryTheory.CategoryStruct.comp self.inv self.hom = CategoryTheory.CategoryStruct.id Y
This theorem states that for any category `C` and for any two objects `X` and `Y` in `C` that are isomorphic, the composition of the inverse of the isomorphism (`self.inv`) followed by the isomorphism itself (`self.hom`) is equal to the identity morphism on the target object `Y`. In other words, if we go from `Y` to `X` using the inverse and then return to `Y` using the original isomorphism, it's as if we did nothing. This is one of the fundamental properties of isomorphisms in category theory.
More concisely: For any isomorphism `f` from object `X` to object `Y` in a category `C`, the composition `f.hom * f.inv` equals the identity morphism `id Y`.
|
CategoryTheory.Iso.inv_hom_id_assoc
theorem CategoryTheory.Iso.inv_hom_id_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y) {Z : C} (h : Y ⟶ Z),
CategoryTheory.CategoryStruct.comp self.inv (CategoryTheory.CategoryStruct.comp self.hom h) = h
This theorem is in the field of Category Theory and it states that for any category `C` and any two objects `X` and `Y` in `C`, given an isomorphism `self` between `X` and `Y`, and a morphism `h` from `Y` to another object `Z` in `C`, the composition of the inverse of `self` with the composition of `self` and `h` is equal to `h`. In mathematical terms, it states that for an isomorphism `f: X → Y` with inverse `f⁻¹: Y → X`, we have `f⁻¹ ∘ (f ∘ h) = h` for any morphism `h: Y → Z`. This theorem essentially encapsulates the property of isomorphisms that reversing an isomorphism and then following it gives the identity, in the context of additional composition with a morphism `h`.
More concisely: For any isomorphism $f:X \rightarrow Y$ in a category with inverse $f^{-1}:Y \rightarrow X$, and any morphism $h:Y \rightarrow Z$, we have $f^{-1} \circ (f \circ h) = h$.
|
CategoryTheory.IsIso.out
theorem CategoryTheory.IsIso.out :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.IsIso f],
∃ inv,
CategoryTheory.CategoryStruct.comp f inv = CategoryTheory.CategoryStruct.id X ∧
CategoryTheory.CategoryStruct.comp inv f = CategoryTheory.CategoryStruct.id Y
This theorem states the existence of an inverse morphism in a category. Given a category `C` and objects `X` and `Y` within `C`, if there exists a morphism `f` from `X` to `Y` which is an isomorphism, then there exists an inverse of `f`, denoted as `inv`. The composition of `f` and `inv` in that order is the identity morphism on `X`, and the composition of `inv` and `f` in that order is the identity morphism on `Y`. In other words, `f` and `inv` are inverse morphisms in the category.
More concisely: If `f` is an isomorphism from object `X` to object `Y` in category `C`, then there exists an inverse morphism `inv` of `f` such that `f ∘ inv = id_X` and `inv ∘ f = id_Y`.
|
CategoryTheory.IsIso.eq_comp_inv
theorem CategoryTheory.IsIso.eq_comp_inv :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ⟶ Y) [inst_1 : CategoryTheory.IsIso α]
{f : Z ⟶ Y} {g : Z ⟶ X},
g = CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv α) ↔ CategoryTheory.CategoryStruct.comp g α = f
The theorem `CategoryTheory.IsIso.eq_comp_inv` states that for any category `C` and objects `X`, `Y`, and `Z` within this category, given a morphism `α` from `X` to `Y` which is an isomorphism, and morphisms `f` from `Z` to `Y` and `g` from `Z` to `X`, then `g` is equal to the composition of `f` and the inverse of `α` if and only if the composition of `g` and `α` is equal to `f`. This theorem is a fundamental result in category theory expressing the interchangeability of a morphism with its inverse in a composition.
More concisely: For any category C and objects X, Y, and Z, if α : X ↔ Y is an isomorphism and f : Z → Y and g : Z → X are morphisms such that g ∘ α = f and α ∘ g = id\_Y, then g = f ∘ α^(-1).
|
CategoryTheory.Iso.symm_symm_eq
theorem CategoryTheory.Iso.symm_symm_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y), α.symm.symm = α
This theorem states that in the setting of category theory, for any category `C` and any two objects `X` and `Y` in `C`, the double inversion (or double symmetry) of an isomorphism `α` from `X` to `Y` equals the original isomorphism `α`. In other words, if you have an isomorphism and apply the 'inverse' operation twice, you recover the original isomorphism.
More concisely: In category theory, for any isomorphism α : X ↔ Y between objects X and Y, α⁻ⁱⁱ = α holds. (Here, α⁻ⁱ denotes the double inverse or double dual of α.)
|
CategoryTheory.IsIso.inv_hom_id
theorem CategoryTheory.IsIso.inv_hom_id :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f],
CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) f = CategoryTheory.CategoryStruct.id Y
This theorem, `CategoryTheory.IsIso.inv_hom_id`, states that for any category `C` and any two objects `X` and `Y` in `C`, if `f` is an isomorphism from `X` to `Y` (denoted as `f : X ⟶ Y`), then the composition of the inverse of `f` (denoted as `CategoryTheory.inv f`) and `f` itself is equal to the identity morphism on `Y` (denoted as `CategoryTheory.CategoryStruct.id Y`). In other words, if `f` is an invertible function, then the inverse of `f` followed by `f` brings us back to where we started. This is a key characteristic of isomorphisms in category theory.
More concisely: For any category `C` and objects `X` and `Y` with an isomorphism `f : X ⟶ Y`, the composition of `CategoryTheory.inv f` and `f` is equal to the identity morphism on `Y`, i.e., `CategoryTheory.inv f ∘ f = CategoryTheory.id Y`.
|
CategoryTheory.Iso.inv_comp_eq
theorem CategoryTheory.Iso.inv_comp_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z},
CategoryTheory.CategoryStruct.comp α.inv f = g ↔ f = CategoryTheory.CategoryStruct.comp α.hom g
This theorem is about the composition of morphisms in a category theory context. It states that for any category `C`, and any objects `X`, `Y`, `Z` in `C`, given an isomorphism `α` from `X` to `Y` and morphisms `f` from `X` to `Z` and `g` from `Y` to `Z`, the composition of the inverse of `α` and `f` is equal to `g` if and only if `f` is equal to the composition of `α` and `g`. In simpler terms, if you can get from `X` to `Z` by first following the reverse of `α` and then `f`, this is the same as going directly from `Y` to `Z` using `g`. Likewise, going from `X` to `Z` using `f` is the same as first transforming `X` to `Y` using `α` and then going to `Z` using `g`.
More concisely: In a category `C`, given objects `X`, `Y`, `Z`, an isomorphism `α: X ≅ Y`, and morphisms `f: X → Z`, `g: Y → Z`, the following are equivalent: `f = g ∘ α` and `g = f ∘ α^−1`.
|
CategoryTheory.Iso.hom_comp_eq_id
theorem CategoryTheory.Iso.hom_comp_eq_id :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {f : Y ⟶ X},
CategoryTheory.CategoryStruct.comp α.hom f = CategoryTheory.CategoryStruct.id X ↔ f = α.inv
This theorem, `CategoryTheory.Iso.hom_comp_eq_id`, states that for any category `C` and any two objects `X` and `Y` in `C`, if there is an isomorphism `α` from `X` to `Y` and a morphism `f` from `Y` to `X`, then the composition of the morphisms `α.hom` and `f` equals the identity morphism on `X` if and only if `f` equals the inverse of `α`. This theorem is related to the properties of isomorphisms in category theory, where an isomorphism is a morphism that has an inverse.
More concisely: For any category C, given isomorphisms α : X ↔ Y and f : Y ↔ X in C, hom α ∘ f = id\_X if and only if f = α^(-1).
|
Mathlib.CategoryTheory.Iso._auxLemma.3
theorem Mathlib.CategoryTheory.Iso._auxLemma.3 :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ⟶ Y) [inst_1 : CategoryTheory.IsIso α]
{f : X ⟶ Z} {g : Y ⟶ Z},
(CategoryTheory.CategoryStruct.comp (CategoryTheory.inv α) f = g) =
(f = CategoryTheory.CategoryStruct.comp α g)
This theorem states that within a category `C` with objects `X`, `Y`, and `Z`, given an isomorphic morphism `α` from `X` to `Y`, and two morphisms `f` from `X` to `Z` and `g` from `Y` to `Z`, the composition of the inverse of `α` and `f` is equal to `g` if and only if `f` is equal to the composition of `α` and `g`. In other words, it captures a form of commutativity of composition with respect to an isomorphism and its inverse in category theory.
More concisely: Given an isomorphism α : X ↔ Y and morphisms f : X -> Z and g : Y -> Z in a category C, f ∘ α^(-1) = g if and only if f = α ∘ g.
|
Mathlib.CategoryTheory.Iso._auxLemma.14
theorem Mathlib.CategoryTheory.Iso._auxLemma.14 :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X X' Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X')
(g' : X' ⟶ Y) (h : Z ≅ Y),
(CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h.inv) =
CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h.inv)) =
(CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g')
The theorem, named `Mathlib.CategoryTheory.Iso._auxLemma.14`, states that for any category `C` of Type `u`, for any objects `W, X, X', Y, Z` in `C`, and for any morphisms `f: W ⟶ X`, `g: X ⟶ Y`, `f': W ⟶ X'`, `g': X' ⟶ Y`, and isomorphism `h: Z ≅ Y` in the category `C`, the composition of `f` and `g` followed by the inverse of `h` is equal to the composition of `f'` and `g'` followed by the inverse of `h` if and only if the composition of `f` and `g` is equal to the composition of `f'` and `g'`. In mathematical terms, it means `(f ⋅ (g ⋅ h.inv)) = (f' ⋅ (g' ⋅ h.inv))` if and only if `(f ⋅ g) = (f' ⋅ g')`.
More concisely: For any objects and morphisms in a category, the composition of two morphisms followed by an isomorphism and its inverse is equal to the composition of two other morphisms and the same isomorphism and its inverse if and only if the original compositions are equal.
|