Projections along complementary subcomodules

Complementary subcomodules determine a projection of the ambient comodule onto either complement. This file equips the underlying Submodule.projection with the proof that it commutes with the coaction.

Main declarations

• TauCeti.Subcomodule.projection: the comodule projection onto a subcomodule along a complementary subcomodule.

noncomputable def TauCeti.Subcomodule.projection {R : Type u} {C : Type v} {V : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup V] [Module R V] [Comodule R C V] (W Q : Subcomodule R C V) (h : IsCompl W.toSubmodule Q.toSubmodule) : Comodule.Hom R C V V

The projection onto a subcomodule W along a complementary subcomodule Q, as a comodule endomorphism. Its underlying linear map is Submodule.projection.

Equations

• W.projection Q h = { toLinearMap := W.toSubmodule.projection Q.toSubmodule h, map_coact := ⋯ }

@[simp]

theorem TauCeti.Subcomodule.projection_toLinearMap {R : Type u} {C : Type v} {V : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup V] [Module R V] [Comodule R C V] (W Q : Subcomodule R C V) (h : IsCompl W.toSubmodule Q.toSubmodule) : (W.projection Q h).toLinearMap = W.toSubmodule.projection Q.toSubmodule h

The underlying linear map of TauCeti.Subcomodule.projection is the linear projection Submodule.projection.

@[simp]

theorem TauCeti.Subcomodule.projection_apply_mem {R : Type u} {C : Type v} {V : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup V] [Module R V] [Comodule R C V] {W Q : Subcomodule R C V} (h : IsCompl W.toSubmodule Q.toSubmodule) (v : V) : (W.projection Q h) v ∈ W

The projection onto W along Q takes values in W.

@[simp]

theorem TauCeti.Subcomodule.projection_apply_of_mem_left {R : Type u} {C : Type v} {V : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup V] [Module R V] [Comodule R C V] {W Q : Subcomodule R C V} (h : IsCompl W.toSubmodule Q.toSubmodule) {v : V} (hv : v ∈ W) : (W.projection Q h) v = v

The projection onto W along Q fixes W pointwise.

@[simp]

theorem TauCeti.Subcomodule.projection_apply_of_mem_right {R : Type u} {C : Type v} {V : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup V] [Module R V] [Comodule R C V] {W Q : Subcomodule R C V} (h : IsCompl W.toSubmodule Q.toSubmodule) {v : V} (hv : v ∈ Q) : (W.projection Q h) v = 0

The projection onto W along Q vanishes on Q.