Kummer's Criterion and Regular Primes in Lean

7.3. Exact p-saturation🔗

Let G be an abelian group and H\le E\le G. We use the exact image of the p-th power map: H^p := \{h^p : h\in H\}. This is not a closure or saturation of the image; it is the literal subgroup of p-th powers.

Definition7.3.1
uses 0
Used by 3
Reverse dependency previews
Preview
Theorem 7.3.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

Exact p-saturation. The subgroup H is p-saturated in E if H\le E and H\cap E^p \subseteq H^p. Equivalently, whenever x\in H and x=y^p for some y\in E, there exists z\in H such that x=z^p.

Lean code for Definition7.3.1●2 definitions
  • defdefined in BernoulliRegular/CyclotomicUnits/Saturation.lean
    complete
    def BernoulliRegular.pSaturated.{u_2} {G : Type u_2} [CommGroup G]
  (H E : Subgroup G) (p : ℕ) : Prop
    def BernoulliRegular.pSaturated.{u_2}
  {G : Type u_2} [CommGroup G]
  (H E : Subgroup G) (p : ℕ) : Prop
    `H` is `p`-saturated in `E` if an element of `H` that is a `p`th power in
`E` is already a `p`th power in `H`.
  • defdefined in BernoulliRegular/CyclotomicUnits/Saturation.lean
    complete
    def BernoulliRegular.pPowerSubgroup.{u_2} {G : Type u_2} [CommGroup G]
  (H : Subgroup G) (p : ℕ) : Subgroup G
    def BernoulliRegular.pPowerSubgroup.{u_2}
  {G : Type u_2} [CommGroup G]
  (H : Subgroup G) (p : ℕ) : Subgroup G
    Exact image of the `p`th-power map on a subgroup.  This is not a closure.

The useful criterion for C^+_{\mathrm{sq}} is stated in terms of exponent vectors. Every element of C^+_{\mathrm{sq}} can be written as (-1)^s\prod_{a=2}^{(p-1)/2}\varepsilon_a^{e_a}, s,e_a\in\mathbb{Z}. The following criterion uses these exponent vectors.

Theorem7.3.2
Statement uses 2
Statement dependency previews
Preview
Definition 7.2.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N

Exponent criterion for saturation. Assume that for every expression x=(-1)^s\prod_a \varepsilon_a^{e_a}\in C^+_{\mathrm{sq}} which is a p-th power in E^+, all exponents satisfy e_a\equiv 0 \pmod p. Then C^+_{\mathrm{sq}} is p-saturated in E^+.

Definition 7.3.1 Definition 7.2.1

Lean code for Theorem7.3.2●5 theorems
  • theoremdefined in BernoulliRegular/CyclotomicUnits/Saturation.lean
    complete
    theorem BernoulliRegular.exists_CPlusExponentProduct_of_mem_CPlus.{u_1} {p : ℕ}
  [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_three : 3 ≤ p)
  {x :
    (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K))ˣ}
  (hx : x ∈ BernoulliRegular.CPlus hp_three) :
  ∃ s e, BernoulliRegular.CPlusExponentProduct hp_three s e = x
    theorem BernoulliRegular.exists_CPlusExponentProduct_of_mem_CPlus.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)]
  {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_three : 3 ≤ p)
  {x :
    (NumberField.RingOfIntegers
        ↥(NumberField.maximalRealSubfield
            K))ˣ}
  (hx :
    x ∈ BernoulliRegular.CPlus hp_three) :
  ∃ s e,
    BernoulliRegular.CPlusExponentProduct
        hp_three s e =
      x
    Every element of `CPlus` has an integer-exponent expression in the sign and
