Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_GaloisRep_ComplexConjugation.lean

definition module

Complex conjugation in the absolute Galois group of

Working with \overline{\mathbb{Q}} realised as AlgebraicClosure ℚ, this module fixes an embedding into \mathbb{C} and the resulting involution in \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}). First, complexEmbedding is a \mathbb{Q}-algebra homomorphism \overline{\mathbb{Q}} \to \mathbb{C}, obtained by lifting along the algebraic extension \overline{\mathbb{Q}}/\mathbb{Q} into the algebraically closed field \mathbb{C}; it is in general not canonical, so a choice is made once and for all and all later statements refer to it. Via this embedding, \mathbb{C} is regarded as an \overline{\mathbb{Q}}-algebra, with the tower \mathbb{Q} \subseteq \overline{\mathbb{Q}} \subseteq \mathbb{C}. Next, complexConjAlgEquiv is complex conjugation z \mapsto \bar z on \mathbb{C}, packaged as a \mathbb{Q}-algebra automorphism of \mathbb{C} (conjugation fixes the rational numbers); it satisfies complexConjAlgEquiv * complexConjAlgEquiv = 1. Since \overline{\mathbb{Q}} is normal over \mathbb{Q}, restriction of \mathbb{Q}-automorphisms of \mathbb{C} to \overline{\mathbb{Q}} is a group homomorphism, and complexConjugation is defined as the image of complexConjAlgEquiv under it: the element c \in \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) characterised by complexEmbedding_complexConjugation, namely that the chosen embedding intertwines c with conjugation on \mathbb{C}, \iota(c x) = \overline{\iota(x)} for all x \in \overline{\mathbb{Q}}. That c is an involution is recorded in three forms: c \cdot c = 1, c^2 = 1 and c^{-1} = c.

The ExtCitation namespace supplies the archimedean local datum: archimedeanDecomposition is the subgroup \langle c \rangle of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) generated by c (as the subgroup of integer powers), archimedeanGen is c viewed as an element of that subgroup, and archimedeanLoc is the inclusion homomorphism of the subgroup into the absolute Galois group, sending archimedeanGen to complexConjugation.

Relation to Mathlib

Mathlib provides the ingredients — AlgebraicClosure ℚ, the lift of an algebraic extension into an algebraically closed field, the conjugation automorphism starRingAut of \mathbb{C}, and restriction of automorphisms along a normal subextension — but no named complex conjugation element of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}); the fixed embedding complexEmbedding and the element complexConjugation are this project's choices.

Where it is used

The element c is the archimedean ingredient of the Galois-theoretic input to the proof: it gives the decomposition group at the real place, used for the oddness of the mod p representation attached to a Frey curve (the cyclotomic character takes the value -1 at c) and for parity computations of H^0 at the real place.

References

  1. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154
  2. J.-P. Serre, Propriétés galoisiennes des points d'ordre fini des courbes elliptiques, Inventiones Mathematicae 15 (1972), 259–331

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_GaloisRep_ComplexConjugation.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

set_option autoImplicit false

local instance isAlgebraicQbar_cc : Algebra.IsAlgebraic ℚ (AlgebraicClosure ℚ) :=
  AlgebraicClosure.isAlgebraic ℚ
local instance isAlgClosureQbar_cc : IsAlgClosure ℚ (AlgebraicClosure ℚ) :=
  ⟨inferInstance, inferInstance⟩
local instance normalQbar_cc : Normal ℚ (AlgebraicClosure ℚ) :=
  IsAlgClosure.normal ℚ (AlgebraicClosure ℚ)
noncomputable local instance instDecEqQbar_cc : DecidableEq (AlgebraicClosure ℚ) :=
  Classical.decEq _

noncomputable def complexEmbedding : AlgebraicClosure ℚ →ₐ[ℚ] ℂ :=
  IsAlgClosed.lift

noncomputable local instance instAlgebraQbarComplex : Algebra (AlgebraicClosure ℚ) ℂ :=
  complexEmbedding.toRingHom.toAlgebra
local instance instTowerQbarComplex : IsScalarTower ℚ (AlgebraicClosure ℚ) ℂ :=
  IsScalarTower.of_algebraMap_eq' (Subsingleton.elim _ _)

noncomputable def complexConjAlgEquiv : ℂ ≃ₐ[ℚ] ℂ :=
  AlgEquiv.ofRingEquiv (f := starRingAut) fun x => map_ratCast (starRingEnd ℂ) x

@[simp] lemma complexConjAlgEquiv_apply (z : ℂ) : complexConjAlgEquiv z = starRingEnd ℂ z := rfl

lemma complexConjAlgEquiv_mul_self : complexConjAlgEquiv * complexConjAlgEquiv = 1 :=
  AlgEquiv.ext fun z => Complex.conj_conj z

noncomputable def complexConjugation : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ :=
  AlgEquiv.restrictNormalHom (F := ℚ) (K₁ := ℂ) (AlgebraicClosure ℚ) complexConjAlgEquiv

theorem complexEmbedding_complexConjugation (x : AlgebraicClosure ℚ) :
    complexEmbedding (complexConjugation x) = starRingEnd ℂ (complexEmbedding x) :=
  AlgEquiv.restrictNormal_commutes complexConjAlgEquiv (AlgebraicClosure ℚ) x

theorem complexConjugation_mul_self : complexConjugation * complexConjugation = 1 := by
  rw [complexConjugation, ← map_mul, complexConjAlgEquiv_mul_self, map_one]

theorem complexConjugation_sq : complexConjugation ^ 2 = 1 := by
  rw [sq]; exact complexConjugation_mul_self

theorem complexConjugation_inv : complexConjugation⁻¹ = complexConjugation :=
  inv_eq_of_mul_eq_one_right complexConjugation_mul_self

namespace ExtCitation

noncomputable def archimedeanDecomposition :
    Subgroup (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) :=
  Subgroup.zpowers complexConjugation

noncomputable def archimedeanGen : archimedeanDecomposition :=
  ⟨complexConjugation, Subgroup.mem_zpowers complexConjugation⟩

noncomputable def archimedeanLoc :
    archimedeanDecomposition →* (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) :=
  archimedeanDecomposition.subtype

@[simp] lemma archimedeanLoc_archimedeanGen :
    archimedeanLoc archimedeanGen = complexConjugation := rfl

end ExtCitation

Statements phrased using this module (34)