CategoryTheory.CommSq.flip
theorem CategoryTheory.CommSq.flip :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
{i : Y ⟶ Z}, CategoryTheory.CommSq f g h i → CategoryTheory.CommSq g f i h
This theorem states that given a category `C` of any type `C` and any objects `W`, `X`, `Y`, and `Z` in this category, along with morphisms `f: W ⟶ X`, `g: W ⟶ Y`, `h: X ⟶ Z`, and `i: Y ⟶ Z`, if there exists a commutative square with the given morphisms, then there also exists a commutative square when the roles of `f` and `g`, and `h` and `i` are flipped. In other words, if you can move from `W` to `Z` via either `f` and `h` or `g` and `i`, then you can also do so if you swap the roles of `f` and `g`, and `h` and `i`.
More concisely: Given a commutative square in a category with morphisms `f: W ⟶ X`, `g: W ⟶ Y`, `h: X ⟶ Z`, and `i: Y ⟶ Z`, if it exists, then interchanging the roles of `f` and `g`, and `h` and `i`, also yields a commutative square.
|
CategoryTheory.CommSq.op
theorem CategoryTheory.CommSq.op :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
{i : Y ⟶ Z}, CategoryTheory.CommSq f g h i → CategoryTheory.CommSq i.op h.op g.op f.op
This theorem states that given a commutative square in a category, there exists an associated commutative square in the opposite category. More specifically, for a category `C` and objects `W`, `X`, `Y`, and `Z` with morphisms `f : W ⟶ X`, `g : W ⟶ Y`, `h : X ⟶ Z`, and `i : Y ⟶ Z` that form a commutative square, the theorem asserts that if these morphisms form a commutative square (which is represented by `CategoryTheory.CommSq f g h i`), then the opposite morphisms `i.op`, `h.op`, `g.op`, and `f.op` also form a commutative square in the opposite category (`CategoryTheory.CommSq i.op h.op g.op f.op`).
More concisely: Given a commutative square in a category, the opposites of its morphisms form a commutative square in the opposite category.
|
CategoryTheory.CommSq.fac_right
theorem CategoryTheory.CommSq.fac_right :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
{g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g) [hsq : sq.HasLift],
CategoryTheory.CategoryStruct.comp sq.lift p = g
This theorem states that in the context of a commutative square in a category, given objects `A`, `B`, `X`, `Y` and morphisms `f : A ⟶ X`, `i : A ⟶ B`, `p : X ⟶ Y`, `g : B ⟶ Y` which form the commutative square, and assuming that the square has a lift (an additional morphism that makes two triangles commute with the original square), the composition of the lift and the morphism `p : X ⟶ Y` equals the morphism `g : B ⟶ Y`. In mathematical terms, if the square has a lift `l : B ⟶ X`, then `l ≫ p = g`. This is essentially stating a property of the commuting of the diagram, that is, the pathway from `B` to `Y` via the lift and `p` is the same as going directly from `B` to `Y` via `g`.
More concisely: Given a commutative square with lift in a category, the composition of the lift and the morphism to the right bottom vertex equals the morphism to the bottom right vertex.
|
CategoryTheory.CommSq.HasLift.mk'
theorem CategoryTheory.CommSq.HasLift.mk' :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
{g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g}, sq.LiftStruct → sq.HasLift
This theorem from category theory, `CategoryTheory.CommSq.HasLift.mk'`, states that for any category `C`, and any objects `A`, `B`, `X`, `Y` in `C`, and morphisms `f : A ⟶ X`, `i : A ⟶ B`, `p : X ⟶ Y`, and `g : B ⟶ Y` forming a commutative square `sq`, if a lifting structure for this commutative square exists, then the commutative square has a lift. In other words, if we can find a way to "complete" the square in such a way that all paths from `A` to `Y` are equivalent, then a lift exists for this square. This is a fundamental concept in category theory, related to the idea of universal constructions and commuting diagrams.
More concisely: If a commutative square in a category has a lifting structure, then it has a lift.
|
CategoryTheory.CommSq.w
theorem CategoryTheory.CommSq.w :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
{i : Y ⟶ Z},
CategoryTheory.CommSq f g h i → CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g i
This theorem is in the field of Category Theory, specifically working within a categorical structure. The theorem states that for any category `C` with objects `W`, `X`, `Y`, `Z`, and morphisms `f`, `g`, `h`, `i` (with `f` and `g` originating from `W`, `h` from `X` to `Z`, and `i` from `Y` to `Z`), if the square formed by these morphisms commutes according to `CategoryTheory.CommSq`, then the composition of morphisms `f` and `h` is equal to the composition of `g` and `i`. In other words, applying `f` and then `h` is the same as applying `g` and then `i`. This is essentially the definition of commuting diagram, where the paths through the diagram represent the same morphism.
More concisely: If in a commutative square in a category with morphisms `f: W -> X`, `g: W -> Y`, `h: X -> Z`, `i: Y -> Z`, `CategoryTheory.CommSq h g f i`, then `h ∘ f = g ∘ i`.
|
CategoryTheory.CommSq.fac_left
theorem CategoryTheory.CommSq.fac_left :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
{g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g) [hsq : sq.HasLift],
CategoryTheory.CategoryStruct.comp i sq.lift = f
This theorem states that in the context of a category `C`, for any commutative square `sq`, which is determined by objects `A, B, X, Y` and morphisms `f : A ⟶ X`, `i : A ⟶ B`, `p : X ⟶ Y`, `g : B ⟶ Y` such that `f` followed by `p` is the same as `i` followed by `g`, if the commutative square `sq` has a lift, then the composition of the morphism `i` and the lift of the square `sq` equals to the morphism `f`. In terms of category theory, this means that if we have a diagonal morphism providing a lift for the commutative square, then traversing the square via this morphism and `i` is equivalent to directly traversing via `f`.
More concisely: If a commutative square in a category has a lift, then the composition of the morphism along the left edge and the lift equals the morphism along the bottom edge.
|
CategoryTheory.CommSq.unop
theorem CategoryTheory.CommSq.unop :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {W X Y Z : Cᵒᵖ} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
{i : Y ⟶ Z}, CategoryTheory.CommSq f g h i → CategoryTheory.CommSq i.unop h.unop g.unop f.unop
This theorem states that, given a commutative square in the opposite category, the corresponding square in the original category also commutes. For any category `C` and objects `W`, `X`, `Y`, `Z` in its opposite category `Cᵒᵖ`, if the morphisms `f`, `g`, `h`, `i` form a commutative square, then the ‘unop’ of these morphisms (which is a way of reversing the arrows from the opposite category back to the original category) also form a commutative square in `C`.
More concisely: In any category, if the morphisms and their opposites in the corresponding commutative square in the opposite category form a commutative square, then the original morphisms in the category also commute.
|
CategoryTheory.CommSq.HasLift.exists_lift
theorem CategoryTheory.CommSq.HasLift.exists_lift :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
{g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g} [self : sq.HasLift], Nonempty sq.LiftStruct
This theorem states that for any category `C` and any commutative square `sq` in `C` with objects `A`, `B`, `X`, `Y` and morphisms `f`, `i`, `p`, `g` such that `A` maps to `X` via `f`, `A` maps to `B` via `i`, `X` maps to `Y` via `p`, and `B` maps to `Y` via `g`, if the commutative square has a lift, then there exists a `LiftStruct` for the square. Here, `LiftStruct` is a structure that encapsulates a possible lift of the commutative square, that is, a morphism that makes the resulting larger square commute.
More concisely: Given a commutative square in a category with object mapper functions `f: A -> X`, `i: A -> B`, `p: X -> Y`, and `g: B -> Y`, if `f` and `i` factor through `p` and `g`, respectively, and there exists a lift of the square, then there exists a lift structure for the square.
|
CategoryTheory.CommSq.LiftStruct.fac_left
theorem CategoryTheory.CommSq.LiftStruct.fac_left :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
{g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g} (self : sq.LiftStruct),
CategoryTheory.CategoryStruct.comp i self.l = f
This theorem is about the commutative nature of a specific diagram in Category Theory. Specifically, it states that for any objects A, B, X, and Y in a Category C, along with morphisms f : A ⟶ X, i : A ⟶ B, p : X ⟶ Y and g : B ⟶ Y that form a commutative square, the composition of the morphisms i and `self.l` is equal to f. In other words, for any lifting structure `self` of the square, the upper left triangle of the diagram commutes.
More concisely: For any commutative square in a category with objects A, B, X, Y and morphisms f : A ⟶ X, i : A ⟶ B, p : X ⟶ Y, and g : B ⟶ Y, the composition i ∘ `self.l` equals f for any lifting structure self of the square.
|
CategoryTheory.CommSq.LiftStruct.fac_right
theorem CategoryTheory.CommSq.LiftStruct.fac_right :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
{g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g} (self : sq.LiftStruct),
CategoryTheory.CategoryStruct.comp self.l p = g
This theorem, named `CategoryTheory.CommSq.LiftStruct.fac_right`, states that in any category `C`, given objects `A`, `B`, `X`, and `Y`, and morphisms `f: A ⟶ X`, `i: A ⟶ B`, `p: X ⟶ Y`, and `g: B ⟶ Y` forming a commutative square, if there is a lift structure `self` existing for this commutative square, then the composition of the lift morphism `l` from `self` and the morphism `p` is equal to the morphism `g`. This is encapsulating the concept of commutativity of the lower right triangle in the diagram of the commutative square and its lift structure.
More concisely: Given a commutative square in a category with a lift structure, the composition of the lift morphism and the right vertical morphism equals the morphism along the lower right edge.
|
CategoryTheory.CommSq.map
theorem CategoryTheory.CommSq.map :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2}
[inst_1 : CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) {W X Y Z : C} {f : W ⟶ X}
{g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z},
CategoryTheory.CommSq f g h i → CategoryTheory.CommSq (F.map f) (F.map g) (F.map h) (F.map i)
The theorem `CategoryTheory.CommSq.map` states that for any categories `C` and `D`, a functor `F` from `C` to `D`, and for any objects `W`, `X`, `Y`, `Z` in `C`, along with morphisms `f: W ⟶ X`, `g: W ⟶ Y`, `h: X ⟶ Z` and `i: Y ⟶ Z`, if a commutative square exists in `C` with sides `f`, `g`, `h`, `i`, then a corresponding commutative square also exists in the category `D` with sides mapped by the functor `F`. Here, a commutative square refers to a diagram of four objects and four morphisms that commute, meaning that the diagram can be traversed in two different ways to get from one object to another, yielding the same result.
More concisely: Given any commutative square in a category `C`, the image under a functor `F` from `C` to another category `D` forms a commutative square in `D`.
|
CategoryTheory.CommSq.vert_inv
theorem CategoryTheory.CommSq.vert_inv :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {W X Y Z : C} {f : W ⟶ X} {i : Y ⟶ Z} {g : W ≅ Y}
{h : X ≅ Z}, CategoryTheory.CommSq f g.hom h.hom i → CategoryTheory.CommSq i g.inv h.inv f
The theorem `CategoryTheory.CommSq.vert_inv` states that for any category `C`, and objects `W`, `X`, `Y`, `Z` in `C` with morphisms `f: W ⟶ X`, `i: Y ⟶ Z`, and isomorphisms `g: W ≅ Y` and `h: X ≅ Z`, if a commutative square is formed with `f`, `g.hom`, `h.hom` and `i`, then another commutative square is formed with `i`, `g.inv`, `h.inv` and `f`. In other words, if we have a commutative diagram involving these arrows, we can invert the vertical arrows to get another commutative diagram.
More concisely: Given any commutative square in a category with isomorphisms as two of its sides, the interchange of these isomorphisms with the other two morphisms results in another commutative square.
|