Documentation

TauCeti.Algebra.Coalgebra.Comodule.Finite.Dual

Duals of finite-dimensional comodules #

This file bundles the linear dual of a finite-dimensional right comodule over a Hopf algebra as an object of FGComoduleCat. The underlying coaction is the basis-free dual coaction constructed in TauCeti.Algebra.Coalgebra.Comodule.Dual.

Main declaration #

References #

This is the finite-dimensional specialization of the standard dual-comodule construction; see Sweedler, Hopf Algebras, Chapter 2.

source
@[reducible, inline]
noncomputable abbrev TauCeti.FGComoduleCat.dual (k : Type u) [Field k] (H : Type v) [Semiring H] [HopfAlgebra k H] (M : FGComoduleCat k H) :
FGComoduleCat k H

The linear dual of a finite-dimensional right comodule, with the coaction induced by the antipode.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.FGComoduleCat.dual_obj (k : Type u) [Field k] (H : Type v) [Semiring H] [HopfAlgebra k H] (M : FGComoduleCat k H) :
    (dual k H M).obj = ComoduleCat.of k H (Module.Dual k ↑M)

    The ambient comodule underlying the finite dual is the linear dual equipped with Comodule.dual.

    source
    @[simp]
    theorem TauCeti.FGComoduleCat.dual_coe (k : Type u) [Field k] (H : Type v) [Semiring H] [HopfAlgebra k H] (M : FGComoduleCat k H) :
    ↑(dual k H M) = Module.Dual k ↑M

    The carrier of the finite dual is the ordinary linear dual.

    source
    @[simp]
    theorem TauCeti.FGComoduleCat.dual_coact (k : Type u) [Field k] (H : Type v) [Semiring H] [HopfAlgebra k H] (M : FGComoduleCat k H) :
    Comodule.coact = Comodule.dualCoact

    The coaction on the finite dual is the basis-free dual coaction.

    source
    @[simp]
    theorem TauCeti.FGComoduleCat.incl_dual (k : Type u) [Field k] (H : Type v) [Semiring H] [HopfAlgebra k H] (M : FGComoduleCat k H) :
    incl.obj (dual k H M) = ComoduleCat.of k H (Module.Dual k ↑M)

    The inclusion into all comodules sends the finite dual to the ambient dual comodule.

    source
    @[simp]
    theorem TauCeti.FGComoduleCat.forget₂_semimoduleCat_dual_obj (k : Type u) [Field k] (H : Type v) [Semiring H] [HopfAlgebra k H] (M : FGComoduleCat k H) :
    (CategoryTheory.forget₂ (FGComoduleCat k H) (SemimoduleCat k)).obj (dual k H M) = ↧(Module.Dual k ↑M)

    Forgetting the finite dual to semimodules gives the ordinary linear-dual module.