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 : X ⟶ 𝟙_ C) (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 : C} {X : C} {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 : C) (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 : C) (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_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {T : C} {X : C} {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_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {T : C} {X : C} {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_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {T : C} {X : C} {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

@[simp]

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

theorem CategoryTheory.ChosenFiniteProducts.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {T : C} {X : C} {Y : C} (f : T ⟶ CategoryTheory.MonoidalCategory.tensorObj X Y) (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.tensorHom_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {X₁ : C} {X₂ : C} {Y₁ : C} {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_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {X₁ : C} {X₂ : C} {Y₁ : C} {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_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {X₁ : C} {X₂ : C} {Y₁ : C} {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.tensorHom_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {X₁ : C} {X₂ : C} {Y₁ : C} {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.whiskerLeft_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) {Y₁ : C} {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_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) {Y₁ : C} {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_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) {Y₁ : C} {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.whiskerLeft_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) {Y₁ : C} {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.whiskerRight_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {X₁ : C} {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_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {X₁ : C} {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_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {X₁ : C} {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.whiskerRight_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {X₁ : C} {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.associator_hom_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) (Y : C) (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_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) (Y : C) (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_snd_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) (Y : C) (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_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) (Y : C) (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_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) (Y : C) (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_hom_snd_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) (Y : C) (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_inv_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) (Y : C) (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 {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) (Y : C) (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_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) (Y : C) (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_fst_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) (Y : C) (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_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) (Y : C) (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.associator_inv_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) (Y : C) (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)

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

• ⋯ = ⋯