Dissertationen zum Thema „Isomorphisme de type“

Dans toute cette thèse, k désigne un corps de caractéristique différente de 2 et par variété nous désignons un k-schéma, séparé et de type fini. Nous allons étudier $X(\alpha_1)$ et $X(\alpha_2)$, les variétés homogènes projectives associées à chacune des deux racines d'un groupes de type $G_(2)$. La pemière d'entre elles, $X(\alpha_1)$, est une quadrique projective de dimension 5 associée à une voisine de Pfister et l'autre, $X(\alpha_2)$, est une variété de Fano (de genre 10). Ces deux variétés ne sont pas isomorphes, pourtant elles le deviennent en tant qu'objets d'une catégorie plus large, à savoir la catégorie des correspondances (et par conséquent également dans la catégorie des motifs de Chow). Nous établissons que ce résultat est vrai que les variétés soient déployées ou non. Dans un premier chapitre, nous rappelons quelques résultats classiques sur les algèbres d'octonions et construisons un modèle d'algèbres d'octonions déployée. Dans le second, nous présentons les variétés mises en jeu et rappelons pour cela des notions essentielles de la théorie des groupes algébriques ainsi que de celle des foncteurs de points. Dans le troisième chapitre, nous construisons une structure cellulaire de $X(\alpha_2)$ lorsqu'elle est déployée, étape essentielle de notre travail. C'est également dans ce chapitre que nous calculons les relations définissant la structure d'anneau de $X(\alpha_2)$. Enfin, dans le quatrième et dernier chapitre, nous introduisons la catégorie des correspondances avant de prouver notre théorème de nilpotence dans le cas particulier de la variété $X(\alpha_2)$, puis nous établissons l'isomorphisme motivique en toute généralité.

Dans toute cette thèse, k désigne un corps de caractéristique différente de 2 et par variété nous désignons un k-schêma, séparé et de type fini. Nous allons étudier X(α1) et X(α2), les variétés homogènes projectives associées à chacune des deux racines d'un groupes de type G2. La pemière d'entre elles, X(α1), est une quadrique projective de dimension 5 associée à une voisine de PFISTER et l'autre, X(α2), est une variété de FANO (de genre 10). Ces deux variétés ne sont pas isomorphes, pourtant elles le deviennent en tant qu'objets d'une catégorie plus large, à savoir la catégorie des correspondances (et par conséquent également dans la catégorie des motifs de CHOW). Nous établissons que ce résultat est vrai que les variétés soient déployées ou non. Dans un premier chapitre, nous rappelons quelques résultats classiques sur les algèbres d'octonions et construisons un modèle d'algèbres d'octonions déployée. Dans le second, nous présentons les variétés mises en jeu et rappelons pour cela des notions essentielles de la théorie des groupes algébriques ainsi que de celle des foncteurs de points. Dans le troisième chapitre, nous construisons une structure cellulaire de X(α2) lorsqu'elle est déployée, étape essentielle de notre travail. C'est également dans ce chapitre que nous calculons les relations définissant la structure d'anneau de X(α2). Enfin, dans le quatrième et dernier chapitre, nous introduisons la catégorie des correspondances avant de prouver notre théorème de nilpotence dans le cas particulier de la variété X(α2), puis, nous établissons l'isomorphisme motivique en toute généralité.

Le sujet de cette thèse est sur le lambda-calcul décoré avec des types, communément appelé « lambda-calcul typé à la Church ». Nous étudions des versions de ce lambda-calcul muni de types intersections, tels que ceux décrits dans le livre « Lambda-calculus with types » de Barendregt, Dekkers et Statman ; les types unions, qui ont été introduits par Plotkin, MacQueen et Sethi ; et les types dépendants, tels qu'ils ont été décrits par Plotkin, Harper et Honsell lorsqu'ils ont introduit le Logical Framework d'Edinbourgh LF. Les types intersections et unions sont un moyen d'exprimer du polymorphisme ad hoc et sont une alternative au polymorphisme paramétrique de Girard. Les types dépendants ont été introduits pour formaliser la logique intuitionniste avec la correspondance de Curry-Howard. Le système de types obtenu peut être enrichi avec une relation de soutypage décidable. La combinaison de ces trois disciplines de type donne lieu à une famille de calculs qui peuvent être paramétrés et classifiés. Nous appelons le système générique le Delta-calcul. Nous discutons ensuite des décisions de conception qui nous ont amené à la formulation de ces calculs, nous étudions leur métathéorie, et nous présentons divers exemples d'applications avant de présenter une implémentation logicielle du Delta-calcul, avec une description des algorithmes de vérification de type, de raffinement, de soutypage, d'évaluation, ainsi que de l'interface en ligne de commande. Ce travail de recherche peut être vu comme un petit pas franchi dans la direction d'une théorie des types alternative pour définir du polymorphisme dans les langages de programmation et dans les assistants de preuve interactifs
The subject of this thesis is about lambda-calculus decorated with types, usually called "Church-style typed lambda-calculus". We study this lambda-calculus enhanced with Intersection types, as described by Barendregt, Dekkers and Statman in the book "Lambda-calculus with Types"; Union types, as introduced by Plotkin, MacQueen and Sethi; and Dependent types, as described by Plotkin, Harper and Honsell when they introduced the Edinburgh Logical Framework LF. Intersection and union types are a way to express ad hoc polymorphism and are an alternative to the parametric polymorphism of Girard. Dependent types were introduced as a way to formalize intuitionistic logic using the "proof-as-lambda-terms / formulas-as-types" Curry-Howard principle. The resulting type system can be enriched with a decidable subtyping relation. Combining these three type disciplines gives rise to a family of calculi that can be parametrized and classified: we call the resulting system the Delta-calculus. We then discuss the design decisions which have led us to the formulation of these calculi, study their metatheory, and provide various examples of applications; and we finally present a software implementation of the Delta-calculus, with a description of the type checker, the refinement algorithm, the subtyping algorithm, the evaluation algorithm and the command-line interface. This work can be understood as a little step toward an alternative type theory to defining polymorphic programming languages and interactive proof assistants

Cette thèse étudie l'extension du lambda-calcul simplement typé par diverses relations de récriture préservant la terminaison et la confluence. Il s'agit d'assurer, dans un premier temps, que certains types sont isomorphes. Or le problème est indécidable pour les types inductifs : nous avons donc ajouté au calcul des réductions spécifiques résolvant la question dans certains cas, à savoir le codage des types produits et unité et surtout la notion de copie paramétrée. Délaissant ensuite les isomorphismes, nous considérons de nouvelles réductions permettant d'établir des structures algébriques sur les types finis : nous envisageons d'une part la définition d'une catégorie sur un fragment du calcul ; et, d'autre part, la représentation du groupe symétrique par décomposition des permutations en produits de cycles disjoints. Ces résultats sont obtenus par des techniques de récriture abstraite, dont certaines développées spécifiquement pour la thèse
This PhD thesis copes with extensions of the simply-typed lambda-calculus by various rewrite relations preserving termination and confluence. Our first purpose is to ensure that some types become isomorphic. As far as inductive types are concerned, this problem is undecidable: therefore, we added some particular reductions solving it only in peculiar cases, namely the inductive encoding of the product and unit types and, more importantly, the notion of parameterised copy. Next, leaving isomorphims, we consider new reductions enabling to set up some algebraic structures on finite types: firstly, we deal with the definition of a category on a fragment of the calculus; and, secondly, with the representation of the symmetric group by factorisation of permutations as products of disjoint cycles. These results are obtained using techniques from abstract rewriting theory, some of which we have specifically developped for this thesis

