CategoryTheory.Limits.Cofan.IsColimit.hom_ext
theorem CategoryTheory.Limits.Cofan.IsColimit.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type u_1} {F : I → C}
{c : CategoryTheory.Limits.Cofan F},
CategoryTheory.Limits.IsColimit c →
∀ {A : C} (f g : c.pt ⟶ A),
(∀ (i : I), CategoryTheory.CategoryStruct.comp (c.inj i) f = CategoryTheory.CategoryStruct.comp (c.inj i) g) →
f = g
The theorem `CategoryTheory.Limits.Cofan.IsColimit.hom_ext` states that in a category `C`, for any cofan `c` over a diagram `F : I → C` that has the property of being a colimit, if we have two morphisms `f` and `g` from the tip of the cofan to some object `A` in `C` such that the composition of `f` and `g` respectively with each "injection" (or morphism) from the diagram to the tip of the cofan yields the same result, then `f` and `g` must be the same. In other words, the morphism from the colimit of the cofan to any other object is determined uniquely by the way it interacts with the morphisms making up the cocone, embodying a universal property of colimits in category theory.
More concisely: In a category with colimits, if two morphisms from the tip of a cocone over a diagram to an object have the same image under all injections from the diagram, then they are equal.
|
CategoryTheory.Limits.Sigma.ι_comp_map'
theorem CategoryTheory.Limits.Sigma.ι_comp_map' :
∀ {β : Type w} {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C}
[inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct g] (p : α → β)
(q : (a : α) → f a ⟶ g (p a)) (a : α),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f a) (CategoryTheory.Limits.Sigma.map' p q) =
CategoryTheory.CategoryStruct.comp (q a) (CategoryTheory.Limits.Sigma.ι g (p a))
This theorem states that for any two types `α` and `β`, and a category `C`, given functions `f : α → C` and `g : β → C` which have coproducts, and a function `p : α → β` as well as a family of morphisms `q : (a : α) → f a ⟶ g (p a)`, for any `a : α`, the composition of the `a`-th inclusion of `f` and the map induced by `p` and `q` on the sigma-object over `f` is equal to the composition of the morphism `q a` and the `p(a)`-th inclusion of `g`. This shows a compatibility between the operation of taking coproducts and the composition of morphisms in the category.
More concisely: For any types `α` and `β` and a category `C`, given functions `f : α → C`, `g : β → C`, and a morphism `p : α → β`, if `f` and `g` have coproducts and there are given morphisms `q : ∀ a : α, f a → g (p a)`, then the composition of the coproduct inclusion of `f a` and `p` with `q a` equals the composition of `q a` and the coproduct inclusion of `g (p a)` for all `a : α`.
|
CategoryTheory.Limits.Cofan.IsColimit.fac
theorem CategoryTheory.Limits.Cofan.IsColimit.fac :
∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : β → C}
{c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f : (i : β) → F i ⟶ A)
(i : β), CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.Limits.Cofan.IsColimit.desc hc f) = f i
The theorem `CategoryTheory.Limits.Cofan.IsColimit.fac` states that for any category `C`, a function `F` from an arbitrary type `β` to `C`, a cofan `c` over `F`, a colimit `hc` of `c`, an object `A` of `C`, and a family of morphisms `f` from each `F i` to `A` for all `i` in `β`, the composition of the `i`-th injection from the cofan `c` and the morphism from the colimit `hc` to `A` that is constructed via `f`, is equal to the `i`-th morphism in `f`.
In other words, it shows that the morphism created by `CategoryTheory.Limits.Cofan.IsColimit.desc` from the colimit to `A`, when composed with the `i`-th injection from the cofan, yields the original `i`-th morphism from `F i` to `A`. This property is crucial for the concept of a colimit in category theory, reflecting the universal property that colimits satisfy.
More concisely: For any category C, given a cofan c over a function F from type β to C, a colimit hc of c, and a family of morphisms f from Fi to A, the diagram commutes, i.e., for all i in β, the composition of the injection from Fi to c and the morphism from hc to A along f equals the morphism f itself.
|
CategoryTheory.Limits.piComparison_comp_π
theorem CategoryTheory.Limits.piComparison_comp_π :
∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C)
[inst_2 : CategoryTheory.Limits.HasProduct f] [inst_3 : CategoryTheory.Limits.HasProduct fun b => G.obj (f b)]
(b : β),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piComparison G f)
(CategoryTheory.Limits.Pi.π (fun b => G.obj (f b)) b) =
G.map (CategoryTheory.Limits.Pi.π f b)
The theorem `CategoryTheory.Limits.piComparison_comp_π` states that, given any type `β`, categories `C` and `D`, a functor `G` from `C` to `D`, and a function `f : β → C` for which the product exists in both `C` and `D`, for any element `b : β`, the composition of the "pi comparison" morphism associated with `G` and `f` and the `b`-th projection from the pi object over `G.obj ∘ f` is equal to the `G`-map of the `b`-th projection from the pi object over `f`. Here, the "pi comparison" morphism is a natural transformation between functors from the category of `β`-indexed families of objects in `C` to `D`, which is part of the definition of a product in a category.
More concisely: Given a functor G from category C to D, a type β, and a function f : β → C such that the product exists in both C and D, for all b : β, the composition of the pi comparison morphism and the b-th projection from the pi object over G ∘ f equals the G-map of the b-th projection from the pi object over f.
|
CategoryTheory.Limits.Pi.hom_ext
theorem CategoryTheory.Limits.Pi.hom_ext :
∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C}
[inst_1 : CategoryTheory.Limits.HasProduct f] {X : C} (g₁ g₂ : X ⟶ ∏ f),
(∀ (b : β),
CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Pi.π f b) =
CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Pi.π f b)) →
g₁ = g₂
This theorem, `CategoryTheory.Limits.Pi.hom_ext`, states that for any category `C`, any indexing type `β`, and any function `f : β → C` that has a product in `C`, if we have two morphisms `g₁, g₂: X ⟶ ∏ f` from some object `X` to the product of `f`, then `g₁` is equal to `g₂` if and only if for all `b` in `β`, the composition of `g₁` and the `b`-th projection from the product of `f` is equal to the composition of `g₂` and the same projection. In essence, two morphisms to a product are the same if they make the same diagram commute with all projection maps from the product.
More concisely: Given a category \(C\), a function \(f : \beta \rightarrow C\) with product \(\prod f\), and morphisms \(g\_1, g\_2 : X \rightarrow \prod f\), \(g\_1 = g\_2\) if and only if \(g\_1 \circ p\_b = g\_2 \circ p\_b\) for all \(b \in \beta\), where \(p\_b\) denotes the \(b\)-th projection from \(\prod f\).
|
CategoryTheory.Limits.Sigma.hom_ext
theorem CategoryTheory.Limits.Sigma.hom_ext :
∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C}
[inst_1 : CategoryTheory.Limits.HasCoproduct f] {X : C} (g₁ g₂ : ∐ f ⟶ X),
(∀ (b : β),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) g₁ =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) g₂) →
g₁ = g₂
This theorem, `CategoryTheory.Limits.Sigma.hom_ext`, states the following in the language of category theory:
Given a category `C`, a function `f` from some type `β` to objects of `C`, and an object `X` in `C`, if `f` has coproduct (denoted as `∐ f`) in the category `C`, then for any two morphisms `g₁` and `g₂` from the coproduct `∐ f` to `X`, if for every `b` in `β`, the composition of the `b`-th inclusion morphism from `f b` to `∐ f` and `g₁` equals the composition of the `b`-th inclusion morphism and `g₂`, then `g₁` equals `g₂`.
In simpler terms, it asserts the uniqueness of morphisms from the coproduct to another object, given certain conditions. If two morphisms coincide when composed with the inclusion morphisms into the coproduct for every element in the domain of `f`, then those two morphisms are equal.
More concisely: Given a functor `f : C → C` from a category `C` with a coproduct `∐ f`, if for all objects `b` in the domain of `f` and morphisms `g₁, g₂ : ∐ f → X`, `g₁ ∘ i_b = g₂ ∘ i_b` implies `g₁ = g₂`, then `∐ f` has a unique coproduct morphism to `X`.
|
CategoryTheory.Limits.Sigma.ι_comp_map'_assoc
theorem CategoryTheory.Limits.Sigma.ι_comp_map'_assoc :
∀ {β : Type w} {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C}
[inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct g] (p : α → β)
(q : (a : α) → f a ⟶ g (p a)) (a : α) {Z : C} (h : ∐ g ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f a)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.map' p q) h) =
CategoryTheory.CategoryStruct.comp (q a)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι g (p a)) h)
This theorem in Category Theory states that for any types `α` and `β` and any category `C`, given two functors `f : α → C` and `g : β → C` that both have coproducts, a function `p : α → β`, a natural transformation `q : (a : α) → f a ⟶ g (p a)` from `f` to `g` and another object `Z` in `C` with a morphism `h : ∐ g ⟶ Z`, the composition of the inclusion of `f a` into the coproduct of `f`, the map from the coproduct of `f` to the coproduct of `g` induced by `p` and `q`, and `h` is the same as the composition of `q a`, the inclusion of `g (p a)` into the coproduct of `g`, and `h`.
In simpler terms, it says that in the given context, we can either first map from `f a` to `g (p a)` and then include the result into the coproduct or we can first include `f a` into the coproduct and then map the entire coproduct over, and in both cases we end up with the same morphism from `f a` to `Z` after we compose with `h`.
More concisely: For any categories C, types α and β, functors f : α → C and g : β → C with coproducts, natural transformation q : (a : α) → fa ➔ g (pa), and morphism h : ∐ g ➔ Z, the diagram commutes: fa ��� ∐ f ⟶ Z if and only if q a ⟶ g (pa) ⟶ h holds.
|
CategoryTheory.Limits.Pi.map'_comp_π
theorem CategoryTheory.Limits.Pi.map'_comp_π :
∀ {β : Type w} {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C}
[inst_1 : CategoryTheory.Limits.HasProduct f] [inst_2 : CategoryTheory.Limits.HasProduct g] (p : β → α)
(q : (b : β) → f (p b) ⟶ g b) (b : β),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map' p q) (CategoryTheory.Limits.Pi.π g b) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f (p b)) (q b)
The theorem `CategoryTheory.Limits.Pi.map'_comp_π` states the following: Given two types `α` and `β`, a category `C`, two functions `f: α → C` and `g: β → C` that have products in `C`, a function `p: β → α`, and a family of morphisms `q: (b : β) → f (p b) ⟶ g b`, for any element `b` in `β`, the composition of the map induced by `p` and `q` with the `b`-th projection from the product of `g` is equal to the composition of the `p b`-th projection from the product of `f` with the `b`-th morphism in the family `q`. In other words, this theorem relates the composition of morphisms in terms of their products, emphasizing the interplay between composition, products, and the specific morphisms in the category.
More concisely: Given functions `f: α → C`, `g: β → C`, `p: β → α`, and families of morphisms `q: (b : β) → f (p b) ⟶ g b`, the maps `(π₁ ∘ q) (b) = (g b) ∘ (π₂ (p, b))` for all `b: β`, where `π₁` and `π₂` are the projections of the products of `f` and `g` and `β × α`, respectively.
|