Documentation

TauCeti.Algebra.Coalgebra.Comodule.Trivial

Trivial comodules #

For a coalgebra C over R and a group-like element g : GroupLike R C, every R-module M has a right C-comodule structure with coaction m ↦ m ⊗ g. In a bialgebra, taking g = 1 gives the trivial comodule. This is the comodule-theoretic analogue of the trivial representation, and the tensor-unit ingredient for the monoidal category of comodules over a Hopf algebra.

The main definitions are intentionally explicit named comodule structures, not global instances: many modules carry nontrivial coactions, and typeclass search should not silently choose the trivial one.

Main definitions #

References #

This supplies a small prerequisite for the Tau Ceti reductive-groups roadmap, ReductiveGroups/README.md in TauCetiRoadmap, Layer 1 target "Comodules over a coalgebra/Hopf algebra", specifically the tensor-unit side of the requested tensor-product and rigid monoidal comodule category. It uses Mathlib's bialgebra API from Mathlib.RingTheory.Bialgebra.GroupLike.

source
def TauCeti.Comodule.groupLikeCoact {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) :
M →ₗ[R] TensorProduct R M C

The map m ↦ m ⊗ g attached to a group-like element g : GroupLike R C, as an R-linear map M →ₗ[R] M ⊗[R] C. It serves as the coaction of the comodule structure Comodule.groupLike g.

