Documentation

Mathlib.CategoryTheory.ChosenFiniteProducts

Categories with chosen finite products #

We introduce a class, ChosenFiniteProducts, which bundles explicit choices for a terminal object and binary products in a category C. This is primarily useful for categories which have finite products with good definitional properties, such as the category of types.

Given a category with such an instance, we also provide the associated symmetric monoidal structure so that one can write X ⊗ Y for the explicit binary product and 𝟙_ C for the explicit terminal object.

Implementation notes #

For cartesian monoidal categories, the oplax-monoidal/monoidal/braided structure of a functor F preserving finite products is uniquely determined. See the ofChosenFiniteProducts declarations.

We however develop the theory for any F.OplaxMonoidal/F.Monoidal/F.Braided instance instead of requiring it to be the ofChosenFiniteProducts one. This is to avoid diamonds: Consider eg 𝟭 C and F ⋙ G.

In applications requiring a finite preserving functor to be oplax-monoidal/monoidal/braided, avoid attribute [local instance] ofChosenFiniteProducts but instead turn on the corresponding ofChosenFiniteProducts declaration for that functor only.

Projects #

Construct an instance of chosen finite products in the category of affine scheme, using the tensor product.
Construct chosen finite products in other categories appearing "in nature".

class CategoryTheory.ChosenFiniteProducts (C : Type u) [Category.{v, u} C] :

Type (max u v)

An instance of ChosenFiniteProducts C bundles an explicit choice of a binary product of two objects of C, and a terminal object in C.

Users should use the monoidal notation: X ⊗ Y for the product and 𝟙_ C for the terminal object.

product (X Y : C) : Limits.LimitCone (Limits.pair X Y)
A choice of a limit binary fan for any two objects of the category.
terminal : Limits.LimitCone (Functor.empty C)
A choice of a terminal object.

Instances

@[instance 100]

instance CategoryTheory.ChosenFiniteProducts.instMonoidalCategory (C : Type u) [Category.{v, u} C] [ChosenFiniteProducts C] :

MonoidalCategory C

Equations

One or more equations did not get rendered due to their size.

@[instance 100]

instance CategoryTheory.ChosenFiniteProducts.instSymmetricCategory (C : Type u) [Category.{v, u} C] [ChosenFiniteProducts C] :

SymmetricCategory C

Equations

One or more equations did not get rendered due to their size.

theorem CategoryTheory.ChosenFiniteProducts.braiding_eq_braiding {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y : C) :

β_ X Y = Limits.BinaryFan.braiding (product X Y).isLimit (product Y X).isLimit

def CategoryTheory.ChosenFiniteProducts.toUnit {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X : C) :

X ⟶ MonoidalCategoryStruct.tensorUnit C

The unique map to the terminal object.

Equations

One or more equations did not get rendered due to their size.

Instances For

instance CategoryTheory.ChosenFiniteProducts.instUniqueHomTensorUnit {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X : C) :

Unique (X ⟶ MonoidalCategoryStruct.tensorUnit C)

Equations

CategoryTheory.ChosenFiniteProducts.instUniqueHomTensorUnit X = { default := CategoryTheory.ChosenFiniteProducts.toUnit X, uniq := ⋯ }

theorem CategoryTheory.ChosenFiniteProducts.toUnit_unique {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X : C} (f g : X ⟶ MonoidalCategoryStruct.tensorUnit C) :

f = g

This lemma follows from the preexisting Unique instance, but it is often convenient to use it directly as apply toUnit_unique forcing lean to do the necessary elaboration.

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.comp_toUnit {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y : C} (f : X ⟶ Y) :

CategoryStruct.comp f (toUnit Y) = toUnit X

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.comp_toUnit_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y : C} (f : X ⟶ Y) {Z : C} (h : MonoidalCategoryStruct.tensorUnit C ⟶ Z) :

CategoryStruct.comp f (CategoryStruct.comp (toUnit Y) h) = CategoryStruct.comp (toUnit X) h

def CategoryTheory.ChosenFiniteProducts.lift {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) :

T ⟶ MonoidalCategoryStruct.tensorObj X Y

Construct a morphism to the product given its two components.

Equations

CategoryTheory.ChosenFiniteProducts.lift f g = (CategoryTheory.ChosenFiniteProducts.product X Y).isLimit.lift (CategoryTheory.Limits.BinaryFan.mk f g)

Instances For

def CategoryTheory.ChosenFiniteProducts.fst {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y : C) :

MonoidalCategoryStruct.tensorObj X Y ⟶ X

The first projection from the product.

Equations

CategoryTheory.ChosenFiniteProducts.fst X Y = CategoryTheory.Limits.BinaryFan.fst (CategoryTheory.ChosenFiniteProducts.product X Y).cone

Instances For

def CategoryTheory.ChosenFiniteProducts.snd {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y : C) :

MonoidalCategoryStruct.tensorObj X Y ⟶ Y

The second projection from the product.

Equations

CategoryTheory.ChosenFiniteProducts.snd X Y = CategoryTheory.Limits.BinaryFan.snd (CategoryTheory.ChosenFiniteProducts.product X Y).cone

Instances For

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_fst {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) :

CategoryStruct.comp (lift f g) (fst X Y) = f

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_fst_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) {Z : C} (h : X ⟶ Z) :

CategoryStruct.comp (lift f g) (CategoryStruct.comp (fst X Y) h) = CategoryStruct.comp f h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_snd {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) :

CategoryStruct.comp (lift f g) (snd X Y) = g

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_snd_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) {Z : C} (h : Y ⟶ Z) :

CategoryStruct.comp (lift f g) (CategoryStruct.comp (snd X Y) h) = CategoryStruct.comp g h

