Exact pairings of finite biproducts #
In a monoidal preadditive category, the tensor product distributes over finite biproducts. As a
consequence, dualizable objects are closed under finite biproducts: if Y i is a right dual of
X i for every i in a finite index type, then ⨁ Y is a right dual of ⨁ X. The
coevaluation is the sum of the coevaluations of the summands and the evaluation is the sum of the
evaluations of the summands:
η = ∑ i, η_ (X i) (Y i) ≫ (biproduct.ι X i ⊗ₘ biproduct.ι Y i)
ε = ∑ i, (biproduct.π Y i ⊗ₘ biproduct.π X i) ≫ ε_ (X i) (Y i)
In a category of modules or of sheaves of modules this shows that finite free objects, which are finite biproducts of copies of the unit, are dualizable.
Main declarations #
TauCeti.ExactPairing.unit_evaluationandTauCeti.ExactPairing.unit_coevaluation: the evaluation and coevaluation of Mathlib's self-pairing of the unit;TauCeti.ExactPairing.biproduct: the exact pairing between⨁ Xand⨁ Yinduced by exact pairings betweenX iandY i;TauCeti.ExactPairing.biproduct_ι_tensorHom_biproduct_ι_evaluationandTauCeti.ExactPairing.coevaluation_biproduct_π_tensorHom_biproduct_π, with their_of_nevariants: the evaluation and coevaluation are, componentwise, those of the summands on the diagonal and zero off it.
theorem
TauCeti.whiskerLeft_tensorHom_associator_inv_tensorHom_whiskerRight
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{Z Z' A B X Y D : C}
(a : A ⟶ X)
(b : B ⟶ Y)
(c : Z ⟶ Z')
(d : X ⟶ D)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.MonoidalCategoryStruct.tensorHom a b))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv
(CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.tensorHom c d) Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z A B).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom
(CategoryTheory.MonoidalCategoryStruct.tensorHom c (CategoryTheory.CategoryStruct.comp a d)) b)
Moving a tensor product of morphisms past the inverse associator: the two middle factors compose.
theorem
TauCeti.whiskerLeft_tensorHom_associator_inv_tensorHom_whiskerRight_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{Z Z' A B X Y D : C}
(a : A ⟶ X)
(b : B ⟶ Y)
(c : Z ⟶ Z')
(d : X ⟶ D)
{Z✝ : C}
(h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Z' D) Y ⟶ Z✝)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.MonoidalCategoryStruct.tensorHom a b))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.tensorHom c d) Y)
h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z A B).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom
(CategoryTheory.MonoidalCategoryStruct.tensorHom c (CategoryTheory.CategoryStruct.comp a d)) b)
h)
Moving a tensor product of morphisms past the inverse associator: the two middle factors compose.
theorem
TauCeti.tensorHom_whiskerRight_associator_hom_whiskerLeft_tensorHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{Z Z' A B X Y D : C}
(a : A ⟶ X)
(b : B ⟶ Y)
(c : Y ⟶ D)
(d : Z ⟶ Z')
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.tensorHom a b) Z)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.tensorHom c d))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A B Z).hom
(CategoryTheory.MonoidalCategoryStruct.tensorHom a
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp b c) d))
Moving a tensor product of morphisms past the associator: the two middle factors compose.
theorem
TauCeti.tensorHom_whiskerRight_associator_hom_whiskerLeft_tensorHom_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{Z Z' A B X Y D : C}
(a : A ⟶ X)
(b : B ⟶ Y)
(c : Y ⟶ D)
(d : Z ⟶ Z')
{Z✝ : C}
(h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj D Z') ⟶ Z✝)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.tensorHom a b) Z)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.tensorHom c d))
h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A B Z).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom a
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp b c) d))
h)
Moving a tensor product of morphisms past the associator: the two middle factors compose.
theorem
TauCeti.coevaluation_evaluation_tensorHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{Z X Y W : C}
[CategoryTheory.ExactPairing X Y]
(c : Z ⟶ Y)
(b : Y ⟶ W)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (η_ X Y))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom
(CategoryTheory.MonoidalCategoryStruct.tensorHom c (CategoryTheory.CategoryStruct.id X)) b)
(CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε_ X Y) W))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).hom
(CategoryTheory.CategoryStruct.comp c
(CategoryTheory.CategoryStruct.comp b (CategoryTheory.MonoidalCategoryStruct.leftUnitor W).inv))
The first zigzag identity of an exact pairing, with morphisms c and b inserted on the outer
factors.
theorem
TauCeti.evaluation_coevaluation_tensorHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{Z X Y W : C}
[CategoryTheory.ExactPairing X Y]
(a : X ⟶ W)
(d : Z ⟶ X)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (η_ X Y) Z)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom a
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id Y) d))
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (ε_ X Y)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom
(CategoryTheory.CategoryStruct.comp d
(CategoryTheory.CategoryStruct.comp a (CategoryTheory.MonoidalCategoryStruct.rightUnitor W).inv))
The second zigzag identity of an exact pairing, with morphisms d and a inserted on the
outer factors.
@[simp]
theorem
TauCeti.ExactPairing.unit_evaluation
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
:
The evaluation of the canonical self-pairing of the unit is the right unitor.
@[simp]
theorem
TauCeti.ExactPairing.unit_coevaluation
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
:
The coevaluation of the canonical self-pairing of the unit is the inverse right unitor.
@[instance_reducible]
noncomputable instance
TauCeti.ExactPairing.biproduct
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Preadditive C]
[CategoryTheory.MonoidalPreadditive C]
{ι : Type w}
[Finite ι]
(X Y : ι → C)
[CategoryTheory.Limits.HasBiproduct X]
[CategoryTheory.Limits.HasBiproduct Y]
[(i : ι) → CategoryTheory.ExactPairing (X i) (Y i)]
:
CategoryTheory.ExactPairing (⨁ X) (⨁ Y)
Exact pairings are closed under finite biproducts: if Y i is a right dual of X i for each
i, then ⨁ Y is a right dual of ⨁ X, with coevaluation and evaluation the sums of those of
the summands.
Equations
- One or more equations did not get rendered due to their size.
theorem
TauCeti.ExactPairing.biproduct_coevaluation
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Preadditive C]
[CategoryTheory.MonoidalPreadditive C]
{ι : Type w}
[Finite ι]
(X Y : ι → C)
[CategoryTheory.Limits.HasBiproduct X]
[CategoryTheory.Limits.HasBiproduct Y]
[(i : ι) → CategoryTheory.ExactPairing (X i) (Y i)]
[Fintype ι]
:
η_ (⨁ X) (⨁ Y) = ∑ i : ι,
CategoryTheory.CategoryStruct.comp (η_ (X i) (Y i))
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Limits.biproduct.ι X i)
(CategoryTheory.Limits.biproduct.ι Y i))
The coevaluation of the biproduct pairing is the sum of the coevaluations of the summands.
theorem
TauCeti.ExactPairing.biproduct_evaluation
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Preadditive C]
[CategoryTheory.MonoidalPreadditive C]
{ι : Type w}
[Finite ι]
(X Y : ι → C)
[CategoryTheory.Limits.HasBiproduct X]
[CategoryTheory.Limits.HasBiproduct Y]
[(i : ι) → CategoryTheory.ExactPairing (X i) (Y i)]
[Fintype ι]
:
ε_ (⨁ X) (⨁ Y) = ∑ i : ι,
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Limits.biproduct.π Y i)
(CategoryTheory.Limits.biproduct.π X i))
(ε_ (X i) (Y i))
The evaluation of the biproduct pairing is the sum of the evaluations of the summands.
@[simp]
theorem
TauCeti.ExactPairing.biproduct_ι_tensorHom_biproduct_ι_evaluation
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Preadditive C]
[CategoryTheory.MonoidalPreadditive C]
{ι : Type w}
[Finite ι]
{X Y : ι → C}
[CategoryTheory.Limits.HasBiproduct X]
[CategoryTheory.Limits.HasBiproduct Y]
[(i : ι) → CategoryTheory.ExactPairing (X i) (Y i)]
(i : ι)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Limits.biproduct.ι Y i)
(CategoryTheory.Limits.biproduct.ι X i))
(ε_ (⨁ X) (⨁ Y)) = ε_ (X i) (Y i)
On the summand Y i ⊗ X i, the evaluation of the biproduct pairing is the evaluation of the
i-th summand.
@[simp]
theorem
TauCeti.ExactPairing.biproduct_ι_tensorHom_biproduct_ι_evaluation_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Preadditive C]
[CategoryTheory.MonoidalPreadditive C]
{ι : Type w}
[Finite ι]
{X Y : ι → C}
[CategoryTheory.Limits.HasBiproduct X]
[CategoryTheory.Limits.HasBiproduct Y]
[(i : ι) → CategoryTheory.ExactPairing (X i) (Y i)]
(i : ι)
{Z : C}
(h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z)
:
On the summand Y i ⊗ X i, the evaluation of the biproduct pairing is the evaluation of the
i-th summand.
@[simp]
theorem
TauCeti.ExactPairing.biproduct_ι_tensorHom_biproduct_ι_evaluation_of_ne
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Preadditive C]
[CategoryTheory.MonoidalPreadditive C]
{ι : Type w}
[Finite ι]
{X Y : ι → C}
[CategoryTheory.Limits.HasBiproduct X]
[CategoryTheory.Limits.HasBiproduct Y]
[(i : ι) → CategoryTheory.ExactPairing (X i) (Y i)]
{i j : ι}
(h : i ≠ j)
:
On the summand Y i ⊗ X j with i ≠ j, the evaluation of the biproduct pairing vanishes.
@[simp]
theorem
TauCeti.ExactPairing.biproduct_ι_tensorHom_biproduct_ι_evaluation_of_ne_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Preadditive C]
[CategoryTheory.MonoidalPreadditive C]
{ι : Type w}
[Finite ι]
{X Y : ι → C}
[CategoryTheory.Limits.HasBiproduct X]
[CategoryTheory.Limits.HasBiproduct Y]
[(i : ι) → CategoryTheory.ExactPairing (X i) (Y i)]
{i j : ι}
(h : i ≠ j)
{Z : C}
(h✝ : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z)
:
On the summand Y i ⊗ X j with i ≠ j, the evaluation of the biproduct pairing vanishes.
@[simp]
theorem
TauCeti.ExactPairing.coevaluation_biproduct_π_tensorHom_biproduct_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Preadditive C]
[CategoryTheory.MonoidalPreadditive C]
{ι : Type w}
[Finite ι]
{X Y : ι → C}
[CategoryTheory.Limits.HasBiproduct X]
[CategoryTheory.Limits.HasBiproduct Y]
[(i : ι) → CategoryTheory.ExactPairing (X i) (Y i)]
(i : ι)
:
CategoryTheory.CategoryStruct.comp (η_ (⨁ X) (⨁ Y))
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Limits.biproduct.π X i)
(CategoryTheory.Limits.biproduct.π Y i)) = η_ (X i) (Y i)
The coevaluation of the biproduct pairing, projected to X i ⊗ Y i, is the coevaluation of
the i-th summand.
@[simp]
theorem
TauCeti.ExactPairing.coevaluation_biproduct_π_tensorHom_biproduct_π_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Preadditive C]
[CategoryTheory.MonoidalPreadditive C]
{ι : Type w}
[Finite ι]
{X Y : ι → C}
[CategoryTheory.Limits.HasBiproduct X]
[CategoryTheory.Limits.HasBiproduct Y]
[(i : ι) → CategoryTheory.ExactPairing (X i) (Y i)]
(i : ι)
{Z : C}
(h : CategoryTheory.MonoidalCategoryStruct.tensorObj (X i) (Y i) ⟶ Z)
:
The coevaluation of the biproduct pairing, projected to X i ⊗ Y i, is the coevaluation of
the i-th summand.
@[simp]
theorem
TauCeti.ExactPairing.coevaluation_biproduct_π_tensorHom_biproduct_π_of_ne
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Preadditive C]
[CategoryTheory.MonoidalPreadditive C]
{ι : Type w}
[Finite ι]
{X Y : ι → C}
[CategoryTheory.Limits.HasBiproduct X]
[CategoryTheory.Limits.HasBiproduct Y]
[(i : ι) → CategoryTheory.ExactPairing (X i) (Y i)]
{i j : ι}
(h : i ≠ j)
:
The coevaluation of the biproduct pairing, projected to X i ⊗ Y j with i ≠ j, vanishes.
@[simp]
theorem
TauCeti.ExactPairing.coevaluation_biproduct_π_tensorHom_biproduct_π_of_ne_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Preadditive C]
[CategoryTheory.MonoidalPreadditive C]
{ι : Type w}
[Finite ι]
{X Y : ι → C}
[CategoryTheory.Limits.HasBiproduct X]
[CategoryTheory.Limits.HasBiproduct Y]
[(i : ι) → CategoryTheory.ExactPairing (X i) (Y i)]
{i j : ι}
(h : i ≠ j)
{Z : C}
(h✝ : CategoryTheory.MonoidalCategoryStruct.tensorObj (X i) (Y j) ⟶ Z)
:
The coevaluation of the biproduct pairing, projected to X i ⊗ Y j with i ≠ j, vanishes.