Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_Mathlib_RingTheory_Valuation_LowerRamificationGroupGenerator.lean

definition module

Ramification depth computed from a single algebra generator

The module records the standard monogenicity device for ramification filtrations. The starting point is a divisibility lemma: for a commutative A-algebra R and x,y \in R, x-y divides \mathrm{aeval}\,x\,p - \mathrm{aeval}\,y\,p for every p \in A[X] (Polynomial.sub_dvd_aeval_sub). Consequently, for an A-algebra endomorphism \sigma of R and r \in A[x] one has \sigma x - x \mid \sigma r - r, and if A[x] = R (i.e. Algebra.adjoin A {x} = ⊤) this holds for all r \in R. The same statements are transported to a monoid G acting on R by ring automorphisms, under the hypothesis that the chosen \sigma \in G fixes the image of A pointwise, \sigma \cdot \mathrm{algebraMap}_{A,R}(a) = \mathrm{algebraMap}_{A,R}(a).

For R a discrete valuation ring with additive valuation addVal R, a group G acting by ring automorphisms and an A-algebra structure on R, the consequence is that \mathrm{addVal}(\sigma x - x) \le \mathrm{addVal}(\sigma r - r) for all r, hence that the ramification depth \mathrm{ramificationDepth}\,R\,G\,\sigma = \inf_{r \in R} \mathrm{addVal}(\sigma r - r) is attained at any single generator: it equals \mathrm{addVal}(\sigma x - x) whenever A[x] = R and \sigma fixes A. In particular the value \mathrm{addVal}(\sigma x - x) is independent of the generator chosen, and membership of \sigma in the i-th lower ramification group (the inertia subgroup of \mathfrak{m}^{i+1}, i.e. \sigma r - r \in \mathfrak{m}^{i+1} for all r) is equivalent to i+1 \le \mathrm{addVal}(\sigma x - x) in \mathbb{N}\cup\{\infty\}, and equivalently to \sigma x - x \in \mathfrak{m}^{i+1}. A variant replaces the fixing hypothesis by an SMulCommClass G A R assumption, and two further corollaries restate the depth formula and the membership criterion for a discretely valued valuation subring A \subseteq L with L/K an extension of fields, with G the decomposition subgroup of A over K.

Relation to Mathlib

The notions ramificationDepth and lowerRamificationGroup used here are the project's, defined in the imported modules on top of Mathlib's Ideal.inertia, IsDiscreteValuationRing.addVal and ValuationSubring.decompositionSubgroup; the first lemma is the aeval form of Mathlib's Polynomial.sub_dvd_eval_sub.

Where it is used

These criteria are the computational entry point to the lower ramification filtration: once the valuation ring is generated by one element over the base, ramification depths and the groups G_i are read off from the valuation of \sigma x - x for that generator.

References

  1. J.-P. Serre, Local Fields, Graduate Texts in Mathematics 67, Springer, 1979, Ch. IV §1

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_Mathlib_RingTheory_Valuation_LowerRamificationGroupDepth

set_option autoImplicit false

open IsLocalRing

theorem Polynomial.sub_dvd_aeval_sub {A R : Type*} [CommSemiring A] [CommRing R] [Algebra A R]
    (x y : R) (p : Polynomial A) :
    x - y ∣ Polynomial.aeval x p - Polynomial.aeval y p := by
  rw [Polynomial.aeval_def, Polynomial.aeval_def, ← Polynomial.eval_map, ← Polynomial.eval_map]
  exact Polynomial.sub_dvd_eval_sub x y _

theorem AlgHom.sub_dvd_sub_of_mem_adjoin_singleton {A R : Type*} [CommSemiring A] [CommRing R]
    [Algebra A R] (σ : R →ₐ[A] R) {x r : R} (hr : r ∈ Algebra.adjoin A {x}) :
    σ x - x ∣ σ r - r := by
  rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.mem_range] at hr
  obtain ⟨p, rfl⟩ := hr
  rw [← Polynomial.aeval_algHom_apply]
  exact Polynomial.sub_dvd_aeval_sub _ _ _

theorem AlgHom.sub_dvd_sub_of_adjoin_singleton_eq_top {A R : Type*} [CommSemiring A]
    [CommRing R] [Algebra A R] (σ : R →ₐ[A] R) {x : R} (hx : Algebra.adjoin A {x} = ⊤)
    (r : R) : σ x - x ∣ σ r - r :=
  σ.sub_dvd_sub_of_mem_adjoin_singleton (by rw [hx]; exact Algebra.mem_top)

