[MATHS] Je vous offre un POULET

Ok les kheys j'ai bien tout relu et édité (en tout cas la partie sur les F-algèbres). J'ai corrigé des problèmes de notation, des tournures de phrases, et des trucs erronés théoriquement. Un immense merci au khey qui a pointé les problèmes qu'il a vu : j'avais mal compris certains trucs du sujet, nofake
https://github.com/JeanGalte/Th-orie/blob/main/falgebres/alg_et_coalg.pdf

Je vais me coucher, demain cours à 7h45.

Le 04 avril 2024 à 00:09:22 :
Ok non en fait khey je crois que t'as raison, j'écris pour m'en convanicre.
G+H c'est un produit libre de groupe, on crée une nouvelle loi ex nihilo (honnêtement je connaissais pas produit libre). La propriété pourrait rester vraie si on peut savoir si un élément du produit libre vient du premier ou du second groupe sommé, ça nous permettrait de faire le "pattern matching". Par exemple, quand on fait 1+G, 1 c'est <1|> et G c'est <générateurs de G | relations sur les générateurs>, et 1+G c'est le produit libre donc <[1} U générateurs de G | relations sur les générateurs de G>, donc c'est exactement G tu as raison.
En revanche sur wiki ils disent "Now use the coproduct (the disjoint union of sets) to glue the three morphisms in one", ils font le coproduit des groupes, donc soit ils se trompent, soit ils "redescendent au niveau ensemble", mais c'est pas expliqué

On redescend bien au niveau ensemble

Le 04 avril 2024 à 02:05:58 :
Ok les kheys j'ai bien tout relu et édité (en tout cas la partie sur les F-algèbres). J'ai corrigé des problèmes de notation, des tournures de phrases, et des trucs erronés théoriquement. Un immense merci au khey qui a pointé les problèmes qu'il a vu : j'avais mal compris certains trucs du sujet, nofake
https://github.com/JeanGalte/Th-orie/blob/main/falgebres/alg_et_coalg.pdf

Je vais me coucher, demain cours à 7h45.

Très bien ! Effectivement, la page wiki n'est pas très claire dans le sens où elle ne spécifie pas que l'endofoncteur agit sur la catégorie des ensembles, et donc que le produit et le coproduit sont ceux de cette catégorie

L'idée c'est de pouvoir avoir des groupes dans n'importe quelle catégorie (donc en particulier Ens) avec assez de structure, en compactant toute l'information dans un seul foncteur.

Ça ne te fait pas changer grand-chose au final, les erreurs font partie du métier

Je ne connaissais pas les F-algèbres, mais je connais les algèbres sur une monade, l'esprit est similaire sauf que ton endofoncteur a davantage de structure (encodant directement l'existence de constantes telles que le neutre pour un groupe, et l'associativité d'éventuelles lois). Et pour les algèbres sur une monade, on retrouve exactement les algèbres de base (par exemple des groupes pour la monade associée aux groupes, des anneaux pour celle des anneaux, des espaces compacts pour celle des espaces compacts etc.)

Continue d'écrire en français, n'écoute pas ces traîtres

Le 04 avril 2024 à 16:18:37 :

Le 04 avril 2024 à 02:05:58 :
Ok les kheys j'ai bien tout relu et édité (en tout cas la partie sur les F-algèbres). J'ai corrigé des problèmes de notation, des tournures de phrases, et des trucs erronés théoriquement. Un immense merci au khey qui a pointé les problèmes qu'il a vu : j'avais mal compris certains trucs du sujet, nofake
https://github.com/JeanGalte/Th-orie/blob/main/falgebres/alg_et_coalg.pdf

Je vais me coucher, demain cours à 7h45.

Très bien ! Effectivement, la page wiki n'est pas très claire dans le sens où elle ne spécifie pas que l'endofoncteur agit sur la catégorie des ensembles, et donc que le produit et le coproduit sont ceux de cette catégorie

L'idée c'est de pouvoir avoir des groupes dans n'importe quelle catégorie (donc en particulier Ens) avec assez de structure, en compactant toute l'information dans un seul foncteur.

Ça ne te fait pas changer grand-chose au final, les erreurs font partie du métier

Je ne connaissais pas les F-algèbres, mais je connais les algèbres sur une monade, l'esprit est similaire sauf que ton endofoncteur a davantage de structure (encodant directement l'existence de constantes telles que le neutre pour un groupe, et l'associativité d'éventuelles lois). Et pour les algèbres sur une monade, on retrouve exactement les algèbres de base (par exemple des groupes pour la monade associée aux groupes, des anneaux pour celle des anneaux, des espaces compacts pour celle des espaces compacts etc.)

