Formalizing groups in type theory

TL;DR

This paper formalizes fundamental group theory concepts within a variant of type theory, enabling precise proofs and potential implementation in proof assistants based on the calculus of constructions.

Contribution

It introduces a simple, general definition of a group in the Calculus of Constructions with Definitions, formalizing key concepts and theorems in group theory.

Findings

Formal definitions of groups, subgroups, cosets, conjugates, normal subgroups, and quotient groups.

Formal derivation of related theorems within the type theory.

Potential for implementation in proof assistants based on calculus of constructions.

Abstract

In this paper we formalize some foundation concepts and theorems of group theory in a variant of type theory called the Calculus of Constructions with Definitions. In this theory we introduce definition of a group, which is both general and simple enough to use in formal proofs. Based on this definition, we formalize the concepts of subgroup, coset, conjugate, normal subgroup, and quotient group, and formally derive some related theorems. We aim to keep these formalizations transparent and concise, and as close as possible to the standard mathematical theory. The results can be implemented in proof assistants that are based on calculus of constructions.