Additive structure on comodule morphisms

This file records the pointwise additive-monoid structure on morphisms of right comodules. The underlying linear maps already have zero, addition, natural-number scalar multiplication, and finite sums; the only point to check is that these operations still commute with the coactions.

This is basic infrastructure for the reductive-groups roadmap Layer 1 target "Comodules over a coalgebra/Hopf algebra": the representation category of an affine group scheme should have additive hom-sets before finite-dimensional, tensor, and dual structures are built on top.

@[instance_reducible]

instance TauCeti.Comodule.Hom.instZero {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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] : Zero (Hom R C M N)

The zero morphism of right comodules.

Equations

• TauCeti.Comodule.Hom.instZero = { zero := let __LinearMap := 0; { toLinearMap := __LinearMap, map_coact := ⋯ } }

@[instance_reducible]

instance TauCeti.Comodule.Hom.instAdd {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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] : Add (Hom R C M N)

Addition of right-comodule morphisms, defined pointwise.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.Comodule.Hom.instSMul {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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] : SMul R (Hom R C M N)

Scalar multiplication of right-comodule morphisms, defined pointwise.

Equations

• TauCeti.Comodule.Hom.instSMul = { smul := fun (r : R) (f : TauCeti.Comodule.Hom R C M N) => let __LinearMap := r • f.toLinearMap; { toLinearMap := __LinearMap, map_coact := ⋯ } }

@[simp]

theorem TauCeti.Comodule.Hom.zero_toLinearMap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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] : toLinearMap 0 = 0

The zero comodule morphism has the zero linear map underneath.

@[simp]

theorem TauCeti.Comodule.Hom.add_toLinearMap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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

Addition of comodule morphisms is addition of the underlying linear maps.

@[simp]

theorem TauCeti.Comodule.Hom.smul_toLinearMap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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] (r : R) (f : Hom R C M N) : (r • f).toLinearMap = r • f.toLinearMap

Scalar multiplication of comodule morphisms is scalar multiplication of the underlying linear maps.

@[simp]

theorem TauCeti.Comodule.Hom.zero_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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] (m : M) : 0 m = 0

The zero comodule morphism evaluates to zero.

@[simp]

theorem TauCeti.Comodule.Hom.add_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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

Addition of comodule morphisms is pointwise addition.

@[simp]

theorem TauCeti.Comodule.Hom.smul_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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] (r : R) (f : Hom R C M N) (m : M) : (r • f) m = r • f m

Scalar multiplication of comodule morphisms is pointwise scalar multiplication.

@[instance_reducible]

instance TauCeti.Comodule.Hom.instAddCommMonoid {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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] : AddCommMonoid (Hom R C M N)

Comodule morphisms form an additive commutative monoid under pointwise zero and addition, with the default natural-number scalar multiplication nsmulRec.

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.Comodule.Hom.toLinearMapAddMonoidHom {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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] : Hom R C M N →+ M →ₗ[R] N

The map sending a comodule morphism to its underlying linear map, bundled as an additive monoid homomorphism.

Equations

• TauCeti.Comodule.Hom.toLinearMapAddMonoidHom = { toFun := fun (f : TauCeti.Comodule.Hom R C M N) => f.toLinearMap, map_zero' := ⋯, map_add' := ⋯ }

@[instance_reducible]

instance TauCeti.Comodule.Hom.instModule {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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] : Module R (Hom R C M N)

Comodule morphisms form an R-module under pointwise scalar multiplication.

Equations

• TauCeti.Comodule.Hom.instModule = { toSMul := TauCeti.Comodule.Hom.instSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[simp]

theorem TauCeti.Comodule.Hom.nsmul_toLinearMap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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] (n : ℕ) (f : Hom R C M N) : (n • f).toLinearMap = n • f.toLinearMap

Natural-number scalar multiplication of comodule morphisms is natural-number scalar multiplication of the underlying linear maps.

@[simp]

theorem TauCeti.Comodule.Hom.nsmul_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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] (n : ℕ) (f : Hom R C M N) (m : M) : (n • f) m = n • f m

Natural-number scalar multiplication of comodule morphisms is pointwise.

@[simp]

theorem TauCeti.Comodule.Hom.sum_toLinearMap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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] {ι : Type u_1} (s : Finset ι) (f : ι → Hom R C M N) : (∑ i ∈ s, f i).toLinearMap = ∑ i ∈ s, (f i).toLinearMap

Finite sums of comodule morphisms are finite sums of the underlying linear maps.

@[simp]

theorem TauCeti.Comodule.Hom.sum_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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] {ι : Type u_1} (s : Finset ι) (f : ι → Hom R C M N) (m : M) : (∑ i ∈ s, f i) m = ∑ i ∈ s, (f i) m

Finite sums of comodule morphisms are evaluated pointwise.

@[simp]

theorem TauCeti.Comodule.Hom.add_comp {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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 additive in the left argument.

@[simp]

theorem TauCeti.Comodule.Hom.comp_add {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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 additive in the right argument.

@[simp]

theorem TauCeti.Comodule.Hom.smul_comp {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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] (r : R) (g : Hom R C N P) (f : Hom R C M N) : (r • g).comp f = r • g.comp f

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

@[simp]

theorem TauCeti.Comodule.Hom.comp_smul {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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] (r : R) (g : Hom R C N P) (f : Hom R C M N) : g.comp (r • f) = r • g.comp f

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

@[simp]

theorem TauCeti.Comodule.Hom.zero_comp {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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] (f : Hom R C M N) : comp 0 f = 0

Composing the zero morphism on the left gives the zero morphism.

@[simp]

theorem TauCeti.Comodule.Hom.comp_zero {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring 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) : g.comp 0 = 0

Composing the zero morphism on the right gives the zero morphism.