Cette thèse porte sur l'adaptation de la réalisabilité et la paramétricité au cas des types dépendants dans le cadre des Systèmes de Types Purs. Nous décrivons une méthode systématique pour construire une logique à partir d'un langage de programmation, tous deux décrits comme des systèmes de types purs. Cette logique fournit des formules pour exprimer des propriétés des programmes et elle offre un cadre formel adéquat pour développer une théorie de la réalisabilité au sein de laquelle les réalisateurs des formules sont exactement les programmes du langage de départ. Notre cadre permet alors de considérer les théorèmes de représentation pour le système T de Gödel et le système F de Girard comme deux instances d'un théorème plus général.Puis, nous expliquons comment les relations logiques de la théorie de la paramétricité peuvent s'exprimer en terme de réalisabilité, ce qui montre que la logique engendrée fournit un cadre adéquat pour développer une théorie de la paramétricité du langage de départ. Pour finir, nous montrons comment cette théorie de la paramétricité peut-être adaptée au système sous-jacent à l'assistant de preuve Coq et nous donnons un exemple d'application original de la paramétricité à la formalisation des mathématiques.

La sémantique des jeux offre un cadre souple et précis pour l'interprétation des langages de programmation. Cette thèse l'illustre à travers d'une part l'étude de la notion de polymorphisme et son pendant logique : la quantification du second ordre, et d'autre part la caractérisation de | certaines propriétés syntaxiques via les modèles de jeux. Le polymorphisme est d'abord envisagé sous sa forme la plus usuelle, le système F à la Church. On en propose un nouveau modèle de jeux, complet, inspiré de travaux antérieurs mais dans lequel il sera cette fois possible d'effectuer des calculs. La question syntaxique de la caractérisation des isomorphismes de typas peut alors être résolue à l'intérieur même de ce modèle, en prouvant l'invariance par isomorphisme d'une structure appelée hyperforêt. Cette approche sémantique permet de retrouver un résultat dû à Roberto Di Cosmo. Une autre variante de la logique du second ordre, le système F à la Curry, est étudiée et modélisée de manière partielle mais suffisamment précise pour permettre là encore la caractérisation des isomorphismes de types par un invariant géométrique. Le système équationnel correspondant enrichit celui des isomorphismes du système F à la. Church d'une nouvelle équation, non triviale. Une extension à la logique classique des résultats obtenus pour te système F à Sa Church est proposée à travers la construction dans les jeux d'une hyperdoctrine de contrôle, structure catégorique adaptée à la logique du second ordre
Game semantics is a flexible and precise framework for interpreting programming languages. The present dissertation illustrates this fact in two ways : first by studying polymorphism and its logical counterpart : second-order quantification, and second by caracterising sorne syntactic properties via game models. Polymorphism is first considered in its most usual form, Church- style System F, We propose a new, complete, game model, inspired by previous works but in which we will be able to do effective calculations. The syntactic question of characterising type isomorphisms can then be solved inside this model, by proving the invariance through isomorphism of some structure called hyperforest. This semantic approach allows to retrieve a result by Roberto Di Cosmo, Another variant of second- order logic, namely Curry- style System F, is studied and modellsed, partially but with enough precision to give once again a characterisation of type isomorphisms through a geometric invariant. The corresponding equationnal system is an enrichment of that of Church-style isomorphisms by a news non-trivial, equation. An extension to classical logic of the results for Church-style System F is proposed, through theconstruction of a game model which results in a control hyperdoctrine, ie a categorical structuresuitable for second- order classical logic

In this thesis we have presented original homomorphic images of permutations and monomial progenitors. In some cases we have used the double coset enumeration tech- nique to construct the images and for all of the homomorphic images that we have discovered, the isomorphism type of each group is given. The homomorphic images discovered include Linear groups, Alternating groups, and two sporadic simple groups J1 and J2X2 where J1 is the smallest Janko group and J2 is the second Janko sporadic group.

In this thesis, we have presented our discovery of true finite homomorphic images of various permutation and monomial progenitors, such as 2*7: D14, 2*7 : (7 : 2), 2*6 : S3 x 2, 2*8: S4, 2*72: (32:(2S4)), and 11*2 :m D10. We have given delightful symmetric presentations and very nice permutation representations of these images which include, the Mathieu groups M11, M12, the 4-fold cover of the Mathieu group M22, 2 x L2(8), and L2(13). Moreover, we have given constructions, by using the technique of double coset enumeration, for some of the images, including M11 and M12. We have given proofs, either by hand or computer-based, of the isomorphism type of each image. In addition, we use Iwasawa's Lemma to prove that L2(13) over A5, L2(8) over D14, L2(13) over D14, L2(27) over 2D14, and M11 over 2S4 are simple groups. All of the work presented in this thesis is original to the best of our knowledge.