instance CategoryTheory.ChosenFiniteProducts.mono_lift_of_mono_left {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [Mono f] :

Mono (lift f g)

instance CategoryTheory.ChosenFiniteProducts.mono_lift_of_mono_right {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [Mono g] :

Mono (lift f g)

theorem CategoryTheory.ChosenFiniteProducts.hom_ext {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {T X Y : C} (f g : T ⟶ MonoidalCategoryStruct.tensorObj X Y) (h_fst : CategoryStruct.comp f (fst X Y) = CategoryStruct.comp g (fst X Y)) (h_snd : CategoryStruct.comp f (snd X Y) = CategoryStruct.comp g (snd X Y)) :

f = g

theorem CategoryTheory.ChosenFiniteProducts.hom_ext_iff {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {T X Y : C} {f g : T ⟶ MonoidalCategoryStruct.tensorObj X Y} :

f = g ↔ CategoryStruct.comp f (fst X Y) = CategoryStruct.comp g (fst X Y) ∧ CategoryStruct.comp f (snd X Y) = CategoryStruct.comp g (snd X Y)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.comp_lift {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {V W X Y : C} (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) :

CategoryStruct.comp f (lift g h) = lift (CategoryStruct.comp f g) (CategoryStruct.comp f h)

theorem CategoryTheory.ChosenFiniteProducts.comp_lift_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {V W X Y : C} (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) {Z : C} (h✝ : MonoidalCategoryStruct.tensorObj X Y ⟶ Z) :

CategoryStruct.comp f (CategoryStruct.comp (lift g h) h✝) = CategoryStruct.comp (lift (CategoryStruct.comp f g) (CategoryStruct.comp f h)) h✝

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_fst_snd {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y : C} :

lift (fst X Y) (snd X Y) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X Y)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_comp_fst_snd {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y Z : C} (f : X ⟶ MonoidalCategoryStruct.tensorObj Y Z) :

lift (CategoryStruct.comp f (fst Y Z)) (CategoryStruct.comp f (snd Y Z)) = f

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.tensorHom_fst {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) :

CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) (fst X₂ Y₂) = CategoryStruct.comp (fst X₁ Y₁) f

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.tensorHom_fst_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) {Z : C} (h : X₂ ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) (CategoryStruct.comp (fst X₂ Y₂) h) = CategoryStruct.comp (fst X₁ Y₁) (CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.tensorHom_snd {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) :

CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) (snd X₂ Y₂) = CategoryStruct.comp (snd X₁ Y₁) g

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.tensorHom_snd_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) {Z : C} (h : Y₂ ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) (CategoryStruct.comp (snd X₂ Y₂) h) = CategoryStruct.comp (snd X₁ Y₁) (CategoryStruct.comp g h)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_map {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {V W X Y Z : C} (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) :

CategoryStruct.comp (lift f g) (MonoidalCategoryStruct.tensorHom h k) = lift (CategoryStruct.comp f h) (CategoryStruct.comp g k)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_map_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {V W X Y Z : C} (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) {Z✝ : C} (h✝ : MonoidalCategoryStruct.tensorObj Y Z ⟶ Z✝) :

CategoryStruct.comp (lift f g) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom h k) h✝) = CategoryStruct.comp (lift (CategoryStruct.comp f h) (CategoryStruct.comp g k)) h✝

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_fst_comp_snd_comp {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {W X Y Z : C} (g : W ⟶ X) (g' : Y ⟶ Z) :

lift (CategoryStruct.comp (fst W Y) g) (CategoryStruct.comp (snd W Y) g') = MonoidalCategoryStruct.tensorHom g g'

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.whiskerLeft_fst {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X g) (fst X Y₂) = fst X Y₁

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.whiskerLeft_fst_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) {Z : C} (h : X ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X g) (CategoryStruct.comp (fst X Y₂) h) = CategoryStruct.comp (fst X Y₁) h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.whiskerLeft_snd {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X g) (snd X Y₂) = CategoryStruct.comp (snd X Y₁) g

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.whiskerLeft_snd_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) {Z : C} (h : Y₂ ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X g) (CategoryStruct.comp (snd X Y₂) h) = CategoryStruct.comp (snd X Y₁) (CategoryStruct.comp g h)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.whiskerRight_fst {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Y) (fst X₂ Y) = CategoryStruct.comp (fst X₁ Y) f

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.whiskerRight_fst_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) {Z : C} (h : X₂ ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Y) (CategoryStruct.comp (fst X₂ Y) h) = CategoryStruct.comp (fst X₁ Y) (CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.whiskerRight_snd {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Y) (snd X₂ Y) = snd X₁ Y

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.whiskerRight_snd_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) {Z : C} (h : Y ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Y) (CategoryStruct.comp (snd X₂ Y) h) = CategoryStruct.comp (snd X₁ Y) h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_whiskerRight {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : Y ⟶ W) :

CategoryStruct.comp (lift f g) (MonoidalCategoryStruct.whiskerRight h Z) = lift (CategoryStruct.comp f h) g

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : Y ⟶ W) {Z✝ : C} (h✝ : MonoidalCategoryStruct.tensorObj W Z ⟶ Z✝) :

CategoryStruct.comp (lift f g) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight h Z) h✝) = CategoryStruct.comp (lift (CategoryStruct.comp f h) g) h✝

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_whiskerLeft {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : Z ⟶ W) :

CategoryStruct.comp (lift f g) (MonoidalCategoryStruct.whiskerLeft Y h) = lift f (CategoryStruct.comp g h)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_whiskerLeft_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : Z ⟶ W) {Z✝ : C} (h✝ : MonoidalCategoryStruct.tensorObj Y W ⟶ Z✝) :

CategoryStruct.comp (lift f g) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Y h) h✝) = CategoryStruct.comp (lift f (CategoryStruct.comp g h)) h✝

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_hom_fst {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y Z : C) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).hom (fst X (MonoidalCategoryStruct.tensorObj Y Z)) = CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj X Y) Z) (fst X Y)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_hom_fst_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y Z : C) {Z✝ : C} (h : X ⟶ Z✝) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).hom (CategoryStruct.comp (fst X (MonoidalCategoryStruct.tensorObj Y Z)) h) = CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (fst X Y) h)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_hom_snd_fst {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y Z : C) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).hom (CategoryStruct.comp (snd X (MonoidalCategoryStruct.tensorObj Y Z)) (fst Y Z)) = CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj X Y) Z) (snd X Y)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_hom_snd_fst_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y Z : C) {Z✝ : C} (h : Y ⟶ Z✝) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).hom (CategoryStruct.comp (snd X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (fst Y Z) h)) = CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (snd X Y) h)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_hom_snd_snd {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y Z : C) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).hom (CategoryStruct.comp (snd X (MonoidalCategoryStruct.tensorObj Y Z)) (snd Y Z)) = snd (MonoidalCategoryStruct.tensorObj X Y) Z

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_hom_snd_snd_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y Z : C) {Z✝ : C} (h : Z ⟶ Z✝) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).hom (CategoryStruct.comp (snd X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (snd Y Z) h)) = CategoryStruct.comp (snd (MonoidalCategoryStruct.tensorObj X Y) Z) h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_inv_fst_fst {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y Z : C) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).inv (CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj X Y) Z) (fst X Y)) = fst X (MonoidalCategoryStruct.tensorObj Y Z)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_inv_fst_fst_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y Z : C) {Z✝ : C} (h : X ⟶ Z✝) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).inv (CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (fst X Y) h)) = CategoryStruct.comp (fst X (MonoidalCategoryStruct.tensorObj Y Z)) h

@[deprecated CategoryTheory.ChosenFiniteProducts.associator_inv_fst_fst (since := "2025-04-01")]

theorem CategoryTheory.ChosenFiniteProducts.associator_inv_fst {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y Z : C) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).inv (CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj X Y) Z) (fst X Y)) = fst X (MonoidalCategoryStruct.tensorObj Y Z)

Alias of CategoryTheory.ChosenFiniteProducts.associator_inv_fst_fst.

@[deprecated CategoryTheory.ChosenFiniteProducts.associator_inv_fst_fst_assoc (since := "2025-04-01")]

theorem CategoryTheory.ChosenFiniteProducts.associator_inv_fst_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y Z : C) {Z✝ : C} (h : X ⟶ Z✝) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).inv (CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (fst X Y) h)) = CategoryStruct.comp (fst X (MonoidalCategoryStruct.tensorObj Y Z)) h

Alias of CategoryTheory.ChosenFiniteProducts.associator_inv_fst_fst_assoc.

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_inv_fst_snd {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y Z : C) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).inv (CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj X Y) Z) (snd X Y)) = CategoryStruct.comp (snd X (MonoidalCategoryStruct.tensorObj Y Z)) (fst Y Z)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_inv_fst_snd_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y Z : C) {Z✝ : C} (h : Y ⟶ Z✝) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).inv (CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (snd X Y) h)) = CategoryStruct.comp (snd X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (fst Y Z) h)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_inv_snd {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y Z : C) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).inv (snd (MonoidalCategoryStruct.tensorObj X Y) Z) = CategoryStruct.comp (snd X (MonoidalCategoryStruct.tensorObj Y Z)) (snd Y Z)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_inv_snd_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y Z : C) {Z✝ : C} (h : Z ⟶ Z✝) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).inv (CategoryStruct.comp (snd (MonoidalCategoryStruct.tensorObj X Y) Z) h) = CategoryStruct.comp (snd X (MonoidalCategoryStruct.tensorObj Y Z)) (CategoryStruct.comp (snd Y Z) h)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_lift_associator_hom {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) :

