Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_HahnSeries_Monodromy.lean

definition module

Character twists of Hahn series; point transport along fixing automorphisms

Let R be a commutative ring. For a character \chi \colon \mathrm{Multiplicative}\,\mathbb{Q} \to R^{\times}, HahnSeries.hahnTwistFun sends a Hahn series x with value group \mathbb{Q} to the series whose coefficient in degree a \in \mathbb{Q} is \chi(a)\,x_a; since the multipliers are units, the support is unchanged and remains partially well-ordered. HahnSeries.hahnTwist packages this as an R-algebra automorphism of HahnSeries ℚ R (relative to the power-series algebra structure), with inverse the twist by \chi^{-1}; multiplicativity comes from \chi(a+b)=\chi(a)\chi(b) on the antidiagonal, and \chi(0)=1 gives compatibility with the algebra map. A lemma layer records the coefficients, the action on a monomial \mathrm{single}\ a\ r \mapsto \mathrm{single}\ a\ (\chi(a)r), and the invariance of the support and of the order. HahnSeries.hahnTwistHom is the resulting monoid homomorphism from the character group to the group of R-algebra automorphisms. HahnSeries.MonoChar R is the subgroup of characters normalised by \chi(1)=1, i.e. the kernel of evaluation at the element 1 \in \mathbb{Q}, and HahnSeries.monodromy R is its image under hahnTwistHom; consequently every element of monodromy R fixes the monomial \mathrm{single}\ 1\ 1.

The second part concerns a Weierstrass curve E over a field K which is an algebra over a field k, together with an automorphism \sigma \in \mathrm{Aut}_k(K) satisfying E^{\sigma} = E, i.e. the coefficientwise image of E under \sigma is E itself. Then \sigma preserves nonsingular affine solutions, and WeierstrassCurve.Affine.Point.fixedTransport is the induced additive automorphism of the group of affine points: it fixes the point at infinity and sends (x,y) to (\sigma x, \sigma y). Additivity rests on the compatibility of \mathrm{negY}, the slope and the addition formulas with \sigma under the invariance hypothesis, with the case distinction of the chord–tangent law handled through the auxiliary declarations.

Relation to Mathlib

