Theorems · Definition · category theory

CoalgCat.of

(R : Type u) →
  [inst : CommRing R] → (X : Type v) → [inst_1 : AddCommGroup X] → [inst_2 : Module R X] → [Coalgebra R X] → CoalgCat R

The object in the category of R-coalgebras associated to an R-coalgebra.

Defined in

Mathlib.Algebra.Category.CoalgCat.Basic

Cited by

24 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

CommRingAddCommGroupModuleCoalgebra