Subcoalgebras spanned by group-like elements

This file defines the subcoalgebra spanned by a set of group-like elements, together with the singleton span, a finite-generation theorem for finite sets of group-like elements, and a Module.Finite instance for singleton spans.

The subcoalgebra spanned by all group-like elements is the full subcoalgebra exactly when the group-like elements span the carrier as a module, a condition invariant under coalgebra equivalence. Over a domain the group-like elements are linearly independent, so they then form a basis, groupLikeBasis.

References

This file uses the GroupLike and IsGroupLikeElem API from Mathlib.RingTheory.Coalgebra.GroupLike, by Yaël Dillies and Michał Mrugała.

def TauCeti.Subcoalgebra.groupLikeSetSpan {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (s : Set (GroupLike R C)) : Subcoalgebra R C

The subcoalgebra spanned by a set of group-like elements.

Equations

• TauCeti.Subcoalgebra.groupLikeSetSpan s = { carrier := Submodule.span R (GroupLike.val '' s), comul_mem' := ⋯ }

@[simp]

theorem TauCeti.Subcoalgebra.groupLikeSetSpan_toSubmodule {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (s : Set (GroupLike R C)) : (groupLikeSetSpan s).toSubmodule = Submodule.span R (GroupLike.val '' s)

The underlying submodule of the subcoalgebra spanned by a set of group-like elements is the linear span of their underlying elements.

@[simp]

theorem TauCeti.Subcoalgebra.mem_groupLikeSetSpan {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {s : Set (GroupLike R C)} {c : C} : c ∈ groupLikeSetSpan s ↔ c ∈ Submodule.span R (GroupLike.val '' s)

theorem TauCeti.Subcoalgebra.groupLike_mem_groupLikeSetSpan {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {s : Set (GroupLike R C)} {g : GroupLike R C} (hg : g ∈ s) : ↑g ∈ groupLikeSetSpan s

A group-like element in the generating set belongs to the subcoalgebra it spans.

theorem TauCeti.Subcoalgebra.groupLikeSetSpan_le {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {s : Set (GroupLike R C)} {D : Subcoalgebra R C} : groupLikeSetSpan s ≤ D ↔ ∀ g ∈ s, ↑g ∈ D

Universal property for subcoalgebras spanned by a set of group-like elements.

theorem TauCeti.Subcoalgebra.groupLikeSetSpan_mono {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {s t : Set (GroupLike R C)} (hst : s ⊆ t) : groupLikeSetSpan s ≤ groupLikeSetSpan t

Monotonicity of the subcoalgebra spanned by a set of group-like elements.

theorem TauCeti.Subcoalgebra.groupLikeSetSpan_eq_top_iff_span_eq_top {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : groupLikeSetSpan Set.univ = ⊤ ↔ Submodule.span R (Set.range GroupLike.val) = ⊤

The subcoalgebra spanned by all group-like elements is the full subcoalgebra exactly when the underlying group-like elements span the carrier as a module.

theorem TauCeti.Subcoalgebra.groupLikeSetSpan_eq_top_iff_of_coalgEquiv {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {D : Type w} [AddCommMonoid D] [Module R D] [Coalgebra R D] (e : C ≃ₗc[R] D) : groupLikeSetSpan Set.univ = ⊤ ↔ groupLikeSetSpan Set.univ = ⊤

A coalgebra equivalence preserves the property that the group-like elements span the whole carrier.

def TauCeti.Subcoalgebra.groupLikeSpan {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) : Subcoalgebra R C

The subcoalgebra spanned by a group-like element.

Equations

• TauCeti.Subcoalgebra.groupLikeSpan g = TauCeti.Subcoalgebra.groupLikeSetSpan {g}

theorem TauCeti.Subcoalgebra.groupLikeSpan_le {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {g : GroupLike R C} {D : Subcoalgebra R C} : groupLikeSpan g ≤ D ↔ ↑g ∈ D

Universal property for the subcoalgebra spanned by one group-like element.

@[simp]

theorem TauCeti.Subcoalgebra.groupLikeSpan_toSubmodule {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) : (groupLikeSpan g).toSubmodule = R ∙ ↑g

The underlying submodule of the subcoalgebra spanned by one group-like element is the submodule generated by (g : C).

theorem TauCeti.Subcoalgebra.groupLike_mem_groupLikeSpan {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) : ↑g ∈ groupLikeSpan g

A group-like element belongs to its span subcoalgebra.

@[simp]

theorem TauCeti.Subcoalgebra.mem_groupLikeSpan {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {g : GroupLike R C} {c : C} : c ∈ groupLikeSpan g ↔ ∃ (r : R), r • ↑g = c

Membership in the subcoalgebra spanned by a group-like element.

theorem TauCeti.Subcoalgebra.groupLikeSetSpan_finite {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (s : Set (GroupLike R C)) (hs : s.Finite) : Module.Finite R ↥(groupLikeSetSpan s).toSubmodule

A subcoalgebra spanned by a finite set of group-like elements is finitely generated.

instance TauCeti.Subcoalgebra.groupLikeSpan_finite {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) : Module.Finite R ↥(groupLikeSpan g).toSubmodule

The underlying submodule of the subcoalgebra spanned by one group-like element is finitely generated.

noncomputable def TauCeti.Subcoalgebra.groupLikeBasis {S : Type u} {D : Type v} [CommRing S] [IsDomain S] [AddCommGroup D] [Module S D] [Module.IsTorsionFree S D] [Coalgebra S D] (h : groupLikeSetSpan Set.univ = ⊤) : Module.Basis (GroupLike S D) S D

Over a domain, the group-like elements of a torsion-free coalgebra that they span form a basis of it.

Equations

• TauCeti.Subcoalgebra.groupLikeBasis h = Module.Basis.mk ⋯ ⋯

@[simp]

theorem TauCeti.Subcoalgebra.groupLikeBasis_apply {S : Type u} {D : Type v} [CommRing S] [IsDomain S] [AddCommGroup D] [Module S D] [Module.IsTorsionFree S D] [Coalgebra S D] (h : groupLikeSetSpan Set.univ = ⊤) (g : GroupLike S D) : (groupLikeBasis h) g = ↑g

The basis vector of groupLikeBasis indexed by a group-like element is that element.