CategoryTheory.StructuredArrow.eq_mk
theorem CategoryTheory.StructuredArrow.eq_mk :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D}
(f : CategoryTheory.StructuredArrow S T), f = CategoryTheory.StructuredArrow.mk f.hom
This theorem, referred to as the Eta rule for structured arrows, states that for any structured arrow `f` in the context of two categories `C` and `D` where `S` is an object in `D` and `T` is a functor from `C` to `D`, `f` is equal to the structured arrow constructed using the morphism `f.hom` from `S` to the functor application `T.obj Y`. In other words, a structured arrow is completely determined by its underlying morphism. For rewriting, it is recommended to use `StructuredArrow.eta` instead, as equality of objects can introduce complications.
More concisely: For any structured arrow `f` from object `X` in category `C` to object `Y` in category `D`, where `T` is a functor from `C` to `D`, the structured arrow `f` is equal to the structured arrow constructed using `f.hom` and `T.obj Y`.
|
CategoryTheory.StructuredArrow.w
theorem CategoryTheory.StructuredArrow.w :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D}
{A B : CategoryTheory.StructuredArrow S T} (f : A ⟶ B),
CategoryTheory.CategoryStruct.comp A.hom (T.map f.right) = B.hom
This theorem is about structured arrows in category theory. Given two categories, `C` and `D`, with `S` being an object in `D` and `T` being a functor from `C` to `D`, the theorem states that for any two structured arrows `A` and `B` from `S` to `T`, and a morphism `f` from `A` to `B`, the composition of the morphism from `A` to `B` with the application of the functor `T` to the right component of `f` is equal to the morphism from `B` to `T`. In other words, it captures a commutativity property where traversal via the functor and the morphism is same as direct traversal via the morphism in the structured arrow.
More concisely: Given functors T : C -> D between categories C and D, objects S in D, structured arrows A, B : S -> T, and a morphism f : A -> B in C, the composition of T(B) \* f = A \* T(g), where g is the right component of f.
|
CategoryTheory.StructuredArrow.IsUniversal.fac
theorem CategoryTheory.StructuredArrow.IsUniversal.fac :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D}
{f : CategoryTheory.StructuredArrow S T} (h : f.IsUniversal) (g : CategoryTheory.StructuredArrow S T),
CategoryTheory.CategoryStruct.comp f.hom (T.map (h.desc g)) = g.hom
This theorem states that for any structured arrow in a category, it can be factored through a universal arrow. More precisely, given any category `C` and `D`, a functor `T` from `C` to `D`, an object `S` in `D`, and a universally structured arrow `f` from `S` to `T(C)`, for any structured arrow `g` from `S` to `T(C)`, the composition of the morphism of `f` and the `T`-mapped image of the morphism obtained from `f` to `g` by the universal property of `f`, equals to the morphism of `g`. This highlights the property that a universal arrow is initial in the category of structured arrows, from which every other arrow can be obtained via unique morphisms.
More concisely: Given any functor T from category C to D, object S in D, and universally structured arrow f : S -> T(C), for any structured arrow g : S -> T(C), the composition of f and the unique morphism from g to f via the universal property equals g.
|
Mathlib.CategoryTheory.Comma.StructuredArrow._auxLemma.1
theorem Mathlib.CategoryTheory.Comma.StructuredArrow._auxLemma.1 :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D}
{X Y : CategoryTheory.StructuredArrow S T} (f g : X ⟶ Y), (f = g) = (f.right = g.right)
The theorem states that, in the context of category theory, given any categories `C` and `D`, a functor `T` from `C` to `D`, an object `S` in `D`, and objects `X` and `Y` that are structured arrows from `S` to `T`, any two morphisms `f` and `g` from `X` to `Y` are equal if and only if their right components are equal. This theorem essentially states that the equality of morphisms in a comma category (specifically, structured arrows) can be determined by the equality of their right components, which are morphisms in `D`.
More concisely: Given functors `T` from category `C` to `D`, objects `S` in `D`, and structured arrows `X ↓ S ↑ Y` in the comma category `Cdown D`, morphisms `f` and `g` from `X` to `Y` are equal if and only if their right components `T(f)` and `T(g)` are equal in `D`.
|
CategoryTheory.CostructuredArrow.epi_of_epi_left
theorem CategoryTheory.CostructuredArrow.epi_of_epi_left :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D}
{A B : CategoryTheory.CostructuredArrow S T} (f : A ⟶ B) [h : CategoryTheory.Epi f.left], CategoryTheory.Epi f
This theorem, `CategoryTheory.CostructuredArrow.epi_of_epi_left`, states that in category theory, given any two costructured arrows `A` and `B` from a functor `S` to an object `T`, if a morphism `f` from `A` to `B` is such that the `left` part of `f` is an epimorphism (surjective morphism), then the morphism `f` itself is also an epimorphism. This is within the context of two categories `C` and `D`. The converse of this theorem holds true under additional assumptions, as indicated by the theorem `epi_iff_epi_left`.
More concisely: If `f` is a morphism from a costructured arrow `A` to `B` in a category such that the left part of `f` is an epimorphism, then `f` is an epimorphism.
|
CategoryTheory.CostructuredArrow.eqToHom_left
theorem CategoryTheory.CostructuredArrow.eqToHom_left :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D}
{X Y : CategoryTheory.CostructuredArrow S T} (h : X = Y),
(CategoryTheory.eqToHom h).left = CategoryTheory.eqToHom ⋯
This theorem states that for any two objects `X` and `Y` in the category of Costructured Arrows from functor `S` to object `T`, if `X` is equal to `Y` (denoted by `h : X = Y`), then the left component of the morphism created by `CategoryTheory.eqToHom` from `X` to `Y` is equal to the morphism created by `CategoryTheory.eqToHom` corresponding to some other equality. Here, `CategoryTheory.eqToHom` is a function that creates a morphism from an equality between two objects in a category.
More concisely: Given objects `X` and `Y` in the category of Arrows from functor `S` to object `T`, if `X = Y`, then the morphism from `X` to `Y` given by `CategoryTheory.eqToHom` is equal to the morphism given by some other equality `h`.
|
CategoryTheory.CostructuredArrow.eq_mk
theorem CategoryTheory.CostructuredArrow.eq_mk :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D}
(f : CategoryTheory.CostructuredArrow S T), f = CategoryTheory.CostructuredArrow.mk f.hom
This theorem states the eta rule for costructured arrows in category theory. Given any categories `C` and `D`, a functor `S` from `C` to `D`, and an object `T` in `D`, for any costructured arrow `f` from `S` to `T`, it is equal to the costructured arrow constructed from `f.hom`, the homomorphism of `f`. This theorem is used for rewriting in Lean, but it's recommended to use `CostructuredArrow.eta` instead to avoid potential issues with equality of objects.
More concisely: For any categories C and D, functor S from C to D, object T in D, and constructed arrow f from S to T, f is equal to the constructed arrow constructed from f.hom, the homomorphism of f.
|
CategoryTheory.CostructuredArrow.IsUniversal.hom_ext
theorem CategoryTheory.CostructuredArrow.IsUniversal.hom_ext :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D}
{f : CategoryTheory.CostructuredArrow S T},
f.IsUniversal →
∀ {c : C} {η η' : c ⟶ f.left},
CategoryTheory.CategoryStruct.comp (S.map η) f.hom = CategoryTheory.CategoryStruct.comp (S.map η') f.hom →
η = η'
This theorem is stating that given a category `C`, and another category `D`, and a functor `S` from `C` to `D`, and an object `T` in `D`, and a costructured arrow `f` from `S` to `T`, if `f` is universal, then for any object `c` in `C` and any two morphisms `η` and `η'` from `c` to the source of `f`, if the compositions of the images of `η` and `η'` under the functor `S` with the morphism `f.hom` are equal, then `η` and `η'` must be equal. In other words, two morphisms into a universal `S`-costructured arrow are the same if their images under the functor `S` become the same after being composed with the universal arrow.
More concisely: Given a functor `S` from category `C` to category `D`, an object `T` in `D`, a universal `S`-constructed arrow `f` from `T`, and objects `c` in `C` with morphisms `η, η'` to the source of `f`, if `S(η) ∘ f.hom = S(η') ∘ f.hom`, then `η = η'`.
|
CategoryTheory.CostructuredArrow.IsUniversal.fac
theorem CategoryTheory.CostructuredArrow.IsUniversal.fac :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D}
{f : CategoryTheory.CostructuredArrow S T} (h : f.IsUniversal) (g : CategoryTheory.CostructuredArrow S T),
CategoryTheory.CategoryStruct.comp (S.map (h.lift g)) f.hom = g.hom
This theorem states that for any costructured arrow `f` in a category theory context, if `f` is universal, then any other costructured arrow `g` can be factored through `f`. Specifically, this means that the composition of the morphism obtained by applying `S.map` to the lifting of `g` by `h` and the morphism `f.hom` is equal to `g.hom`. Here, `C` and `D` are the types representing the categories, `T` is an object in `D`, and `S` is a functor from `C` to `D`.
More concisely: Given a universal arrow `f` in a functor `S` from category `C` to category `D`, for any arrow `g` in `D` with domain object `T`, there exists an arrow `h` in `C` with `S(h) = g` such that `f.hom ; S.map h = g.hom`.
|
Mathlib.CategoryTheory.Comma.StructuredArrow._auxLemma.2
theorem Mathlib.CategoryTheory.Comma.StructuredArrow._auxLemma.2 :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D}
{X Y : CategoryTheory.CostructuredArrow S T} (f g : X ⟶ Y), (f = g) = (f.left = g.left)
This theorem states that in the context of category theory, given two categories `C` and `D` of types `u₁` and `u₂` respectively, a functor `S` from `C` to `D`, and an object `T` in `D`, for any two costructured arrows `X` and `Y` from `S` to `T`, any two morphisms `f` and `g` from `X` to `Y` are equal if and only if their left components are equal.
More concisely: Given functors `S : C -> D` between categories `C` and `D`, and objects `T` in `D`, if for any two arrows `X, Y : S -> T`, morphisms `f, g : X -> Y` have equal left components, then `f = g`.
|
CategoryTheory.StructuredArrow.hom_ext
theorem CategoryTheory.StructuredArrow.hom_ext :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D}
{X Y : CategoryTheory.StructuredArrow S T} (f g : X ⟶ Y), f.right = g.right → f = g
This theorem states that for any two categories 'C' and 'D', a functor 'T' from 'C' to 'D', an object 'S' from 'D', and two objects 'X' and 'Y' from the structured arrows from 'S' to 'T', if there exist two morphisms 'f' and 'g' from 'X' to 'Y' such that their right components are equal, then the two morphisms themselves are equal. This is an equality condition for morphisms in the context of structured arrows in category theory.
More concisely: For any categories 'C' and 'D', functor 'T' from 'C' to 'D', object 'S' in 'D', and structured arrows 'X' and 'Y' from 'S' to 'T', if there exist morphisms 'f' and 'g' with equal right components from 'X' to 'Y', then 'f' = 'g'.
|
CategoryTheory.StructuredArrow.mono_of_mono_right
theorem CategoryTheory.StructuredArrow.mono_of_mono_right :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D}
{A B : CategoryTheory.StructuredArrow S T} (f : A ⟶ B) [h : CategoryTheory.Mono f.right], CategoryTheory.Mono f
In the context of Category Theory, this theorem states that for any two objects `A` and `B` in the category of structured arrows from `S` to a functor `T`, if there is a morphism `f` from `A` to `B` such that the 'right' part of this morphism is a monomorphism, then `f` itself is a monomorphism. This is essentially a statement about the preservation of the monomorphism property under certain conditions in the structured arrow category. The converse of this statement requires additional assumptions, as pointed out in the comment.
More concisely: In the category of structured arrows from S to a functor T, if a morphism from object A to object B has a monic right component, then the morphism itself is monic.
|
CategoryTheory.CostructuredArrow.w
theorem CategoryTheory.CostructuredArrow.w :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D}
{A B : CategoryTheory.CostructuredArrow S T} (f : A ⟶ B),
CategoryTheory.CategoryStruct.comp (S.map f.left) B.hom = A.hom
The theorem `CategoryTheory.CostructuredArrow.w` states that for any categories `C` and `D`, a functor `S` from `C` to `D`, an object `T` in `D`, and costructured arrows `A` and `B` from `S` to `T`, if there exists a morphism `f` from `A` to `B`, then the composition of the mapping of `f.left` under `S` and `B.hom` is equal to `A.hom`. In other words, the diagram involving the category `C`, the category `D`, the functor `S`, and the costructured arrows `A` and `B` commutes for any morphism `f` from `A` to `B`.
More concisely: For any functors S from category C to D, objects T in D, and costructured arrows A and B from S to T, if there exists a morphism f from A to B, then the diagram commutes, that is, S(A.hom) ∘ f.left = B.hom.
Or more succinctly: Given functor S, objects T in D and A,B in S/T, and a morphism f: A → B, we have S(A.hom) ∘ f.left = B.hom.
|
CategoryTheory.StructuredArrow.IsUniversal.hom_ext
theorem CategoryTheory.StructuredArrow.IsUniversal.hom_ext :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D}
{f : CategoryTheory.StructuredArrow S T},
f.IsUniversal →
∀ {c : C} {η η' : f.right ⟶ c},
CategoryTheory.CategoryStruct.comp f.hom (T.map η) = CategoryTheory.CategoryStruct.comp f.hom (T.map η') →
η = η'
This theorem in category theory states that for any category `C` with objects of type `u₁`, and a category `D` with objects of type `u₂`, given a functor `T` from `C` to `D` and a `T`-structured arrow `f` from object `S` in `D`, if `f` is universal, then for any object `c` in `C` and any two morphisms `η` and `η'` from `f.right` to `c`, if the image of `η` and `η'` under the functor `T` are equal after precomposing with the morphism `f.hom`, then `η` is equal to `η'`. Here, "precomposing with the morphism `f.hom`" refers to the operation of composing `f.hom` with the image of `η` (or `η'`) under `T`.
More concisely: If in a category `C` with object type `u₁` and a category `D` with object type `u₂`, a universal `T`-structured arrow `f` from `D` to `C` and two morphisms `η` and `η'` from `f.right` to an object `c` in `C` satisfy the condition that `T(η) ∘ f.hom = T(η') ∘ f.hom`, then `η = η'`.
|