Categories with chosen finite products #
We introduce a class, ChosenFiniteProducts, which bundles explicit choices
for a terminal object and binary products in a category C.
This is primarily useful for categories which have finite products with good
definitional properties, such as the category of types.
Given a category with such an instance, we also provide the associated
symmetric monoidal structure so that one can write X ⊗ Y for the explicit
binary product and 𝟙_ C for the explicit terminal object.
Projects #
- Construct an instance of chosen finite products in the category of affine scheme, using the tensor product.
- Construct chosen finite products in other categories appearing "in nature".
class
CategoryTheory.ChosenFiniteProducts
(C : Type u)
[CategoryTheory.Category.{v, u} C]
:
Type (max u v)
An instance of ChosenFiniteProducts C bundles an explicit choice of a binary
product of two objects of C, and a terminal object in C.
Users should use the monoidal notation: X ⊗ Y for the product and 𝟙_ C for
the terminal object.
- product : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)
A choice of a limit binary fan for any two objects of the category.
- terminal : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C)
A choice of a terminal object.
Instances
@[instance 100]
instance
CategoryTheory.ChosenFiniteProducts.instMonoidalCategory
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
:
Equations
- One or more equations did not get rendered due to their size.
@[instance 100]
instance
CategoryTheory.ChosenFiniteProducts.instSymmetricCategory
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
:
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.ChosenFiniteProducts.toUnit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
:
X ⟶ 𝟙_ C
The unique map to the terminal object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.ChosenFiniteProducts.instUniqueHomTensorUnit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
:
Equations
- CategoryTheory.ChosenFiniteProducts.instUniqueHomTensorUnit X = { default := CategoryTheory.ChosenFiniteProducts.toUnit X, uniq := ⋯ }
theorem
CategoryTheory.ChosenFiniteProducts.toUnit_unique
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{X : C}
(f : X ⟶ 𝟙_ C)
(g : X ⟶ 𝟙_ C)
:
f = g
This lemma follows from the preexisting Unique instance, but
it is often convenient to use it directly as apply toUnit_unique forcing
lean to do the necessary elaboration.
def
CategoryTheory.ChosenFiniteProducts.lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{T : C}
{X : C}
{Y : C}
(f : T ⟶ X)
(g : T ⟶ Y)
:
Construct a morphism to the product given its two components.
Equations
- CategoryTheory.ChosenFiniteProducts.lift f g = (CategoryTheory.ChosenFiniteProducts.product X Y).isLimit.lift (CategoryTheory.Limits.BinaryFan.mk f g)
Instances For
def
CategoryTheory.ChosenFiniteProducts.fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
(Y : C)
:
The first projection from the product.
Equations
Instances For
def
CategoryTheory.ChosenFiniteProducts.snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
(Y : C)
:
The second projection from the product.
Equations
Instances For
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.lift_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{T : C}
{X : C}
{Y : C}
(f : T ⟶ X)
(g : T ⟶ Y)
{Z : C}
(h : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.lift_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{T : C}
{X : C}
{Y : C}
(f : T ⟶ X)
(g : T ⟶ Y)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.lift_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{T : C}
{X : C}
{Y : C}
(f : T ⟶ X)
(g : T ⟶ Y)
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.lift_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{T : C}
{X : C}
{Y : C}
(f : T ⟶ X)
(g : T ⟶ Y)
:
instance
CategoryTheory.ChosenFiniteProducts.mono_lift_of_mono_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{W : C}
{X : C}
{Y : C}
(f : W ⟶ X)
(g : W ⟶ Y)
[CategoryTheory.Mono f]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.ChosenFiniteProducts.mono_lift_of_mono_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{W : C}
{X : C}
{Y : C}
(f : W ⟶ X)
(g : W ⟶ Y)
[CategoryTheory.Mono g]
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.ChosenFiniteProducts.hom_ext_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{T : C}
{X : C}
{Y : C}
{f : T ⟶ CategoryTheory.MonoidalCategory.tensorObj X Y}
{g : T ⟶ CategoryTheory.MonoidalCategory.tensorObj X Y}
:
f = g ↔ CategoryTheory.CategoryStruct.comp f (CategoryTheory.ChosenFiniteProducts.fst X Y) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.ChosenFiniteProducts.fst X Y) ∧ CategoryTheory.CategoryStruct.comp f (CategoryTheory.ChosenFiniteProducts.snd X Y) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.ChosenFiniteProducts.snd X Y)
theorem
CategoryTheory.ChosenFiniteProducts.hom_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{T : C}
{X : C}
{Y : C}
(f : T ⟶ CategoryTheory.MonoidalCategory.tensorObj X Y)
(g : T ⟶ CategoryTheory.MonoidalCategory.tensorObj X Y)
(h_fst : CategoryTheory.CategoryStruct.comp f (CategoryTheory.ChosenFiniteProducts.fst X Y) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.ChosenFiniteProducts.fst X Y))
(h_snd : CategoryTheory.CategoryStruct.comp f (CategoryTheory.ChosenFiniteProducts.snd X Y) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.ChosenFiniteProducts.snd X Y))
:
f = g
theorem
CategoryTheory.ChosenFiniteProducts.comp_lift_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{V : C}
{W : C}
{X : C}
{Y : C}
(f : V ⟶ W)
(g : W ⟶ X)
(h : W ⟶ Y)
{Z : C}
(h : CategoryTheory.MonoidalCategory.tensorObj X Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.comp_lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{V : C}
{W : C}
{X : C}
{Y : C}
(f : V ⟶ W)
(g : W ⟶ X)
(h : W ⟶ Y)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.lift_fst_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{X : C}
{Y : C}
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.tensorHom_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{X₁ : C}
{X₂ : C}
{Y₁ : C}
{Y₂ : C}
(f : X₁ ⟶ X₂)
(g : Y₁ ⟶ Y₂)
{Z : C}
(h : X₂ ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.tensorHom_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{X₁ : C}
{X₂ : C}
{Y₁ : C}
{Y₂ : C}
(f : X₁ ⟶ X₂)
(g : Y₁ ⟶ Y₂)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.tensorHom_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{X₁ : C}
{X₂ : C}
{Y₁ : C}
{Y₂ : C}
(f : X₁ ⟶ X₂)
(g : Y₁ ⟶ Y₂)
{Z : C}
(h : Y₂ ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.tensorHom_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{X₁ : C}
{X₂ : C}
{Y₁ : C}
{Y₂ : C}
(f : X₁ ⟶ X₂)
(g : Y₁ ⟶ Y₂)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.lift_map_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{V : C}
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : V ⟶ W)
(g : V ⟶ X)
(h : W ⟶ Y)
(k : X ⟶ Z✝)
{Z : C}
(h : CategoryTheory.MonoidalCategory.tensorObj Y Z✝ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.lift f g)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom h✝ k) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.lift (CategoryTheory.CategoryStruct.comp f h✝)
(CategoryTheory.CategoryStruct.comp g k))
h
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.lift_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{V : C}
{W : C}
{X : C}
{Y : C}
{Z : C}
(f : V ⟶ W)
(g : V ⟶ X)
(h : W ⟶ Y)
(k : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.lift_fst_comp_snd_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{W : C}
{X : C}
{Y : C}
{Z : C}
(g : W ⟶ X)
(g' : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.whiskerLeft_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
{Y₁ : C}
{Y₂ : C}
(g : Y₁ ⟶ Y₂)
{Z : C}
(h : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.whiskerLeft_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
{Y₁ : C}
{Y₂ : C}
(g : Y₁ ⟶ Y₂)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.whiskerLeft_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
{Y₁ : C}
{Y₂ : C}
(g : Y₁ ⟶ Y₂)
{Z : C}
(h : Y₂ ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.whiskerLeft_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
{Y₁ : C}
{Y₂ : C}
(g : Y₁ ⟶ Y₂)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.whiskerRight_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{X₁ : C}
{X₂ : C}
(f : X₁ ⟶ X₂)
(Y : C)
{Z : C}
(h : X₂ ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.whiskerRight_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{X₁ : C}
{X₂ : C}
(f : X₁ ⟶ X₂)
(Y : C)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.whiskerRight_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{X₁ : C}
{X₂ : C}
(f : X₁ ⟶ X₂)
(Y : C)
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.whiskerRight_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{X₁ : C}
{X₂ : C}
(f : X₁ ⟶ X₂)
(Y : C)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.associator_hom_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
(Y : C)
(Z : C)
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z✝).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.fst X (CategoryTheory.MonoidalCategory.tensorObj Y Z✝)) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z✝)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst X Y) h)
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.associator_hom_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
(Y : C)
(Z : C)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom
(CategoryTheory.ChosenFiniteProducts.fst X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z)
(CategoryTheory.ChosenFiniteProducts.fst X Y)
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.associator_hom_snd_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
(Y : C)
(Z : C)
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z✝).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z✝))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst Y Z✝) h)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z✝)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X Y) h)
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.associator_hom_snd_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
(Y : C)
(Z : C)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z))
(CategoryTheory.ChosenFiniteProducts.fst Y Z)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z)
(CategoryTheory.ChosenFiniteProducts.snd X Y)
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.associator_hom_snd_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
(Y : C)
(Z : C)
{Z : C}
(h : Z✝ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z✝).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z✝))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd Y Z✝) h)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.snd (CategoryTheory.MonoidalCategory.tensorObj X Y) Z✝) h
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.associator_hom_snd_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
(Y : C)
(Z : C)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z))
(CategoryTheory.ChosenFiniteProducts.snd Y Z)) = CategoryTheory.ChosenFiniteProducts.snd (CategoryTheory.MonoidalCategory.tensorObj X Y) Z
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.associator_inv_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
(Y : C)
(Z : C)
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z✝).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z✝)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst X Y) h)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.fst X (CategoryTheory.MonoidalCategory.tensorObj Y Z✝)) h
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.associator_inv_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
(Y : C)
(Z : C)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z)
(CategoryTheory.ChosenFiniteProducts.fst X Y)) = CategoryTheory.ChosenFiniteProducts.fst X (CategoryTheory.MonoidalCategory.tensorObj Y Z)
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.associator_inv_fst_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
(Y : C)
(Z : C)
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z✝).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z✝)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X Y) h)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z✝))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst Y Z✝) h)
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.associator_inv_fst_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
(Y : C)
(Z : C)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z)
(CategoryTheory.ChosenFiniteProducts.snd X Y)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z))
(CategoryTheory.ChosenFiniteProducts.fst Y Z)
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.associator_inv_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
(Y : C)
(Z : C)
{Z : C}
(h : Z✝ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z✝).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.snd (CategoryTheory.MonoidalCategory.tensorObj X Y) Z✝) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z✝))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd Y Z✝) h)
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.associator_inv_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
(Y : C)
(Z : C)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv
(CategoryTheory.ChosenFiniteProducts.snd (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z))
(CategoryTheory.ChosenFiniteProducts.snd Y Z)
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.leftUnitor_inv_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
{Z : C}
(h : 𝟙_ C ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.leftUnitor_inv_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.leftUnitor_inv_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
{Z : C}
(h : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.leftUnitor_inv_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.rightUnitor_inv_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
{Z : C}
(h : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.rightUnitor_inv_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.rightUnitor_inv_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
{Z : C}
(h : 𝟙_ C ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.rightUnitor_inv_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
(X : C)
:
noncomputable def
CategoryTheory.ChosenFiniteProducts.ofFiniteProducts
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasFiniteProducts C]
:
Construct an instance of ChosenFiniteProducts C given an instance of HasFiniteProducts C.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[instance 100]
instance
CategoryTheory.ChosenFiniteProducts.instHasFiniteProducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
:
Equations
- ⋯ = ⋯
@[reducible, inline]
abbrev
CategoryTheory.ChosenFiniteProducts.terminalComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
:
F.obj (𝟙_ C) ⟶ 𝟙_ D
When C and D have chosen finite products and F : C ⥤ D is any functor,
terminalComparison F is the unique map F (𝟙_ C) ⟶ 𝟙_ D.
Equations
Instances For
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.map_toUnit_comp_terminalCompariso_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
{Z : D}
(h : 𝟙_ D ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.map_toUnit_comp_terminalCompariso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
:
noncomputable def
CategoryTheory.ChosenFiniteProducts.preservesLimitEmptyOfIsIsoTerminalComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.terminalComparison F)]
:
If terminalComparison F is an Iso, then F preserves terminal objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.ChosenFiniteProducts.preservesTerminalIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
[h : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F]
:
F.obj (𝟙_ C) ≅ 𝟙_ D
If F preserves terminal objects, then terminalComparison F is an isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.preservesTerminalIso_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F]
:
instance
CategoryTheory.ChosenFiniteProducts.terminalComparison_isIso_of_preservesLimits
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.ChosenFiniteProducts.prodComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
(B : C)
:
F.obj (CategoryTheory.MonoidalCategory.tensorObj A B) ⟶ CategoryTheory.MonoidalCategory.tensorObj (F.obj A) (F.obj B)
When C and D have chosen finite products and F : C ⥤ D is any functor,
prodComparison F A B is the canonical comparison morphism from F (A ⊗ B) to F(A) ⊗ F(B).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.prodComparison_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
(B : C)
{Z : D}
(h : F.obj A ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.prodComparison_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
(B : C)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)
(CategoryTheory.ChosenFiniteProducts.fst (F.obj A) (F.obj B)) = F.map (CategoryTheory.ChosenFiniteProducts.fst A B)
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.prodComparison_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
(B : C)
{Z : D}
(h : F.obj B ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.prodComparison_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
(B : C)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)
(CategoryTheory.ChosenFiniteProducts.snd (F.obj A) (F.obj B)) = F.map (CategoryTheory.ChosenFiniteProducts.snd A B)
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.inv_prodComparison_map_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
(B : C)
[CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)]
{Z : D}
(h : F.obj A ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B))
(CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ChosenFiniteProducts.fst A B)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (F.obj A) (F.obj B)) h
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.inv_prodComparison_map_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
(B : C)
[CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B))
(F.map (CategoryTheory.ChosenFiniteProducts.fst A B)) = CategoryTheory.ChosenFiniteProducts.fst (F.obj A) (F.obj B)
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.inv_prodComparison_map_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
(B : C)
[CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)]
{Z : D}
(h : F.obj B ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B))
(CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ChosenFiniteProducts.snd A B)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd (F.obj A) (F.obj B)) h
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.inv_prodComparison_map_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
(B : C)
[CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B))
(F.map (CategoryTheory.ChosenFiniteProducts.snd A B)) = CategoryTheory.ChosenFiniteProducts.snd (F.obj A) (F.obj B)
theorem
CategoryTheory.ChosenFiniteProducts.prodComparison_natural_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
{A : C}
{B : C}
{A' : C}
{B' : C}
(f : A ⟶ A')
(g : B ⟶ B')
{Z : D}
(h : CategoryTheory.MonoidalCategory.tensorObj (F.obj A') (F.obj B') ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.tensorHom f g))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A' B') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g)) h)
theorem
CategoryTheory.ChosenFiniteProducts.prodComparison_natural
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
{A : C}
{B : C}
{A' : C}
{B' : C}
(f : A ⟶ A')
(g : B ⟶ B')
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.tensorHom f g))
(CategoryTheory.ChosenFiniteProducts.prodComparison F A' B') = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)
(CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g))
Naturality of the prodComparison morphism in both arguments.
theorem
CategoryTheory.ChosenFiniteProducts.prodComparison_natural_whiskerLeft_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
{A : C}
{B : C}
{B' : C}
(g : B ⟶ B')
{Z : D}
(h : CategoryTheory.MonoidalCategory.tensorObj (F.obj A) (F.obj B') ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.whiskerLeft A g))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A B') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj A) (F.map g)) h)
theorem
CategoryTheory.ChosenFiniteProducts.prodComparison_natural_whiskerLeft
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
{A : C}
{B : C}
{B' : C}
(g : B ⟶ B')
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.whiskerLeft A g))
(CategoryTheory.ChosenFiniteProducts.prodComparison F A B') = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)
(CategoryTheory.MonoidalCategory.whiskerLeft (F.obj A) (F.map g))
Naturality of the prodComparison morphism in the right argument.
theorem
CategoryTheory.ChosenFiniteProducts.prodComparison_natural_whiskerRight_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
{A : C}
{B : C}
{A' : C}
(f : A ⟶ A')
{Z : D}
(h : CategoryTheory.MonoidalCategory.tensorObj (F.obj A') (F.obj B) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.whiskerRight f B))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A' B) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.map f) (F.obj B)) h)
theorem
CategoryTheory.ChosenFiniteProducts.prodComparison_natural_whiskerRight
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
{A : C}
{B : C}
{A' : C}
(f : A ⟶ A')
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.whiskerRight f B))
(CategoryTheory.ChosenFiniteProducts.prodComparison F A' B) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)
(CategoryTheory.MonoidalCategory.whiskerRight (F.map f) (F.obj B))
Naturality of the prodComparison morphism in the left argument.
theorem
CategoryTheory.ChosenFiniteProducts.prodComparison_inv_natural_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
{A : C}
{B : C}
{A' : C}
{B' : C}
[CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)]
(f : A ⟶ A')
(g : B ⟶ B')
[CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A' B')]
{Z : D}
(h : F.obj (CategoryTheory.MonoidalCategory.tensorObj A' B') ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B))
(CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.tensorHom f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g))
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A' B')) h)
theorem
CategoryTheory.ChosenFiniteProducts.prodComparison_inv_natural
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
{A : C}
{B : C}
{A' : C}
{B' : C}
[CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)]
(f : A ⟶ A')
(g : B ⟶ B')
[CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A' B')]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B))
(F.map (CategoryTheory.MonoidalCategory.tensorHom f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g))
(CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A' B'))
If the product comparison morphism is an iso, its inverse is natural in both argument.
theorem
CategoryTheory.ChosenFiniteProducts.prodComparison_inv_natural_whiskerLeft_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
{A : C}
{B : C}
{B' : C}
[CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)]
(g : B ⟶ B')
[CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B')]
{Z : D}
(h : F.obj (CategoryTheory.MonoidalCategory.tensorObj A B') ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B))
(CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.whiskerLeft A g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj A) (F.map g))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B'))
h)
theorem
CategoryTheory.ChosenFiniteProducts.prodComparison_inv_natural_whiskerLeft
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
{A : C}
{B : C}
{B' : C}
[CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)]
(g : B ⟶ B')
[CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B')]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B))
(F.map (CategoryTheory.MonoidalCategory.whiskerLeft A g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj A) (F.map g))
(CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B'))
If the product comparison morphism is an iso, its inverse is natural in the right argument.
theorem
CategoryTheory.ChosenFiniteProducts.prodComparison_inv_natural_whiskerRight_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
{A : C}
{B : C}
{A' : C}
[CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)]
(f : A ⟶ A')
[CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A' B)]
{Z : D}
(h : F.obj (CategoryTheory.MonoidalCategory.tensorObj A' B) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B))
(CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.whiskerRight f B)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.map f) (F.obj B))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A' B))
h)
theorem
CategoryTheory.ChosenFiniteProducts.prodComparison_inv_natural_whiskerRight
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
{A : C}
{B : C}
{A' : C}
[CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)]
(f : A ⟶ A')
[CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A' B)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A B))
(F.map (CategoryTheory.MonoidalCategory.whiskerRight f B)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.map f) (F.obj B))
(CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F A' B))
If the product comparison morphism is an iso, its inverse is natural in the left argument.
theorem
CategoryTheory.ChosenFiniteProducts.prodComparison_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
{A : C}
{B : C}
{E : Type u₂}
[CategoryTheory.Category.{v₂, u₂} E]
[CategoryTheory.ChosenFiniteProducts E]
(G : CategoryTheory.Functor D E)
:
CategoryTheory.ChosenFiniteProducts.prodComparison (F.comp G) A B = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.ChosenFiniteProducts.prodComparison F A B))
(CategoryTheory.ChosenFiniteProducts.prodComparison G (F.obj A) (F.obj B))
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.prodComparison_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{A : C}
{B : C}
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
(B : C)
:
def
CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
:
((CategoryTheory.MonoidalCategory.curriedTensor C).obj A).comp F ⟶ F.comp ((CategoryTheory.MonoidalCategory.curriedTensor D).obj (F.obj A))
The product comparison morphism from F(A ⊗ -) to FA ⊗ F-, whose components are given by
prodComparison.
Equations
- CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans F A = { app := fun (B : C) => CategoryTheory.ChosenFiniteProducts.prodComparison F A B, naturality := ⋯ }
Instances For
theorem
CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
{A : C}
{E : Type u₂}
[CategoryTheory.Category.{v₂, u₂} E]
[CategoryTheory.ChosenFiniteProducts E]
(G : CategoryTheory.Functor D E)
:
CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans (F.comp G) A = CategoryTheory.CategoryStruct.comp
(CategoryTheory.whiskerRight (CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans F A) G)
(CategoryTheory.whiskerLeft F (CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans G (F.obj A)))
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{A : C}
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatTrans_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
:
def
CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatTrans
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
:
(CategoryTheory.MonoidalCategory.curriedTensor C).comp ((CategoryTheory.whiskeringRight C C D).obj F) ⟶ F.comp ((CategoryTheory.MonoidalCategory.curriedTensor D).comp ((CategoryTheory.whiskeringLeft C D D).obj F))
The product comparison morphism from F(- ⊗ -) to F- ⊗ F-, whose components are given by
prodComparison.
Equations
- CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatTrans F = { app := fun (A : C) => CategoryTheory.ChosenFiniteProducts.prodComparisonNatTrans F A, naturality := ⋯ }
Instances For
theorem
CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatTrans_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
{E : Type u₂}
[CategoryTheory.Category.{v₂, u₂} E]
[CategoryTheory.ChosenFiniteProducts E]
(G : CategoryTheory.Functor D E)
:
CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatTrans (F.comp G) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.whiskerRight (CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatTrans F)
((CategoryTheory.whiskeringRight C D E).obj G))
(CategoryTheory.whiskerLeft F
(CategoryTheory.whiskerRight (CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatTrans G)
((CategoryTheory.whiskeringLeft C D E).obj F)))
instance
CategoryTheory.ChosenFiniteProducts.instIsIsoFunctorProdComparisonNatTransOfProdComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
[∀ (B : C), CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.ChosenFiniteProducts.instIsIsoFunctorProdComparisonBifunctorNatTransOfProdComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
[∀ (A B : C), CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.ChosenFiniteProducts.isLimitChosenFiniteProductsOfPreservesLimits
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
(F : CategoryTheory.Functor C D)
(A : C)
(B : C)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F]
:
If F preserves the limit of the pair (A, B), then the binary fan given by
(F.map fst A B, F.map (snd A B)) is a limit cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.ChosenFiniteProducts.prodComparisonIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
(B : C)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F]
:
F.obj (CategoryTheory.MonoidalCategory.tensorObj A B) ≅ CategoryTheory.MonoidalCategory.tensorObj (F.obj A) (F.obj B)
If F preserves the limit of the pair (A, B), then prodComparison F A B is an isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.prodComparisonIso_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
(B : C)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F]
:
instance
CategoryTheory.ChosenFiniteProducts.isIso_prodComparison_of_preservesLimit_pair
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
(B : C)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F]
:
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.prodComparisonNatIso_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
[(B : C) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F]
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.prodComparisonNatIso_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
[(B : C) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F]
:
noncomputable def
CategoryTheory.ChosenFiniteProducts.prodComparisonNatIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
[(B : C) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F]
:
((CategoryTheory.MonoidalCategory.curriedTensor C).obj A).comp F ≅ F.comp ((CategoryTheory.MonoidalCategory.curriedTensor D).obj (F.obj A))
The natural isomorphism F(A ⊗ -) ≅ FA ⊗ F-, provided each prodComparison F A B is an
isomorphism (as B changes).
Equations
Instances For
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatIso_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
[(A B : C) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F]
:
@[simp]
theorem
CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatIso_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
[(A B : C) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F]
:
noncomputable def
CategoryTheory.ChosenFiniteProducts.prodComparisonBifunctorNatIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
[(A B : C) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F]
:
(CategoryTheory.MonoidalCategory.curriedTensor C).comp ((CategoryTheory.whiskeringRight C C D).obj F) ≅ F.comp ((CategoryTheory.MonoidalCategory.curriedTensor D).comp ((CategoryTheory.whiskeringLeft C D D).obj F))
The natural isomorphism of bifunctors F(- ⊗ -) ≅ F- ⊗ F-, provided each
prodComparison F A B is an isomorphism.
Equations
Instances For
noncomputable def
CategoryTheory.ChosenFiniteProducts.preservesLimitPairOfIsIsoProdComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(A : C)
(B : C)
[CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)]
:
If prodComparison F A B is an isomorphism, then F preserves the limit of pair A B.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.ChosenFiniteProducts.preservesLimitsOfShapeDiscreteWalkingPairOfIsoProdComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
[∀ (A B : C), CategoryTheory.IsIso (CategoryTheory.ChosenFiniteProducts.prodComparison F A B)]
:
If prodComparison F A B is an isomorphism for all A B then F preserves limits of shape
Discrete (WalkingPair).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.toOplaxMonoidalFunctorOfChosenFiniteProducts_δ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
(X : C)
(Y : C)
:
F.toOplaxMonoidalFunctorOfChosenFiniteProducts.δ X Y = CategoryTheory.ChosenFiniteProducts.prodComparison F X Y
@[simp]
theorem
CategoryTheory.Functor.toOplaxMonoidalFunctorOfChosenFiniteProducts_η
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
:
F.toOplaxMonoidalFunctorOfChosenFiniteProducts.η = CategoryTheory.ChosenFiniteProducts.terminalComparison F
@[simp]
theorem
CategoryTheory.Functor.toOplaxMonoidalFunctorOfChosenFiniteProducts_toFunctor
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
:
F.toOplaxMonoidalFunctorOfChosenFiniteProducts.toFunctor = F
def
CategoryTheory.Functor.toOplaxMonoidalFunctorOfChosenFiniteProducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
:
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.
Instances For
instance
CategoryTheory.instIsIsoηToOplaxMonoidalFunctorOfChosenFiniteProducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F]
:
CategoryTheory.IsIso F.toOplaxMonoidalFunctorOfChosenFiniteProducts.η
Equations
- ⋯ = ⋯
instance
CategoryTheory.instIsIsoδToOplaxMonoidalFunctorOfChosenFiniteProducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
(A : C)
(B : C)
:
CategoryTheory.IsIso (F.toOplaxMonoidalFunctorOfChosenFiniteProducts.δ A B)
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Functor.toMonoidalFunctorOfChosenFiniteProducts_toLaxMonoidalFunctor_μ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F]
[CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
(X : C)
(Y : C)
:
F.toMonoidalFunctorOfChosenFiniteProducts.μ X Y = CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.prodComparison F X Y)
@[simp]
theorem
CategoryTheory.Functor.toMonoidalFunctorOfChosenFiniteProducts_toLaxMonoidalFunctor_ε
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F]
[CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
:
F.toMonoidalFunctorOfChosenFiniteProducts.ε = CategoryTheory.inv (CategoryTheory.ChosenFiniteProducts.terminalComparison F)
@[simp]
theorem
CategoryTheory.Functor.toMonoidalFunctorOfChosenFiniteProducts_toLaxMonoidalFunctor_toFunctor
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F]
[CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
:
F.toMonoidalFunctorOfChosenFiniteProducts.toFunctor = F
noncomputable def
CategoryTheory.Functor.toMonoidalFunctorOfChosenFiniteProducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F]
[CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
:
If F preserves finite products, the oplax monoidal functor
F.toOplaxMonoidalFunctorOfChosenFiniteProducts can be promoted to a strong monoidal functor.
Equations
- F.toMonoidalFunctorOfChosenFiniteProducts = CategoryTheory.MonoidalFunctor.fromOplaxMonoidalFunctor F.toOplaxMonoidalFunctorOfChosenFiniteProducts
Instances For
instance
CategoryTheory.instIsEquivalenceToMonoidalFunctorOfChosenFiniteProducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ChosenFiniteProducts C]
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.ChosenFiniteProducts D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F]
[CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
[F.IsEquivalence]
:
F.toMonoidalFunctorOfChosenFiniteProducts.IsEquivalence
Equations
- ⋯ = inst