CategoryTheory.CartesianClosed.curry_eq_iff
theorem CategoryTheory.CartesianClosed.curry_eq_iff :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A X Y : C}
[inst_1 : CategoryTheory.Limits.HasFiniteProducts C] [inst_2 : CategoryTheory.Exponentiable A] (f : A ⨯ Y ⟶ X)
(g : Y ⟶ A ⟹ X), CategoryTheory.CartesianClosed.curry f = g ↔ f = CategoryTheory.CartesianClosed.uncurry g
This theorem states that in a category `C` with finite products and an exponentiable object `A`, for morphisms `f : A ⨯ Y ⟶ X` and `g : Y ⟶ A ⟹ X`, `f` is the uncurrying of `g` if and only if `g` is the currying of `f`. In other words, the currying and uncurrying operations are inverses of each other. These operations stem from the concept of a Cartesian closed category, where there exists an adjunction between the -⨯ Y and Y⟹- functors, with currying as the unit and uncurrying as the counit of the adjunction.
More concisely: In a Cartesian closed category with finite products, the currying and uncurrying operations are mutually inverse morphism transformations between the product and function types.
|
CategoryTheory.strict_initial
theorem CategoryTheory.strict_initial :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
[inst_1 : CategoryTheory.Limits.HasFiniteProducts C] [inst_2 : CategoryTheory.Exponentiable A] {I : C},
CategoryTheory.Limits.IsInitial I → ∀ (f : A ⟶ I), CategoryTheory.IsIso f
This theorem states that if a category `C` has an initial object `I` and finite products, and `A` is an exponentiable object in `C`, then any morphism `f` from `A` to `I` is an isomorphism. More specifically, the initial object `I` is a strict initial object; that is, any morphism to `I` is an isomorphism. A key aspect of this theorem is that it actually shows a slightly stronger version: any morphism to an initial object from an exponentiable object is an isomorphism, enhancing the strength of the initial object's property.
More concisely: In a category with finite products and an initial object, any morphism from an exponentiable object to the initial object is an isomorphism.
|
CategoryTheory.initial_mono
theorem CategoryTheory.initial_mono :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
{I : C} (B : C) (t : CategoryTheory.Limits.IsInitial I) [inst_2 : CategoryTheory.CartesianClosed C],
CategoryTheory.Mono (t.to B)
The theorem `CategoryTheory.initial_mono` states that in a Cartesian Closed Category (CCC) `C`, which has finite products, if there exists an initial object `I`, then every morphism from this initial object `I` to any other object `B` in the category `C` is a monomorphism. A monomorphism, often abbreviated as mono, is a morphism (or map) in category theory which is left-cancellative, meaning that if two morphisms are equal after being composed with this morphism, then they were equal to begin with.
More concisely: In a Cartesian Closed Category with finite products and an initial object, every morphism from the initial object is a monomorphism.
|
CategoryTheory.CartesianClosed.uncurry_eq
theorem CategoryTheory.CartesianClosed.uncurry_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A X Y : C}
[inst_1 : CategoryTheory.Limits.HasFiniteProducts C] [inst_2 : CategoryTheory.Exponentiable A] (g : Y ⟶ A ⟹ X),
CategoryTheory.CartesianClosed.uncurry g =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id A) g)
((CategoryTheory.exp.ev A).app X)
This theorem states that for any category `C` with finite products and any object `A` that is exponentiable, for any morphism `g` from `Y` to the exponential object of `A` and `X`, the uncurrying of `g` is equivalent to the composition of the mapping of the product of `A` and `g` with the application of the evaluation natural transformation at `X`. In other words, it expresses that uncurrying in a cartesian closed category can be seen as a process involving the composition of other morphisms in the category.
More concisely: In a cartesian closed category with finite products, for any exponentiable object `A` and any morphism `g` from `Y` to `A^X`, the uncurried version of `g` is equal to the composition of `g` with the evaluation at `X` of the product of `A` and `g`.
|