Cette thèse s'intéresse à l'égalité des preuves et des formules en logique linéaire, avec des contributions en particulier dans le fragment multiplicatif-additif de cette logique. En logique linéaire, et dans de nombreuses autres logiques (telle que la logique intuitionniste), on dispose de deux transformations sur les preuves : l'élimination des coupures et l'expansion des axiomes. On souhaite très souvent identifier deux preuves reliées par ces transformations, étant donné qu'elles le sont sémantiquement (dans un modèle catégorique par exemple). Cette situation est similaire à celle du λ-calcul où les termes sont identifiés à β-réduction et η-expansion près, opérations qui, par le prisme de la correspondance de Curry-Howard, se rapportent respectivement à l'élimination des coupures et à l'expansion des axiomes. Nous montrons ici que cette identification des preuves correspond exactement à l'identification des preuves à commutation de règle près, qui est une troisième opération sur les preuves bien connue et plus facile à manipuler. Notre démonstration considère uniquement la logique linéaire multiplicative-additive, même si nous conjecturons que ce résultat est vrai pour la logique linéaire dans son entièreté.Non seulement des preuves peuvent être identifiées à élimination des coupures et expansion des axiomes près, mais aussi des formules. Deux formules sont isomorphes si elles sont reliées par des preuves dont les compositions donnent l'identité, toujours à élimination des coupures et expansion des axiomes près. Ces formules sont alors réellement considérées comme les mêmes, et toute utilisation de l'une peut être remplacée par une utilisation de l'autre. Nous donnons une théorie équationnelle caractérisant exactement les formules isomorphes dans la logique linéaire multiplicative-additive. Un problème généralisant les isomorphismes est celui des rétractions, qui intuitivement correspondent aux couples de formules où la première peut être remplacée par la seconde - mais pas nécessairement la seconde par la première, contrairement aux isomorphismes. Étudier les rétractions est bien plus complexe, et nous avons caractérisé les rétractions des atomes dans le fragment multiplicatif de la logique linéaire.Pour l'étude des deux problèmes précédents, la syntaxe usuelle des preuves du calcul des séquents semble mal adaptée, car on considère des preuves à commutation de règle prés. Une partie de la logique linéaire possède une meilleure syntaxe dans ce cas : les réseaux de preuve, qui sont des graphes représentant des preuves quotientées par les commutations de règle. Cette syntaxe fut un outil indispensable pour caractériser isomorphismes et rétractions. Malheureusement, les réseaux de preuve ne sont pas (ou mal) définis en présence des unités. Pour nos problèmes, cette restriction conduit à une étude du cas sans unité dans les réseaux avec le coeur de la démonstration, précédé d'un travail en calcul des séquents pour prendre en compte les unités.Cette thèse développe par ailleurs une partie de la théorie des réseaux de preuve en fournissant une simple preuve du théorème de séquentialisation, qui relie les deux syntaxes des réseaux de preuve et du calcul des séquents, justifiant qu'elles décrivent les mêmes objets sous-jacents. Cette nouvelle démonstration s'obtient comme corollaire d'une généralisation du théorème de Yeo. Ce dernier résultat s'exprime entièrement dans la théorie des graphes aux arêtes colorées, et permet de déduire des preuves de sequentialisation pour différentes définitions de réseaux de preuve. Enfin, nous avons aussi formalisé les réseaux de preuve du fragment multiplicatif de la logique linéaire dans l'assistant de preuve Coq, avec en particulier une implémentation de notre nouvelle preuve de séquentialisation
This study is concerned with the equality of proofs and formulas in linear logic, with in particular contributions for the multiplicative-additive fragment of this logic. In linear logic, and as in many other logics (such as intuitionistic logic), there are two transformations on proofs: cut-elimination and axiom-expansion. One often wishes to identify two proofs related by these transformations, as it is the case semantically (in a categorical model for instance). This situation is similar to the one in the λ-calculus where terms are identified up to β-reduction and η-expansion, operations that, through the prism of the Curry-Howard correspondence, are related respectively to cut-elimination and axiom-expansion. We show here that this identification corresponds exactly to identifying proofs up to rule commutation, a third well-known operation on proofs which is easier to manipulate. We prove so only in multiplicative-additive linear logic, even if we conjecture such a result holds in full linear logic.Not only proofs but also formulas can be identified up to cut-elimination and axiom-expansion. Two formulas are isomorphic if there are proofs between them whose compositions yield identities, still up to cut-elimination and axiom-expansion. These formulas are then really considered to be the same, and every use of one can be replaced with one use of the other. We give an equational theory characterizing exactly isomorphic formulas in multiplicative-additive linear logic. A generalization of an isomorphism is a retraction, which intuitively corresponds to a couple of formulas where the first can be replaced by the second -- but not necessarily the other way around, contrary to an isomorphism. Studying retractions is more complicated, and we characterize retractions to an atom in the multiplicative fragment of linear logic.When studying the two previous problems, the usual syntax of proofs from sequent calculus seems ill-suited because we consider proofs up to rule commutation. Part of linear logic can be expressed in a better adapted syntax in this case: proof-nets, which are graphs representing proofs quotiented by rule commutation. This syntax was an instrumental tool for the characterization of isomorphisms and retractions. Unfortunately, proof-nets are not (or badly) defined with units. Concerning our issues, this restriction leads to a study of the unit-free case by means of proof-nets with the crux of the demonstration, preceded by a work in sequent calculus to handle the units. Besides, this thesis also develops part of the theory of proof-nets by providing a simple proof of the sequentialization theorem, which relates the two syntaxes of proof-net and sequent calculus, substantiating that they describe the same underlying objects. This new demonstration is obtained as a corollary of a generalization of Yeo's theorem. This last result is fully expressed in the theory of edge-colored graphs, and allows to recover proofs of sequentialization for various definitions of proof-nets. Finally, we also formalized proof-nets for the multiplicative fragment of linear logic in the proof assistant Coq, with notably an implementation of our new sequentialization proof

Two applications of a binary tree data type based on a simple pairing function (a bijection between natural numbers and pairs of natural numbers) are explored. First, the tree is used to encode natural numbers, and algorithms that perform basic arithmetic computations are presented along with formal proofs of their correctness. Second, using this "canonical" representation as a base type, algorithms for encoding and decoding additional isomorphic data types of other mathematical constructs (sets, sequences, etc.) are also developed. An experimental application to a memory management system is constructed and explored using these isomorphic types. A practical analysis of this system's runtime complexity and space savings are provided, along with a proof of concept framework for both applications of the binary tree type, in the Java programming language.

Le but de cette thèse est d'étudier la somme et le zéro dans deux principaux cadres : les isomorphismes de types et la normalisation de lambda-termes. Les isomorphismes de type avaient déjà été étudiés dans le cadre du lambda-calcul simplement typé avec paires surjectives mais sans somme. Pour aborder le cas avec somme et zéro, j'ai commencé par restreindre l'étude au cas des isomorphismes linéaires, dans le cadre de la logique linéaire, ce qui a conduit à une caractérisation remarquablement simple de ces isomorphismes, obtenue grâce à une méthode syntaxique sur les réseaux de preuve. Le cadre plus général de la logique intuitionniste correspond au problème ouvert de la caractérisation des isomorphismes dans les catégories bi-cartésiennes fermées. J'ai pu apporter une contribution à cette étude en montrant qu'il n'y a pas d'axiomatisation finie de ces isomorphismes. Pour cela, j'ai tiré partie de travaux en théorie des nombres portant sur un problème énoncé par Alfred Tarski et connu sous le nom du « problème des égalités du lycée ». Pendant tout ce travail sur les isomorphismes de types, s'est posé le problème de trouver une forme canonique pour représenter les lambda-termes, que ce soit dans le but de nier l'existence d'un isomorphisme par une étude de cas sur la forme du terme, ou pour vérifier leur existence dans le cas des fonctions très complexes que j'étais amené à manipuler. Cette réflexion a abouti à poser une définition « extensionnelle » de forme normale pour le lambda-calcul avec somme et zéro, obtenue par des méthodes catégoriques grâce aux relations logiques de Grothendieck, apportant ainsi une nouvelle avancée dans l'étude de la question réputée difficile de la normalisation de ce lambda-calcul. Enfin je montrerai comment il est possible d'obtenir une version « intentionnelle » de ce résultat en utilisant la normalisation par évaluation. J'ai pu ainsi donner une adaptation de la technique d' évaluation partielle dirigée par les types pour qu'elle produise un résultat dans cette forme normale, ce qui en réduit considérablement la taille et diminue aussi beaucoup le temps de normalisation dans le cas des isomorphismes de types considérés auparavant.

