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.

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

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

def CategoryTheory.ChosenFiniteProducts.lift {C : Type u} [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

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

@[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.leftUnitor_inv_fst {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] (X : C) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).inv (fst (𝟙_ 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 : 𝟙_ C ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).inv (CategoryStruct.comp (fst (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 (𝟙_ 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 : 𝟙_ C ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).inv (CategoryStruct.comp (snd X (𝟙_ C)) h) = CategoryStruct.comp (toUnit X) 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 (𝟙_ C) ⟶ 𝟙_ D

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

Equations

• CategoryTheory.ChosenFiniteProducts.terminalComparison F = CategoryTheory.ChosenFiniteProducts.toUnit (F.obj (𝟙_ C))

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.map_toUnit_comp_terminalCompariso {C : Type u} [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)

@[simp]

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 : 𝟙_ D ⟶ Z) : CategoryStruct.comp (F.map (toUnit A)) (CategoryStruct.comp (terminalComparison F) h) = CategoryStruct.comp (toUnit (F.obj A)) h

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 (𝟙_ C) ≅ 𝟙_ D

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

Equations

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

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.preservesTerminalIso_hom {C : Type u} [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)

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)

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_inv {C : Type u} [Category.{v, u} C] [ChosenFiniteProducts C] {D : Type u₁} [Category.{v₁, u₁} D] [ChosenFiniteProducts D] (F : Functor C D) (A : C) [∀ (B : C), Limits.PreservesLimit (Limits.pair A B) F] : (prodComparisonNatIso F A).inv = inv (prodComparisonNatTrans F A)

@[simp]

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

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

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

Equations

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

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

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

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

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.PreservesLimit (empty C) 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.PreservesLimitsOfShape (Discrete Limits.WalkingPair) 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.PreservesLimit (empty C) F] [Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F] : F.Monoidal

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

Equations

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