Documentation

TauCeti.Algebra.Coalgebra.Comodule.Preadditive

Preadditive structure on comodule categories #

This file records the additive-group structure on morphisms of right comodules over a coalgebra over a commutative ring, and uses it to make the bundled comodule category preadditive. It also provides the faithful additive forgetful functor to ModuleCat R.

The semiring-level files already show that comodule morphisms are closed under zero, addition, scalar multiplication, and finite sums. Over a ring, every semimodule is an additive group by Module.addCommMonoidToAddCommGroup; the same pointwise operations also give negatives and subtraction of comodule morphisms. This is the categorical additive infrastructure needed before the reductive-groups roadmap's finite-dimensional comodule representation category can be developed.

Main declarations #

References #

This supplies a prerequisite for ReductiveGroups/README.md in TauCetiRoadmap, Layer 1 target "Comodules over a coalgebra/Hopf algebra": the finite-dimensional comodule representation category should be an additive category before tensor products, duals, and Tannakian structure are built on top.

source
@[instance_reducible]
instance TauCeti.Comodule.Hom.instAddCommGroup {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] :
AddCommGroup (Hom R C M N)

Comodule morphisms over a commutative ring form an additive commutative group under pointwise operations.

Equations
source
@[simp]
theorem TauCeti.Comodule.Hom.neg_toLinearMap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) :
(-f).toLinearMap = -f.toLinearMap

Negation of comodule morphisms is negation of the underlying linear maps.

source
@[simp]
theorem TauCeti.Comodule.Hom.sub_toLinearMap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f g : Hom R C M N) :
(f - g).toLinearMap = f.toLinearMap - g.toLinearMap

Subtraction of comodule morphisms is subtraction of the underlying linear maps.

source
@[simp]
theorem TauCeti.Comodule.Hom.zsmul_toLinearMap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (z : ℤ) (f : Hom R C M N) :
(z • f).toLinearMap = z • f.toLinearMap

Integer scalar multiplication of comodule morphisms is integer scalar multiplication of the underlying linear maps.

source
@[simp]
theorem TauCeti.Comodule.Hom.neg_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) (m : M) :
(-f) m = -f m

Negation of comodule morphisms is pointwise negation.

source
@[simp]
theorem TauCeti.Comodule.Hom.sub_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f g : Hom R C M N) (m : M) :
(f - g) m = f m - g m

Subtraction of comodule morphisms is pointwise subtraction.

source
@[simp]
theorem TauCeti.Comodule.Hom.zsmul_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (z : ℤ) (f : Hom R C M N) (m : M) :
(z • f) m = z • f m

Integer scalar multiplication of comodule morphisms is pointwise.

source
@[simp]
theorem TauCeti.Comodule.Hom.neg_comp {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (g : Hom R C N P) (f : Hom R C M N) :
(-g).comp f = -g.comp f

Composition of comodule morphisms is compatible with negation in the left argument.

source
@[simp]
theorem TauCeti.Comodule.Hom.comp_neg {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (g : Hom R C N P) (f : Hom R C M N) :
g.comp (-f) = -g.comp f

Composition of comodule morphisms is compatible with negation in the right argument.

source
@[simp]
theorem TauCeti.Comodule.Hom.sub_comp {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (g h : Hom R C N P) (f : Hom R C M N) :
(g - h).comp f = g.comp f - h.comp f

Composition of comodule morphisms is subtractive in the left argument.

source
@[simp]
theorem TauCeti.Comodule.Hom.comp_sub {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (g : Hom R C N P) (f h : Hom R C M N) :
g.comp (f - h) = g.comp f - g.comp h

Composition of comodule morphisms is subtractive in the right argument.

source
@[instance_reducible]
instance TauCeti.ComoduleCat.instAddCommGroupCarrier (R : Type u) [CommRing R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : ComoduleCat R C) :
AddCommGroup ↑M.toSemimoduleCat

A bundled comodule over a ring has an additive group as its underlying module.

Equations
source
@[instance_reducible]
instance TauCeti.ComoduleCat.homAddCommGroup (R : Type u) [CommRing R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) :
AddCommGroup (M ⟶ N)

Categorical morphisms form an additive commutative group over a commutative ring.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem TauCeti.ComoduleCat.toLinearMap_neg (R : Type u) [CommRing R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f : M ⟶ N) :
(-f).toLinearMap = -f.toLinearMap

Negation of morphisms is negation of the underlying linear maps.

source
@[simp]
theorem TauCeti.ComoduleCat.toLinearMap_sub (R : Type u) [CommRing R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f g : M ⟶ N) :
(f - g).toLinearMap = f.toLinearMap - g.toLinearMap

Subtraction of morphisms is subtraction of the underlying linear maps.

source
@[simp]
theorem TauCeti.ComoduleCat.toLinearMap_zsmul (R : Type u) [CommRing R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (z : ℤ) (f : M ⟶ N) :
(z • f).toLinearMap = z • f.toLinearMap

Integer scalar multiplication of morphisms is integer scalar multiplication of the underlying linear maps.

source
@[simp]
theorem TauCeti.ComoduleCat.neg_apply (R : Type u) [CommRing R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f : M ⟶ N) (m : ↑M.toSemimoduleCat) :
(CategoryTheory.ConcreteCategory.hom (-f)) m = -(CategoryTheory.ConcreteCategory.hom f) m

Negation of morphisms acts by pointwise negation.

source
@[simp]
theorem TauCeti.ComoduleCat.sub_apply (R : Type u) [CommRing R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f g : M ⟶ N) (m : ↑M.toSemimoduleCat) :
(CategoryTheory.ConcreteCategory.hom (f - g)) m = (CategoryTheory.ConcreteCategory.hom f) m - (CategoryTheory.ConcreteCategory.hom g) m

Subtraction of morphisms acts by pointwise subtraction.

source
@[simp]
theorem TauCeti.ComoduleCat.zsmul_apply (R : Type u) [CommRing R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (z : ℤ) (f : M ⟶ N) (m : ↑M.toSemimoduleCat) :
(CategoryTheory.ConcreteCategory.hom (z • f)) m = z • (CategoryTheory.ConcreteCategory.hom f) m

Integer scalar multiplication of morphisms acts pointwise.

source
@[instance_reducible]
instance TauCeti.ComoduleCat.preadditive (R : Type u) [CommRing R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] :
CategoryTheory.Preadditive (ComoduleCat R C)

The category of right comodules over a coalgebra over a commutative ring is preadditive.

Equations
  • One or more equations did not get rendered due to their size.
source
@[instance_reducible]
noncomputable instance TauCeti.ComoduleCat.instHasForget₂HomCarrierModuleCatLinearMapIdCarrier {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] :
CategoryTheory.HasForget₂ (ComoduleCat R C) (ModuleCat R)

Forget a comodule over a ring to its underlying module.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem TauCeti.ComoduleCat.forget₂_moduleCat_map {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f : M ⟶ N) :
ModuleCat.Hom.hom ((CategoryTheory.forget₂ (ComoduleCat R C) (ModuleCat R)).map f) = f.toLinearMap

The underlying linear map of a forgotten comodule morphism.

source
instance TauCeti.ComoduleCat.instFaithfulModuleCatForget₂HomCarrierLinearMapIdCarrier {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] :
(CategoryTheory.forget₂ (ComoduleCat R C) (ModuleCat R)).Faithful
source
instance TauCeti.ComoduleCat.instAdditiveModuleCatForget₂HomCarrierLinearMapIdCarrier {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] :
(CategoryTheory.forget₂ (ComoduleCat R C) (ModuleCat R)).Additive