Hahn series with their power-series algebra structure, and the affine point group of a Weierstrass curve together with the behaviour of the addition formulas under a ring homomorphism, are Mathlib's; the character twist, the normalised character subgroup and the monodromy subgroup are the project's own, as is the transport of points along an automorphism fixing the curve (Mathlib's point maps go along a base change of the curve rather than from invariance of a fixed curve).

Where it is used

These constructions supply, on the one hand, a group of automorphisms of fractional-power expansions that acts trivially on the distinguished monomial of degree 1, and on the other hand the action of a field automorphism fixing a Weierstrass curve on its group of affine points; both are used by later modules of the development.

References

  1. J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 2nd ed., 2009

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

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib.RingTheory.HahnSeries.PowerSeries ↗
import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point ↗

noncomputable section

namespace HahnSeries

variable {R : Type*} [CommRing R]

def hahnTwistFun (χ : Multiplicative ℚ →* Rˣ) (x : HahnSeries ℚ R) : HahnSeries ℚ R where
  coeff a := χ (Multiplicative.ofAdd a) * x.coeff a
  isPWO_support' := x.isPWO_support'.mono fun a ha => by
    simp only [Function.mem_support] at ha ⊢
    exact fun h => ha (by rw [h, mul_zero])

theorem coeff_hahnTwistFun (χ : Multiplicative ℚ →* Rˣ) (x : HahnSeries ℚ R) (a : ℚ) :
    (hahnTwistFun χ x).coeff a = χ (Multiplicative.ofAdd a) * x.coeff a :=
  rfl

theorem support_hahnTwistFun (χ : Multiplicative ℚ →* Rˣ) (x : HahnSeries ℚ R) :
    (hahnTwistFun χ x).support = x.support := by
  ext a
  rw [mem_support, mem_support, coeff_hahnTwistFun]
  exact not_congr (Units.mul_right_eq_zero _)

theorem hahnTwistFun_single (χ : Multiplicative ℚ →* Rˣ) (a : ℚ) (r : R) :
    hahnTwistFun χ (single a r) = single a (χ (Multiplicative.ofAdd a) * r) := by
  ext b
  rw [coeff_hahnTwistFun]
  by_cases hb : b = a
  · subst hb
    rw [coeff_single_same, coeff_single_same]
  · rw [coeff_single_of_ne hb, coeff_single_of_ne hb, mul_zero]

def hahnTwist (χ : Multiplicative ℚ →* Rˣ) : HahnSeries ℚ R ≃ₐ[R] HahnSeries ℚ R where
  toFun := hahnTwistFun χ
  invFun := hahnTwistFun χ⁻¹
  left_inv x := by
    ext a
    rw [coeff_hahnTwistFun, coeff_hahnTwistFun, ← mul_assoc, ← Units.val_mul,
      MonoidHom.inv_apply, inv_mul_cancel, Units.val_one, one_mul]
  right_inv x := by
    ext a
    rw [coeff_hahnTwistFun, coeff_hahnTwistFun, ← mul_assoc, ← Units.val_mul,
      MonoidHom.inv_apply, mul_inv_cancel, Units.val_one, one_mul]
  map_mul' x y := by
    ext a
    have hset : Finset.antidiagonal (hahnTwistFun χ x).isPWO_support
        (hahnTwistFun χ y).isPWO_support a =
        Finset.antidiagonal x.isPWO_support y.isPWO_support a := by
      ext ij
      simp only [Finset.mem_antidiagonal, support_hahnTwistFun]
    rw [coeff_hahnTwistFun, coeff_mul, coeff_mul, hset, Finset.mul_sum]
    refine Finset.sum_congr rfl fun ij hij => ?_
    obtain ⟨-, -, hsum⟩ := Finset.mem_antidiagonal.mp hij
    rw [coeff_hahnTwistFun, coeff_hahnTwistFun, mul_mul_mul_comm, ← Units.val_mul, ← map_mul,
      ← ofAdd_add, hsum]
  map_add' x y := by
    ext a
    rw [coeff_hahnTwistFun, coeff_add, coeff_add, coeff_hahnTwistFun, coeff_hahnTwistFun,
      mul_add]
  commutes' r := by
    have hC : algebraMap R (HahnSeries ℚ R) r = HahnSeries.C r := by
      rw [HahnSeries.algebraMap_apply', PowerSeries.algebraMap_eq, HahnSeries.ofPowerSeries_C]
    have hCs : (HahnSeries.C r : HahnSeries ℚ R) = single (0 : ℚ) r := rfl
    show hahnTwistFun χ _ = _
    rw [hC, hCs, hahnTwistFun_single, ofAdd_zero, map_one, Units.val_one, one_mul]

@[simp]
theorem coeff_hahnTwist (χ : Multiplicative ℚ →* Rˣ) (x : HahnSeries ℚ R) (a : ℚ) :
    (hahnTwist χ x).coeff a = χ (Multiplicative.ofAdd a) * x.coeff a :=
  rfl

theorem hahnTwist_single (χ : Multiplicative ℚ →* Rˣ) (a : ℚ) (r : R) :
    hahnTwist χ (single a r) = single a (χ (Multiplicative.ofAdd a) * r) :=
  hahnTwistFun_single χ a r

theorem support_hahnTwist (χ : Multiplicative ℚ →* Rˣ) (x : HahnSeries ℚ R) :
    (hahnTwist χ x).support = x.support :=
  support_hahnTwistFun χ x

theorem order_hahnTwist (χ : Multiplicative ℚ →* Rˣ) (x : HahnSeries ℚ R) :
    (hahnTwist χ x).order = x.order := by
  by_cases hx : x = 0
  · rw [hx, map_zero]
  · have hx' : hahnTwist χ x ≠ 0 := fun h =>
      hx ((hahnTwist χ).injective (by rw [h, map_zero]))
    refine le_antisymm (order_le_of_coeff_ne_zero ?_) (order_le_of_coeff_ne_zero ?_)
    · rw [coeff_hahnTwist]
      exact fun h0 => hx (coeff_order_eq_zero.mp ((Units.mul_right_eq_zero _).mp h0))
    · exact fun h0 => hx' (coeff_order_eq_zero.mp (by rw [coeff_hahnTwist, h0, mul_zero]))

variable (R) in

def MonoChar : Subgroup (Multiplicative ℚ →* Rˣ) :=
  (MonoidHom.eval (Multiplicative.ofAdd (1 : ℚ))).ker

theorem mem_monoChar_iff {χ : Multiplicative ℚ →* Rˣ} :
    χ ∈ MonoChar R ↔ χ (Multiplicative.ofAdd (1 : ℚ)) = 1 :=
  Iff.rfl

def hahnTwistHom : (Multiplicative ℚ →* Rˣ) →* (HahnSeries ℚ R ≃ₐ[R] HahnSeries ℚ R) where
  toFun := hahnTwist
  map_one' := by
    refine AlgEquiv.ext fun x => ?_
    ext a
    rw [coeff_hahnTwist, MonoidHom.one_apply, Units.val_one, one_mul, AlgEquiv.one_apply]
  map_mul' χ₁ χ₂ := by
    refine AlgEquiv.ext fun x => ?_
    ext a
    rw [coeff_hahnTwist, AlgEquiv.mul_apply, coeff_hahnTwist, coeff_hahnTwist,
      MonoidHom.mul_apply, Units.val_mul, mul_assoc]

theorem hahnTwistHom_apply (χ : Multiplicative ℚ →* Rˣ) :
    (hahnTwistHom : (Multiplicative ℚ →* Rˣ) →* (HahnSeries ℚ R ≃ₐ[R] HahnSeries ℚ R)) χ =
      hahnTwist χ :=
  rfl

variable (R) in

def monodromy : Subgroup (HahnSeries ℚ R ≃ₐ[R] HahnSeries ℚ R) :=
  (MonoChar R).map hahnTwistHom

theorem fixes_single_one_of_mem_monodromy {m : HahnSeries ℚ R ≃ₐ[R] HahnSeries ℚ R}
    (hm : m ∈ monodromy R) :
    m (single (1 : ℚ) (1 : R)) = single (1 : ℚ) (1 : R) := by
  obtain ⟨χ, hχ, rfl⟩ := hm
  rw [hahnTwistHom_apply, hahnTwist_single, mem_monoChar_iff.mp hχ, Units.val_one, one_mul]

end HahnSeries

namespace WeierstrassCurve.Affine.Point

open WeierstrassCurve

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

theorem nonsingular_of_fixed (σ : K ≃ₐ[k] K) (E : WeierstrassCurve K)
    (hE : E.map (σ : K →+* K) = E) {x y : K} (h : E.toAffine.Nonsingular x y) :
    E.toAffine.Nonsingular (σ x) (σ y) := by
  have hE2 : E.toAffine.map (σ : K →+* K) = E.toAffine := hE
  have h' := (Affine.map_nonsingular (W := E.toAffine) (f := (σ : K →+* K))
    σ.injective x y).mpr h
  rwa [hE2] at h'

private def fixedFun (σ : K ≃ₐ[k] K) (E : WeierstrassCurve K)
    (hE : E.map (σ : K →+* K) = E) : E.toAffine.Point → E.toAffine.Point := fun P =>
  match P with
  | 0 => 0
  | some x y h => some (σ x) (σ y) (nonsingular_of_fixed σ E hE h)

private theorem map_symm_eq (σ : K ≃ₐ[k] K) (E : WeierstrassCurve K)
    (hE : E.map (σ : K →+* K) = E) : E.map (σ.symm : K →+* K) = E := by
  conv_lhs => rw [← hE]
  rw [WeierstrassCurve.map_map]
  have h : (σ.symm : K →+* K).comp (σ : K →+* K) = RingHom.id K := by
    ext z
    exact σ.symm_apply_apply z
  rw [h, WeierstrassCurve.map_id]

private theorem fixedFun_add [DecidableEq K] (σ : K ≃ₐ[k] K) (E : WeierstrassCurve K)
    (hE : E.map (σ : K →+* K) = E) (P Q : E.toAffine.Point) :
    fixedFun σ E hE (P + Q) = fixedFun σ E hE P + fixedFun σ E hE Q := by
  have hE2 : E.toAffine.map (σ : K →+* K) = E.toAffine := hE
  have hneg : ∀ x y : K, E.toAffine.negY (σ x) (σ y) = σ (E.toAffine.negY x y) := by
    intro x y
    conv_lhs => rw [← hE2]
    exact Affine.map_negY (W' := E.toAffine) (σ : K →+* K) x y
  have hslope : ∀ x₁ x₂ y₁ y₂ : K,
      E.toAffine.slope (σ x₁) (σ x₂) (σ y₁) (σ y₂) = σ (E.toAffine.slope x₁ x₂ y₁ y₂) := by
    intro x₁ x₂ y₁ y₂
    conv_lhs => rw [← hE2]
    exact Affine.map_slope (W := E.toAffine) (σ : K →+* K) x₁ x₂ y₁ y₂
  have haddX : ∀ x₁ x₂ ℓ : K,
      E.toAffine.addX (σ x₁) (σ x₂) (σ ℓ) = σ (E.toAffine.addX x₁ x₂ ℓ) := by
    intro x₁ x₂ ℓ
    conv_lhs => rw [← hE2]
    exact Affine.map_addX (W' := E.toAffine) (σ : K →+* K) x₁ x₂ ℓ
  have haddY : ∀ x₁ x₂ y₁ ℓ : K,
      E.toAffine.addY (σ x₁) (σ x₂) (σ y₁) (σ ℓ) = σ (E.toAffine.addY x₁ x₂ y₁ ℓ) := by
    intro x₁ x₂ y₁ ℓ
    conv_lhs => rw [← hE2]
    exact Affine.map_addY (W' := E.toAffine) (f := (σ : K →+* K)) (x₁ := x₁) (x₂ := x₂)
      (y₁ := y₁) (ℓ := ℓ)
  rcases P with _ | ⟨x₁, y₁, h₁⟩ <;> rcases Q with _ | ⟨x₂, y₂, h₂⟩
  any_goals rfl
  by_cases hxy : x₁ = x₂ ∧ y₁ = E.toAffine.negY x₂ y₂
  · rw [add_of_Y_eq hxy.1 hxy.2]
    exact (add_of_Y_eq (congrArg σ hxy.1) (by rw [hxy.2, hneg])).symm
  · have hxy' : ¬(σ x₁ = σ x₂ ∧ σ y₁ = E.toAffine.negY (σ x₂) (σ y₂)) := fun h =>
      hxy ⟨σ.injective h.1, σ.injective (by rw [hneg] at h; exact h.2)⟩
    rw [add_some hxy]
    show some _ _ _ = some _ _ _ + some _ _ _
    rw [add_some hxy']
    congr 1
    · rw [hslope, haddX]
    · rw [hslope, haddY]

def fixedTransport [DecidableEq K] (σ : K ≃ₐ[k] K) (E : WeierstrassCurve K)
    (hE : E.map (σ : K →+* K) = E) : E.toAffine.Point ≃+ E.toAffine.Point where
  toFun := fixedFun σ E hE
  invFun := fixedFun σ.symm E (map_symm_eq σ E hE)
  left_inv P := by
    rcases P with _ | ⟨x, y, h⟩
    · rfl
    · show some _ _ _ = some x y h
      congr 1
      · exact σ.symm_apply_apply x
      · exact σ.symm_apply_apply y
  right_inv P := by
    rcases P with _ | ⟨x, y, h⟩
    · rfl
    · show some _ _ _ = some x y h
      congr 1
      · exact σ.apply_symm_apply x
      · exact σ.apply_symm_apply y
  map_add' := fixedFun_add σ E hE

theorem fixedTransport_zero [DecidableEq K] (σ : K ≃ₐ[k] K) (E : WeierstrassCurve K)
    (hE : E.map (σ : K →+* K) = E) : fixedTransport σ E hE 0 = 0 :=
  rfl

theorem fixedTransport_some [DecidableEq K] (σ : K ≃ₐ[k] K) (E : WeierstrassCurve K)
    (hE : E.map (σ : K →+* K) = E) (x y : K) (h : E.toAffine.Nonsingular x y) :
    fixedTransport σ E hE (some x y h) = some (σ x) (σ y) (nonsingular_of_fixed σ E hE h) :=
  rfl

end WeierstrassCurve.Affine.Point

end

Statements phrased using this module (2)