We will explore progenitors extensively throughout this project. The progenitor, developed by Robert T Curtis, is a special type of infinite group formed by a semi-direct product of a free group m*n and a transitive permutation group of degree n. Since progenitors are infinite, we add necessary relations to produce finite homomorphic images. Curtis found that any non-abelian simple group is a homomorphic image of a progenitor of the form 2*n: N. In particular, we will investigate progenitors that generate two of the Mathieu sporadic groups, M11 and M11, as well as some classical groups. We will prove their existences a variety of different ways, including the process of double coset enumeration, Iwasawa's Lemma, and linear fractional mappings. We will also investigate the various techniques of finding finite images and their corresponding isomorphism types.

En utilisant une technique de reecriture de termes dans un langage formel de categories, un theoreme de coherence d'une classe d'isomorphismes canoniques est prouvee dans les categories localement closes. Une telle methode trouve ses applications dans l'etude de la decidabilite et de la coherence des isomorphismes de types

L'objet de cette thèse est la méta-théorie du Calcul des Constructions Inductives (CCI), c'est à dire les Calcul des Constructions étendu par des types et des prédicats inductifs. Le Calcul des Constructions a été présenté en 1985 par Thierry Coquand. Il s'agit d'un lambda-calcul typé qui, à travers l'isomorphisme dit de Curry-Howard, peut-être vu comme un formalisme logique. Ce système qui étend à la fois la logique d'ordre superieur de Church et les systèmes de Martin-Löf est particulièrement expressif du point de vue algorithmique et peut facilement être mis en oeuvre sur ordinateur.
Dans le Calcul des Constructions originel, les types de données (entiers, listes, sommes, etc) sont représentés dans le lambda-calcul à travers un codage imprédicatif. Cette solution est élégante mais conduit à un certain nombre de difficultés pratiques et théoriques. Pour y remédier, Thierry Coquand et Christine Paulin-Mohring on proposé d'étendre le formalisme par un mécanisme génerique de définitions inductives. C'est cette extension, utilisée dans le système Coq, qui est étudiée dans cette thèse. Le résultat essentiel est que le système vérifie bien la proprieté de normalisation forte. On en déduit les proprietés de cohérence logique, de confluence et de décidabilité du typage.
L'aspect le plus spectaculaire de l'extension par des types inductifs est la possibilité de définir de nouveaux types et de nouvelles propositions par récurrence structurelle (élimination forte). Cette caractéristique, qui donne toute sa signification à la notion de types dépendants, augmente énormément le pouvoir de la règle de conversion, et par là, la difficulté de la preuve de normalisation. L'interprétation de l'élimination forte dans une preuve de normalisation par réductibilité est la nouveauté essentielle de ce travail.
De plus, nous considérons ici un système avec eta-conversion. Une conséquence est que la propriété de confluence n'est plus combinatoire et doit être prouvée après la normalisation, ce qui augmente à nouveau la difficulté de la preuve de celle-ci. A ce titre, nous présentons également quelques résultats nouveaux sur des systèmes non-normalisants qui montrent que pour des lambda-calculs typés, la propriété de confluence est logique et non combinatoire.

The goal of this presentation is to find original symmetric presentations of finite groups. It is frequently the case, that progenitors factored by appropriate relations produce simple and even sporadic groups as homomorphic images. We have discovered two of the twenty-six sporadic simple groups namely, M12, J1 and the Lie type group Suz(8). In addition several linear and classical groups will also be presented. We will present several progenitors including: 2*12: 22 x (3 : 2), 2*11: PSL2(11), 2*5: (5 : 4) which have produced the homomorphic images: M12 : 2, Suz(8) x 2, and J1 x 2. We will give monomial progenitors whose homomorphic images are: 17*10 :m PGL2(9), 3*4:m Z2 ≀D4 , and 13*2:m (22 x 3) : 2 which produce the homomorphic images:132 : ((2 x 13) : (2 x 3)), 2 x S9, and (22)•PGL4(3). Once we have a presentation of a group we can verify the group's existence through double coset enumeration. We will give proofs of isomorphism types of the presented images: S3 x PGL2(7) x S5, 28:A5, and 2•U4(2):2.

At the heart of the connections between Proof Theory and Type Theory, the Curry-Howard correspondence provides proof-terms with computational features and equational theories, i.e. notions of normalisation and equivalence. This dissertation contributes to extend its framework in the directions of proof-theoretic formalisms (such as sequent calculus) that are appealing for logical purposes like proof-search, powerful systems beyond propositional logic such as type theories, and classical (rather than intuitionistic) reasoning. Part I is entitled Proof-terms for Intuitionistic Implicational Logic. Its contributions use rewriting techniques on proof-terms for natural deduction (Lambda-calculus) and sequent calculus, and investigate normalisation and cut-elimination, with call-by-name and call-by-value semantics. In particular, it introduces proof-term calculi for multiplicative natural deduction and for the depth-bounded sequent calculus G4. The former gives rise to the calculus Lambdalxr with explicit substitutions, weakenings and contractions that refines the Lambda-calculus and Beta-reduction, and preserves strong normalisation with a full notion of composition of substitutions. The latter gives a new insight to cut-elimination in G4. Part II, entitled Type Theory in Sequent Calculus develops a theory of Pure Type Sequent Calculi (PTSC), which are sequent calculi that are equivalent (with respect to provability and normalisation) to Pure Type Systems but better suited for proof-search, in connection with proof-assistant tactics and proof-term enumeration algorithms. Part III, entitled Towards Classical Logic, presents some approaches to classical type theory. In particular it develops a sequent calculus for a classical version of System F_omega. Beyond such a type theory, the notion of equivalence of classical proofs becomes crucial and, with such a notion based on parallel rewriting in the Calculus of Structures, we compute canonical representatives of equivalent proofs.

This thesis is composed of three separate parts. The first part deals with definability and productivity issues of equational systems defining polymorphic stream functions. The main result consists of showing such systems composed of only unary stream functions complete with respect to specifying computable unary polymorphic stream functions. The second part deals with syntactic and semantic notions of isomorphism of finitary inductive types and associated decidability issues. We show isomorphism of so-called guarded types decidable in the set and syntactic model, verifying that the answers coincide. The third part deals with homotopy levels of hierarchical univalent universes in homotopy type theory, showing that the n-th universe of n-types has truncation level strictly n+1.