CategoryStruct.comp (lift (lift f g) h) (MonoidalCategoryStruct.associator Y Z W).hom = lift f (lift g h)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_lift_associator_hom_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) {Z✝ : C} (h✝ : MonoidalCategoryStruct.tensorObj Y (MonoidalCategoryStruct.tensorObj Z W) ⟶ Z✝) :

CategoryStruct.comp (lift (lift f g) h) (CategoryStruct.comp (MonoidalCategoryStruct.associator Y Z W).hom h✝) = CategoryStruct.comp (lift f (lift g h)) h✝

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_lift_associator_inv {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) :

CategoryStruct.comp (lift f (lift g h)) (MonoidalCategoryStruct.associator Y Z W).inv = lift (lift f g) h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_lift_associator_inv_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) {Z✝ : C} (h✝ : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj Y Z) W ⟶ Z✝) :

CategoryStruct.comp (lift f (lift g h)) (CategoryStruct.comp (MonoidalCategoryStruct.associator Y Z W).inv h✝) = CategoryStruct.comp (lift (lift f g) h) h✝

theorem CategoryTheory.ChosenFiniteProducts.leftUnitor_hom {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X : C) :

(MonoidalCategoryStruct.leftUnitor X).hom = snd (MonoidalCategoryStruct.tensorUnit C) X

theorem CategoryTheory.ChosenFiniteProducts.rightUnitor_hom {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X : C) :

(MonoidalCategoryStruct.rightUnitor X).hom = fst X (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.leftUnitor_inv_fst {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X : C) :

CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).inv (fst (MonoidalCategoryStruct.tensorUnit C) X) = toUnit X

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.leftUnitor_inv_fst_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X : C) {Z : C} (h : MonoidalCategoryStruct.tensorUnit C ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).inv (CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorUnit C) X) h) = CategoryStruct.comp (toUnit X) h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.leftUnitor_inv_snd {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X : C) :

CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).inv (snd (MonoidalCategoryStruct.tensorUnit C) X) = CategoryStruct.id X

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.leftUnitor_inv_snd_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X : C) {Z : C} (h : X ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).inv (CategoryStruct.comp (snd (MonoidalCategoryStruct.tensorUnit C) X) h) = h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.rightUnitor_inv_fst {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X : C) :

CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).inv (fst X (MonoidalCategoryStruct.tensorUnit C)) = CategoryStruct.id X

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.rightUnitor_inv_fst_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X : C) {Z : C} (h : X ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).inv (CategoryStruct.comp (fst X (MonoidalCategoryStruct.tensorUnit C)) h) = h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.rightUnitor_inv_snd {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X : C) :

CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).inv (snd X (MonoidalCategoryStruct.tensorUnit C)) = toUnit X

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.rightUnitor_inv_snd_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X : C) {Z : C} (h : MonoidalCategoryStruct.tensorUnit C ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).inv (CategoryStruct.comp (snd X (MonoidalCategoryStruct.tensorUnit C)) h) = CategoryStruct.comp (toUnit X) h

theorem CategoryTheory.ChosenFiniteProducts.whiskerLeft_toUnit_comp_rightUnitor_hom {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y : C) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (toUnit Y)) (MonoidalCategoryStruct.rightUnitor X).hom = fst X Y

theorem CategoryTheory.ChosenFiniteProducts.whiskerLeft_toUnit_comp_rightUnitor_hom_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y : C) {Z : C} (h : X ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (toUnit Y)) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).hom h) = CategoryStruct.comp (fst X Y) h

theorem CategoryTheory.ChosenFiniteProducts.whiskerRight_toUnit_comp_leftUnitor_hom {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y : C) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (toUnit X) Y) (MonoidalCategoryStruct.leftUnitor Y).hom = snd X Y

theorem CategoryTheory.ChosenFiniteProducts.whiskerRight_toUnit_comp_leftUnitor_hom_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X Y : C) {Z : C} (h : Y ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (toUnit X) Y) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Y).hom h) = CategoryStruct.comp (snd X Y) h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_leftUnitor_hom {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y : C} (f : X ⟶ MonoidalCategoryStruct.tensorUnit C) (g : X ⟶ Y) :

CategoryStruct.comp (lift f g) (MonoidalCategoryStruct.leftUnitor Y).hom = g

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_leftUnitor_hom_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y : C} (f : X ⟶ MonoidalCategoryStruct.tensorUnit C) (g : X ⟶ Y) {Z : C} (h : Y ⟶ Z) :

CategoryStruct.comp (lift f g) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Y).hom h) = CategoryStruct.comp g h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_rightUnitor_hom {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y : C} (f : X ⟶ Y) (g : X ⟶ MonoidalCategoryStruct.tensorUnit C) :

CategoryStruct.comp (lift f g) (MonoidalCategoryStruct.rightUnitor Y).hom = f

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_rightUnitor_hom_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y : C} (f : X ⟶ Y) (g : X ⟶ MonoidalCategoryStruct.tensorUnit C) {Z : C} (h : Y ⟶ Z) :

CategoryStruct.comp (lift f g) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Y).hom h) = CategoryStruct.comp f h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.braiding_hom_fst {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y : C} :

CategoryStruct.comp (β_ X Y).hom (fst Y X) = snd X Y

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.braiding_hom_fst_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y Z : C} (h : Y ⟶ Z) :

CategoryStruct.comp (β_ X Y).hom (CategoryStruct.comp (fst Y X) h) = CategoryStruct.comp (snd X Y) h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.braiding_hom_snd {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y : C} :

CategoryStruct.comp (β_ X Y).hom (snd Y X) = fst X Y

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.braiding_hom_snd_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y Z : C} (h : X ⟶ Z) :

CategoryStruct.comp (β_ X Y).hom (CategoryStruct.comp (snd Y X) h) = CategoryStruct.comp (fst X Y) h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.braiding_inv_fst {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y : C} :

CategoryStruct.comp (β_ X Y).inv (fst X Y) = snd Y X

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.braiding_inv_fst_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y Z : C} (h : X ⟶ Z) :

CategoryStruct.comp (β_ X Y).inv (CategoryStruct.comp (fst X Y) h) = CategoryStruct.comp (snd Y X) h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.braiding_inv_snd {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y : C} :

CategoryStruct.comp (β_ X Y).inv (snd X Y) = fst Y X

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.braiding_inv_snd_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y Z : C} (h : Y ⟶ Z) :

CategoryStruct.comp (β_ X Y).inv (CategoryStruct.comp (snd X Y) h) = CategoryStruct.comp (fst Y X) h

