CategoryTheory.Functor.rightOp_leftOp_eq
theorem CategoryTheory.Functor.rightOp_leftOp_eq :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D), F.rightOp.leftOp = F
This theorem states that for any category `C` of type `u₁` and any category `D` of type `u₂`, given a functor `F` from the opposite category `Cᵒᵖ` to `D`, applying the right and left opposite operations to `F` consecutively will yield `F` itself. In other words, the right opposite of the left opposite of a functor is the functor itself. It is, however, advised to use the isomorphism `rightOpLeftOpIso` whenever possible, instead of this equality of functors.
More concisely: The right and left opposite functors of a functor between categories commute up to isomorphism. In other words, the right opposite of the left opposite of a functor is naturally isomorphic to the original functor.
|
CategoryTheory.isIso_op_iff
theorem CategoryTheory.isIso_op_iff :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
CategoryTheory.IsIso f.op ↔ CategoryTheory.IsIso f
This theorem states that for any category `C` and any morphism `f` from object `X` to object `Y` in the category, `f` is an isomorphism if and only if its opposite `f.op` is an isomorphism. In other words, a morphism in a category is an isomorphism if and only if its reverse morphism in the opposite category is also an isomorphism.
More concisely: In any category, a morphism is an isomorphism if and only if its opposite morphism is an isomorphism.
|
CategoryTheory.isIso_unop_iff
theorem CategoryTheory.isIso_unop_iff :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y),
CategoryTheory.IsIso f.unop ↔ CategoryTheory.IsIso f
This theorem states that in the context of category theory, for any category `C` and objects `X` and `Y` in the opposite category `Cᵒᵖ`, a morphism `f` from `X` to `Y` is an isomorphism if and only if its 'unop' (the operation of taking the 'opposite' morphism) is an isomorphism. In more intuitive terms, this theorem captures the idea that reversing the direction of arrows preserves isomorphisms in the category theory sense.
More concisely: In category theory, an opposite morphism of an isomorphism is an isomorphism in the opposite category.
|
CategoryTheory.op_id
theorem CategoryTheory.op_id :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C},
(CategoryTheory.CategoryStruct.id X).op = CategoryTheory.CategoryStruct.id (Opposite.op X)
The theorem `CategoryTheory.op_id` states that for any category `C` and any object `X` in `C`, taking the opposite of the identity morphism on `X` is the same as the identity morphism on the opposite of `X`. In other words, given any category and any object in that category, the operation of "oppositing" commutes with the operation of taking the identity morphism.
More concisely: For any category C and object X in C, the opposite of the identity morphism on X is equal to the identity morphism on the opposite of X.
|
Quiver.Hom.unop_op
theorem Quiver.Hom.unop_op : ∀ {C : Type u₁} [inst : Quiver C] {X Y : C} (f : X ⟶ Y), f.op.unop = f
This theorem states that for any type `C` which has a quiver (directed graph) structure, and any two objects `X` and `Y` in `C`, if we have a morphism `f` from `X` to `Y`, then operating on `f` with the `op` function and then undoing the operation with the `unop` function returns the original morphism `f`. In other words, the `unop` function is the inverse of the `op` function on the set of morphisms from `X` to `Y` in the category `C`. This result is independent of the specific objects `X` and `Y` and the morphism `f`.
More concisely: For any category `C` with objects `X` and `Y` and a morphism `f` from `X` to `Y`, the inverse of the operation `op(f)` on morphisms is given by `unop(op(f)) = f`.
|
CategoryTheory.unop_comp
theorem CategoryTheory.unop_comp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z},
(CategoryTheory.CategoryStruct.comp f g).unop = CategoryTheory.CategoryStruct.comp g.unop f.unop
The theorem `CategoryTheory.unop_comp` states that for any category `C` and any objects `X`, `Y`, and `Z` in the opposite category `Cᵒᵖ`, and morphisms `f` from `X` to `Y` and `g` from `Y` to `Z`, the unopposite of the composition of `f` and `g` (i.e., `(CategoryTheory.CategoryStruct.comp f g).unop`) is equal to the composition of the unoppisite of `g` and the unopposite of `f` (i.e., `CategoryTheory.CategoryStruct.comp g.unop f.unop`). In terms of category theory, this theorem demonstrates that reversing the arrows in a category also reverses the order of composition of morphisms.
More concisely: In the opposite category of any category C, the unopposites of morphism compositions are equal: `(f.unop ∘ g.unop) = g.unop ∘ f.unop`, for any morphisms `f: X ← Y` and `g: Y ← Z` in C.
|
Quiver.Hom.op_unop
theorem Quiver.Hom.op_unop : ∀ {C : Type u₁} [inst : Quiver C] {X Y : Cᵒᵖ} (f : X ⟶ Y), f.unop.op = f
The theorem `Quiver.Hom.op_unop` states that for any type `C` with structure `Quiver`, and any two categories `X` and `Y` in the opposite category `Cᵒᵖ`, if there is a morphism `f` from `X` to `Y`, then the operation of first applying the `unop` operation to `f` and then the `op` operation, results in `f` itself. Essentially, the `unop` and `op` operations are inverses of each other for all morphisms in the opposite category `Cᵒᵖ`.
More concisely: For any morphism $f$ in the opposite category of a quiver $C$, we have $(\op \circ \unop)(f) = (\unop \circ \op)(f) = f$.
|
Quiver.Hom.op_inj
theorem Quiver.Hom.op_inj : ∀ {C : Type u₁} [inst : Quiver C] {X Y : C}, Function.Injective Quiver.Hom.op
The theorem `Quiver.Hom.op_inj` states that for any type `C` that forms a quiver (i.e., a category-like structure), and any two objects `X` and `Y` in `C`, the operation of forming the opposite of a morphism (or arrow), given by the function `Quiver.Hom.op`, is injective. In other words, no two distinct morphisms from `X` to `Y` in `C` will become identical when their direction is reversed.
More concisely: For any quiver `C`, the opposite operation on morphisms `Quiver.Hom.op` is an injection from `C.Hom(X, Y)` to `C.Hom(Y, X)` for all objects `X` and `Y` in `C`.
|
CategoryTheory.isIso_of_op
theorem CategoryTheory.isIso_of_op :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y)
[inst_1 : CategoryTheory.IsIso f.op], CategoryTheory.IsIso f
This theorem states that, within the context of category theory, if the opposite `f.op` of a morphism `f` from object `X` to object `Y` in a category `C` is an isomorphism, then the original morphism `f` must also be an isomorphism. The caveat mentioned in the comment suggests that this theorem cannot be made into an instance, as it would cause a loop in the instance resolution process.
More concisely: If the opposite morphism of `f` is an isomorphism in a category `C`, then `f` is an isomorphism.
|
Quiver.Hom.unop_inj
theorem Quiver.Hom.unop_inj : ∀ {C : Type u₁} [inst : Quiver C] {X Y : Cᵒᵖ}, Function.Injective Quiver.Hom.unop := by
sorry
The theorem `Quiver.Hom.unop_inj` states that for any category `C` with its quiver structure, and any two objects `X` and `Y` in the opposite category `Cᵒᵖ`, the function `Quiver.Hom.unop` is injective. In other words, if two morphisms in the opposite category `Cᵒᵖ` from `X` to `Y` have the same "unopposite" in `C` (meaning they map to the same morphism in `C` when the direction of the arrows is reversed), then the two morphisms in `Cᵒᵖ` were the same to begin with. This guarantees that the process of "unoppositing" does not lose information.
More concisely: The theorem `Quiver.Hom.unop_inj` asserts that the function `Quiver.Hom.unop` is an injection on morphisms in the opposite category of any quivered category.
|
CategoryTheory.op_comp
theorem CategoryTheory.op_comp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z},
(CategoryTheory.CategoryStruct.comp f g).op = CategoryTheory.CategoryStruct.comp g.op f.op
The theorem `CategoryTheory.op_comp` states that for any category `C` and any three objects `X`, `Y`, `Z` in this category, and any two morphisms `f: X ⟶ Y` and `g: Y ⟶ Z`, the opposite of the composition of `f` and `g` (denoted `(CategoryTheory.CategoryStruct.comp f g).op`) is equal to the composition of the opposites of `g` and `f` (denoted `CategoryTheory.CategoryStruct.comp g.op f.op`). In other words, reversing the direction of morphisms in a composition in a category is equivalent to reversing the order of the composition.
More concisely: For any category C and morphisms f : X 券 ↘ Y and g : Y peon ↘ Z, (f ∘ g)^op = g^op ∘ f^op, where (∘) denotes composition and ^op denotes the opposite operation.
|
CategoryTheory.unop_id
theorem CategoryTheory.unop_id :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ},
(CategoryTheory.CategoryStruct.id X).unop = CategoryTheory.CategoryStruct.id X.unop
This theorem states that for any Category `C` and any object `X` in the opposite category `Cᵒᵖ`, the unop of the identity morphism on `X` is equal to the identity morphism on the unop of `X`. In more mathematical terms, it says that unopping the identity does not change the identity, i.e., if we take an object in the opposite category, its identity morphism remains the same even if we apply the unop operation.
More concisely: For any category `C` and object `X` in `Cᵒᵖ`, the unop of the identity morphism on `X` equals the identity morphism on the unop of `X`. In other words, `(id_X)ᵒᵖ = id_(Xᵒᵖ)` in `C`.
|