CategoryTheory.CommSq.right_adjoint
theorem CategoryTheory.CommSq.right_adjoint :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
[inst_1 : CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C}
{A B : C} {X Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : G.obj A ⟶ X} {v : G.obj B ⟶ Y},
CategoryTheory.CommSq u (G.map i) p v →
∀ (adj : G ⊣ F), CategoryTheory.CommSq ((adj.homEquiv A X) u) i (F.map p) ((adj.homEquiv B Y) v)
This theorem states that given an adjunction `G ⊣ F` between categories `C` and `D`, and a commutative square in `D` where the left map is `G.map i` and the right map is `p`, we can find an "adjoint" commutative square in `C`. This adjoint square has `i` as its left map and `F.map p` as its right map. Here, `i` is a morphism in `C`, and `p` is a morphism in `D`. The commutativity of the original square implies the commutativity of the adjoint square. In other words, given a diagram in `D` that commutes when transformed under `G`, the theorem guarantees there exists a corresponding diagram in `C` that commutes when transformed under `F`.
More concisely: Given an adjunction between categories and a commutative square in one of them, there exists an adjoint commutative square in the other category with the given morphisms as their respective left and right maps, preserving commutativity.
|
CategoryTheory.CommSq.right_adjoint_hasLift_iff
theorem CategoryTheory.CommSq.right_adjoint_hasLift_iff :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
[inst_1 : CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C}
{A B : C} {X Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : G.obj A ⟶ X} {v : G.obj B ⟶ Y}
(sq : CategoryTheory.CommSq u (G.map i) p v) (adj : G ⊣ F), ⋯.HasLift ↔ sq.HasLift
This theorem, in the category theory context, states that for two given categories `C` and `D`, along with functors `G : C → D` and `F : D → C`, and two morphisms `i : A ⟶ B` in the category `C` and `p : X ⟶ Y` in the category `D`, a commutative square `sq` formed by `u : G(A) ⟶ X` and `v : G(B) ⟶ Y` and the mapped morphism `G.map i` and `p` has a lifting if and only if the right adjoint square of `sq` under the adjunction `G ⊣ F` also has a lifting. Here, a lifting of a commutative square refers to an additional morphism that makes two separate commutative triangles.
More concisely: For functors G : C -> D and F : D -> C, natural transformations i : F o G -> 1\_C and p : 1\_D -> G o F, and morphisms x : A -> B in C and y : X -> Y in D, there is a morphism z : B -> Y making the diagrams commute if and only if there is a morphism w : A -> X making the corresponding right adjoint diagrams commute.
|
CategoryTheory.CommSq.left_adjoint_hasLift_iff
theorem CategoryTheory.CommSq.left_adjoint_hasLift_iff :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
[inst_1 : CategoryTheory.Category.{u_3, u_2} D] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C}
{A B : C} {X Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : A ⟶ F.obj X} {v : B ⟶ F.obj Y}
(sq : CategoryTheory.CommSq u i (F.map p) v) (adj : G ⊣ F), ⋯.HasLift ↔ sq.HasLift
This theorem states that for any categories `C` and `D`, functors `G` from `C` to `D` and `F` from `D` to `C`, objects `A` and `B` from `C`, objects `X` and `Y` from `D`, morphisms `i` from `A` to `B`, `p` from `X` to `Y`, `u` from `A` to the object `F` maps `X` to, and `v` from `B` to the object `F` maps `Y` to, if there exists a commutative square `sq` given by these data and an adjunction `adj` between `G` and `F`, then there exists a lift for the adjoint square if and only if there exists a lift for the original square `sq`.
This theorem is a statement about the relationship between the properties of a commutative square in a category and its corresponding adjoint square.
More concisely: Given any commutative square in the 2-category of categories, functors, and natural transformations, and an adjunction between the functors involved, the existence of a lifting of the adjoint square is equivalent to the existence of a lifting of the original square.
|
CategoryTheory.CommSq.left_adjoint
theorem CategoryTheory.CommSq.left_adjoint :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
[inst_1 : CategoryTheory.Category.{u_3, u_2} D] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C}
{A B : C} {X Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : A ⟶ F.obj X} {v : B ⟶ F.obj Y},
CategoryTheory.CommSq u i (F.map p) v →
∀ (adj : G ⊣ F), CategoryTheory.CommSq ((adj.homEquiv A X).symm u) (G.map i) p ((adj.homEquiv B Y).symm v)
The theorem `CategoryTheory.CommSq.left_adjoint` states that given an adjunction `G ⊣ F` between two categories `C` and `D`, for any commutative square where the left map is `i` and the right map is `F.map p`, there exists an adjoint commutative square. In this adjoint square, the left map is `G.map i` and the right map is `p`. This theorem holds for arbitrary objects `A`, `B` in `C` and `X`, `Y` in `D` and morphisms `i : A ⟶ B` and `p : X ⟶ Y`. The theorem also requires morphisms `u : A ⟶ F.obj X` and `v : B ⟶ F.obj Y` that make the initial square commutative. The adjoint square is then constructed using the hom-set bijections provided by the adjunction `G ⊣ F`.
More concisely: Given an adjunction between categories and commutative squares with commutative left triangle, there exists an adjoint commutative square with the given left map being the adjoint of the right map under the adjunction.
|