Dependently typed programming languages allow the type system to express arbitrary propositions of intuitionistic logic, thanks to the Curry-Howard isomorphism. Taking full advantage of this type system requires defining more types than usual, in order to encode logical correctness criteria into the definitions of datatypes. While an abundance of specialized types helps ensure correctness, it comes at the cost of needing to redefine common functions for each specialized type. This dissertation makes an effort to attack the problem of code reuse in dependently typed languages. Our solution is to write generic functions, which can be applied to any datatype. Such a generic function can be applied to datatypes that are defined at the time the generic function was written, but they can also be applied to any datatype that is defined in the future. Our solution builds upon previous work on generic programming within dependently typed programming. Type theory supports generic programming using a construction known as a universe. A universe can be considered the model of a programming language, such that writing functions over it models writing generic programs in the programming language. Historically, there has been a trade-off between the expressive power of the modeled programming language, and the kinds of generic functions that can be written in it. Our dissertation shows that no such trade-off is necessary, and that we can write future-proof generic functions in a model of a dependently typed programming language with a rich collection of types.

The main aim of this thesis is to make formal proofs more universal by expressing them in a common logical framework. More specifically, we use the lambda-Pi-calculus modulo rewriting, a lambda calculus equipped with dependent types and term rewriting, as a language for defining logics and expressing proofs in those logics. By representing propositions as types and proofs as programs in this language, we design translations of various systems in a way that is efficient and that preserves their meaning. These translations can then be used for independent proof checking and proof interoperability. In this work, we focus on the translation of logics based on type theory that allow both computation and higher-order quantification as steps of reasoning. Pure type systems are a well-known example of such computational higher-order systems, and form the basis of many modern proof assistants. We design a translation of functional pure type systems to the lambda-Pi-calculus modulo rewriting based on previous work by Cousineau and Dowek. The translation preserves typing, and in particular it therefore also preserves computation. We show that the translation is adequate by proving that it is conservative with respect to the original systems. We also adapt the translation to support universe cumulativity, a feature that is present in modern systems such as intuitionistic type theory and the calculus of inductive constructions. We propose to use explicit coercions to handle the implicit subtyping that is present in cumulativity, bridging the gap between pure type systems and type theory with universes à la Tarski. We also show how to preserve the expressivity of the original systems by adding equations to guarantee that types have a unique term representation, thus maintaining the completeness of the translation. The results of this thesis have been applied in automated proof translation tools. We implemented programs that automatically translate the proofs of HOL, Coq, and Matita, to Dedukti, a type-checker for the lambda-Pi-calculus modulo rewriting. These proofs can then be re-checked and combined together to form new theories in Dedukti, which thus serves as an independent proof checker and a platform for proof interoperability. We tested our tools on a variety of libraries. Experimental results confirm that our translations are correct and that they are efficient compared to the state of the art.

We have investigated several monomial and permutation progenitors, including 2*8 : [8 : 2], 2*18 : [(22 x 3) : (3x2)], 2*16 : [22 : 4], and 2*16 : 24, 5*2 :m [4•22], 5*2 :m [(4x2) :• 2], 103∗2 :m [17 : 2] and 103∗4 :m [17 : 4]. We have discovered original, to the best of our knowledge, symmetric presentations of a number of finite groups, including PSL(2, 7), M12 , A6 : 2, A7 , PSL(2, 25), 25 :• S4, 24 : S3, PSL(2, 271), 12 x PSL(2, 13), and U(3, 7) : 2. We will present our construction of several of these images, including the Mathieu sporadic simple group M12 over the maximal subgroup PSL(2, 11), PSL(2, 17) over D9, PSL(2, 16) : 2 over [24 : 5] and PGL(2, 7) over S3. We will also give our method of finding isomorphism classes of images.

Nous nous intéressons ici à la génération de programmes certifiés
corrects par construction. Ces programmes sont obtenus en
extrayant l'information pertinente de preuves constructives réalisées
dans l'assistant de preuves Coq.

Une telle traduction, ou "extraction", des preuves constructives
en programmes fonctionnels n'est pas nouvelle, elle correspond
à un isomorphisme bien connu sous le nom de Curry-Howard. Et
l'assistant Coq comporte depuis longtemps un tel outil d'extraction.
Mais l'outil précédent présentait d'importantes limitations. Certaines
preuves Coq étaient ainsi hors de son champ d'application, alors que
d'autres engendraient des programmes incorrects.

Afin de résoudre ces limitations, nous avons effectué une refonte
complète de l'extraction dans Coq, tant du point de vue de la théorie
que de l'implantation. Au niveau théorique, cette refonte a entraîné
la réalisation de nouvelles preuves de correction de ce mécanisme
d'extraction, preuves à la fois complexes et originales. Concernant
l'implantation, nous nous sommes efforcés d'engendrer du code
extrait efficace et réaliste, pouvant en particulier être intégré dans des
développement logiciels de plus grande échelle, par le biais de
modules et d'interfaces.

Enfin, nous présentons également plusieurs études de cas illustrant
les possibilités de notre nouvelle extraction. Nous décrivons ainsi la
certification d'une bibliothèque modulaire d'ensembles finis, et
l'obtention de programmes d'arithmétique réelle exacte à partir d'une
formalisation d'analyse réelle constructive. Même si des progrès
restent encore à obtenir, surtout dans ce dernier cas, ces exemples
mettent en évidence le chemin déjà parcouru.