Continue d'écrire en français, n'écoute pas ces traîtres

Oui c'est vraiment des chiens, surtout qu'ils disent "G", et qu'ensuite ils font une autre erreur : ils disent qu'on peut définir un corps de cette façon (dans mon poly j'expplique bien que non). Je pense que quand j'aurai fini ça je vais aller édit cette page, voire la créer en français pour mog la page américaine .

Le changement est pas énorme mais jsp pourquoi, j'ai fait ça jusqu'à 2h du mat hier
J'ai aussi approché les algèbres de monades (en fait je dois avoir un peu de bagout catégorique, parce que je suis en stage dans un truc où je fais de la substitution, donc un truc monadique, sur un système formel), mais que pour des syntaxes, pas pour des exemples algébriques (là pour les F-alg je suis allé les chercher moi-même)

Encore un gros merci à toi khey, si tu es d'accord je voudrais bien te faire relire l'intégralité du document une fois que ce sera produit, parce que je flippe un peu avec toutes les conneries que j'avais écrites

Le 04 avril 2024 à 18:21:44 :
Up pour l'effort
C'est intéressant

tu as lu kheyou ?

Le 04 avril 2024 à 18:05:06 :

Le 04 avril 2024 à 16:18:37 :

Le 04 avril 2024 à 02:05:58 :
Ok les kheys j'ai bien tout relu et édité (en tout cas la partie sur les F-algèbres). J'ai corrigé des problèmes de notation, des tournures de phrases, et des trucs erronés théoriquement. Un immense merci au khey qui a pointé les problèmes qu'il a vu : j'avais mal compris certains trucs du sujet, nofake
https://github.com/JeanGalte/Th-orie/blob/main/falgebres/alg_et_coalg.pdf

Je vais me coucher, demain cours à 7h45.

Très bien ! Effectivement, la page wiki n'est pas très claire dans le sens où elle ne spécifie pas que l'endofoncteur agit sur la catégorie des ensembles, et donc que le produit et le coproduit sont ceux de cette catégorie

L'idée c'est de pouvoir avoir des groupes dans n'importe quelle catégorie (donc en particulier Ens) avec assez de structure, en compactant toute l'information dans un seul foncteur.

Ça ne te fait pas changer grand-chose au final, les erreurs font partie du métier

Je ne connaissais pas les F-algèbres, mais je connais les algèbres sur une monade, l'esprit est similaire sauf que ton endofoncteur a davantage de structure (encodant directement l'existence de constantes telles que le neutre pour un groupe, et l'associativité d'éventuelles lois). Et pour les algèbres sur une monade, on retrouve exactement les algèbres de base (par exemple des groupes pour la monade associée aux groupes, des anneaux pour celle des anneaux, des espaces compacts pour celle des espaces compacts etc.)

Continue d'écrire en français, n'écoute pas ces traîtres

