Subcoalgebras as subcomodules of the regular comodule

Every subcoalgebra of a coalgebra is, by the same underlying submodule, a subcomodule of the regular right comodule. This file records that bridge and its basic order and finiteness API.

This is a Layer 1 prerequisite for the reductive-groups roadmap target on finite-dimensional subcoalgebras and subcomodules: once an element is placed in a finite-dimensional subcoalgebra, the same object is available as a finite-dimensional subcomodule of the regular comodule.

Main declarations

• TauCeti.Subcoalgebra.toRegularSubcomodule: a subcoalgebra as a subcomodule of the regular comodule.
• TauCeti.Subcoalgebra.toRegularSubcomoduleOrderEmbedding: the construction is order reflecting.
• Compatibility with ⊥, ⊤, binary joins, arbitrary joins, and finite generation.

References

This follows immediately from the standard definitions: if Δ(D) ⊆ D ⊗ D, then certainly Δ(D) ⊆ D ⊗ C, so D is a subcomodule of the regular comodule. The definitions of subcoalgebra and subcomodule follow Sweedler, Hopf Algebras, Chapter 2.

def TauCeti.Subcoalgebra.toRegularSubcomodule {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (D : Subcoalgebra R C) : Subcomodule R C C

A subcoalgebra as a subcomodule of the regular right comodule.

The underlying submodule is unchanged; the map D ⊗ D → C ⊗ C factors through D ⊗ C → C ⊗ C by including the second tensor factor.

Equations

• D.toRegularSubcomodule = { carrier := D.toSubmodule, coact_mem' := ⋯ }

@[simp]

theorem TauCeti.Subcoalgebra.toRegularSubcomodule_toSubmodule {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (D : Subcoalgebra R C) : D.toRegularSubcomodule.toSubmodule = D.toSubmodule

The underlying submodule is unchanged when a subcoalgebra is viewed as a subcomodule of the regular comodule.

@[simp]

theorem TauCeti.Subcoalgebra.mem_toRegularSubcomodule {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {D : Subcoalgebra R C} {c : C} : c ∈ D.toRegularSubcomodule ↔ c ∈ D

Membership is unchanged when a subcoalgebra is viewed as a subcomodule of the regular comodule.

theorem TauCeti.Subcoalgebra.toRegularSubcomodule_mono {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {D E : Subcoalgebra R C} (hDE : D ≤ E) : D.toRegularSubcomodule ≤ E.toRegularSubcomodule

Viewing a subcoalgebra as a regular subcomodule is monotone.

def TauCeti.Subcoalgebra.toRegularSubcomoduleOrderEmbedding {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : Subcoalgebra R C ↪o Subcomodule R C C

Viewing subcoalgebras as regular subcomodules is an order embedding.

Equations

• TauCeti.Subcoalgebra.toRegularSubcomoduleOrderEmbedding = { toFun := TauCeti.Subcoalgebra.toRegularSubcomodule, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem TauCeti.Subcoalgebra.toRegularSubcomoduleOrderEmbedding_apply {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (D : Subcoalgebra R C) : toRegularSubcomoduleOrderEmbedding D = D.toRegularSubcomodule

Applying the order embedding from subcoalgebras to regular subcomodules gives toRegularSubcomodule.

@[simp]

theorem TauCeti.Subcoalgebra.toRegularSubcomodule_bot {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : ⊥.toRegularSubcomodule = ⊥

The bottom subcoalgebra is the bottom regular subcomodule.

@[simp]

theorem TauCeti.Subcoalgebra.toRegularSubcomodule_top {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : ⊤.toRegularSubcomodule = ⊤

The top subcoalgebra is the top regular subcomodule.

@[simp]

theorem TauCeti.Subcoalgebra.toRegularSubcomodule_sup {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (D E : Subcoalgebra R C) : (D ⊔ E).toRegularSubcomodule = D.toRegularSubcomodule ⊔ E.toRegularSubcomodule

Viewing subcoalgebras as regular subcomodules preserves binary joins.

@[simp]

theorem TauCeti.Subcoalgebra.toRegularSubcomodule_iSup {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {ι : Sort u_1} (D : ι → Subcoalgebra R C) : (⨆ (i : ι), D i).toRegularSubcomodule = ⨆ (i : ι), (D i).toRegularSubcomodule

Viewing subcoalgebras as regular subcomodules preserves arbitrary joins.

@[simp]

theorem TauCeti.Subcoalgebra.toRegularSubcomodule_sSup {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (S : Set (Subcoalgebra R C)) : (sSup S).toRegularSubcomodule = ⨆ (D : ↑S), (↑D).toRegularSubcomodule

Viewing subcoalgebras as regular subcomodules preserves set-indexed suprema.

@[simp]

theorem TauCeti.Subcoalgebra.toRegularSubcomodule_finset_sup {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {ι : Type u_1} (s : Finset ι) (D : ι → Subcoalgebra R C) : (s.sup D).toRegularSubcomodule = s.sup fun (i : ι) => (D i).toRegularSubcomodule

Viewing subcoalgebras as regular subcomodules preserves finite joins.

theorem TauCeti.Subcoalgebra.toRegularSubcomodule_finite {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (D : Subcoalgebra R C) [Module.Finite R ↥D.toSubmodule] : Module.Finite R ↥D.toRegularSubcomodule.toSubmodule

A finite subcoalgebra is finite as a regular subcomodule.

instance TauCeti.Subcoalgebra.instFiniteToRegularSubcomodule {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (D : Subcoalgebra R C) [Module.Finite R ↥D.toSubmodule] : Module.Finite R ↥D.toRegularSubcomodule.toSubmodule

A finite subcoalgebra is finite as a regular subcomodule.