Related papers: Formalizing Galois Theory

We carry out some of Galois's work in the setting of an arbitrary first-order theory T. We replace the ambient algebraically closed field by a large model M of T, replace fields by definably closed subsets of M, assume that T codes finite…

For a particular class of Galois structures, we prove that the normal extensions are precisely those extensions that are "locally" split epic and trivial, and we use this to prove a "Galois theorem" for normal extensions. Furthermore, we…

We make explicit certain results around the Galois correspondence in the context of definable automorphism groups, and point out the relation to some recent papers dealing with the Galois theory of algebraic differential equations when the…

An algebraic technique is presented that does not use results of model theory and makes it possible to construct a general Galois theory of arbitrary nonlinear systems of partial differential equations. The algebraic technique is based on…

We construct a Galois correspondence for finite purely inseparable field extensions $F/K$, generalising a classical result of Jacobson for extensions of exponent one (where $x^p \in K$ for all $x\in F$).

We present a formalization, in the theorem prover Lean, of the classification of solvable Lie algebras of dimension at most three over arbitrary fields. Lie algebras are algebraic objects which encode infinitesimal symmetries, and as such…

We formalize Hall's Marriage Theorem in the Lean theorem prover for inclusion in mathlib, which is a community-driven effort to build a unified mathematics library for Lean. One goal of the mathlib project is to contain all of the topics of…

This paper explores formalizing Geometric (or Clifford) algebras into the Lean 3 theorem prover, building upon the substantial body of work that is the Lean mathematics library, mathlib. As we use Lean source code to demonstrate many of our…

This report presents a formalization of May's theorem in the proof assistant Coq. It describes how the theorem statement is first translated into Coq definitions, and how it is subsequently proved. Various aspects of the proof and related…

The fundamental theorem of arithmetic factorizes any integer into a product of prime numbers. The Jordan-Holder theorem dissolves many groups by their normal series which can be refined into composition series. The main topic of this thesis…

We classify all cubic function fields over any finite field, particularly developing a complete Galois theory which includes those cases when the constant field is missing certain roots of unity. In doing so, we find criteria which allow…

Recent advances in large language models show strong promise for formal reasoning. However, most LLM-based theorem provers have long been constrained by the need for expert-written formal statements as inputs, limiting their applicability…

This paper introduces a natural extension of Kolchin's differential Galois theory to positive characteristic iterative differential fields, generalizing to the non-linear case the iterative Picard-Vessiot theory recently developed by Matzat…

The aim of the paper is to introduce B-extensions which are the most symmetrical finite field extensions (a finite field extension $L/K$ is called a {\it B-extension} if the endomorphism algebra ${\rm End}_K(L)$ is generated by the algebra…

In (Borceux-Janelidze 2001) they prove a Categorical Galois Theorem for ordinary categories, and establish the main result of (Joyal-Tierney 1984), along with the classical Galois theory of Rings, as instances of this more general result.…

Born from years of teaching undergraduate and graduate algebra courses at Chongqing University, this text is designed to introduce Galois theory while minimizing prerequisites. It seeks to reconnect the abstract machinery of modern algeba:…

We prove the theorems which are equivalent to the Roland's results such that a new form of them allows to consider some generalizations. In particular, we give generators of primes more than a fixed prime.

According to Liouville's Theorem, an indefinite integral of an elementary function is usually not an elementary function. In this notes, we discuss that statement and a proof of this result. The differential Galois group of the extension…

We realize Frobenius conjugacy classes in Galois groups of certain $q$-polynomials over $\mathbb{F}_q(t)$ using specific degree 1 ideals. We combine this with methods from elementary linear algebra and group theory to realize transvections…

A Galois theory of differential fields with parameters is developed in a manner that generalizes Kolchin's theory. It is shown that all connected differential algebraic groups are Galois groups of some appropriate differential field…