English
There exists an arbitrarily chosen representation of an element a in a coalgebra, determined by a left projection, a right projection, and a finite witness for the comultiplication of a.
Русский
Существует произвольное представление элемента a в коалгебре, заданное левым и правым проекциям и конечным свидетелем (index) для копуляризации a.
LaTeX
$$\exists \mathrm{repr} : \mathrm{Coalgebra.Repr}(R,a) \,\text{such that } \mathrm{repr.left} = \mathrm{fst}, \mathrm{repr.right} = \mathrm{snd}, \mathrm{repr.index} \,\text{witnesses a finite comultiplication.}$$
Lean4
/-- An arbitrarily chosen representation. -/
noncomputable def arbitrary (R : Type u) {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A]
[CoalgebraStruct R A] (a : A) : Coalgebra.Repr R a
where
left := Prod.fst
right := Prod.snd
index := TensorProduct.exists_finset (R := R) (CoalgebraStruct.comul a) |>.choose
eq := TensorProduct.exists_finset (R := R) (CoalgebraStruct.comul a) |>.choose_spec.symm
