The even embedding is strong braided monoidal

RS/Classical/Deligne/Doubling.lean builds the even embedding evenEmbed : A ⥤ Doubled A, X ↦ (X, 0), together with its tensor comparison evenEmbedTensorIso, its unit comparison evenEmbedUnitIso and the compatibility of the comparison with the two braidings. This module packages that data as a lax monoidal structure, upgrades it to a strong monoidal structure — both comparisons are isomorphisms by construction — and records that the result is braided.

Every coherence reduces, by Doubled.hom_ext, to a pair of component identities. The odd component of each target is the zero object, so the odd half is automatic; the even half is a biproduct calculation in which the mixed parity blocks are killed because one of their two factors is the zero object.

The module also records the exactness of the even embedding. The even embedding is simultaneously left and right adjoint to the even-component functor evenFunctor of RS/Classical/Deligne/DoubledAbelian.lean, because a morphism into or out of the zero object is unique; so it preserves all limits and all colimits, in particular the finite ones.

@[simp]

theorem RS.Doubled.evenHom_evenEmbedUnitIso_hom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] : evenHom evenEmbedUnitIso.hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)

The even component of the unit comparison is the identity.

@[instance_reducible]

noncomputable instance RS.Doubled.evenEmbedLaxMonoidal {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] : evenEmbed.LaxMonoidal

The even embedding is lax monoidal: the unit comparison is the identity, because the unit of Doubled A is the even embedding of the unit of A, and the tensor comparison is evenEmbedTensorIso.

Equations

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

@[instance_reducible]

noncomputable instance RS.Doubled.evenEmbedMonoidal {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] : evenEmbed.Monoidal

The even embedding is strong monoidal: both comparisons are isomorphisms by construction.

Equations

• RS.Doubled.evenEmbedMonoidal = CategoryTheory.Functor.Monoidal.ofLaxMonoidal RS.Doubled.evenEmbed

The four structure morphisms

These are stated after the strong monoidal structure has been installed, so that their left-hand sides use the instance that a downstream file resolves.

@[simp]

theorem RS.Doubled.evenEmbed_ε {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] : CategoryTheory.Functor.LaxMonoidal.ε evenEmbed = evenEmbedUnitIso.hom

@[simp]

theorem RS.Doubled.evenEmbed_μ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X Y : A) : CategoryTheory.Functor.LaxMonoidal.μ evenEmbed X Y = (evenEmbedTensorIso X Y).hom

@[simp]

theorem RS.Doubled.evenEmbed_η {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] : CategoryTheory.Functor.OplaxMonoidal.η evenEmbed = evenEmbedUnitIso.inv

@[simp]

theorem RS.Doubled.evenEmbed_δ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] (X Y : A) : CategoryTheory.Functor.OplaxMonoidal.δ evenEmbed X Y = (evenEmbedTensorIso X Y).inv

@[instance_reducible]

noncomputable instance RS.Doubled.evenEmbedBraided {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] [CategoryTheory.Limits.HasZeroObject A] [CategoryTheory.SymmetricCategory A] : evenEmbed.Braided

The even embedding is braided: the Koszul sign is invisible on purely even objects, so the tensor comparison intertwines the two braidings.

Equations

• RS.Doubled.evenEmbedBraided = { toMonoidal := RS.Doubled.evenEmbedMonoidal, braided := ⋯ }

noncomputable def RS.Doubled.evenEmbedAdjEvenFunctor {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasZeroObject A] : evenEmbed ⊣ evenFunctor

The even embedding is left adjoint to the even-component functor: a morphism out of the zero object is unique.

Equations

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

noncomputable def RS.Doubled.evenFunctorAdjEvenEmbed {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasZeroObject A] : evenFunctor ⊣ evenEmbed

The even embedding is right adjoint to the even-component functor: a morphism into the zero object is unique.

Equations

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

instance RS.Doubled.evenEmbedPreservesFiniteLimits {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasZeroObject A] : CategoryTheory.Limits.PreservesFiniteLimits evenEmbed

Being a right adjoint, the even embedding is left exact.

instance RS.Doubled.evenEmbedPreservesFiniteColimits {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasZeroObject A] : CategoryTheory.Limits.PreservesFiniteColimits evenEmbed

Being a left adjoint, the even embedding is right exact.