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.

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) [CategoryTheory.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) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)

  A choice of a limit binary fan for any two objects of the category.

• terminal : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C)

  A choice of a terminal object.

@[instance 100]

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

Equations

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

@[instance 100]

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

Equations

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

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

The unique map to the terminal object.

Equations

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

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

Equations

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

theorem CategoryTheory.ChosenFiniteProducts.toUnit_unique {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {X : C} (f g : X ⟶ 𝟙_ 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.

def CategoryTheory.ChosenFiniteProducts.lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) : T ⟶ CategoryTheory.MonoidalCategory.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)

def CategoryTheory.ChosenFiniteProducts.fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X Y : C) : CategoryTheory.MonoidalCategory.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

def CategoryTheory.ChosenFiniteProducts.snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X Y : C) : CategoryTheory.MonoidalCategory.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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

@[simp]

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

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

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_fst_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {X Y : C} : CategoryTheory.ChosenFiniteProducts.lift (CategoryTheory.ChosenFiniteProducts.fst X Y) (CategoryTheory.ChosenFiniteProducts.snd X Y) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Y)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.lift_fst_comp_snd_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {W X Y Z : C} (g : W ⟶ X) (g' : Y ⟶ Z) : CategoryTheory.ChosenFiniteProducts.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst W Y) g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd W Y) g') = CategoryTheory.MonoidalCategory.tensorHom g g'

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_hom_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.ChosenFiniteProducts.fst X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (CategoryTheory.ChosenFiniteProducts.fst X Y)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_hom_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X Y Z : C) {Z✝ : C} (h : X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst X Y) h)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_hom_snd_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (CategoryTheory.ChosenFiniteProducts.fst Y Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (CategoryTheory.ChosenFiniteProducts.snd X Y)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_hom_snd_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X Y Z : C) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst Y Z) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X Y) h)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_hom_snd_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (CategoryTheory.ChosenFiniteProducts.snd Y Z)) = CategoryTheory.ChosenFiniteProducts.snd (CategoryTheory.MonoidalCategory.tensorObj X Y) Z

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_hom_snd_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X Y Z : C) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd Y Z) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_inv_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (CategoryTheory.ChosenFiniteProducts.fst X Y)) = CategoryTheory.ChosenFiniteProducts.fst X (CategoryTheory.MonoidalCategory.tensorObj Y Z)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_inv_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X Y Z : C) {Z✝ : C} (h : X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst X Y) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_inv_fst_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (CategoryTheory.ChosenFiniteProducts.snd X Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (CategoryTheory.ChosenFiniteProducts.fst Y Z)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_inv_fst_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X Y Z : C) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X Y) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst Y Z) h)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_inv_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.ChosenFiniteProducts.snd (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (CategoryTheory.ChosenFiniteProducts.snd Y Z)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.associator_inv_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X Y Z : C) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd Y Z) h)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.leftUnitor_inv_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).inv (CategoryTheory.ChosenFiniteProducts.fst (𝟙_ C) X) = CategoryTheory.ChosenFiniteProducts.toUnit X

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.leftUnitor_inv_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) {Z : C} (h : 𝟙_ C ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (𝟙_ C) X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.toUnit X) h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.leftUnitor_inv_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).inv (CategoryTheory.ChosenFiniteProducts.snd (𝟙_ C) X) = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.leftUnitor_inv_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd (𝟙_ C) X) h) = h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.rightUnitor_inv_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).inv (CategoryTheory.ChosenFiniteProducts.fst X (𝟙_ C)) = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.rightUnitor_inv_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst X (𝟙_ C)) h) = h

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.rightUnitor_inv_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).inv (CategoryTheory.ChosenFiniteProducts.snd X (𝟙_ C)) = CategoryTheory.ChosenFiniteProducts.toUnit X

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.rightUnitor_inv_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) {Z : C} (h : 𝟙_ C ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X (𝟙_ C)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.toUnit X) h

noncomputable def CategoryTheory.ChosenFiniteProducts.ofFiniteProducts (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] : CategoryTheory.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.

