Images of subcoalgebras

This file proves that coalgebra morphisms send subcoalgebras to subcoalgebras. The underlying submodule of the image is the ordinary image of the underlying submodule.

Images preserve finite generation, allowing finite subcoalgebras to be transported along coalgebra morphisms.

Main declarations

• TauCeti.Subcoalgebra.map: the image of a subcoalgebra under a coalgebra morphism.
• TauCeti.Subcoalgebra.mem_map: membership in an image subcoalgebra.
• TauCeti.Subcoalgebra.map_finite: finite generation is preserved by image.

References

This uses the standard fact that a coalgebra morphism preserves comultiplication, so the image of a subcoalgebra is again a subcoalgebra. See Sweedler, Hopf Algebras, Chapter 2.

def TauCeti.Subcoalgebra.map {R : Type u} {C : Type v} {D : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) (A : Subcoalgebra R C) : Subcoalgebra R D

The image of a subcoalgebra under a coalgebra morphism.

Equations

• TauCeti.Subcoalgebra.map f A = { carrier := Submodule.map f.toLinearMap A.carrier, comul_mem' := ⋯ }

@[simp]

theorem TauCeti.Subcoalgebra.map_toSubmodule {R : Type u} {C : Type v} {D : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) (A : Subcoalgebra R C) : (map f A).toSubmodule = Submodule.map f.toLinearMap A.toSubmodule

The underlying submodule of the image subcoalgebra is the image of the underlying submodule.

theorem TauCeti.Subcoalgebra.mem_map {R : Type u} {C : Type v} {D : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] {f : C →ₗc[R] D} {A : Subcoalgebra R C} {d : D} : d ∈ map f A ↔ ∃ c ∈ A, f c = d

Membership in the image subcoalgebra.

theorem TauCeti.Subcoalgebra.mem_map_of_mem {R : Type u} {C : Type v} {D : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) {A : Subcoalgebra R C} {c : C} (hc : c ∈ A) : f c ∈ map f A

The image of an element of a subcoalgebra belongs to the image subcoalgebra.

theorem TauCeti.Subcoalgebra.map_le_iff {R : Type u} {C : Type v} {D : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] {f : C →ₗc[R] D} {A : Subcoalgebra R C} {B : Subcoalgebra R D} : map f A ≤ B ↔ ∀ ⦃c : C⦄, c ∈ A → f c ∈ B

The image subcoalgebra is contained in B exactly when each image of an element of the source subcoalgebra belongs to B.

theorem TauCeti.Subcoalgebra.map_mono {R : Type u} {C : Type v} {D : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) {A B : Subcoalgebra R C} (hAB : A ≤ B) : map f A ≤ map f B

The image construction is monotone in the source subcoalgebra.

@[simp]

theorem TauCeti.Subcoalgebra.map_bot {R : Type u} {C : Type v} {D : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) : map f ⊥ = ⊥

The image of the bottom subcoalgebra is bottom.

@[simp]

theorem TauCeti.Subcoalgebra.map_top_toSubmodule {R : Type u} {C : Type v} {D : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) : (map f ⊤).toSubmodule = f.range

The image of the top subcoalgebra is the range of the coalgebra morphism as a submodule.

@[simp]

theorem TauCeti.Subcoalgebra.map_id {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (A : Subcoalgebra R C) : map (CoalgHom.id R C) A = A

The identity coalgebra morphism leaves a subcoalgebra unchanged.

@[simp]

theorem TauCeti.Subcoalgebra.map_map {R : Type u} {C : Type v} {D : Type w} {E : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] [AddCommMonoid E] [Module R E] [Coalgebra R E] (A : Subcoalgebra R C) (f : C →ₗc[R] D) (g : D →ₗc[R] E) : map g (map f A) = map (g.comp f) A

Images of subcoalgebras compose with coalgebra morphisms.

@[simp]

theorem TauCeti.Subcoalgebra.map_sup {R : Type u} {C : Type v} {D : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) (A B : Subcoalgebra R C) : map f (A ⊔ B) = map f A ⊔ map f B

The image of a binary join is the binary join of the images.

@[simp]

theorem TauCeti.Subcoalgebra.map_iSup {R : Type u} {C : Type v} {D : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] {ι : Sort u_1} (f : C →ₗc[R] D) (A : ι → Subcoalgebra R C) : map f (⨆ (i : ι), A i) = ⨆ (i : ι), map f (A i)

The image of a supremum is the supremum of the images.

@[simp]

theorem TauCeti.Subcoalgebra.map_finset_sup {R : Type u} {C : Type v} {D : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] {ι : Type u_1} (s : Finset ι) (f : C →ₗc[R] D) (A : ι → Subcoalgebra R C) : map f (s.sup A) = s.sup fun (i : ι) => map f (A i)

The image of a finite join is the finite join of the images.

theorem TauCeti.Subcoalgebra.map_finite {R : Type u} {C : Type v} {D : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) (A : Subcoalgebra R C) [Module.Finite R ↥A.toSubmodule] : Module.Finite R ↥(map f A).toSubmodule

The image of a finitely generated subcoalgebra is finitely generated as an R-module.