theorem CategoryTheory.ChosenFiniteProducts.lift_snd_fst {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {X Y : C} :

lift (snd X Y) (fst X Y) = (β_ X Y).hom

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_snd_comp_fst_comp {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {W X Y Z : C} (g : W ⟶ X) (g' : Y ⟶ Z) :

lift (CategoryStruct.comp (snd W Y) g') (CategoryStruct.comp (fst W Y) g) = CategoryStruct.comp (β_ W Y).hom (MonoidalCategoryStruct.tensorHom g' g)

theorem CategoryTheory.ChosenFiniteProducts.lift_snd_comp_fst_comp_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {W X Y Z : C} (g : W ⟶ X) (g' : Y ⟶ Z) {Z✝ : C} (h : MonoidalCategoryStruct.tensorObj Z X ⟶ Z✝) :

CategoryStruct.comp (lift (CategoryStruct.comp (snd W Y) g') (CategoryStruct.comp (fst W Y) g)) h = CategoryStruct.comp (β_ W Y).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom g' g) h)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_braiding_hom {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) :

CategoryStruct.comp (lift f g) (β_ X Y).hom = lift g f

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_braiding_hom_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) {Z : C} (h : MonoidalCategoryStruct.tensorObj Y X ⟶ Z) :

CategoryStruct.comp (lift f g) (CategoryStruct.comp (β_ X Y).hom h) = CategoryStruct.comp (lift g f) h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_braiding_inv {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) :

CategoryStruct.comp (lift f g) (β_ Y X).inv = lift g f

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_braiding_inv_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) {Z : C} (h : MonoidalCategoryStruct.tensorObj Y X ⟶ Z) :

CategoryStruct.comp (lift f g) (CategoryStruct.comp (β_ Y X).inv h) = CategoryStruct.comp (lift g f) h

noncomputable def CategoryTheory.ChosenFiniteProducts.ofFiniteProducts (C : Type u) [Category.{v, u} C] [Limits.HasFiniteProducts C] :

ChosenFiniteProducts C

Construct an instance of ChosenFiniteProducts C given an instance of HasFiniteProducts C.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[instance 100]

instance CategoryTheory.ChosenFiniteProducts.instHasFiniteProducts {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] :

Limits.HasFiniteProducts C

@[reducible, inline]

abbrev CategoryTheory.ChosenFiniteProducts.terminalComparison {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) :

F.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ MonoidalCategoryStruct.tensorUnit D

When C and D have chosen finite products and F : C ⥤ D is any functor, terminalComparison F is the unique map F (𝟙_ C) ⟶ 𝟙_ D.

Equations

CategoryTheory.ChosenFiniteProducts.terminalComparison F = CategoryTheory.ChosenFiniteProducts.toUnit (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))

Instances For

theorem CategoryTheory.ChosenFiniteProducts.map_toUnit_comp_terminalComparison {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A : C) :

CategoryStruct.comp (F.map (toUnit A)) (terminalComparison F) = toUnit (F.obj A)

theorem CategoryTheory.ChosenFiniteProducts.map_toUnit_comp_terminalComparison_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A : C) {Z : D} (h : MonoidalCategoryStruct.tensorUnit D ⟶ Z) :

CategoryStruct.comp (F.map (toUnit A)) (CategoryStruct.comp (terminalComparison F) h) = CategoryStruct.comp (toUnit (F.obj A)) h

@[deprecated CategoryTheory.ChosenFiniteProducts.map_toUnit_comp_terminalComparison (since := "2025-04-09")]

theorem CategoryTheory.ChosenFiniteProducts.map_toUnit_comp_terminalCompariso {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A : C) :

CategoryStruct.comp (F.map (toUnit A)) (terminalComparison F) = toUnit (F.obj A)

Alias of CategoryTheory.ChosenFiniteProducts.map_toUnit_comp_terminalComparison.

@[deprecated CategoryTheory.ChosenFiniteProducts.map_toUnit_comp_terminalComparison_assoc (since := "2025-04-09")]

theorem CategoryTheory.ChosenFiniteProducts.map_toUnit_comp_terminalCompariso_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A : C) {Z : D} (h : MonoidalCategoryStruct.tensorUnit D ⟶ Z) :

CategoryStruct.comp (F.map (toUnit A)) (CategoryStruct.comp (terminalComparison F) h) = CategoryStruct.comp (toUnit (F.obj A)) h

Alias of CategoryTheory.ChosenFiniteProducts.map_toUnit_comp_terminalComparison_assoc.

theorem CategoryTheory.ChosenFiniteProducts.preservesLimit_empty_of_isIso_terminalComparison {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) [IsIso (terminalComparison F)] :

Limits.PreservesLimit (Functor.empty C) F

If terminalComparison F is an Iso, then F preserves terminal objects.

noncomputable def CategoryTheory.ChosenFiniteProducts.preservesTerminalIso {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) [h : Limits.PreservesLimit (Functor.empty C) F] :

F.obj (MonoidalCategoryStruct.tensorUnit C) ≅ MonoidalCategoryStruct.tensorUnit D

If F preserves terminal objects, then terminalComparison F is an isomorphism.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.preservesTerminalIso_hom {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) [Limits.PreservesLimit (Functor.empty C) F] :

(preservesTerminalIso F).hom = terminalComparison F

instance CategoryTheory.ChosenFiniteProducts.terminalComparison_isIso_of_preservesLimits {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) [Limits.PreservesLimit (Functor.empty C) F] :

IsIso (terminalComparison F)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.preservesTerminalIso_id {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] :

preservesTerminalIso (Functor.id C) = Iso.refl ((Functor.id C).obj (MonoidalCategoryStruct.tensorUnit C))

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.preservesTerminalIso_comp {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) {E : Type u₂} [Category.{v₂, u₂} E] [ChosenFiniteProducts E] (G : Functor D E) [Limits.PreservesLimit (Functor.empty C) F] [Limits.PreservesLimit (Functor.empty D) G] [Limits.PreservesLimit (Functor.empty C) (F.comp G)] :

preservesTerminalIso (F.comp G) = G.mapIso (preservesTerminalIso F) ≪≫ preservesTerminalIso G

def CategoryTheory.ChosenFiniteProducts.prodComparison {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A B : C) :

F.obj (MonoidalCategoryStruct.tensorObj A B) ⟶ MonoidalCategoryStruct.tensorObj (F.obj A) (F.obj B)

When C and D have chosen finite products and F : C ⥤ D is any functor, prodComparison F A B is the canonical comparison morphism from F (A ⊗ B) to F(A) ⊗ F(B).

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_fst {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A B : C) :

CategoryStruct.comp (prodComparison F A B) (fst (F.obj A) (F.obj B)) = F.map (fst A B)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_fst_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A B : C) {Z : D} (h : F.obj A ⟶ Z) :

CategoryStruct.comp (prodComparison F A B) (CategoryStruct.comp (fst (F.obj A) (F.obj B)) h) = CategoryStruct.comp (F.map (fst A B)) h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_snd {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A B : C) :

CategoryStruct.comp (prodComparison F A B) (snd (F.obj A) (F.obj B)) = F.map (snd A B)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_snd_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A B : C) {Z : D} (h : F.obj B ⟶ Z) :

CategoryStruct.comp (prodComparison F A B) (CategoryStruct.comp (snd (F.obj A) (F.obj B)) h) = CategoryStruct.comp (F.map (snd A B)) h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.inv_prodComparison_map_fst {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A B : C) [IsIso (prodComparison F A B)] :

CategoryStruct.comp (inv (prodComparison F A B)) (F.map (fst A B)) = fst (F.obj A) (F.obj B)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.inv_prodComparison_map_fst_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A B : C) [IsIso (prodComparison F A B)] {Z : D} (h : F.obj A ⟶ Z) :

CategoryStruct.comp (inv (prodComparison F A B)) (CategoryStruct.comp (F.map (fst A B)) h) = CategoryStruct.comp (fst (F.obj A) (F.obj B)) h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.inv_prodComparison_map_snd {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A B : C) [IsIso (prodComparison F A B)] :

CategoryStruct.comp (inv (prodComparison F A B)) (F.map (snd A B)) = snd (F.obj A) (F.obj B)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.inv_prodComparison_map_snd_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A B : C) [IsIso (prodComparison F A B)] {Z : D} (h : F.obj B ⟶ Z) :

