Subcoalgebras

This file defines subcoalgebras of a coalgebra as submodules whose elements have comultiplication in the tensor square of the submodule. It is deliberately a lightweight predicate-style API: over a general commutative semiring, the map D ⊗ D → C ⊗ C need not be known injective, so the induced coalgebra structure on D is not registered here.

This is a Layer 1 prerequisite for the reductive-groups roadmap target on finite-dimensional subcoalgebras and the fundamental theorem of comodules. Later work can use Module.Finite R D.toSubmodule to state finitely generated subcoalgebras.

Main definitions

• TauCeti.Subcoalgebra: a submodule stable under comultiplication.
• TauCeti.Subcoalgebra.toSubmodule: the underlying submodule.
• ⊤ and ⊥: the full and zero subcoalgebras.

References

This follows the standard coalgebra definition: a subcoalgebra D ≤ C satisfies Δ(D) ⊆ D ⊗ D. See Sweedler, Hopf Algebras, Chapter 2.

theorem TauCeti.Subcoalgebra.comul_mem_tensorSquare_top {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] (c : C) : CoalgebraStruct.comul c ∈ (TensorProduct.map ⊤.subtype ⊤.subtype).range

The comultiplication of any element lies in the tensor square of the top submodule, because the inclusion of ⊤ is surjective.

Only the comultiplication map is involved, not the coalgebra axioms, so this is stated over CoalgebraStruct; it is what makes ⊤ a subcoalgebra.

structure TauCeti.Subcoalgebra (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : Type v

A subcoalgebra of an R-coalgebra C.

It is an R-submodule carrier such that the comultiplication of every element of carrier lies in the range of carrier ⊗ carrier → C ⊗ C.

• carrier : Submodule R C

  The underlying submodule of a subcoalgebra.

• comul_mem' ⦃c : C⦄ : c ∈ self.carrier → CoalgebraStruct.comul c ∈ (TensorProduct.map self.carrier.subtype self.carrier.subtype).range

  The comultiplication of an element of the submodule lies in its tensor square.

@[instance_reducible]

instance TauCeti.Subcoalgebra.instSetLike {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : SetLike (Subcoalgebra R C) C

Equations

• TauCeti.Subcoalgebra.instSetLike = { coe := fun (D : TauCeti.Subcoalgebra R C) => ↑D.carrier, coe_injective := ⋯ }

instance TauCeti.Subcoalgebra.instAddSubmonoidClass {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : AddSubmonoidClass (Subcoalgebra R C) C

instance TauCeti.Subcoalgebra.instSMulMemClass {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : SMulMemClass (Subcoalgebra R C) R C

@[instance_reducible]

instance TauCeti.Subcoalgebra.instPartialOrder {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : PartialOrder (Subcoalgebra R C)

Equations

• TauCeti.Subcoalgebra.instPartialOrder = PartialOrder.ofSetLike (TauCeti.Subcoalgebra R C)

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

The underlying submodule of a subcoalgebra.

Equations

• D.toSubmodule = D.carrier

@[simp]

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

@[simp]

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

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

theorem TauCeti.Subcoalgebra.le_def {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {D E : Subcoalgebra R C} : D ≤ E ↔ ∀ ⦃c : C⦄, c ∈ D → c ∈ E

theorem TauCeti.Subcoalgebra.toSubmodule_le_toSubmodule {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {D E : Subcoalgebra R C} : D.toSubmodule ≤ E.toSubmodule ↔ D ≤ E

theorem TauCeti.Subcoalgebra.ext {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {D E : Subcoalgebra R C} (h : ∀ (c : C), c ∈ D ↔ c ∈ E) : D = E

Two subcoalgebras are equal when they contain the same elements.

theorem TauCeti.Subcoalgebra.ext_iff {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {D E : Subcoalgebra R C} : D = E ↔ ∀ (c : C), c ∈ D ↔ c ∈ E

theorem TauCeti.Subcoalgebra.comul_mem {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (D : Subcoalgebra R C) {c : C} (hc : c ∈ D) : CoalgebraStruct.comul c ∈ (TensorProduct.map D.carrier.subtype D.carrier.subtype).range

The comultiplication of an element of a subcoalgebra belongs to its tensor square.

def TauCeti.Subcoalgebra.ofSubmodule {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (D : Submodule R C) (hD : ∀ ⦃c : C⦄, c ∈ D → CoalgebraStruct.comul c ∈ (TensorProduct.map D.subtype D.subtype).range) : Subcoalgebra R C

Constructor from a submodule and the tensor-square stability condition.

Equations

• TauCeti.Subcoalgebra.ofSubmodule D hD = { carrier := D, comul_mem' := hD }

@[simp]

theorem TauCeti.Subcoalgebra.ofSubmodule_carrier {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (D : Submodule R C) (hD : ∀ ⦃c : C⦄, c ∈ D → CoalgebraStruct.comul c ∈ (TensorProduct.map D.subtype D.subtype).range) : (ofSubmodule D hD).carrier = D

@[simp]

theorem TauCeti.Subcoalgebra.mem_ofSubmodule {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {D : Submodule R C} {hD : ∀ ⦃c : C⦄, c ∈ D → CoalgebraStruct.comul c ∈ (TensorProduct.map D.subtype D.subtype).range} {c : C} : c ∈ ofSubmodule D hD ↔ c ∈ D

@[instance_reducible]

instance TauCeti.Subcoalgebra.instTop {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : Top (Subcoalgebra R C)

The full coalgebra as a subcoalgebra.

Equations

• TauCeti.Subcoalgebra.instTop = { top := { carrier := ⊤, comul_mem' := ⋯ } }

@[simp]

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

@[simp]

theorem TauCeti.Subcoalgebra.mem_top {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (c : C) : c ∈ ⊤

@[instance_reducible]

instance TauCeti.Subcoalgebra.instOrderTop {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : OrderTop (Subcoalgebra R C)

Equations

• TauCeti.Subcoalgebra.instOrderTop = { toTop := TauCeti.Subcoalgebra.instTop, le_top := ⋯ }

@[instance_reducible]

instance TauCeti.Subcoalgebra.instBot {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : Bot (Subcoalgebra R C)

The zero submodule as a subcoalgebra.

Equations

• TauCeti.Subcoalgebra.instBot = { bot := { carrier := ⊥, comul_mem' := ⋯ } }

@[simp]

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

@[simp]

theorem TauCeti.Subcoalgebra.mem_bot {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {c : C} : c ∈ ⊥ ↔ c = 0

@[instance_reducible]

instance TauCeti.Subcoalgebra.instOrderBot {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : OrderBot (Subcoalgebra R C)

The zero subcoalgebra is contained in every subcoalgebra.

Equations

• TauCeti.Subcoalgebra.instOrderBot = { toBot := TauCeti.Subcoalgebra.instBot, bot_le := ⋯ }