CategoryTheory.Pi.ext
theorem CategoryTheory.Pi.ext :
∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X Y : (i : I) → C i}
{f g : X ⟶ Y}, (∀ (i : I), f i = g i) → f = g
This theorem, `CategoryTheory.Pi.ext`, states that for any type `I` and a type-dependent family of categories `C`, if `X` and `Y` are two objects in the product category (where the objects are the product of the objects in the individual categories), and if `f` and `g` are two morphisms between these objects, then if for every object `i` in `I` the component of `f` and `g` at `i` are identical, then the morphisms `f` and `g` are identical. In other words, two morphisms in a product category are equal if and only if their components are equal in each of the original categories.
More concisely: In the product category of a family of categories `C` indexed by type `I`, two morphisms between objects `X` and `Y` are equal if and only if their component morphisms at every object `i` in `I` are equal.
|
CategoryTheory.Functor.pi_ext
theorem CategoryTheory.Functor.pi_ext :
∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {A : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} A] (f f' : CategoryTheory.Functor A ((i : I) → C i)),
(∀ (i : I), f.comp (CategoryTheory.Pi.eval C i) = f'.comp (CategoryTheory.Pi.eval C i)) → f = f'
This theorem, `CategoryTheory.Functor.pi_ext`, states that for any type `I`, and a function `C` from `I` to some type, where each `C i` is a category, and also given a type `A` that is a category, two functors `f` and `f'` from `A` to the product of the categories `C i` (indexed by `I`) are considered equal if and only if they agree on every coordinate `i` of `I`. Here, the agreement is defined in terms of composition with the evaluation functor at `i`, which sends an `I`-indexed family of objects to the object over `i`.
More concisely: Two functors from a category `A` to the product of categories indexed by `I`, where each `C i` is a category, are equal if and only if they agree on every coordinate `i` in terms of composition with the evaluation functor.
|