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) [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.

@[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.

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)

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

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

@[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✝

@[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

@[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.

@[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))

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.

@[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.

@[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 := ⋯ }

@[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 := ⋯ }

@[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.

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.

@[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)

@[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

@[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)

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)

@[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 : C → Prop} (hP₀ : Limits.ClosedUnderLimitsOfShape (Discrete PEmpty.{1}) P) (hP₂ : Limits.ClosedUnderLimitsOfShape (Discrete Limits.WalkingPair) P) : ChosenFiniteProducts (FullSubcategory P)

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.

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

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} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) : OplaxMonoidal.η F = ChosenFiniteProducts.terminalComparison F

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

instance CategoryTheory.Functor.instIsIsoη {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] : IsIso (OplaxMonoidal.η F)

instance CategoryTheory.Functor.instIsIsoδ {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 B : C) : IsIso (OplaxMonoidal.δ F A B)

noncomputable 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] : 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

@[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) (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) (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) (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) (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 : 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 : 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

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) [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) [Limits.PreservesFiniteProducts F] (X Y : C) : LaxMonoidal.μ F X Y = (ChosenFiniteProducts.prodComparisonIso F X Y).inv

@[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) [Limits.PreservesFiniteProducts F] {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) [Limits.PreservesFiniteProducts F] {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.lift_μ {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] {X Y Z : C} (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) [Limits.PreservesFiniteProducts F] {X Y Z : C} (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) [Limits.PreservesFiniteProducts F] (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) [Limits.PreservesFiniteProducts F] (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) [Limits.PreservesFiniteProducts F] (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) [Limits.PreservesFiniteProducts F] (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] {F : Functor C D} [Limits.PreservesFiniteProducts F] {E : Type u₂} [Category.{v₂, u₂} E] [ChosenFiniteProducts E] {G : Functor D E} [Limits.PreservesFiniteProducts G] (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] {F : Functor C D} [Limits.PreservesFiniteProducts F] {E : Type u₂} [Category.{v₂, u₂} E] [ChosenFiniteProducts E] {G : Functor D E} [Limits.PreservesFiniteProducts G] (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)

noncomputable 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] : F.Braided

A finite-product-preserving functor between categories with chosen finite products is braided.

Equations

• F.braidedOfChosenFiniteProducts = { toMonoidal := F.monoidalOfChosenFiniteProducts, braided := ⋯ }

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) [Limits.PreservesFiniteProducts F] [F.Full] [F.Faithful] : ChosenFiniteProducts F.EssImageSubcategory

Equations

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

@[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) [Limits.PreservesFiniteProducts F] [F.Full] [F.Faithful] (X Y : FullSubcategory F.essImage) (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_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) [Limits.PreservesFiniteProducts F] [F.Full] [F.Faithful] : ChosenFiniteProducts.terminal.cone.pt.obj = MonoidalCategoryStruct.tensorUnit D

@[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) [Limits.PreservesFiniteProducts F] [F.Full] [F.Faithful] (X Y : FullSubcategory F.essImage) (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_π_app {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] [F.Full] [F.Faithful] (X_1 : Discrete PEmpty.{1}) : ChosenFiniteProducts.terminal.cone.π.app X_1 = ⋯.elim

@[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) [Limits.PreservesFiniteProducts F] [F.Full] [F.Faithful] : ChosenFiniteProducts.terminal.isLimit = Limits.IsTerminal.isTerminalOfObj (fullSubcategoryInclusion F.essImage) { obj := MonoidalCategoryStruct.tensorUnit D, property := ⋯ } (Limits.IsTerminal.ofUnique (MonoidalCategoryStruct.tensorUnit D))

@[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) [Limits.PreservesFiniteProducts F] [F.Full] [F.Faithful] (X Y : FullSubcategory F.essImage) : (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) [Limits.PreservesFiniteProducts F] [F.Full] [F.Faithful] (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) [Limits.PreservesFiniteProducts F] [F.Full] [F.Faithful] (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) [Limits.PreservesFiniteProducts F] [F.Full] [F.Faithful] (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) [Limits.PreservesFiniteProducts F] [F.Full] [F.Faithful] {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) [Limits.PreservesFiniteProducts F] [F.Full] [F.Faithful] {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) [Limits.PreservesFiniteProducts F] [F.Full] [F.Faithful] {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) [Limits.PreservesFiniteProducts F] [F.Full] [F.Faithful] (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) [Limits.PreservesFiniteProducts F] [F.Full] [F.Faithful] (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) [Limits.PreservesFiniteProducts F] [F.Full] [F.Faithful] (X : F.EssImageSubcategory) : ChosenFiniteProducts.toUnit X = ChosenFiniteProducts.toUnit X.obj

instance CategoryTheory.NatTrans.monoidal_of_preservesFiniteProducts {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F G : Functor C D) [Limits.PreservesFiniteProducts F] [Limits.PreservesFiniteProducts G] (α : F ⟶ G) : IsMonoidal α