CategoryStruct.comp (inv (prodComparison F A B)) (CategoryStruct.comp (F.map (snd A B)) h) = CategoryStruct.comp (snd (F.obj A) (F.obj B)) h

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_natural {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) {A B A' B' : C} (f : A ⟶ A') (g : B ⟶ B') :

CategoryStruct.comp (F.map (MonoidalCategoryStruct.tensorHom f g)) (prodComparison F A' B') = CategoryStruct.comp (prodComparison F A B) (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g))

Naturality of the prodComparison morphism in both arguments.

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_natural_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) {A B A' B' : C} (f : A ⟶ A') (g : B ⟶ B') {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj A') (F.obj B') ⟶ Z) :

CategoryStruct.comp (F.map (MonoidalCategoryStruct.tensorHom f g)) (CategoryStruct.comp (prodComparison F A' B') h) = CategoryStruct.comp (prodComparison F A B) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) h)

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_natural_whiskerLeft {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) {A B B' : C} (g : B ⟶ B') :

CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft A g)) (prodComparison F A B') = CategoryStruct.comp (prodComparison F A B) (MonoidalCategoryStruct.whiskerLeft (F.obj A) (F.map g))

Naturality of the prodComparison morphism in the right argument.

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_natural_whiskerLeft_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) {A B B' : C} (g : B ⟶ B') {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj A) (F.obj B') ⟶ Z) :

CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft A g)) (CategoryStruct.comp (prodComparison F A B') h) = CategoryStruct.comp (prodComparison F A B) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj A) (F.map g)) h)

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_natural_whiskerRight {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) {A B A' : C} (f : A ⟶ A') :

CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f B)) (prodComparison F A' B) = CategoryStruct.comp (prodComparison F A B) (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj B))

Naturality of the prodComparison morphism in the left argument.

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_natural_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) {A B A' : C} (f : A ⟶ A') {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj A') (F.obj B) ⟶ Z) :

CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f B)) (CategoryStruct.comp (prodComparison F A' B) h) = CategoryStruct.comp (prodComparison F A B) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj B)) h)

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_inv_natural {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) {A B A' B' : C} [IsIso (prodComparison F A B)] (f : A ⟶ A') (g : B ⟶ B') [IsIso (prodComparison F A' B')] :

CategoryStruct.comp (inv (prodComparison F A B)) (F.map (MonoidalCategoryStruct.tensorHom f g)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (inv (prodComparison F A' B'))

If the product comparison morphism is an iso, its inverse is natural in both argument.

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_inv_natural_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) {A B A' B' : C} [IsIso (prodComparison F A B)] (f : A ⟶ A') (g : B ⟶ B') [IsIso (prodComparison F A' B')] {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj A' B') ⟶ Z) :

CategoryStruct.comp (inv (prodComparison F A B)) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.tensorHom f g)) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (CategoryStruct.comp (inv (prodComparison F A' B')) h)

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_inv_natural_whiskerLeft {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) {A B B' : C} [IsIso (prodComparison F A B)] (g : B ⟶ B') [IsIso (prodComparison F A B')] :

CategoryStruct.comp (inv (prodComparison F A B)) (F.map (MonoidalCategoryStruct.whiskerLeft A g)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj A) (F.map g)) (inv (prodComparison F A B'))

If the product comparison morphism is an iso, its inverse is natural in the right argument.

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_inv_natural_whiskerLeft_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) {A B B' : C} [IsIso (prodComparison F A B)] (g : B ⟶ B') [IsIso (prodComparison F A B')] {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj A B') ⟶ Z) :

CategoryStruct.comp (inv (prodComparison F A B)) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft A g)) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj A) (F.map g)) (CategoryStruct.comp (inv (prodComparison F A B')) h)

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_inv_natural_whiskerRight {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) {A B A' : C} [IsIso (prodComparison F A B)] (f : A ⟶ A') [IsIso (prodComparison F A' B)] :

CategoryStruct.comp (inv (prodComparison F A B)) (F.map (MonoidalCategoryStruct.whiskerRight f B)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj B)) (inv (prodComparison F A' B))

If the product comparison morphism is an iso, its inverse is natural in the left argument.

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_inv_natural_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) {A B A' : C} [IsIso (prodComparison F A B)] (f : A ⟶ A') [IsIso (prodComparison F A' B)] {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj A' B) ⟶ Z) :

CategoryStruct.comp (inv (prodComparison F A B)) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f B)) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj B)) (CategoryStruct.comp (inv (prodComparison F A' B)) h)

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_comp {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) {A B : C} {E : Type u₂} [Category.{v₂, u₂} E] [ChosenFiniteProducts E] (G : Functor D E) :

prodComparison (F.comp G) A B = CategoryStruct.comp (G.map (prodComparison F A B)) (prodComparison G (F.obj A) (F.obj B))

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_id {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {A B : C} :

prodComparison (Functor.id C) A B = CategoryStruct.id (MonoidalCategoryStruct.tensorObj A B)

def CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A : C) :

((MonoidalCategory.curriedTensor C).obj A).comp F ⟶ F.comp ((MonoidalCategory.curriedTensor D).obj (F.obj A))

The product comparison morphism from F(A ⊗ -) to FA ⊗ F-, whose components are given by prodComparison.

Equations

CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans F A = { app := fun (B : C) => CategoryTheory.ChosenFiniteProducts.prodComparison F A B, naturality := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans_app {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A B : C) :

(prodComparisonNatTrans F A).app B = prodComparison F A B

theorem CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans_comp {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) {A : C} {E : Type u₂} [Category.{v₂, u₂} E] [ChosenFiniteProducts E] (G : Functor D E) :

prodComparisonNatTrans (F.comp G) A = CategoryStruct.comp (whiskerRight (prodComparisonNatTrans F A) G) (whiskerLeft F (prodComparisonNatTrans G (F.obj A)))

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans_id {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {A : C} :

prodComparisonNatTrans (Functor.id C) A = CategoryStruct.id (((MonoidalCategory.curriedTensor C).obj A).comp (Functor.id C))

def CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatTrans {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) :

(MonoidalCategory.curriedTensor C).comp ((whiskeringRight C C D).obj F) ⟶ F.comp ((MonoidalCategory.curriedTensor D).comp ((whiskeringLeft C D D).obj F))

The product comparison morphism from F(- ⊗ -) to F- ⊗ F-, whose components are given by prodComparison.

Equations

CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatTrans F = { app := fun (A : C) => CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans F A, naturality := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatTrans_app {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A : C) :

(prodComparisonBifunctorNatTrans F).app A = prodComparisonNatTrans F A

theorem CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatTrans_comp {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) {E : Type u₂} [Category.{v₂, u₂} E] [ChosenFiniteProducts E] (G : Functor D E) :

prodComparisonBifunctorNatTrans (F.comp G) = CategoryStruct.comp (whiskerRight (prodComparisonBifunctorNatTrans F) ((whiskeringRight C D E).obj G)) (whiskerLeft F (whiskerRight (prodComparisonBifunctorNatTrans G) ((whiskeringLeft C D E).obj F)))

instance CategoryTheory.ChosenFiniteProducts.instIsIsoFunctorProdComparisonNatTransOfProdComparison {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A : C) [∀ (B : C), IsIso (prodComparison F A B)] :

IsIso (prodComparisonNatTrans F A)

instance CategoryTheory.ChosenFiniteProducts.instIsIsoFunctorProdComparisonBifunctorNatTransOfProdComparison {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) [∀ (A B : C), IsIso (prodComparison F A B)] :

IsIso (prodComparisonBifunctorNatTrans F)

noncomputable def CategoryTheory.ChosenFiniteProducts.isLimitChosenFiniteProductsOfPreservesLimits {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C D) (A B : C) [Limits.PreservesLimit (Limits.pair A B) F] :

Limits.IsLimit (Limits.BinaryFan.mk (F.map (fst A B)) (F.map (snd A B)))

If F preserves the limit of the pair (A, B), then the binary fan given by (F.map fst A B, F.map (snd A B)) is a limit cone.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def CategoryTheory.ChosenFiniteProducts.prodComparisonIso {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A B : C) [Limits.PreservesLimit (Limits.pair A B) F] :

F.obj (MonoidalCategoryStruct.tensorObj A B) ≅ MonoidalCategoryStruct.tensorObj (F.obj A) (F.obj B)

If F preserves the limit of the pair (A, B), then prodComparison F A B is an isomorphism.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparisonIso_hom {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A B : C) [Limits.PreservesLimit (Limits.pair A B) F] :

(prodComparisonIso F A B).hom = prodComparison F A B

instance CategoryTheory.ChosenFiniteProducts.isIso_prodComparison_of_preservesLimit_pair {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A B : C) [Limits.PreservesLimit (Limits.pair A B) F] :

IsIso (prodComparison F A B)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparisonIso_id {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (A B : C) :

prodComparisonIso (Functor.id C) A B = Iso.refl ((Functor.id C).obj (MonoidalCategoryStruct.tensorObj A B))

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparisonIso_comp {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A B : C) {E : Type u₂} [Category.{v₂, u₂} E] [ChosenFiniteProducts E] (G : Functor D E) [Limits.PreservesLimit (Limits.pair A B) F] [Limits.PreservesLimit (Limits.pair A B) (F.comp G)] [Limits.PreservesLimit (Limits.pair (F.obj A) (F.obj B)) G] :

prodComparisonIso (F.comp G) A B = G.mapIso (prodComparisonIso F A B) ≪≫ prodComparisonIso G (F.obj A) (F.obj B)

noncomputable def CategoryTheory.ChosenFiniteProducts.prodComparisonNatIso {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A : C) [∀ (B : C), Limits.PreservesLimit (Limits.pair A B) F] :

((MonoidalCategory.curriedTensor C).obj A).comp F ≅ F.comp ((MonoidalCategory.curriedTensor D).obj (F.obj A))

The natural isomorphism F(A ⊗ -) ≅ FA ⊗ F-, provided each prodComparison F A B is an isomorphism (as B changes).

Equations

CategoryTheory.ChosenFiniteProducts.prodComparisonNatIso F A = CategoryTheory.asIso (CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans F A)

Instances For

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparisonNatIso_inv {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A : C) [∀ (B : C), Limits.PreservesLimit (Limits.pair A B) F] :

(prodComparisonNatIso F A).inv = inv (prodComparisonNatTrans F A)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparisonNatIso_hom {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A : C) [∀ (B : C), Limits.PreservesLimit (Limits.pair A B) F] :

(prodComparisonNatIso F A).hom = prodComparisonNatTrans F A

noncomputable def CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatIso {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) [∀ (A B : C), Limits.PreservesLimit (Limits.pair A B) F] :

(MonoidalCategory.curriedTensor C).comp ((whiskeringRight C C D).obj F) ≅ F.comp ((MonoidalCategory.curriedTensor D).comp ((whiskeringLeft C D D).obj F))

The natural isomorphism of bifunctors F(- ⊗ -) ≅ F- ⊗ F-, provided each prodComparison F A B is an isomorphism.

Equations

CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatIso F = CategoryTheory.asIso (CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatTrans F)

Instances For

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatIso_inv {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) [∀ (A B : C), Limits.PreservesLimit (Limits.pair A B) F] :

(prodComparisonBifunctorNatIso F).inv = inv (prodComparisonBifunctorNatTrans F)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatIso_hom {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) [∀ (A B : C), Limits.PreservesLimit (Limits.pair A B) F] :

(prodComparisonBifunctorNatIso F).hom = prodComparisonBifunctorNatTrans F

theorem CategoryTheory.ChosenFiniteProducts.preservesLimit_pair_of_isIso_prodComparison {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A B : C) [IsIso (prodComparison F A B)] :

Limits.PreservesLimit (Limits.pair A B) F

If prodComparison F A B is an isomorphism, then F preserves the limit of pair A B.

theorem CategoryTheory.ChosenFiniteProducts.preservesLimitsOfShape_discrete_walkingPair_of_isIso_prodComparison {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) [∀ (A B : C), IsIso (prodComparison F A B)] :

Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F

If prodComparison F A B is an isomorphism for all A B then F preserves limits of shape Discrete (WalkingPair).

noncomputable def CategoryTheory.ChosenFiniteProducts.fullSubcategory {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {P : ObjectProperty C} (hP₀ : Limits.ClosedUnderLimitsOfShape (Discrete PEmpty.{1}) P) (hP₂ : Limits.ClosedUnderLimitsOfShape (Discrete Limits.WalkingPair) P) :

ChosenFiniteProducts P.FullSubcategory

The restriction of a cartesian-monoidal category along an object property that's closed under finite products is cartesian-monoidal.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem CategoryTheory.Functor.OplaxMonoidal.η_of_chosenFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.OplaxMonoidal] :

η F = ChosenFiniteProducts.terminalComparison F

theorem CategoryTheory.Functor.OplaxMonoidal.δ_of_chosenFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.OplaxMonoidal] (X Y : C) :

δ F X Y = ChosenFiniteProducts.prodComparison F X Y

instance CategoryTheory.Functor.OplaxMonoidal.instIsIsoη {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.OplaxMonoidal] [Limits.PreservesFiniteProducts F] :

instance CategoryTheory.Functor.OplaxMonoidal.instIsIsoδ {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.OplaxMonoidal] [Limits.PreservesFiniteProducts F] (X Y : C) :

IsIso (δ F X Y)

def CategoryTheory.Functor.OplaxMonoidal.ofChosenFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) :

F.OplaxMonoidal

Any functor between cartesian-monoidal categories is oplax monoidal.

This is not made an instance because it would create a diamond for the oplax monoidal structure on the identity and composition of functors.

Equations

One or more equations did not get rendered due to their size.

Instances For

instance CategoryTheory.Functor.OplaxMonoidal.instSubsingleton {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) :

Subsingleton F.OplaxMonoidal

Any functor between cartesian-monoidal categories is oplax monoidal in a unique way.

@[simp]

theorem CategoryTheory.Functor.Monoidal.toUnit_ε {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Monoidal] (X : C) :

CategoryStruct.comp (ChosenFiniteProducts.toUnit (F.obj X)) (LaxMonoidal.ε F) = F.map (ChosenFiniteProducts.toUnit X)

@[simp]

theorem CategoryTheory.Functor.Monoidal.toUnit_ε_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Monoidal] (X : C) {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ Z) :

CategoryStruct.comp (ChosenFiniteProducts.toUnit (F.obj X)) (CategoryStruct.comp (LaxMonoidal.ε F) h) = CategoryStruct.comp (F.map (ChosenFiniteProducts.toUnit X)) h

@[simp]

theorem CategoryTheory.Functor.Monoidal.δ_fst {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Monoidal] (X Y : C) :

CategoryStruct.comp (OplaxMonoidal.δ F X Y) (ChosenFiniteProducts.fst (F.obj X) (F.obj Y)) = F.map (ChosenFiniteProducts.fst X Y)

@[simp]

theorem CategoryTheory.Functor.Monoidal.δ_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Monoidal] (X Y : C) {Z : D} (h : F.obj X ⟶ Z) :

CategoryStruct.comp (OplaxMonoidal.δ F X Y) (CategoryStruct.comp (ChosenFiniteProducts.fst (F.obj X) (F.obj Y)) h) = CategoryStruct.comp (F.map (ChosenFiniteProducts.fst X Y)) h

@[simp]

theorem CategoryTheory.Functor.Monoidal.δ_snd {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Monoidal] (X Y : C) :

CategoryStruct.comp (OplaxMonoidal.δ F X Y) (ChosenFiniteProducts.snd (F.obj X) (F.obj Y)) = F.map (ChosenFiniteProducts.snd X Y)

@[simp]

theorem CategoryTheory.Functor.Monoidal.δ_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Monoidal] (X Y : C) {Z : D} (h : F.obj Y ⟶ Z) :

CategoryStruct.comp (OplaxMonoidal.δ F X Y) (CategoryStruct.comp (ChosenFiniteProducts.snd (F.obj X) (F.obj Y)) h) = CategoryStruct.comp (F.map (ChosenFiniteProducts.snd X Y)) h

@[simp]

theorem CategoryTheory.Functor.Monoidal.lift_δ {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) {X Y Z : C} [F.Monoidal] (f : X ⟶ Y) (g : X ⟶ Z) :

CategoryStruct.comp (F.map (ChosenFiniteProducts.lift f g)) (OplaxMonoidal.δ F Y Z) = ChosenFiniteProducts.lift (F.map f) (F.map g)

@[simp]

theorem CategoryTheory.Functor.Monoidal.lift_δ_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) {X Y Z : C} [F.Monoidal] (f : X ⟶ Y) (g : X ⟶ Z) {Z✝ : D} (h : MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj Z) ⟶ Z✝) :

CategoryStruct.comp (F.map (ChosenFiniteProducts.lift f g)) (CategoryStruct.comp (OplaxMonoidal.δ F Y Z) h) = CategoryStruct.comp (ChosenFiniteProducts.lift (F.map f) (F.map g)) h

@[simp]

theorem CategoryTheory.Functor.Monoidal.lift_μ {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) {X Y Z : C} [F.Monoidal] (f : X ⟶ Y) (g : X ⟶ Z) :

CategoryStruct.comp (ChosenFiniteProducts.lift (F.map f) (F.map g)) (LaxMonoidal.μ F Y Z) = F.map (ChosenFiniteProducts.lift f g)

@[simp]

theorem CategoryTheory.Functor.Monoidal.lift_μ_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) {X Y Z : C} [F.Monoidal] (f : X ⟶ Y) (g : X ⟶ Z) {Z✝ : D} (h : F.obj (MonoidalCategoryStruct.tensorObj Y Z) ⟶ Z✝) :

CategoryStruct.comp (ChosenFiniteProducts.lift (F.map f) (F.map g)) (CategoryStruct.comp (LaxMonoidal.μ F Y Z) h) = CategoryStruct.comp (F.map (ChosenFiniteProducts.lift f g)) h

@[simp]

theorem CategoryTheory.Functor.Monoidal.μ_fst {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Monoidal] (X Y : C) :

CategoryStruct.comp (LaxMonoidal.μ F X Y) (F.map (ChosenFiniteProducts.fst X Y)) = ChosenFiniteProducts.fst (F.obj X) (F.obj Y)

@[simp]

theorem CategoryTheory.Functor.Monoidal.μ_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Monoidal] (X Y : C) {Z : D} (h : F.obj X ⟶ Z) :