theorem MulSemiringAction.smul_sub_dvd_smul_sub_of_mem_adjoin_singleton
    {A R : Type*} [CommSemiring A] [CommRing R] [Algebra A R]
    {G : Type*} [Monoid G] [MulSemiringAction G R] {σ : G}
    (hfix : ∀ a : A, σ • algebraMap A R a = algebraMap A R a)
    {x r : R} (hr : r ∈ Algebra.adjoin A {x}) :
    σ • x - x ∣ σ • r - r :=
  AlgHom.sub_dvd_sub_of_mem_adjoin_singleton
    { toFun := fun y => σ • y
      map_one' := smul_one σ
      map_mul' := fun y z => smul_mul' σ y z
      map_zero' := smul_zero σ
      map_add' := fun y z => smul_add σ y z
      commutes' := hfix } hr

theorem MulSemiringAction.smul_sub_dvd_smul_sub_of_adjoin_singleton_eq_top
    {A R : Type*} [CommSemiring A] [CommRing R] [Algebra A R]
    {G : Type*} [Monoid G] [MulSemiringAction G R] {σ : G}
    (hfix : ∀ a : A, σ • algebraMap A R a = algebraMap A R a)
    {x : R} (hx : Algebra.adjoin A {x} = ⊤) (r : R) :
    σ • x - x ∣ σ • r - r :=
  MulSemiringAction.smul_sub_dvd_smul_sub_of_mem_adjoin_singleton hfix
    (by rw [hx]; exact Algebra.mem_top)

namespace IsDiscreteValuationRing

variable {R : Type*} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable {G : Type*} [Group G] [MulSemiringAction G R]
variable {A : Type*} [CommSemiring A] [Algebra A R]

theorem addVal_smul_sub_le_of_adjoin_singleton_eq_top {σ : G}
    (hfix : ∀ a : A, σ • algebraMap A R a = algebraMap A R a)
    {x : R} (hx : Algebra.adjoin A {x} = ⊤) (r : R) :
    addVal R (σ • x - x) ≤ addVal R (σ • r - r) :=
  addVal_le_iff_dvd.mpr
    (MulSemiringAction.smul_sub_dvd_smul_sub_of_adjoin_singleton_eq_top hfix hx r)

theorem ramificationDepth_eq_addVal_of_adjoin_singleton_eq_top {σ : G}
    (hfix : ∀ a : A, σ • algebraMap A R a = algebraMap A R a)
    {x : R} (hx : Algebra.adjoin A {x} = ⊤) :
    ramificationDepth R G σ = addVal R (σ • x - x) := by
  refine le_antisymm ?_ ?_
  · rw [ramificationDepth_def]
    exact iInf_le _ x
  · rw [ramificationDepth_def]
    exact le_iInf fun r => addVal_smul_sub_le_of_adjoin_singleton_eq_top hfix hx r

theorem mem_lowerRamificationGroup_iff_le_addVal_of_adjoin_singleton_eq_top {i : ℕ} {σ : G}
    (hfix : ∀ a : A, σ • algebraMap A R a = algebraMap A R a)
    {x : R} (hx : Algebra.adjoin A {x} = ⊤) :
    σ ∈ IsLocalRing.lowerRamificationGroup R G i ↔
      (i : ℕ∞) + 1 ≤ addVal R (σ • x - x) := by
  rw [mem_lowerRamificationGroup_iff_le_ramificationDepth,
    ramificationDepth_eq_addVal_of_adjoin_singleton_eq_top hfix hx]

theorem mem_lowerRamificationGroup_iff_smul_sub_mem_pow_of_adjoin_singleton_eq_top {i : ℕ}
    {σ : G} (hfix : ∀ a : A, σ • algebraMap A R a = algebraMap A R a)
    {x : R} (hx : Algebra.adjoin A {x} = ⊤) :
    σ ∈ IsLocalRing.lowerRamificationGroup R G i ↔
      σ • x - x ∈ (IsLocalRing.maximalIdeal R) ^ (i + 1) := by
  rw [mem_lowerRamificationGroup_iff_le_addVal_of_adjoin_singleton_eq_top hfix hx,
    mem_maximalIdeal_pow_iff_le_addVal, Nat.cast_add_one]

theorem addVal_smul_sub_eq_of_adjoin_singleton_eq_top {σ : G}
    (hfix : ∀ a : A, σ • algebraMap A R a = algebraMap A R a) {x y : R}
    (hx : Algebra.adjoin A {x} = ⊤) (hy : Algebra.adjoin A {y} = ⊤) :
    addVal R (σ • x - x) = addVal R (σ • y - y) :=
  (ramificationDepth_eq_addVal_of_adjoin_singleton_eq_top hfix hx).symm.trans
    (ramificationDepth_eq_addVal_of_adjoin_singleton_eq_top hfix hy)

theorem ramificationDepth_eq_addVal_of_smulCommClass [SMulCommClass G A R] (σ : G)
    {x : R} (hx : Algebra.adjoin A {x} = ⊤) :
    ramificationDepth R G σ = addVal R (σ • x - x) :=
  ramificationDepth_eq_addVal_of_adjoin_singleton_eq_top (fun a => smul_algebraMap σ a) hx

theorem mem_lowerRamificationGroup_iff_le_addVal_of_smulCommClass [SMulCommClass G A R]
    {i : ℕ} {σ : G} {x : R} (hx : Algebra.adjoin A {x} = ⊤) :
    σ ∈ IsLocalRing.lowerRamificationGroup R G i ↔
      (i : ℕ∞) + 1 ≤ addVal R (σ • x - x) :=
  mem_lowerRamificationGroup_iff_le_addVal_of_adjoin_singleton_eq_top
    (fun a => smul_algebraMap σ a) hx

end IsDiscreteValuationRing

namespace ValuationSubring

variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
variable {A : ValuationSubring L} [IsDiscreteValuationRing A]
variable {O : Type*} [CommSemiring O] [Algebra O A]

theorem ramificationDepth_eq_addVal_of_adjoin_singleton_eq_top {σ : A.decompositionSubgroup K}
    (hfix : ∀ a : O, σ • algebraMap O A a = algebraMap O A a)
    {x : A} (hx : Algebra.adjoin O {x} = ⊤) :
    A.ramificationDepth K σ = IsDiscreteValuationRing.addVal A (σ • x - x) :=
  IsDiscreteValuationRing.ramificationDepth_eq_addVal_of_adjoin_singleton_eq_top hfix hx

theorem mem_lowerRamificationGroup_iff_le_addVal_of_adjoin_singleton_eq_top {i : ℕ}
    {σ : A.decompositionSubgroup K}
    (hfix : ∀ a : O, σ • algebraMap O A a = algebraMap O A a)
    {x : A} (hx : Algebra.adjoin O {x} = ⊤) :
    σ ∈ A.lowerRamificationGroup K i ↔
      (i : ℕ∞) + 1 ≤ IsDiscreteValuationRing.addVal A (σ • x - x) :=
  IsDiscreteValuationRing.mem_lowerRamificationGroup_iff_le_addVal_of_adjoin_singleton_eq_top
    hfix hx

end ValuationSubring

section Gates

example (p : Polynomial ℤ) :
    (-Polynomial.X - Polynomial.X : Polynomial ℤ) ∣
      (Polynomial.aeval (-Polynomial.X : Polynomial ℤ) p - p) := by
  have h := AlgHom.sub_dvd_sub_of_adjoin_singleton_eq_top
    (Polynomial.aeval (-Polynomial.X : Polynomial ℤ)) Polynomial.adjoin_X p
  rwa [Polynomial.aeval_X] at h

example : ¬ ((Polynomial.aeval (Polynomial.X + 1 : Polynomial ℤ) (1 : Polynomial ℤ) - 1) ∣
      (Polynomial.aeval (Polynomial.X + 1 : Polynomial ℤ) (Polynomial.X : Polynomial ℤ)
        - Polynomial.X)) := by
  intro h
  rw [map_one, sub_self, zero_dvd_iff, Polynomial.aeval_X, add_sub_cancel_left] at h
  exact one_ne_zero h

example : ¬ ((Polynomial.aeval (Polynomial.X + 1 : Polynomial ℤ) (Polynomial.X ^ 2 : Polynomial ℤ)
        - Polynomial.X ^ 2) ∣
      (Polynomial.aeval (Polynomial.X + 1 : Polynomial ℤ) (Polynomial.X : Polynomial ℤ)
        - Polynomial.X)) := by
  intro h
  have h1 := Polynomial.eval_dvd (x := (1 : ℤ)) h
  simp only [map_pow, Polynomial.aeval_X, Polynomial.eval_sub, Polynomial.eval_pow,
    Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_one] at h1
  norm_num at h1

example {R : Type*} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    {G : Type*} [Group G] [MulSemiringAction G R] :
    IsDiscreteValuationRing.ramificationDepth R G (1 : G) =
      IsDiscreteValuationRing.addVal R ((1 : G) • (0 : R) - 0) := by
  have htop : Algebra.adjoin R ({0} : Set R) = ⊤ := by
    rw [eq_top_iff]
    intro r _
    simpa using (Algebra.adjoin R ({0} : Set R)).algebraMap_mem r
  exact IsDiscreteValuationRing.ramificationDepth_eq_addVal_of_adjoin_singleton_eq_top
    (fun a => one_smul G _) htop

example {R : Type*} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    {G : Type*} [Group G] [MulSemiringAction G R] {A : Type*} [CommSemiring A] [Algebra A R]
    {σ : G} (hfix : ∀ a : A, σ • algebraMap A R a = algebraMap A R a)
    {x : R} (hx : Algebra.adjoin A {x} = ⊤) :
    σ ∈ IsLocalRing.lowerRamificationGroup R G 0 ↔
      σ • x - x ∈ IsLocalRing.maximalIdeal R := by
  rw [IsDiscreteValuationRing.mem_lowerRamificationGroup_iff_smul_sub_mem_pow_of_adjoin_singleton_eq_top
    hfix hx]
  simp

end Gates

/--
info: 'Polynomial.sub_dvd_aeval_sub' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in #print axioms Polynomial.sub_dvd_aeval_sub

/--
info: 'AlgHom.sub_dvd_sub_of_mem_adjoin_singleton' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in #print axioms AlgHom.sub_dvd_sub_of_mem_adjoin_singleton

/--
info: 'AlgHom.sub_dvd_sub_of_adjoin_singleton_eq_top' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in #print axioms AlgHom.sub_dvd_sub_of_adjoin_singleton_eq_top

/--
info: 'MulSemiringAction.smul_sub_dvd_smul_sub_of_mem_adjoin_singleton' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in #print axioms MulSemiringAction.smul_sub_dvd_smul_sub_of_mem_adjoin_singleton

/--
info: 'MulSemiringAction.smul_sub_dvd_smul_sub_of_adjoin_singleton_eq_top' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in #print axioms MulSemiringAction.smul_sub_dvd_smul_sub_of_adjoin_singleton_eq_top

/--
info: 'IsDiscreteValuationRing.addVal_smul_sub_le_of_adjoin_singleton_eq_top' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in #print axioms IsDiscreteValuationRing.addVal_smul_sub_le_of_adjoin_singleton_eq_top

/--
info: 'IsDiscreteValuationRing.ramificationDepth_eq_addVal_of_adjoin_singleton_eq_top' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in #print axioms IsDiscreteValuationRing.ramificationDepth_eq_addVal_of_adjoin_singleton_eq_top

/--
info: 'IsDiscreteValuationRing.mem_lowerRamificationGroup_iff_le_addVal_of_adjoin_singleton_eq_top' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in #print axioms IsDiscreteValuationRing.mem_lowerRamificationGroup_iff_le_addVal_of_adjoin_singleton_eq_top

/--
info: 'IsDiscreteValuationRing.mem_lowerRamificationGroup_iff_smul_sub_mem_pow_of_adjoin_singleton_eq_top' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in #print axioms IsDiscreteValuationRing.mem_lowerRamificationGroup_iff_smul_sub_mem_pow_of_adjoin_singleton_eq_top

/--
info: 'IsDiscreteValuationRing.addVal_smul_sub_eq_of_adjoin_singleton_eq_top' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in #print axioms IsDiscreteValuationRing.addVal_smul_sub_eq_of_adjoin_singleton_eq_top

/--
info: 'IsDiscreteValuationRing.ramificationDepth_eq_addVal_of_smulCommClass' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in #print axioms IsDiscreteValuationRing.ramificationDepth_eq_addVal_of_smulCommClass

/--
info: 'IsDiscreteValuationRing.mem_lowerRamificationGroup_iff_le_addVal_of_smulCommClass' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in #print axioms IsDiscreteValuationRing.mem_lowerRamificationGroup_iff_le_addVal_of_smulCommClass

/--
info: 'ValuationSubring.ramificationDepth_eq_addVal_of_adjoin_singleton_eq_top' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in #print axioms ValuationSubring.ramificationDepth_eq_addVal_of_adjoin_singleton_eq_top

/--
info: 'ValuationSubring.mem_lowerRamificationGroup_iff_le_addVal_of_adjoin_singleton_eq_top' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in #print axioms ValuationSubring.mem_lowerRamificationGroup_iff_le_addVal_of_adjoin_singleton_eq_top

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).