Documentation

TauCeti.Algebra.Coalgebra.Comodule.Zero

The zero comodule #

This file adds the zero object for right comodules over a coalgebra. This is Layer 1 infrastructure for the reductive-groups roadmap target "Comodules over a coalgebra/Hopf algebra": before the finite-dimensional comodule category can be used as the additive representation category, it needs the standard zero object compatible with the existing zero morphisms.

The zero comodule is implemented by the unique coaction on PUnit. The bundled API exposes the named zero objects through their IsZero characterizations, rather than through the concrete carrier.

Main declarations #

References #

The construction is the standard zero object in the category of comodules; see Sweedler, Hopf Algebras, Chapter 2. It supplies an additive-category prerequisite for ReductiveGroups/README.md in TauCetiRoadmap, Layer 1, "Comodules over a coalgebra/Hopf algebra". The proof that a subsingleton bundled comodule is zero follows Mathlib's SemimoduleCat.isZero_of_subsingleton / ModuleCat.isZero_of_subsingleton pattern.

source
@[instance_reducible]
instance TauCeti.Comodule.instPUnit (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] :
Comodule R C PUnit.{u_1 + 1}

The unique right-comodule structure on the zero module PUnit.

Equations
source
def TauCeti.ComoduleCat.zero (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] :
ComoduleCat R C

The bundled zero right comodule.

Equations
Instances For
    source
    theorem TauCeti.ComoduleCat.subsingleton_zero (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] :
    Subsingleton ↑(zero R C).toSemimoduleCat

    The named zero comodule has subsingleton carrier.

    source
    theorem TauCeti.ComoduleCat.isZero_of_subsingleton (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : ComoduleCat R C) [Subsingleton ↑M.toSemimoduleCat] :
    CategoryTheory.Limits.IsZero M

    A comodule whose underlying type is subsingleton is a zero object.

    source
    theorem TauCeti.ComoduleCat.isZero_zero (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] :
    CategoryTheory.Limits.IsZero (zero R C)

    The named zero comodule is a zero object.

    source
    theorem TauCeti.ComoduleCat.zero_hom_eq_zero (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : ComoduleCat R C) (f : zero R C ⟶ M) :
    f = 0

    Any morphism from the named zero comodule is zero.

    source
    theorem TauCeti.ComoduleCat.hom_zero_eq_zero (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : ComoduleCat R C) (f : M ⟶ zero R C) :
    f = 0

    Any morphism to the named zero comodule is zero.

    source
    @[simp]
    theorem TauCeti.ComoduleCat.isZero_zero_to (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : ComoduleCat R C) :
    ⋯.to_ M = 0

    The canonical morphism out of the named zero comodule is the zero morphism.

    source
    @[simp]
    theorem TauCeti.ComoduleCat.isZero_zero_from (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : ComoduleCat R C) :
    ⋯.from_ M = 0

    The canonical morphism into the named zero comodule is the zero morphism.

    source
    theorem TauCeti.ComoduleCat.zero_hom_ext (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : ComoduleCat R C} (f g : zero R C ⟶ M) :
    f = g

    Morphisms from the named zero comodule are unique.

    source
    theorem TauCeti.ComoduleCat.zero_hom_ext_iff {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : ComoduleCat R C} {f g : zero R C ⟶ M} :
    f = g ↔ True
    source
    theorem TauCeti.ComoduleCat.hom_zero_ext (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : ComoduleCat R C} (f g : M ⟶ zero R C) :
    f = g

    Morphisms to the named zero comodule are unique.

    source
    theorem TauCeti.ComoduleCat.hom_zero_ext_iff {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : ComoduleCat R C} {f g : M ⟶ zero R C} :
    f = g ↔ True
    source
    instance TauCeti.ComoduleCat.hasZeroObject (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] :
    CategoryTheory.Limits.HasZeroObject (ComoduleCat R C)

    The category of right comodules has a zero object.