Definitions/Def_FieldTheory_RatAlgClosureGalois.lean

This module contains a single instance declaration and no new mathematical notion. The field \overline{\mathbb{Q}}, realised as AlgebraicClosure ℚ, admits two \mathbb{Q}-algebra structures that are definitionally equal but syntactically distinct: AlgebraicClosure.instAlgebra ℚ, under which Mathlib records that the extension is Galois, and DivisionRing.toRatAlgebra, the canonical \mathbb{Q}-algebra structure carried by every division ring of characteristic zero. The declaration AlgebraicClosure.Rat.isGalois asserts IsGalois ℚ (AlgebraicClosure ℚ) with the algebra argument pinned explicitly, using @, to DivisionRing.toRatAlgebra; that is, the extension \mathbb{Q} \subseteq \overline{\mathbb{Q}}, viewed through that second structure, is normal and separable in Mathlib's sense. Mathematically this is just the statement that an algebraic closure of a field of characteristic zero is a Galois extension of it; the content of the module is entirely that the statement is available with the algebra slot filled by the canonical \mathbb{Q}-algebra structure that Mathlib attaches to every characteristic-zero division ring (Mathlib.Algebra.Algebra.Rat). The proof is Mathlib's IsAlgClosure.isGalois applied with the other, AlgebraicClosure.instAlgebra ℚ, structure, the two being interchangeable by definitional unfolding. Once this instance is in scope, the derived facts keyed on IsGalois — normality, separability, the fixed-field correspondence, and (with the profinite material) the compactness, Hausdorffness and total disconnectedness of the Krull-topologised automorphism group AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ — are usable with either of the two \mathbb{Q}-algebra structures.