Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_NumberField_InfinitePlaceTransport.lean

definition module

Transporting completions of a number field along conjugate infinite places

The context is a field extension K/E (an arbitrary Algebra E K of fields), an automorphism \sigma : K \simeq_{\mathrm{alg}[E]} K, and infinite places w, w' of K related by \sigma \cdot w = w' for Mathlib's action of K \simeq_{\mathrm{alg}[E]} K on InfinitePlace K. Two elementary consequences of such an equality are recorded: apply_apply_of_smul_eq, that w'(\sigma x) = w(x) for all x \in K, and inv_smul_eq_of_smul_eq, that \sigma^{-1} \cdot w' = w. A general preliminary, uniformContinuous_congr_of_forall_eq, says that for absolute values v on R and v' on S and a ring isomorphism f : R \simeq S with v'(f x) = v(x) for all x, the induced map WithAbs.congr v v' f between the absolute-value-normed copies of R and S is an isometry, hence uniformly continuous; applied to w, w', \sigma this gives uniformContinuous_congr_of_smul_eq.

The main definition, transport σ h for h : \sigma \cdot w = w', is a ring isomorphism K_w \simeq K_{w'} between the completions of K at w and at w': it is obtained by identifying w.Completion with the uniform-space completion of WithAbs w.1, applying the completion of the isometry WithAbs.congr attached to \sigma (whose inverse comes from the isometry attached to \sigma^{-1} and h read backwards), and identifying back with w'.Completion. Accompanying lemmas describe it: transport_apply and toCompletion_transport express it through UniformSpace.Completion.map, transport_coe states that it extends \sigma, sending the image of x \in K in K_w to the image of \sigma x in K_{w'}, and continuous_transport records continuity. Finally transportUnits σ h is the induced multiplicative isomorphism K_w^\times \simeq K_{w'}^\times obtained by functoriality of units, with coe_transportUnits identifying the underlying element of a transported unit with the transport of the underlying element.

Relation to Mathlib

No new structures are introduced: the construction is assembled from Mathlib's action of K ≃ₐ[E] K on InfinitePlace K, the comparison WithAbs.congr of absolute-value-normed copies of a field, UniformSpace.Completion.mapRingEquiv, and InfinitePlace.Completion.equiv.

Where it is used

The transport maps give the comparison between the completion at a place w and the completion at a conjugate place \sigma w, so that Galois-equivariant descriptions of archimedean local factors — products \prod_{w' \mid v} K_{w'}^\times indexed by the places above a place of E and the action of the stabiliser of w on K_w — can be stated without casts.

References

  1. J. Neukirch, Algebraic Number Theory, Grundlehren der mathematischen Wissenschaften 322, Springer, 1999, Ch. II–III

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_NumberField_InfinitePlaceTransport.lean

Declarations

Source

import Mathlib

set_option autoImplicit false

open NumberField

namespace NumberField.InfinitePlaceTransport

section general
variable {R S : Type*} [Field R] [Field S]

theorem uniformContinuous_congr_of_forall_eq (v : AbsoluteValue R ℝ) (v' : AbsoluteValue S ℝ) (f : R ≃+* S)
    (h : ∀ x, v' (f x) = v x) : UniformContinuous (WithAbs.congr v v' f) :=
  (AddMonoidHomClass.isometry_of_norm (WithAbs.congr v v' f) fun x => by
    rw [WithAbs.norm_eq_apply_ofAbs, WithAbs.norm_eq_apply_ofAbs, WithAbs.congr_apply]
    exact h _).uniformContinuous

end general

variable {E K : Type*} [Field E] [Field K] [Algebra E K]

theorem apply_apply_of_smul_eq {σ : K ≃ₐ[E] K} {w w' : InfinitePlace K} (h : σ • w = w') (x : K) : w' (σ x) = w x := by
  rw [← h, InfinitePlace.smul_apply, AlgEquiv.symm_apply_apply]

theorem inv_smul_eq_of_smul_eq {σ : K ≃ₐ[E] K} {w w' : InfinitePlace K} (h : σ • w = w') : σ⁻¹ • w' = w := by
  rw [← h, inv_smul_smul]

theorem uniformContinuous_congr_of_smul_eq {σ : K ≃ₐ[E] K} {w w' : InfinitePlace K} (h : σ • w = w') :
    UniformContinuous (WithAbs.congr w.1 w'.1 ((σ : K ≃ₐ[E] K) : K ≃+* K)) :=
  uniformContinuous_congr_of_forall_eq w.1 w'.1 _ (apply_apply_of_smul_eq h)

noncomputable def transport (σ : K ≃ₐ[E] K) {w w' : InfinitePlace K} (h : σ • w = w') : w.Completion ≃+* w'.Completion :=
  (InfinitePlace.Completion.equiv w).trans
    ((UniformSpace.Completion.mapRingEquiv (WithAbs.congr w.1 w'.1 ((σ : K ≃ₐ[E] K) : K ≃+* K))
      (uniformContinuous_congr_of_smul_eq h).continuous
      ((uniformContinuous_congr_of_smul_eq (inv_smul_eq_of_smul_eq h)).continuous.congr fun _ => rfl)).trans
    (InfinitePlace.Completion.equiv w').symm)

theorem transport_apply (σ : K ≃ₐ[E] K) {w w' : InfinitePlace K} (h : σ • w = w') (x : w.Completion) :
    transport σ h x = .ofCompletion
      (UniformSpace.Completion.map (WithAbs.congr w.1 w'.1 ((σ : K ≃ₐ[E] K) : K ≃+* K)) x.toCompletion) :=
  rfl

theorem toCompletion_transport (σ : K ≃ₐ[E] K) {w w' : InfinitePlace K} (h : σ • w = w') (x : w.Completion) :
    (transport σ h x).toCompletion
      = UniformSpace.Completion.map (WithAbs.congr w.1 w'.1 ((σ : K ≃ₐ[E] K) : K ≃+* K)) x.toCompletion :=
  rfl

theorem transport_coe (σ : K ≃ₐ[E] K) {w w' : InfinitePlace K} (h : σ • w = w') (x : WithAbs w.1) :
    transport σ h (x : w.Completion) = ((WithAbs.congr w.1 w'.1 ((σ : K ≃ₐ[E] K) : K ≃+* K) x : WithAbs w'.1) : w'.Completion) := by
  rw [transport_apply, InfinitePlace.Completion.coe_toCompletion,
    UniformSpace.Completion.map_coe (uniformContinuous_congr_of_smul_eq h)]

theorem continuous_transport (σ : K ≃ₐ[E] K) {w w' : InfinitePlace K} (h : σ • w = w') : Continuous (transport σ h) :=
  (InfinitePlace.Completion.continuous_ofCompletion w').comp
    (UniformSpace.Completion.continuous_map.comp (InfinitePlace.Completion.continuous_toCompletion w))

noncomputable abbrev transportUnits (σ : K ≃ₐ[E] K) {w w' : InfinitePlace K} (h : σ • w = w') :
    (w.Completion)ˣ ≃* (w'.Completion)ˣ :=
  Units.mapEquiv (transport σ h).toMulEquiv

theorem coe_transportUnits (σ : K ≃ₐ[E] K) {w w' : InfinitePlace K} (h : σ • w = w') (u : (w.Completion)ˣ) :
    ((transportUnits σ h u : (w'.Completion)ˣ) : w'.Completion) = transport σ h (u : w.Completion) := rfl

end NumberField.InfinitePlaceTransport

Statements phrased using this module (12)