Equations
Instances For
    source
    @[implicit_reducible]
    def TauCeti.Comodule.groupLike {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) :
    Comodule R C M

    The right C-comodule structure on an R-module attached to a group-like element g : GroupLike R C, with coaction m ↦ m ⊗ g.

    This is not registered as a global instance: an R-module can carry many coactions, and the group-like coaction should be selected explicitly with Comodule.groupLike.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Comodule.groupLike_coact_apply {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) (m : M) :
      coact m = m ⊗ₜ[R] ↑g

      The coaction attached to a group-like element sends m to m ⊗ g.

      source
      @[simp]
      theorem TauCeti.Comodule.groupLike_coact {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) :
      coact = (TensorProduct.mk R M C).flip ↑g

      The coaction attached to a group-like element is the map m ↦ m ⊗ g.

      source
      def TauCeti.Comodule.Hom.ofGroupLike {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) (f : M →ₗ[R] N) :
      Hom R C M N

      A linear map is automatically a comodule morphism between the comodules attached to the same group-like element.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.Comodule.Hom.ofGroupLike_toLinearMap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) (f : M →ₗ[R] N) :
        (ofGroupLike g f).toLinearMap = f

        The underlying linear map of Hom.ofGroupLike g f is f.

        source
        @[simp]
        theorem TauCeti.Comodule.Hom.ofGroupLike_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) (f : M →ₗ[R] N) (m : M) :
        (ofGroupLike g f) m = f m

        The comodule morphism induced by a linear map between group-like comodules applies as that linear map.

        source
        @[simp]
        theorem TauCeti.Comodule.Hom.ofGroupLike_id {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) :
        ofGroupLike g LinearMap.id = id R C M

        The comodule morphism induced by the identity linear map between group-like comodules is the identity comodule morphism.

        source
        @[simp]
        theorem TauCeti.Comodule.Hom.ofGroupLike_comp {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid C] [Module R C] [Coalgebra R C] {P : Type u_1} [AddCommMonoid P] [Module R P] (g : GroupLike R C) (h : N →ₗ[R] P) (f : M →ₗ[R] N) :
        ofGroupLike g (h ∘ₗ f) = (ofGroupLike g h).comp (ofGroupLike g f)

        The comodule morphism induced by a composite linear map between group-like comodules is the composite of the induced comodule morphisms.

        source
        def TauCeti.Comodule.Hom.groupLikeEquiv {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) :
        Hom R C M N ≃ (M →ₗ[R] N)

        Comodule morphisms between comodules attached to the same group-like element are exactly ordinary linear maps.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem TauCeti.Comodule.Hom.groupLikeEquiv_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) (f : Hom R C M N) :
          (groupLikeEquiv g) f = f.toLinearMap

          Applying groupLikeEquiv returns the underlying linear map.

          source
          @[simp]
          theorem TauCeti.Comodule.Hom.groupLikeEquiv_symm_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) (f : M →ₗ[R] N) :
          (groupLikeEquiv g).symm f = ofGroupLike g f

          The inverse of groupLikeEquiv sends a linear map to the corresponding morphism of group-like comodules.

          source
          @[simp]
          theorem TauCeti.Comodule.Hom.groupLikeEquiv_symm_apply_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) (f : M →ₗ[R] N) (m : M) :
          ((groupLikeEquiv g).symm f) m = f m

          Pointwise form of groupLikeEquiv_symm_apply.

          source
          @[implicit_reducible]
          def TauCeti.Comodule.trivial {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring C] [Bialgebra R C] :
          Comodule R C M

          The trivial right C-comodule structure on an R-module.

          This is not registered as a global instance: an R-module can carry many coactions, and the trivial one should be selected explicitly with Comodule.trivial.

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.Comodule.trivial_coact_apply {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring C] [Bialgebra R C] (m : M) :
            coact m = m ⊗ₜ[R] 1

            The coaction of the trivial right comodule sends m to m ⊗ 1.

            source
            @[simp]
            theorem TauCeti.Comodule.trivial_coact {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring C] [Bialgebra R C] :
            coact = (TensorProduct.mk R M C).flip 1

            The coaction of the trivial right comodule is the map m ↦ m ⊗ 1.

            source
            def TauCeti.Comodule.Hom.ofTrivial {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring C] [Bialgebra R C] (f : M →ₗ[R] N) :
            Hom R C M N

            A linear map between trivial comodules is automatically a comodule morphism.

            Equations
            Instances For
              source
              @[simp]
              theorem TauCeti.Comodule.Hom.ofTrivial_toLinearMap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring C] [Bialgebra R C] (f : M →ₗ[R] N) :
              (ofTrivial f).toLinearMap = f

              The underlying linear map of Hom.ofTrivial f is f.

              source
              @[simp]
              theorem TauCeti.Comodule.Hom.ofTrivial_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring C] [Bialgebra R C] (f : M →ₗ[R] N) (m : M) :
              (ofTrivial f) m = f m

              The comodule morphism induced by a linear map between trivial comodules applies as that linear map.

              source
              @[simp]
              theorem TauCeti.Comodule.Hom.ofTrivial_id {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring C] [Bialgebra R C] :
              ofTrivial LinearMap.id = id R C M

              The comodule morphism induced by the identity linear map between trivial comodules is the identity comodule morphism.

              source
              @[simp]
              theorem TauCeti.Comodule.Hom.ofTrivial_comp {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring C] [Bialgebra R C] {P : Type u_1} [AddCommMonoid P] [Module R P] (g : N →ₗ[R] P) (f : M →ₗ[R] N) :
              ofTrivial (g ∘ₗ f) = (ofTrivial g).comp (ofTrivial f)

              The comodule morphism induced by a composite linear map between trivial comodules is the composite of the induced comodule morphisms.

              source
              def TauCeti.Comodule.Hom.trivialEquiv {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring C] [Bialgebra R C] :
              Hom R C M N ≃ (M →ₗ[R] N)

              Comodule morphisms between trivial comodules are exactly ordinary linear maps.

              Equations
              Instances For
                source
                @[simp]
                theorem TauCeti.Comodule.Hom.trivialEquiv_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring C] [Bialgebra R C] (f : Hom R C M N) :
                trivialEquiv f = f.toLinearMap

                Applying trivialEquiv returns the underlying linear map.

                source
                @[simp]
                theorem TauCeti.Comodule.Hom.trivialEquiv_symm_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring C] [Bialgebra R C] (f : M →ₗ[R] N) :
                trivialEquiv.symm f = ofTrivial f

                The inverse of trivialEquiv sends a linear map to the corresponding morphism of trivial comodules.

                source
                theorem TauCeti.Comodule.Hom.trivialEquiv_symm_apply_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring C] [Bialgebra R C] (f : M →ₗ[R] N) (m : M) :
                (trivialEquiv.symm f) m = f m

                Pointwise form of trivialEquiv_symm_apply.

                source
                @[reducible, inline]
                abbrev TauCeti.ComoduleCat.trivial (R : Type u) (C : Type v) [CommSemiring R] [Semiring C] [Bialgebra R C] :
                ComoduleCat R C

                The bundled trivial right comodule over a bialgebra.

                This is the tensor-unit candidate for the monoidal category of right comodules: its underlying R-module is R, and its coaction is r ↦ r ⊗ 1.

                Equations
                Instances For