Monoidal structure on the Karoubi envelope #
For a monoidal category C, the Karoubi envelope Karoubi C inherits a
monoidal structure:
- Objects:
(A, p) ⊗ (B, q) = (A ⊗ B, p ⊗ₘ q), the tensor of idempotents being idempotent by the interchange law. - Morphisms:
f ⊗ₘ gon underlying morphisms. - Unit:
(𝟙_ C, 𝟙 (𝟙_ C)). - Structural isomorphisms: conjugates of the associators and unitors
of
Cby the idempotents — e.g. the associator has underlying morphism((p ⊗ₘ q) ⊗ₘ r) ≫ α_{A,B,C}.hom.
The canonical functor toKaroubi C : C ⥤ Karoubi C is strong monoidal.
When C is braided (respectively symmetric), so is Karoubi C.
Auxiliary lemmas for idempotent-conjugated morphisms #
Decomposition of tensor products with compositions #
When one argument of ⊗ₘ is idempotent, a composition in the other argument
can be extracted as a composition of tensor products. These lemmas are needed
because rw / simp cannot rewrite subexpressions inside ⊗ₘ arguments
due to dependent-type motive construction failures.
Naturality of structural isomorphisms with idempotents #
These lemmas state the naturality of the associator, left unitor, and
right unitor (and their inverses) applied to the idempotent morphisms of
Karoubi objects. They are proved outside any Karoubi-struct context so
that rw with id_tensorHom/tensorHom_id avoids dependent-type
motive failures.
Data: MonoidalCategoryStruct on Karoubi C #
The monoidal data on the Karoubi envelope: tensor of idempotents, conjugated structural isomorphisms.
Equations
- One or more equations did not get rendered due to their size.
Simp lemmas for the Karoubi monoidal data #
These unfold the .f and .p projections of the Karoubi monoidal
structure to morphisms in C. They are all definitional equalities.
Axioms: MonoidalCategory on Karoubi C #
The monoidal axioms (interchange, naturality, pentagon, triangle) are
proved by reducing to the underlying morphisms in C via hom_ext and
the Karoubi simp lemmas p_comp, comp_p, idem.
Bridge lemmas: tensorHom form of C axioms #
The mathlib MonoidalCategory axioms for C use ◁ / ▷ (whiskerLeft /
whiskerRight) while ofTensorHom expects 𝟙 X ⊗ₘ f / f ⊗ₘ 𝟙 Y.
These helpers restate the relevant C axioms in tensorHom form, proved
outside the Karoubi struct context where rw [id_tensorHom] is safe.
Those data satisfy the monoidal axioms, each inherited from the ambient category by conjugation.
Equations
- RS.karoubiMonoidal = CategoryTheory.MonoidalCategory.ofTensorHom ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
The canonical functor toKaroubi C is strong monoidal #
Strong monoidality #
The functor toKaroubi C : C ⥤ Karoubi C sends X to ⟨X, 𝟙 X⟩. It
preserves the tensor unit on the nose and the tensor product up to the
canonical identification 𝟙 X ⊗ₘ 𝟙 Y = 𝟙 (X ⊗ Y).
The embedding is monoidal.
Equations
- One or more equations did not get rendered due to their size.
Braided and symmetric structure on Karoubi C #
When C carries a braided (resp. symmetric) monoidal structure, so does
Karoubi C. The braiding on Karoubi C has underlying morphism
(p ⊗ₘ q) ≫ (β_ A B).hom, conjugating the braiding of C by the
tensor of idempotents.
The braiding isomorphism on Karoubi objects, defined prior to the instance
so that simp lemmas for the .f projection are available inside the axiom
proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A braiding on the ambient category conjugates to one on the envelope.
Equations
- RS.karoubiBraided = { braiding := RS.karoubiBraidingIso, braiding_naturality_right := ⋯, braiding_naturality_left := ⋯, hexagon_forward := ⋯, hexagon_reverse := ⋯ }
And a symmetric one stays symmetric.
Equations
- RS.karoubiSymmetric = { toBraidedCategory := RS.karoubiBraided, symmetry := ⋯ }