CategoryStruct.comp (LaxMonoidal.μ F X Y) (CategoryStruct.comp (F.map (ChosenFiniteProducts.fst X Y)) h) = CategoryStruct.comp (ChosenFiniteProducts.fst (F.obj X) (F.obj Y)) h

@[simp]

theorem CategoryTheory.Functor.Monoidal.μ_snd {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Monoidal] (X Y : C) :

CategoryStruct.comp (LaxMonoidal.μ F X Y) (F.map (ChosenFiniteProducts.snd X Y)) = ChosenFiniteProducts.snd (F.obj X) (F.obj Y)

@[simp]

theorem CategoryTheory.Functor.Monoidal.μ_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Monoidal] (X Y : C) {Z : D} (h : F.obj Y ⟶ Z) :

CategoryStruct.comp (LaxMonoidal.μ F X Y) (CategoryStruct.comp (F.map (ChosenFiniteProducts.snd X Y)) h) = CategoryStruct.comp (ChosenFiniteProducts.snd (F.obj X) (F.obj Y)) h

theorem CategoryTheory.Functor.Monoidal.μ_comp {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] {E : Type u₃} [Category.{v₃, u₃} E] [ChosenFiniteProducts E] (F : Functor C D) (G : Functor D E) [F.Monoidal] [G.Monoidal] [(F.comp G).Monoidal] (X Y : C) :