the finite cyclotomic-unit generators.
  • theoremdefined in BernoulliRegular/CyclotomicUnits/Saturation.lean
    complete
    theorem BernoulliRegular.CPlus_pSaturated_of_generator_exponents_modP_zero.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p)
  (h :
    ∀ (s : ℤ) (e : Fin ((p - 3) / 2) → ℤ),
      BernoulliRegular.CPlusExponentProduct hp_three s e ∈
          BernoulliRegular.pPowerSubgroup BernoulliRegular.EPlus p →
        ∀ (a : Fin ((p - 3) / 2)), ↑(e a) = 0) :
  BernoulliRegular.pSaturated (BernoulliRegular.CPlus hp_three)
    BernoulliRegular.EPlus p
    theorem BernoulliRegular.CPlus_pSaturated_of_generator_exponents_modP_zero.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)]
  {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p)
  (h :
    ∀ (s : ℤ) (e : Fin ((p - 3) / 2) → ℤ),
      BernoulliRegular.CPlusExponentProduct
            hp_three s e ∈
          BernoulliRegular.pPowerSubgroup
            BernoulliRegular.EPlus p →
        ∀ (a : Fin ((p - 3) / 2)),
          ↑(e a) = 0) :
  BernoulliRegular.pSaturated
    (BernoulliRegular.CPlus hp_three)
    BernoulliRegular.EPlus p
    Concrete group-theoretic saturation criterion for `CPlus`.  CU-14e is
intended to provide the exponent-vanishing hypothesis from the logarithm
determinant; this theorem contains no p-adic logarithm input.
  • theoremdefined in BernoulliRegular/CyclotomicUnits/Saturation.lean
    complete
    theorem BernoulliRegular.CPlusExponentProduct_mem_CPlus.{u_1} {p : ℕ}
  [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) (s : ℤ) (e : Fin ((p - 3) / 2) → ℤ) :
  BernoulliRegular.CPlusExponentProduct hp_three s e ∈
    BernoulliRegular.CPlus hp_three
    theorem BernoulliRegular.CPlusExponentProduct_mem_CPlus.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)]
  {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) (s : ℤ)
  (e : Fin ((p - 3) / 2) → ℤ) :
  BernoulliRegular.CPlusExponentProduct
      hp_three s e ∈
    BernoulliRegular.CPlus hp_three
  • theoremdefined in BernoulliRegular/CyclotomicUnits/Saturation.lean
    complete
    theorem BernoulliRegular.neg_one_zpow_mem_pPowerSubgroup_CPlus.{u_1} {p : ℕ}
  [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) (s : ℤ) :
  (-1) ^ s ∈
    BernoulliRegular.pPowerSubgroup (BernoulliRegular.CPlus hp_three) p
    theorem BernoulliRegular.neg_one_zpow_mem_pPowerSubgroup_CPlus.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)]
  {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p)
  (s : ℤ) :
  (-1) ^ s ∈
    BernoulliRegular.pPowerSubgroup
      (BernoulliRegular.CPlus hp_three) p
  • theoremdefined in BernoulliRegular/CyclotomicUnits/Saturation.lean
    complete
    theorem BernoulliRegular.CPlusExponentProduct_pow_of_exponents_eq_mul.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) (s : ℤ)
  (e k : Fin ((p - 3) / 2) → ℤ)
  (hk : ∀ (a : Fin ((p - 3) / 2)), e a = ↑p * k a) :
  BernoulliRegular.CPlusExponentProduct hp_three s k ^ p =
    BernoulliRegular.CPlusExponentProduct hp_three s e
    theorem BernoulliRegular.CPlusExponentProduct_pow_of_exponents_eq_mul.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)]
  {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p)
  (s : ℤ) (e k : Fin ((p - 3) / 2) → ℤ)
  (hk :
    ∀ (a : Fin ((p - 3) / 2)),
      e a = ↑p * k a) :
  BernoulliRegular.CPlusExponentProduct
        hp_three s k ^
      p =
    BernoulliRegular.CPlusExponentProduct
      hp_three s e
Proof for Theorem 7.3.2
uses 0

Let x\in C^+_{\mathrm{sq}} and suppose x=y^p for some y\in E^+. Choose an exponent expression x=(-1)^s\prod_a \varepsilon_a^{e_a}. By hypothesis, e_a\equiv 0\pmod p for every a, so choose integers k_a with e_a=pk_a. Since p is odd, the sign term is already a p-th power of itself: ((-1)^s)^p=(-1)^s. Therefore x = (-1)^s\prod_a \varepsilon_a^{pk_a} = \left((-1)^s\prod_a \varepsilon_a^{k_a}\right)^p. The element inside the parentheses belongs to C^+_{\mathrm{sq}}, so x is a p-th power inside C^+_{\mathrm{sq}}. This is exactly p-saturation.