Sverige är beroende av nystartade företag och entreprenörer för att finansiera landets välstånd. Riskkapitalbolag innehar ofta en betydande roll för de nya företagen när verksamheten ska utvecklas eller expandera. Bolagen assisterar de nya företagen med ett brett spektrum av nyckelaktiviteter som finansiering, operativt arbete, strategi eller kontaktnät. Tidigare studier visar att riskkapitalfinansierade bolag både växer snabbare och lyckas oftare. Samtidigt visar forskningen att riskkapitalbolag präglas av stort risktagande och övermod vid sina investeringar. Emellertid finns mindre djupgående forskning om vilka konkreta faktorer och omständigheter som resulterar i de olika utfallen. Syftet med examensarbetet är att skapa en bättre förståelse för specifika faktorer som påverkar svenska riskkapitalbolags beslutsfattande och resulterar i särskilda utfall. Undersökningen ämnar att betona likheter och skillnader i riskhanteringen av investeringsval mellan riskkapitalbolagen där utfallen antingen resulterar i nytta eller förlust för bolagen. För att uppfylla syftet har institutionella teorin, kognitiva bias och moderna portföljteorin aktualiserats. Undersökningen genomfördes genom intervjuer med beslutsfattare från åtta stycken konfidentiella riskkapitalbolag. Samtliga bolag kodades om för att säkerställa konfidentialitet i syfte att erhålla djupare inblickar i deras investeringsutfall. De erhållna resultaten visar på att framförallt kognitiva bias men även den institutionella teorin förklarade de olika investeringsutfallen väl. Riskkapitalbolagen präglades av stark övermod vid sina misslyckade investeringar och medelstark vid sina lyckade. Riskkapitalbolagen var också starkt påverkade från både extern tryck av samhället men även av interna riktlinjer vid sina investeringar. Flera branschmönster har också kartlagts vid både lyckade och misslyckade investeringar däribland syndikering av kapital, efterfrågan av serieentreprenörer och att det enligt de själva vanligtvis är entreprenören eller marknaden som är anledningen till att investeringen inte lyckas. Resultatet antyder också att en av de största svårigheterna för riskkapitalbolagen är att bedöma entreprenörernas möjligheter att utveckla företaget. Den mest tänkbara anledningen till att riskkapitalbolagen har starka tendenser till övermod är för att det krävs för att lyckas i branschen. Inget nystartat bolag är riskfritt och för att våga investera i branschen behövs stark tilltro till sin egen förmåga.
Sweden is dependent upon start-ups and entrepreneurs in order to successfully finance domestic prosperity. Venture capital (VC) companies often play a significant role for new companies when the business is to be developed or expanded. The VC companies support the new companies with a wide range of key features. Such as financing, operational work, strategy or contact networks. Previous studies show that VC-financed companies both grow faster and succeed more often than non VC-backed companies. At the same time, research shows that VC-companies are characterized by great risk-taking and audaciousness in their investments. However, there is less in-depth research on what explicit factors and circumstances result in the successful and unsuccessful investments. The purpose of the study is to create a better understanding of similarities and differences in different investment outcomes and highlight the patterns of their investments. Institutional theory, cognitive bias and modern portfolio theory are the theories used in this study. The survey was conducted through eight semi-structured qualitative interviews with different decision makers from VC-companies in Sweden. In order to gain a deeper understanding of their investment outcomes all company names were re-coded. The obtained results showed that cognitive biases was the primary theory of explanation. However, the institutional theory could also explain the different investment outcomes. The VC-companies were characterized by strong audaciousness with their failed investments and medium audaciousness with the successful. The requirement of success in the VC-industry explains why the companies have tendencies to be audacious in their decision making. A strong confidence is needed when investing in start-up companies since these companies imply a great risk. External societal pressure and internal guidelines strongly influence the investments of the VC. The study identified several industry patterns for both successful and unsuccessful investments.  The patterns include syndication of capital and demand for serial entrepreneurs. The study also showed a pattern of venture capitalists explaining their unsuccessful investment due to issues with the entrepreneur or the market. The results suggest that one of the greatest difficulties for VC-companies is to assess the ability of the entrepreneur to develop the company.

Two major applications of lambda calculi in computer science are functional programming languages and mechanized reasoning systems (or, proof assistants). According to the Curry--Howard correspondence, it is possible, in principle, to design a unified language based on a typed lambda calculus for both logical reasoning and programming. However, the different requirements of programming languages and reasoning systems make it difficult to design such a unified language that provides both. Programming languages usually extend lambda calculi with programming-friendly features (e.g., recursive datatypes, general recursion) for supporting the flexibility to model various computations, while sacrificing logical consistency. Logical reasoning systems usually extend lambda calculi with logic-friendly features (e.g., induction principles, dependent types) for paradox-free inference over fine-grained properties, while being more restrictive in modeling computations. In this dissertation, we design and implement a language called Nax that embraces benefits of both. Nax accepts all recursive datatypes, thus, allowing the same flexibility of defining recursive datatypes as in functional languages. Nax supports a number of Mendler-style recursion schemes that can express various kinds of recursive computations and also guarantee termination. Nax supports term-indexed types to support specifications of fine-grained properties. In addition, Nax supports a conservative extension of Hindley--Milner type inference. The theoretical contributions of this dissertation include theories for Mendler-style recursion schemes and term-indexed types, which we developed to establish strong normalization and logical consistency of Nax.

L'assistant de preuve Coq permet de s'assurer mécaniquement de la correction de chaque étape de raisonnement dans une preuve. Ce système peut également servir au développement de programmes certifiés. En effet, Coq utilise en interne un langage typé dérivé du lambda-calcul, le calcul des constructions inductives (CIC). Ce langage est directement utilisable pour programmer, et un mécanisme, l'extraction, permet de traduire les programmes CIC vers des langages à plus large audience tels qu'OCaml, Haskell ou Scheme. L'extraction n'est pas un simple changement de syntaxe: CIC dispose d'un système de types très riche, mais en contrepartie, des entités purement logiques peuvent apparaître dans les programmes et impacter leurs performances. L'extraction se charge également d'effacer ces parties logiques. Dans cette thèse, nous nous attaquons à la certification de l'extraction elle-même. Nous avons prouvé sa correction dans le cadre d'une formalisation entière de Coq en Coq. Cette formalisation ne correspond pas exactement au CIC implanté dans Coq, mais nous avons tout de même réalisé notre étude avec l'implantation concrète de Coq en tête. Nous proposons également une nouvelle méthode de certification des programmes extraits, dans le cadre concret du système Coq existant
The Coq proof assistant mechanically checks the consistency of the logical reasoning in a proof. It can also be used to develop certified programs. Indeed, Coq uses intemally a typed language derived from lambda-calculus, the calculus of inductive constructions (CIC). This language can be directl; used by a programmer, and a procedure, extraction, allows one to translate CIC programs into more widely used languages such as OCaml, Haskell or Scheme. Extraction is not a mere syntax change: the type System of CIC is very rich, but purely logical entities can appear inside programs, impacting their performance. Extraction erases these logical artefacts as well. In this thesis, we tackle certification of the extraction itself. We have proved its correction in the context of a full formalization of Coq in Coq. Even though this formalization is not exactly Coq, we worked on it with the concrete implementation of Coq in mind. We also propose a new way to certify extracted programs, in the concrete setting of the existing Coq System

Dans cette thèse, nous montrons que la traduction logique dite « dialectica » définie par Gödel en 1958 peut être exprimée dans le formalisme de la correspondance de Curry-Howard qui met en relation les preuves venant de la logique avec les programmes informatique. En particulier, on peut la voir comme une forme faible de contrôle délimité permettant d'observer l'utilisation des variables libres d'un terme par le biais des piles contre lesquelles elles se retrouvent coupées. Nous rendons cette constatation formelle en simplifiant la traduction originale de Gödel, grâce à une reformulation linéaire dûe à De Paiva, et en l'exprimant au travers de la machine de Krivine. La simplification de cette traduction permet en outre de l'adapter aisément au cas de la théorie des types dépendants. Un certain nombre de variantes sont en outre définies et étudiées. Par ailleurs, nous formulons une présentation de l'appel par nécessité dans un cadre plus canonique basé sur l'utilisation d'une notion de contexte hétérodoxe, appelés contextes de clôture
In this thesis, we show that the logical translation known as « dialectica » defined by Gödel in 1958 can be expressed in the Curry-Howard correspondance formalism, relating logical proofs to computer programs. In particular, it can be seen as a weak form of delimited control allowing to observe the use of free variables of a term through the stacks against which they are cut. We make this observation formal by simplifying Gödel's original translation, thanks to a linear reformulation due to De Paiva, and expressing it in the Krivine abstract machine. Such a simplification allows for an easy adaptation to the dependently-typed case. Quite a few variants are then defined and scrutinized. In addition, we give a presentation of the call-by-need reduction in a more canonical fashion, based on the use of a heterodox notion of contexts known as closure contexts

