Documentation

TauCeti.Algebra.Coalgebra.Comodule.Finite.Symmetric

The symmetric monoidal category of finite comodules #

This file equips finitely generated right comodules over a commutative bialgebra with their standard symmetric monoidal structure. The braiding is the ordinary tensor-product swap

m ⊗ n ↦ n ⊗ m.

The swap respects the diagonal coaction because commutativity identifies the coefficient products m₁n₁ and n₁m₁. Its compatibility with the coaction is isolated in Comodule.tensorCombine_comm. The remaining naturality, hexagon, and symmetry laws are inherited from SemimoduleCat along the faithful monoidal forgetful functor.

Main declarations #

References #

This is the symmetric-category part of Layer 1 of the Tau Ceti reductive-groups roadmap, ReductiveGroups/README.md in TauCetiRoadmap. It advances the requested rigid monoidal category of finite-dimensional comodules and the later Tannakian reconstruction target. The construction is standard; see Sweedler, Hopf Algebras, Chapter 2. The categorical packaging follows Mathlib's symmetric structure on SemimoduleCat and uses BraidedCategory.ofFaithful and SymmetricCategory.ofFaithful.

source
noncomputable def TauCeti.FGComoduleCat.tensorBraiding (R : Type u) [CommSemiring R] (C : Type v) [CommSemiring C] [Bialgebra R C] (M N : FGComoduleCat R C) :
tensor R C M N ≅ tensor R C N M

The braiding on finite comodules: the ordinary tensor-product swap, which intertwines the diagonal coactions because the coefficient bialgebra is commutative.

Equations
Instances For
    source
    @[instance_reducible]
    noncomputable instance TauCeti.FGComoduleCat.instBraidedCategory (R : Type u) [CommSemiring R] (C : Type v) [CommSemiring C] [Bialgebra R C] :
    CategoryTheory.BraidedCategory (FGComoduleCat R C)

    The tensor-product swap makes finite comodules over a commutative bialgebra braided.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[instance_reducible]
    noncomputable instance TauCeti.FGComoduleCat.instForgetBraided (R : Type u) [CommSemiring R] (C : Type v) [CommSemiring C] [Bialgebra R C] :
    (CategoryTheory.forget₂ (FGComoduleCat R C) (SemimoduleCat R)).Braided

    The forgetful functor from finite comodules to semimodules preserves the braiding.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[instance_reducible]
    noncomputable instance TauCeti.FGComoduleCat.instSymmetricCategory (R : Type u) [CommSemiring R] (C : Type v) [CommSemiring C] [Bialgebra R C] :
    CategoryTheory.SymmetricCategory (FGComoduleCat R C)

    Finite comodules over a commutative bialgebra form a symmetric monoidal category.

    Equations
    source
    @[simp]
    theorem TauCeti.FGComoduleCat.tensorBraiding_eq {R : Type u} [CommSemiring R] {C : Type v} [CommSemiring C] [Bialgebra R C] {M N : FGComoduleCat R C} :
    tensorBraiding R C M N = β_ M N

    The monoidal braiding is the named tensor-product swap.

    source
    @[simp]
    theorem TauCeti.FGComoduleCat.braiding_hom_apply {R : Type u} [CommSemiring R] {C : Type v} [CommSemiring C] [Bialgebra R C] {M N : FGComoduleCat R C} (m : ↑M) (n : ↑N) :
    (CategoryTheory.ConcreteCategory.hom (β_ M N).hom) (m ⊗ₜ[R] n) = n ⊗ₜ[R] m

    The braiding sends m ⊗ n to n ⊗ m.

    source
    @[simp]
    theorem TauCeti.FGComoduleCat.braiding_inv_apply {R : Type u} [CommSemiring R] {C : Type v} [CommSemiring C] [Bialgebra R C] {M N : FGComoduleCat R C} (n : ↑N) (m : ↑M) :
    (CategoryTheory.ConcreteCategory.hom (β_ M N).inv) (n ⊗ₜ[R] m) = m ⊗ₜ[R] n

    The inverse braiding sends n ⊗ m back to m ⊗ n.