Oui c'est vraiment des chiens, surtout qu'ils disent "G", et qu'ensuite ils font une autre erreur : ils disent qu'on peut définir un corps de cette façon (dans mon poly j'expplique bien que non). Je pense que quand j'aurai fini ça je vais aller édit cette page, voire la créer en français pour mog la page américaine .

Le changement est pas énorme mais jsp pourquoi, j'ai fait ça jusqu'à 2h du mat hier
J'ai aussi approché les algèbres de monades (en fait je dois avoir un peu de bagout catégorique, parce que je suis en stage dans un truc où je fais de la substitution, donc un truc monadique, sur un système formel), mais que pour des syntaxes, pas pour des exemples algébriques (là pour les F-alg je suis allé les chercher moi-même)

Encore un gros merci à toi khey, si tu es d'accord je voudrais bien te faire relire l'intégralité du document une fois que ce sera produit, parce que je flippe un peu avec toutes les conneries que j'avais écrites

Mmmh pourquoi pas, si tu m'expliques la partie informatique !

Quand tu définis les foncteurs, tu mets un grand diagramme avec des flèches qui vont, par exemple, de A à F(A). Il ne faut pas faire ça !!! Ce que tu représentes comme une flèche on a vite fait de l'interpréter comme une flèche de la catégorie, or ce n'en est pas une... Les mettre en pointillés ou avec des tirets (ça se fait facilement sur tykzcd) me semble plus judicieux

Tu écris "le" foncteurs constant, or il y en a beaucoup, un pour chaque objet de la catégorie. Et, en particulier, une transformation naturelle entre deux foncteurs constants correspond exactement à un morphisme entre les deux "constantes" auxquels ils correspondent ! Quand est-ce que ça donne un foncteurs qui est objet terminal de la catégorie des foncteurs, ça ?

J'ai l'impression qu'il y a de petites confusions au niveau de ta partie produit/coproduit. Déjà je ne mettrais pas "je pense que la meilleure façon d'apprendre la théorie des catégories...", ça fait un peu pédant pour un premier rapport sur le sujet et je dirais que ça ne coûte pas très cher de mettre la définition formelle du coproduit (et du produit, si tu en as utilité).

Ensuite, il y a une phrase un peu floue "la donnée d'un élément de Z et d'un ensemble X est la donnée d'un élément de Z+X" si je me souviens (je suis sur téléphone c'est compliqué de faire des va et vient). Ce n'est pas bon, et si ce que tu voulais dire c'était "d'un élément d'un ensemble X", ça n'est pas bon non plus, parce que ça correspond à la propriété du produit ça ! Dans Set, un élément de X+Y, c'est la donnée d'un élément de X ou d'un élément de Z. Et à la fin du paragraphe, tu dis que le coproduit dans Set est le produit cartésien, mais non, c'est le produit, ça ! Somme = coproduit, en général en langage catégorique, c'est peut-être d'ici que viennent tes confusions ?

Le 04 avril 2024 à 19:19:01 :

Le 04 avril 2024 à 18:05:06 :

Le 04 avril 2024 à 16:18:37 :

Le 04 avril 2024 à 02:05:58 :
Ok les kheys j'ai bien tout relu et édité (en tout cas la partie sur les F-algèbres). J'ai corrigé des problèmes de notation, des tournures de phrases, et des trucs erronés théoriquement. Un immense merci au khey qui a pointé les problèmes qu'il a vu : j'avais mal compris certains trucs du sujet, nofake
https://github.com/JeanGalte/Th-orie/blob/main/falgebres/alg_et_coalg.pdf

Je vais me coucher, demain cours à 7h45.

Très bien ! Effectivement, la page wiki n'est pas très claire dans le sens où elle ne spécifie pas que l'endofoncteur agit sur la catégorie des ensembles, et donc que le produit et le coproduit sont ceux de cette catégorie

L'idée c'est de pouvoir avoir des groupes dans n'importe quelle catégorie (donc en particulier Ens) avec assez de structure, en compactant toute l'information dans un seul foncteur.

Ça ne te fait pas changer grand-chose au final, les erreurs font partie du métier

Je ne connaissais pas les F-algèbres, mais je connais les algèbres sur une monade, l'esprit est similaire sauf que ton endofoncteur a davantage de structure (encodant directement l'existence de constantes telles que le neutre pour un groupe, et l'associativité d'éventuelles lois). Et pour les algèbres sur une monade, on retrouve exactement les algèbres de base (par exemple des groupes pour la monade associée aux groupes, des anneaux pour celle des anneaux, des espaces compacts pour celle des espaces compacts etc.)

Continue d'écrire en français, n'écoute pas ces traîtres

Oui c'est vraiment des chiens, surtout qu'ils disent "G", et qu'ensuite ils font une autre erreur : ils disent qu'on peut définir un corps de cette façon (dans mon poly j'expplique bien que non). Je pense que quand j'aurai fini ça je vais aller édit cette page, voire la créer en français pour mog la page américaine .

Le changement est pas énorme mais jsp pourquoi, j'ai fait ça jusqu'à 2h du mat hier
J'ai aussi approché les algèbres de monades (en fait je dois avoir un peu de bagout catégorique, parce que je suis en stage dans un truc où je fais de la substitution, donc un truc monadique, sur un système formel), mais que pour des syntaxes, pas pour des exemples algébriques (là pour les F-alg je suis allé les chercher moi-même)

Encore un gros merci à toi khey, si tu es d'accord je voudrais bien te faire relire l'intégralité du document une fois que ce sera produit, parce que je flippe un peu avec toutes les conneries que j'avais écrites

Mmmh pourquoi pas, si tu m'expliques la partie informatique !

Quand tu définis les foncteurs, tu mets un grand diagramme avec des flèches qui vont, par exemple, de A à F(A). Il ne faut pas faire ça !!! Ce que tu représentes comme une flèche on a vite fait de l'interpréter comme une flèche de la catégorie, or ce n'en est pas une... Les mettre en pointillés ou avec des tirets (ça se fait facilement sur tykzcd) me semble plus judicieux

Tu écris "le" foncteurs constant, or il y en a beaucoup, un pour chaque objet de la catégorie. Et, en particulier, une transformation naturelle entre deux foncteurs constants correspond exactement à un morphisme entre les deux "constantes" auxquels ils correspondent ! Quand est-ce que ça donne un foncteurs qui est objet terminal de la catégorie des foncteurs, ça ?

J'ai l'impression qu'il y a de petites confusions au niveau de ta partie produit/coproduit. Déjà je ne mettrais pas "je pense que la meilleure façon d'apprendre la théorie des catégories...", ça fait un peu pédant pour un premier rapport sur le sujet et je dirais que ça ne coûte pas très cher de mettre la définition formelle du coproduit (et du produit, si tu en as utilité).

Ensuite, il y a une phrase un peu floue "la donnée d'un élément de Z et d'un ensemble X est la donnée d'un élément de Z+X" si je me souviens (je suis sur téléphone c'est compliqué de faire des va et vient). Ce n'est pas bon, et si ce que tu voulais dire c'était "d'un élément d'un ensemble X", ça n'est pas bon non plus, parce que ça correspond à la propriété du produit ça ! Dans Set, un élément de X+Y, c'est la donnée d'un élément de X ou d'un élément de Z. Et à la fin du paragraphe, tu dis que le coproduit dans Set est le produit cartésien, mais non, c'est le produit, ça ! Somme = coproduit, en général en langage catégorique, c'est peut-être d'ici que viennent tes confusions ?

Oui bien sûr je suis chaud de répondre à toute question informatique si tu veux

Un foncteur constant est toujours un objet terminal non ? On prend un foncteur constant F, et un foncteur G, on envoie toutes les images de G sur l'image de F, tous les morphismes images de G sur le morphisme identité. On a bien une unique transformation naturelle dans ce cas non ?
J'avoue j'ai pas vérifié la partie naturalité à la main, mais bon

Franchement mettre les defs de produit et coproduit j'ai peur que ça alourdisse vraiment le tout, déjà qu'il y a beaucoup de defs et peu de résultats

Concernant ce que tu penses être une confusion sur le coproduit, j'ai réfléchi et je pense pas, je pense que c'est correct. En gros t'as un élément x d'un ensemble X. Techniquement, si tu sais où est positionné X dans ton coproduit, tu peux dire de x qu'en l'injectant il est un élément de ton coproduit.
Faisons un exemple (je veux pas paraître pédant, je le fais pour me convaincre autant que pour te convaincre) :
Soit n un entier naturel. On sait que n \in \N, donc pour n'importe quel ensemble Y, (0,n) sera dans \N + Y (par définition de l'union disjointe). Du coup on "injecte" n dans le coproduit (à gauche en l'occurrence), ça se note inl(n). "La donnée d'un élément de $\Z$ et d'un ensemble $X$ nous donnent la donnée d'un élément de $\Z + X$"

En revanche, je pense que c'est toi qui te trompes (c'est une subtilité d'infoteux héhé) : un élément de X c'est pas un élément de X+Y, parce que dans X+Y les éléments ils portent avec eux l'information d'où ils viennent exactement (en général on définit ça comme un couple (provenance, élément) je crois), or ton élément de X porte pas ça avec lui : c'est à ça que sert l'injection !

Merci encore de prendre le temps de lire un pdf random sur téléphone, t'es déter pour aider un khey

Si tu es dans une catégorie qui a deux objets distincts A et B avec deux flèches distinctes de A dans B, tu prends n'importe quelle catégorie, par exemple celle des ensembles, et tu prends les deux foncteurs constants F (d'objet "constante" A) et G (d'objet "constante" B). Les deux flèches distinctes allant de A dans B te donnent deux transformations naturelles distinctes de F dans G. Le foncteur G est constant mais n'est pas terminal puisqu'il existe deux transformations naturelles de source F et de but G, et non une unique !

Tu as mis à un moment, je crois, que dans Set il y avait plusieurs objets terminaux. C'est pas du tout une connerie parce que, purement rigoureusement, oui. Mais ils sont tous "les mêmes", étant donné qu'ils sont isomorphes à un unique isomorphisme canonique près. J'imagine que tu le sais bien mais, demande-toi donc, est-ce pareil de prendre le foncteur constant égal à un objet ou à un autre ?

Tu dis "on envoie toutes les images de G sur les images de F", le peut-on seulement ? S'il y a un objet "image par G" qui n'a pas de flèche vers l'objet "constante" de F ! Et tu "tous les morphisme images de G sur l'identité", mais un morphisme de foncteur n'agit pas sur les flèches, attention !

Haha oui je sais comment est construite l'union disjointe ensembliste, j'ai des restes de cours de théorie des ensembles... Je suis d'accord pour ce qui est d'indiquer la provenance si on veut vraiment être rigoureux, mais la donne d'un élément de Z + X, c'est la donnée d'une provenance, alors, disons gauche ou droite, et d'un élément de Z si la provenance est gauche, ou d'un élément de X si la provenance est droite. Pourquoi ce serait la donne d'un élément de Z et d'un ensemble X ?

Le 04 avril 2024 à 22:10:45 :
Si tu es dans une catégorie qui a deux objets distincts A et B avec deux flèches distinctes de A dans B, tu prends n'importe quelle catégorie, par exemple celle des ensembles, et tu prends les deux foncteurs constants F (d'objet "constante" A) et G (d'objet "constante" B). Les deux flèches distinctes allant de A dans B te donnent deux transformations naturelles distinctes de F dans G. Le foncteur G est constant mais n'est pas terminal puisqu'il existe deux transformations naturelles de source F et de but G, et non une unique !

Tu as mis à un moment, je crois, que dans Set il y avait plusieurs objets terminaux. C'est pas du tout une connerie parce que, purement rigoureusement, oui. Mais ils sont tous "les mêmes", étant donné qu'ils sont isomorphes à un unique isomorphisme canonique près. J'imagine que tu le sais bien mais, demande-toi donc, est-ce pareil de prendre le foncteur constant égal à un objet ou à un autre ?

Tu dis "on envoie toutes les images de G sur les images de F", le peut-on seulement ? S'il y a un objet "image par G" qui n'a pas de flèche vers l'objet "constante" de F ! Et tu "tous les morphisme images de G sur l'identité", mais un morphisme de foncteur n'agit pas sur les flèches, attention !

Haha oui je sais comment est construite l'union disjointe ensembliste, j'ai des restes de cours de théorie des ensembles... Je suis d'accord pour ce qui est d'indiquer la provenance si on veut vraiment être rigoureux, mais la donne d'un élément de Z + X, c'est la donnée d'une provenance, alors, disons gauche ou droite, et d'un élément de Z si la provenance est gauche, ou d'un élément de X si la provenance est droite. Pourquoi ce serait la donne d'un élément de Z et d'un ensemble X ?

Dsl j'ai raconté n'importe quoi sur le foncteur constant, j'ai fait un mix batard entre foncteur et transfo naturelle
Ça m'arrive toujours ce genre de trucs cons, me placer au mauvais niveau pour raisonner
En TT aussi, je confonds régulièrement un élément et son type

Sur la provenance aussi tu dis vrai je crois
En fait pour inr, et inl y'a pas de définition "scientifique", parce que c'est un formalisme un peu osef, on comprend bien qu'on injecte. Mais en Coq par contre c'est des constructeurs du type coproduit sur une catégorie (dans UniMath c'est comme ça en tout cas), donc ça dépend pas de l'autre composante (cependant, ça dépend de la nature du coproduit. Genre ça va inférer le type du second summand du coup un inr/inl). J'édit ça, emerce
J'ai l'air fébrile de zinzin en catégories, cet été j'ai prévu le awodey parce que ça traite de trucs qui m'intéressent (dualité, et adjonction notamment), et on me l'a recommandé. Je solicite ton avis : tu penses c'est bien ? ou je suis trop noob ?

Tu devrais prendre le temps de poser formellement les définitions et de vérifier ce que tu écris ! C'est bien d'avoir "l'idée" mais les mathématiques c'est le mariage de l'intuition et de la rigueur, même si je sais que le second peut être mentalement douloureux

Non ! Il y a bien une définition formelle de l'union disjointe dans les ensembles, et, l'une de ces définitions par construction, du moins, utilise cette idée de labeller les éléments.

Pour le bouquin d'Awodey j'en sais trop rien, je ne l'ai pas lu, je viens de regarder le sommaire et ça a l'air assez classique, donc j'imagine que ça va ! Il y a peut-être la partie sur le lien avec le lambda calcul qui diverge de ce qui se fait habituellement dans les bouquins d'initiation aux catégories ? Quoiqu'il en soit le McLane est une référence indémodable, et j'avais bien aimé Category theory in context de Riehl qui est peut-être plus moderne et pédagogique. Mais je t'encourage à lire, tu lis et quand tu n'y arrives plus tu t'arrêtes, puis tu y reviens plus tard et ainsi de suite

Si tu as des concepts spécifiques sur lesquels tu bloques je peux t'aider

Le 05 avril 2024 à 19:19:47 :
Tu devrais prendre le temps de poser formellement les définitions et de vérifier ce que tu écris ! C'est bien d'avoir "l'idée" mais les mathématiques c'est le mariage de l'intuition et de la rigueur, même si je sais que le second peut être mentalement douloureux

Non ! Il y a bien une définition formelle de l'union disjointe dans les ensembles, et, l'une de ces définitions par construction, du moins, utilise cette idée de labeller les éléments.

Pour le bouquin d'Awodey j'en sais trop rien, je ne l'ai pas lu, je viens de regarder le sommaire et ça a l'air assez classique, donc j'imagine que ça va ! Il y a peut-être la partie sur le lien avec le lambda calcul qui diverge de ce qui se fait habituellement dans les bouquins d'initiation aux catégories ? Quoiqu'il en soit le McLane est une référence indémodable, et j'avais bien aimé Category theory in context de Riehl qui est peut-être plus moderne et pédagogique. Mais je t'encourage à lire, tu lis et quand tu n'y arrives plus tu t'arrêtes, puis tu y reviens plus tard et ainsi de suite

Si tu as des concepts spécifiques sur lesquels tu bloques je peux t'aider

Dsl j'ai vraiment troll sur le document, j'aurais dû être plus rigoureux avant de faire un topic.
Y'a une déf formelle d'union disjointe, mais j'ai pas trouvé de définition précise de l'injection justement : d'ailleurs dans UniMath on a deux défs différentes selon les besoins. Du coup jsp si mon truc est si mauvais, je vais "effacer" l'ensemble dans lequel on injecte pas dans la déf, cependant.

Le 09 avril 2024 à 08:17:41 :

Le 05 avril 2024 à 19:19:47 :
Tu devrais prendre le temps de poser formellement les définitions et de vérifier ce que tu écris ! C'est bien d'avoir "l'idée" mais les mathématiques c'est le mariage de l'intuition et de la rigueur, même si je sais que le second peut être mentalement douloureux

Non ! Il y a bien une définition formelle de l'union disjointe dans les ensembles, et, l'une de ces définitions par construction, du moins, utilise cette idée de labeller les éléments.

Pour le bouquin d'Awodey j'en sais trop rien, je ne l'ai pas lu, je viens de regarder le sommaire et ça a l'air assez classique, donc j'imagine que ça va ! Il y a peut-être la partie sur le lien avec le lambda calcul qui diverge de ce qui se fait habituellement dans les bouquins d'initiation aux catégories ? Quoiqu'il en soit le McLane est une référence indémodable, et j'avais bien aimé Category theory in context de Riehl qui est peut-être plus moderne et pédagogique. Mais je t'encourage à lire, tu lis et quand tu n'y arrives plus tu t'arrêtes, puis tu y reviens plus tard et ainsi de suite

Si tu as des concepts spécifiques sur lesquels tu bloques je peux t'aider

Dsl j'ai vraiment troll sur le document, j'aurais dû être plus rigoureux avant de faire un topic.
Y'a une déf formelle d'union disjointe, mais j'ai pas trouvé de définition précise de l'injection justement : d'ailleurs dans UniMath on a deux défs différentes selon les besoins. Du coup jsp si mon truc est si mauvais, je vais "effacer" l'ensemble dans lequel on injecte pas dans la déf, cependant.

Avant de faire un topic à la limite ça va hahaha, ça n'engage pas à grand chose, mais il faudra faire attention avant de l'envoyer à ton directeur !

Une des façons de faire c'est de prendre deux ensembles A et B qui n'appartiennent pas à tes ensembles X et Y, et tu construis l'union comme les pairs (x,A) et (y,B) où x et y appartiennent resp. à X et Y. C'est des formalités ça pour le coup, on montre une fois que ça existe, puis après on se représente assez bien le truc pour ne pas avoir à s'embarrasser de cette définition