LaxMonoidal.μ (F.comp G) X Y = CategoryStruct.comp (LaxMonoidal.μ G (F.obj X) (F.obj Y)) (G.map (LaxMonoidal.μ F X Y))

theorem CategoryTheory.Functor.Monoidal.μ_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] {E : Type u₃} [Category.{v₃, u₃} E] [ChosenFiniteProducts E] (F : Functor C D) (G : Functor D E) [F.Monoidal] [G.Monoidal] [(F.comp G).Monoidal] (X Y : C) {Z : E} (h : G.obj (F.obj (MonoidalCategoryStruct.tensorObj X Y)) ⟶ Z) :

CategoryStruct.comp (LaxMonoidal.μ (F.comp G) X Y) h = CategoryStruct.comp (LaxMonoidal.μ G (F.obj X) (F.obj Y)) (CategoryStruct.comp (G.map (LaxMonoidal.μ F X Y)) h)

theorem CategoryTheory.Functor.Monoidal.ε_of_chosenFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Monoidal] [Limits.PreservesFiniteProducts F] :

LaxMonoidal.ε F = (ChosenFiniteProducts.preservesTerminalIso F).inv

theorem CategoryTheory.Functor.Monoidal.μ_of_chosenFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Monoidal] [Limits.PreservesFiniteProducts F] (X Y : C) :

LaxMonoidal.μ F X Y = (ChosenFiniteProducts.prodComparisonIso F X Y).inv

noncomputable def CategoryTheory.Functor.Monoidal.ofChosenFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [Limits.PreservesFiniteProducts F] :

A finite-product-preserving functor between cartesian monoidal categories is monoidal.

This is not made an instance because it would create a diamond for the monoidal structure on the identity and composition of functors.

Equations

CategoryTheory.Functor.Monoidal.ofChosenFiniteProducts F = CategoryTheory.Functor.Monoidal.ofOplaxMonoidal F

Instances For

instance CategoryTheory.Functor.Monoidal.instSubsingleton {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) :

Subsingleton F.Monoidal

instance CategoryTheory.Functor.Monoidal.instPreservesFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Monoidal] :

Limits.PreservesFiniteProducts F

theorem CategoryTheory.Functor.Monoidal.nonempty_monoidal_iff_preservesFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) :

Nonempty F.Monoidal ↔ Limits.PreservesFiniteProducts F

A functor between cartesian monoidal categories is monoidal iff it preserves finite products.

noncomputable def CategoryTheory.Functor.Braided.ofChosenFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [Limits.PreservesFiniteProducts F] :

A finite-product-preserving functor between cartesian monoidal categories is braided.

This is not made an instance because it would create a diamond for the braided structure on the identity and composition of functors.