In this thesis, we will give our discovery of original symmetric presentations of several important groups. We have investigated permutation and monomial progenitors 2*8: (23: 22), 2*9: (32: 24), 2*10: (24: (2 × 5)), 5*4:m (23: 22), 7*8:m (32: 24), and 3*5:m (24: (2 × 5)). The finite images of the above progenitors include the Mathieu sporadic group M12, the linear groups L2(8) and L2(13), and the extensions S6 × 2, 28 : .L2(8) , and 27 : .A5. We will show our construction of the four groups S3 , L2(8), L2(13), and S6 × 2 over S3, 22, S3 : 2, and S5, by using the technique of double coset enumeration. We will also provide isomorphism types all of the groups that have appeared as finite homomorphic images. We will show that the group L2(8) does not satisfy the conditions of Iwasawas Lemma and that the group L2(13) is simple by Iwasawas Lemma. We give constructions of M22 × 2 and M22 as homomorphic images of the progenitor S6.

L'objet de cette thèse est l'extension des méthodes de la théorie des types intersections non-idempotents, introduite par Gardner et de Carvalho, à des cadres dépassant le lambda-calcul stricto sensu.- Nous proposons d'abord une caractérisation de la normalisation de tête et de la normalisation forte du lambda-mu calcul (déduction naturelle classique) en introduisant des types unions non-idempotents. Comme dans le cas intuitionniste, la non-idempotence nous permet d'extraire du typage des informations quantitatives ainsi que des preuves de terminaison beaucoup plus élémentaires que dans le cas idempotent. Ces résultats nous conduisent à définir une variante à petits pas du lambda-mu-calcul, dans lequel la normalisation forte est aussi caractérisée avec des méthodes quantitatives. - Dans un deuxième temps, nous étendons la caractérisation de la normalisation faible dans le lambda-calcul pur à un lambda-calcul infinitaire étroitement lié aux arbres de Böhm et dû à Klop et al. Ceci donne une réponse positive à une question connue comme le problème de Klop. À cette fin, il est nécessaire d'introduire conjointement un système (système S) de types infinis utilisant une intersection que nous qualifions de séquentielle, et un critère de validité servant à se débarrasser des preuves dégénérées auxquelles les grammaires coinductives de types donnent naissance. Ceci nous permet aussi de donner une solution au problème n°20 de TLCA (caractérisation par les types des permutations héréditaires). Il est à noter que ces deux problèmes n'ont pas de solution dans le cas fini (Tatsuta, 2007).- Enfin, nous étudions le pouvoir expressif des grammaires coinductives de types, en dehors de tout critère de validité. Nous devons encore recourir au système S et nous montrons que tout terme est typable de façon non triviale avec des types infinis et que l'on peut extraire de ces typages des informations sémantiques comme l'ordre (arité) de n'importe quel lambda-terme. Ceci nous amène à introduire une méthode permettant de typer des termes totalement non-productifs, dits termes muets, inspirée de la logique du premier ordre. Ce résultat prouve que, dans l'extension coinductive du modèle relationnel, tout terme a une interprétation non vide. En utilisant une méthode similaire, nous montrons aussi que le système S collapse surjectivement sur l'ensemble des points de ce modèle
In this dissertation, we extend the methods of non-idempotent intersection type theory, pioneered by Gardner and de Carvalho, to some calculi beyond the lambda-calculus.- We first present a characterization of head and strong normalization in the lambda-mu calculus (classical natural deduction) by introducing non-idempotent union types. As in the intuitionistic case, non-idempotency allows us to extract quantitative information from the typing derivations and we obtain proofs of termination that are far more elementary than those in the idempotent case. These results leads us to define a small-step variant of the lambda-mu calculus, in which strong normalization is also characterized by means of quantitative methods.- In the second part of the dissertation, we extend the characterization of weak normalization in the pure lambda-calculus to an infinitary lambda-calculus narrowly related to Böhm trees, which was introduced by Klop et al. This gives a positive answer to a question known as Klop's problem. In that purpose, it is necessary to simultaneously introduce a system (system S) featuring infinite types and resorting to an intersection operator that we call sequential, and a validity criterion in order to discard unsound proofs that coinductive grammars give rise to. This also allows us to give a solution to TLCA problem #20 (type-theoretic characterization of hereditary permutations). It is to be noted that those two problem do not have a solution in the finite case (Tatsuta, 2007).- Finally, we study the expressive power of coinductive type grammars, without any validity criterion. We must once more resort to system S and we show that every term is typable in a non-trivial way with infinite types and that one can extract semantical information from those typings e.g. the order (arity) of any lambda-term. This leads us to introduce a method that allows typing totally unproductive terms (the so-called mute terms), which is inspired from first order logic. This result establishes that, in the coinductive extension of the relational model, every term has a non-empty interpretation. Using a similar method, we also prove that system S surjectively collapses on the set of points of this model

En génie logiciel, les méthodes modernes de développement (ex. Le MDA) s'appuient de manière cruciale sur les notions de modélisation et de transformation. Ces méthodes peuvent s'interpréter à l'aide de la théorie des graphes. La difficulté théorique réside aujourd'hui dans l'ajout sur ces graphes de données supplémentaires sur lesquelles il est nécessaire de pouvoir effectuer des calculs. Notre travail s'est focalisé sur le développement d'un cadre mathématique sûr afin d'appliquer ces transformations. Les théories des catégories (à travers le double pushout) et des types inductifs (fonctions de calcul très expressives) nous ont permis de donner une solution unifiée à ce problème dans laquelle une seule opération permet de travailler sur la structure et de calculer avec les attributs en définissant des fonctions entre graphes possédant une partie contravariante pour le travail des attributs. De plus, les propriétés usuelles des systèmes de réécriture sont vérifiées
Due to the new requirements of modern software, researchers in software engineering have created more efficient development methods based on the concept of modeling (for example, the MDA) to control every stage of development. From a theoretical point of view, these methods are based on graphs and graph transformations. The theoretical difficulty lies in adding on these graphs data on which it must be possible to do computations. Our work has focused on developing a mathematical framework to implement these changes. The theories of categories (through the double pushout) and inductive types (very expressive computation functions) allowed us to provide a unified solution to this problem in which a single operation can transform the structure and compute with the attributes. In addition, the usual properties of rewriting systems are checked