@[instance 100]

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

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev CategoryTheory.ChosenFiniteProducts.terminalComparison {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) : F.obj (𝟙_ C) ⟶ 𝟙_ 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 (𝟙_ C))

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.map_toUnit_comp_terminalCompariso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) (A : C) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ChosenFiniteProducts.toUnit A)) (CategoryTheory.ChosenFiniteProducts.terminalComparison F) = CategoryTheory.ChosenFiniteProducts.toUnit (F.obj A)

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.map_toUnit_comp_terminalCompariso_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) (A : C) {Z : D} (h : 𝟙_ D ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ChosenFiniteProducts.toUnit A)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.terminalComparison F) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.toUnit (F.obj A)) h

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

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

noncomputable def CategoryTheory.ChosenFiniteProducts.preservesTerminalIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) [h : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F] : F.obj (𝟙_ C) ≅ 𝟙_ 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.

@[simp]

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

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

Equations

• ⋯ = ⋯

def CategoryTheory.ChosenFiniteProducts.prodComparison {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) (A B : C) : F.obj (CategoryTheory.MonoidalCategory.tensorObj A B) ⟶ CategoryTheory.MonoidalCategory.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.

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) (A B : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A B) (CategoryTheory.ChosenFiniteProducts.fst (F.obj A) (F.obj B)) = F.map (CategoryTheory.ChosenFiniteProducts.fst A B)

@[simp]

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

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) (A B : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A B) (CategoryTheory.ChosenFiniteProducts.snd (F.obj A) (F.obj B)) = F.map (CategoryTheory.ChosenFiniteProducts.snd A B)

@[simp]

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

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.inv_prodComparison_map_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) (A B : C) [CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)) (F.map (CategoryTheory.ChosenFiniteProducts.fst A B)) = CategoryTheory.ChosenFiniteProducts.fst (F.obj A) (F.obj B)

@[simp]

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

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.inv_prodComparison_map_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) (A B : C) [CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)) (F.map (CategoryTheory.ChosenFiniteProducts.snd A B)) = CategoryTheory.ChosenFiniteProducts.snd (F.obj A) (F.obj B)

@[simp]

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

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

Naturality of the prodComparison morphism in both arguments.

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

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_natural_whiskerLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) {A B B' : C} (g : B ⟶ B') : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.whiskerLeft A g)) (CategoryTheory.ChosenFiniteProducts.prodComparison F A B') = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A B) (CategoryTheory.MonoidalCategory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) {A B B' : C} (g : B ⟶ B') {Z : D} (h : CategoryTheory.MonoidalCategory.tensorObj (F.obj A) (F.obj B') ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.whiskerLeft A g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A B') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A B) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj A) (F.map g)) h)

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_natural_whiskerRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) {A B A' : C} (f : A ⟶ A') : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.whiskerRight f B)) (CategoryTheory.ChosenFiniteProducts.prodComparison F A' B) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A B) (CategoryTheory.MonoidalCategory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) {A B A' : C} (f : A ⟶ A') {Z : D} (h : CategoryTheory.MonoidalCategory.tensorObj (F.obj A') (F.obj B) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.whiskerRight f B)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A' B) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A B) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.map f) (F.obj B)) h)

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_inv_natural {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) {A B A' B' : C} [CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)] (f : A ⟶ A') (g : B ⟶ B') [CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A' B')] : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)) (F.map (CategoryTheory.MonoidalCategory.tensorHom f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g)) (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) {A B A' B' : C} [CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)] (f : A ⟶ A') (g : B ⟶ B') [CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A' B')] {Z : D} (h : F.obj (CategoryTheory.MonoidalCategory.tensorObj A' B') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)) (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.tensorHom f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A' B')) h)

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_inv_natural_whiskerLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) {A B B' : C} [CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)] (g : B ⟶ B') [CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B')] : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)) (F.map (CategoryTheory.MonoidalCategory.whiskerLeft A g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj A) (F.map g)) (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) {A B B' : C} [CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)] (g : B ⟶ B') [CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B')] {Z : D} (h : F.obj (CategoryTheory.MonoidalCategory.tensorObj A B') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)) (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.whiskerLeft A g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj A) (F.map g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B')) h)

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_inv_natural_whiskerRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) {A B A' : C} [CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)] (f : A ⟶ A') [CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A' B)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)) (F.map (CategoryTheory.MonoidalCategory.whiskerRight f B)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.map f) (F.obj B)) (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) {A B A' : C} [CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)] (f : A ⟶ A') [CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A' B)] {Z : D} (h : F.obj (CategoryTheory.MonoidalCategory.tensorObj A' B) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)) (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.whiskerRight f B)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.map f) (F.obj B)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A' B)) h)

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

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparison_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {A B : C} : CategoryTheory.ChosenFiniteProducts.prodComparison (CategoryTheory.Functor.id C) A B = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj A B)

def CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) (A : C) : ((CategoryTheory.MonoidalCategory.curriedTensor C).obj A).comp F ⟶ F.comp ((CategoryTheory.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 := ⋯ }

@[simp]

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

theorem CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) {A : C} {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] [CategoryTheory.ChosenFiniteProducts E] (G : CategoryTheory.Functor D E) : CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans (F.comp G) A = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans F A) G) (CategoryTheory.whiskerLeft F (CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans G (F.obj A)))

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {A : C} : CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans (CategoryTheory.Functor.id C) A = CategoryTheory.CategoryStruct.id (((CategoryTheory.MonoidalCategory.curriedTensor C).obj A).comp (CategoryTheory.Functor.id C))

def CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatTrans {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) : (CategoryTheory.MonoidalCategory.curriedTensor C).comp ((CategoryTheory.whiskeringRight C C D).obj F) ⟶ F.comp ((CategoryTheory.MonoidalCategory.curriedTensor D).comp ((CategoryTheory.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 := ⋯ }

@[simp]

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

theorem CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatTrans_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] [CategoryTheory.ChosenFiniteProducts E] (G : CategoryTheory.Functor D E) : CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatTrans (F.comp G) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatTrans F) ((CategoryTheory.whiskeringRight C D E).obj G)) (CategoryTheory.whiskerLeft F (CategoryTheory.whiskerRight (CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatTrans G) ((CategoryTheory.whiskeringLeft C D E).obj F)))

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.ChosenFiniteProducts.isLimitChosenFiniteProductsOfPreservesLimits {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C D) (A B : C) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk (F.map (CategoryTheory.ChosenFiniteProducts.fst A B)) (F.map (CategoryTheory.ChosenFiniteProducts.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.

noncomputable def CategoryTheory.ChosenFiniteProducts.prodComparisonIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) (A B : C) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F] : F.obj (CategoryTheory.MonoidalCategory.tensorObj A B) ≅ CategoryTheory.MonoidalCategory.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.

@[simp]

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

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

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.ChosenFiniteProducts.prodComparisonNatIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) (A : C) [∀ (B : C), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F] : ((CategoryTheory.MonoidalCategory.curriedTensor C).obj A).comp F ≅ F.comp ((CategoryTheory.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)

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) [∀ (A B : C), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F] : (CategoryTheory.MonoidalCategory.curriedTensor C).comp ((CategoryTheory.whiskeringRight C C D).obj F) ≅ F.comp ((CategoryTheory.MonoidalCategory.curriedTensor D).comp ((CategoryTheory.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)

@[simp]

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

@[simp]

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

theorem CategoryTheory.ChosenFiniteProducts.preservesLimit_pair_of_isIso_prodComparison {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) (A B : C) [CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) [∀ (A B : C), CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F

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

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

Any functor between categories with chosen finite products induces an oplax monoial functor.

Equations

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

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

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

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

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.instIsIsoδ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] (A B : C) : CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.δ F A B)

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Functor.monoidalOfChosenFiniteProducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.ChosenFiniteProducts D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] : F.Monoidal

If F : C ⥤ D is a functor between categories with chosen finite products that preserves finite products, then it is a monoidal functor.

Equations

• F.monoidalOfChosenFiniteProducts = CategoryTheory.Functor.Monoidal.ofOplaxMonoidal F