Coalgèbre

Soit K un corps. Une coalgèbre C sur K est un K-espace vectoriel muni de deux applications K-linéaires ${\displaystyle \Delta :C\to C\otimes C}$ et ${\displaystyle \epsilon :C\to K}$ telles que :

1. ${\displaystyle (\mathrm {id} _{C}\otimes \Delta )\circ \Delta =(\Delta \otimes \mathrm {id} _{C})\circ \Delta }$
2. ${\displaystyle (\mathrm {id} _{C}\otimes \epsilon )\circ \Delta =\mathrm {id} _{C}=(\epsilon \otimes \mathrm {id} _{C})\circ \Delta }$.

L'application ${\displaystyle \Delta }$ s'appelle le coproduit, et ${\displaystyle \epsilon }$ la counité. La première condition s'appelle la coassociativité (notion duale de l'associativité dans les anneaux), et la deuxième est l'analogue de la relation que vérifie l'unité (l'élément neutre de la multiplication) dans un anneau.

La notion de coalgèbre est duale de celle d'algèbre, dans le sens où le dual linéaire de l'espace vectoriel sous-jacent à une coalgèbre C possède une structure naturelle d'algèbre induite par le coproduit de C. En effet, soient f, g deux éléments du dual de C. En posant ${\displaystyle \Delta (x)=\sum x^{(1)}\otimes x^{(2)}}$ pour tout x de C, on définit le produit de f et de g par :

${\displaystyle (f\star g)(x)=(f\otimes g)(\Delta (x))=\sum f(x^{(1)})\times g(x^{(2)})}$.

Le fait que ${\displaystyle \Delta }$ soit coassociatif est exactement la condition qui garantit que ${\displaystyle \star }$ est associatif.

À l'inverse, si A est une algèbre de dimension finie, alors le dual de A possède une structure naturelle de coalgèbre. En effet, la multiplication de A peut être vue comme une application ${\displaystyle \mu :A\otimes A\longrightarrow A}$. En passant au dual, on obtient une application ${\displaystyle \mu ^{*}:A^{*}\longrightarrow (A\otimes A)^{*}}$ définie par

${\displaystyle \forall f\in A^{*},\ (\mu ^{*}(f))(x\otimes y)=f(\mu (x\otimes y))}$.

Or, si A est de dimension finie, il existe un isomorphisme naturel ${\displaystyle (A\otimes A)^{*}\cong A^{*}\otimes A^{*}}$, donc ${\displaystyle \mu ^{*}}$ définit un coproduit, la coassociativité découlant de l'associativité de ${\displaystyle \mu }$.

• Si E est un K-espace vectoriel de base ${\displaystyle \{e_{i}\}_{i\in I}}$, alors on définit un coproduit en posant ${\displaystyle \Delta (e_{i})=e_{i}\otimes e_{i}}$ et en l'étendant linéairement à tout E.

• (en) Bart Jacobs, Introduction to Coalgebra : Towards Mathematics of States and Observation, Cambridge, Cambridge University Press, coll. « Cambridge Tracts in Theoretical Computer Science », octobre 2016, 494 pages (ISBN 978-1-107-17789-5, présentation en ligne).
• Davide Sangiorgi, « On the origins of bisimulation and coinduction », ACM Trans. Program. Lang. Syst, vol. 31(4),‎ 2009, p. 15:1-15:41
• Davide Sangiorgi, Introduction to Bisimulation and Coinduction, Cambridge University Press, 2012.
• Davide Sangiorgi et Jan Rutten, Advanced Topics in Bisimulation and Coinduction, Cambridge University Press, 2011.

Textes d'introduction

• Bart Jacobs et Jan Rutten, « A Tutorial on (Co)Algebras and (Co)Induction », Bulletin EATCS, n^o 62,‎ 1997, p. 222-269 (lire en ligne, consulté le 29 juin 2018) — describes induction and coinduction simultaneously
• Eduardo Giménez et Pierre Castéran, « "A Tutorial on [Co-]Inductive Types in Coq" », 2007 (consulté le 29 juin 2018).
• Dexter Kozen et Alexandra Silva, « Practical coinduction », Mathematical Structures in Computer Science, vol. 27, n^o 07,‎ 2016, p. 1132–1152 (ISSN 0960-1295, DOI 10.1017/S0960129515000493, lire en ligne).
• Pierre-Marie Pédrot, « A Survey of coinduction in Coq », 18 juin 2015 (consulté le 29 juin 2018).

• Cocommutativité
• Bigèbre
• Algèbre de Hopf