In this thesis I study metric aspects of finite nearly simple groups. Its four distinct chapters deal with four different questions. In the first chapter, I give a full description of the normal subgroup lattice of any algebraic ultraproduct of universal finite quasisimple groups. In the second, I investigate approximation questions for arbitrary abstract and topological groups by families of finite groups with conjugacy-invariant norms. In the third chapter, I prove that the map induced by any non-trivial word on the metric ultraproduct of classical groups of Lie type of unbounded rank is always surjective using cohomological and algebraic methods. In the last chapter, it is proved that (simple) metric ultraproducts of finite classical groups of Lie type of unbounded rank with different field sizes are always non-isomorphic. Also, if the field sizes are equal, two such ultraproducts can only be isomorphic if the Lie types are equal or one Lie type is orthogonal and the other symplectic.:Introduction 0 Notation, basic definitions, and facts 0.1 Group theory 0.2 Some ring and field theory 0.3 Ultraproducts and norms 1 The normal subgroup lattice of an algebraic ultraproduct 1.1 Introduction 1.2 Auxiliary geometric results 1.3 Relative bounded normal generation in universal finite quasisimple groups 1.4 The lattice of normal subgroups 2 Metric approximation of groups by finite groups 2.1 Introduction 2.2 Preliminaries 2.2.1 On C-approximable abstract groups 2.2.2 On C-approximable topological groups 2.3 On Sol-approximable groups 2.4 On Fin-approximable groups 2.5 On the approximability of Lie groups 3 Word maps are surjective on metric ultraproducts 3.1 Introduction 3.2 Symmetric groups 3.2.1 Power words 3.2.2 The cycle structure of elements from PSL_2(q) 3.2.3 Effective surjectivity of word maps over finite fields 3.2.4 Proof of Theorem 3.1 3.3 Unitary groups 3.3.1 Proof of Theorem 3.3 3.3.2 Further implications 3.3.3 Concluding remarks 3.4 Finite groups of Lie type 3.4.1 The linear case 3.4.2 The case of quasisimple groups of Lie type stabilizing a form 3.4.3 An alternative way of proving Theorem 3.1 using wreath products 4 Isomorphism questions for metric ultraproducts 4.1 Introduction 4.2 Description of conjugacy classes in S_U, GL_U(q), and PGL_U(q) 4.3 Characterization of torsion elements in S_U , GL_U(q), and PGL_U(q) 4.4 Faithful action of S_U and PGL_U(q) 4.5 Centralizers in S_U , GL_U(q), Sp_U(q), GO_U(q), and GU_U(q) 4.6 Centralizers in PGL_U(q), PSp_U(q), PGO_U(q), and PGU_U(q) 4.7 Double centralizers of torsion elements 4.7.1 The case S_U 4.7.2 The case PGL_U(q), PSp_U(q), PGO_U(q), and PGU_U(q) 4.8 Distinction of metric ultraproducts 4.8.1 Computation of e_G(o) when gcd{o,p}=gcd{o,|Z|}=1 4.8.2 Proof of Theorem 4.1 Index of Symbols Index Bibliography
In dieser Doktorarbeit studiere ich metrische Aspekte von endlichen fast-einfachen Gruppen. Ihre vier Kapitel beschäftigen sich mit vier unterschiedlichen Themenfeldern. Im ersten Kapitel gebe ich eine vollständige Beschreibung des Normalteilerverbandes eines algebraischen Ultraproduktes von universellen endlichen quasieinfachen Gruppen. Im zweiten beschäftige ich mich mit Approximationsfragen für beliebige abstrakte und topologische Gruppen durch Familien von endlichen Gruppen, auf denen eine konjugationsinvariante Norm erklärt ist. Im dritten Kapitel beweise ich, dass die Abbildung auf einem metrischen Ultraprodukt von klassischen Gruppen vom Lie-Typ von unbeschränktem Rang, die von einem beliebigen nicht-trivialen Wort induziert wird, immer surjektiv ist. Dabei verwende ich sowohl kohomologische als auch algebraische Methoden. Im letzten Kapitel beweise ich, dass (einfache) metrische Ultraprodukte von klassischen endlichen Gruppen vom Lie-Typ von unbeschränktem Rang mit unterschiedlicher Körpergröße immer nicht-isomorph sind. Ist die Körpergröße gleich, so können zwei solche Gruppen nur dann isomorph sein, falls sie auch denselben Lie-Typ haben, oder eine vom orthogonalen Typ und die andere vom symplektischen ist.:Introduction 0 Notation, basic definitions, and facts 0.1 Group theory 0.2 Some ring and field theory 0.3 Ultraproducts and norms 1 The normal subgroup lattice of an algebraic ultraproduct 1.1 Introduction 1.2 Auxiliary geometric results 1.3 Relative bounded normal generation in universal finite quasisimple groups 1.4 The lattice of normal subgroups 2 Metric approximation of groups by finite groups 2.1 Introduction 2.2 Preliminaries 2.2.1 On C-approximable abstract groups 2.2.2 On C-approximable topological groups 2.3 On Sol-approximable groups 2.4 On Fin-approximable groups 2.5 On the approximability of Lie groups 3 Word maps are surjective on metric ultraproducts 3.1 Introduction 3.2 Symmetric groups 3.2.1 Power words 3.2.2 The cycle structure of elements from PSL_2(q) 3.2.3 Effective surjectivity of word maps over finite fields 3.2.4 Proof of Theorem 3.1 3.3 Unitary groups 3.3.1 Proof of Theorem 3.3 3.3.2 Further implications 3.3.3 Concluding remarks 3.4 Finite groups of Lie type 3.4.1 The linear case 3.4.2 The case of quasisimple groups of Lie type stabilizing a form 3.4.3 An alternative way of proving Theorem 3.1 using wreath products 4 Isomorphism questions for metric ultraproducts 4.1 Introduction 4.2 Description of conjugacy classes in S_U, GL_U(q), and PGL_U(q) 4.3 Characterization of torsion elements in S_U , GL_U(q), and PGL_U(q) 4.4 Faithful action of S_U and PGL_U(q) 4.5 Centralizers in S_U , GL_U(q), Sp_U(q), GO_U(q), and GU_U(q) 4.6 Centralizers in PGL_U(q), PSp_U(q), PGO_U(q), and PGU_U(q) 4.7 Double centralizers of torsion elements 4.7.1 The case S_U 4.7.2 The case PGL_U(q), PSp_U(q), PGO_U(q), and PGU_U(q) 4.8 Distinction of metric ultraproducts 4.8.1 Computation of e_G(o) when gcd{o,p}=gcd{o,|Z|}=1 4.8.2 Proof of Theorem 4.1 Index of Symbols Index Bibliography