Equations

CategoryTheory.Functor.Braided.ofChosenFiniteProducts F = { toMonoidal := CategoryTheory.Functor.Monoidal.ofChosenFiniteProducts F, braided := ⋯ }

Instances For

instance CategoryTheory.Functor.Braided.instSubsingleton {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) :

Subsingleton F.Braided

@[deprecated CategoryTheory.Functor.OplaxMonoidal.ofChosenFiniteProducts (since := "2025-04-24")]

def CategoryTheory.Functor.oplaxMonoidalOfChosenFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) :

F.OplaxMonoidal

Alias of CategoryTheory.Functor.OplaxMonoidal.ofChosenFiniteProducts.

Any functor between cartesian-monoidal categories is oplax monoidal.

This is not made an instance because it would create a diamond for the oplax monoidal structure on the identity and composition of functors.

Equations

@CategoryTheory.Functor.oplaxMonoidalOfChosenFiniteProducts = @CategoryTheory.Functor.OplaxMonoidal.ofChosenFiniteProducts

Instances For

@[deprecated CategoryTheory.Functor.Monoidal.ofChosenFiniteProducts (since := "2025-04-24")]

def CategoryTheory.Functor.monoidalOfChosenFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [Limits.PreservesFiniteProducts F] :

Alias of CategoryTheory.Functor.Monoidal.ofChosenFiniteProducts.

A finite-product-preserving functor between cartesian monoidal categories is monoidal.

This is not made an instance because it would create a diamond for the monoidal structure on the identity and composition of functors.

Equations

@CategoryTheory.Functor.monoidalOfChosenFiniteProducts = @CategoryTheory.Functor.Monoidal.ofChosenFiniteProducts

Instances For

@[deprecated CategoryTheory.Functor.Braided.ofChosenFiniteProducts (since := "2025-04-24")]

def CategoryTheory.Functor.braidedOfChosenFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [Limits.PreservesFiniteProducts F] :

Alias of CategoryTheory.Functor.Braided.ofChosenFiniteProducts.

A finite-product-preserving functor between cartesian monoidal categories is braided.

This is not made an instance because it would create a diamond for the braided structure on the identity and composition of functors.

Equations

@CategoryTheory.Functor.braidedOfChosenFiniteProducts = @CategoryTheory.Functor.Braided.ofChosenFiniteProducts

Instances For

noncomputable instance CategoryTheory.Functor.EssImageSubcategory.instChosenFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] :

ChosenFiniteProducts F.EssImageSubcategory

Equations

CategoryTheory.Functor.EssImageSubcategory.instChosenFiniteProducts F = CategoryTheory.ChosenFiniteProducts.fullSubcategory ⋯ ⋯

@[simp]

theorem CategoryTheory.Functor.EssImageSubcategory.instChosenFiniteProducts_terminal_isLimit {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] :

ChosenFiniteProducts.terminal.isLimit = Limits.IsTerminal.isTerminalOfObj F.essImage.ι { obj := MonoidalCategoryStruct.tensorUnit D, property := ⋯ } (Limits.IsTerminal.ofUnique (MonoidalCategoryStruct.tensorUnit D))

@[simp]

theorem CategoryTheory.Functor.EssImageSubcategory.instChosenFiniteProducts_terminal_cone_π_app {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] (X_1 : Discrete PEmpty.{1}) :

ChosenFiniteProducts.terminal.cone.π.app X_1 = ⋯.elim

@[simp]

theorem CategoryTheory.Functor.EssImageSubcategory.instChosenFiniteProducts_product_isLimit_lift {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] (X Y : F.essImage.FullSubcategory) (t : Limits.Cone (Limits.pair X Y)) :

(ChosenFiniteProducts.product X Y).isLimit.lift t = ChosenFiniteProducts.lift (Limits.BinaryFan.fst t) (Limits.BinaryFan.snd t)

@[simp]

theorem CategoryTheory.Functor.EssImageSubcategory.instChosenFiniteProducts_terminal_cone_pt_obj {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] :

ChosenFiniteProducts.terminal.cone.pt.obj = MonoidalCategoryStruct.tensorUnit D

@[simp]

theorem CategoryTheory.Functor.EssImageSubcategory.instChosenFiniteProducts_product_cone_π_app {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] (X Y : F.essImage.FullSubcategory) (x✝ : Discrete Limits.WalkingPair) :

(ChosenFiniteProducts.product X Y).cone.π.app x✝ = match x✝.as with | Limits.WalkingPair.left => ChosenFiniteProducts.fst X.obj Y.obj | Limits.WalkingPair.right => ChosenFiniteProducts.snd X.obj Y.obj

@[simp]

theorem CategoryTheory.Functor.EssImageSubcategory.instChosenFiniteProducts_product_cone_pt_obj {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] (X Y : F.essImage.FullSubcategory) :

(ChosenFiniteProducts.product X Y).cone.pt.obj = MonoidalCategoryStruct.tensorObj X.obj Y.obj

theorem CategoryTheory.Functor.EssImageSubcategory.tensor_obj {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] (X Y : F.EssImageSubcategory) :

(MonoidalCategoryStruct.tensorObj X Y).obj = MonoidalCategoryStruct.tensorObj X.obj Y.obj

theorem CategoryTheory.Functor.EssImageSubcategory.fst_def {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] (X Y : F.EssImageSubcategory) :

ChosenFiniteProducts.fst X Y = ChosenFiniteProducts.fst X.obj Y.obj

theorem CategoryTheory.Functor.EssImageSubcategory.snd_def {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] (X Y : F.EssImageSubcategory) :

ChosenFiniteProducts.snd X Y = ChosenFiniteProducts.snd X.obj Y.obj

theorem CategoryTheory.Functor.EssImageSubcategory.lift_def {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] {T X Y : F.EssImageSubcategory} (f : T ⟶ X) (g : T ⟶ Y) :

ChosenFiniteProducts.lift f g = ChosenFiniteProducts.lift f g

theorem CategoryTheory.Functor.EssImageSubcategory.whiskerLeft_def {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] {Y Z : F.EssImageSubcategory} (X : F.EssImageSubcategory) (f : Y ⟶ Z) :

MonoidalCategoryStruct.whiskerLeft X f = MonoidalCategoryStruct.whiskerLeft X.obj f

theorem CategoryTheory.Functor.EssImageSubcategory.whiskerRight_def {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] {Y Z : F.EssImageSubcategory} (f : Y ⟶ Z) (X : F.EssImageSubcategory) :

MonoidalCategoryStruct.whiskerRight f X = MonoidalCategoryStruct.whiskerRight f X.obj

theorem CategoryTheory.Functor.EssImageSubcategory.associator_hom_def {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] (X Y Z : F.EssImageSubcategory) :

(MonoidalCategoryStruct.associator X Y Z).hom = (MonoidalCategoryStruct.associator X.obj Y.obj Z.obj).hom

theorem CategoryTheory.Functor.EssImageSubcategory.associator_inv_def {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] (X Y Z : F.EssImageSubcategory) :

(MonoidalCategoryStruct.associator X Y Z).inv = (MonoidalCategoryStruct.associator X.obj Y.obj Z.obj).inv

theorem CategoryTheory.Functor.EssImageSubcategory.toUnit_def {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] (X : F.EssImageSubcategory) :

ChosenFiniteProducts.toUnit X = ChosenFiniteProducts.toUnit X.obj

instance CategoryTheory.NatTrans.isMonoidal_of_chosenFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F G : Functor C D) [F.Monoidal] [G.Monoidal] (α : F ⟶ G) :