1.5. A conjugation-fixed associate and descent to the real ring of integers🔗

The classification of the unit u is used to modify the generator a by an associate so that the new generator is fixed by conjugation. The serious content is to eliminate the possibility k odd; once this is done, n can be replaced by an even integer because p is odd, and a p-th root of unity adjustment produces the fixed associate.

1.5.1. Eliminating the minus-one factor🔗

Write \zeta = \zeta_p and \pi := \zeta - 1 \in \mathcal{O}. Let P = (\pi) be the unique prime of \mathcal{O} above p, and P^+ \subseteq \mathcal{O}^+ the prime below it. The extension \mathcal{O}^+ \subseteq \mathcal{O} ramifies totally at P^+ with e(P / P^+) = 2, that is, P^+ \mathcal{O} = P^2.

Theorem1.5.1.1

uses 1used by 1✓L∃∀N

Ramification at \pi. The ramification index of P^+ in \mathcal{O} equals 2: P^+ \mathcal{O} = P^2.

Definition 1.1.1

Lean code for Theorem1.5.1.1●1 theorem

theoremdefined in BernoulliRegular/TotallyRealSubfield/Conjugation.lean

complete

theorem BernoulliRegular.ramificationIdx_zetaPrimePlus_eq_two.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (K : Type u_1) [Field K]
  [NumberField K] [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K] :
  (BernoulliRegular.zetaPrimePlus p K).ramificationIdx
      (BernoulliRegular.zetaPrime p K) =
    2

theorem BernoulliRegular.ramificationIdx_zetaPrimePlus_eq_two.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp_odd : p ≠ 2) (K : Type u_1)
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K] :
  (BernoulliRegular.zetaPrimePlus p
          K).ramificationIdx
      (BernoulliRegular.zetaPrime p K) =
    2

The ramification index of `zetaPrime` over `zetaPrimePlus` is `2`.

Proof for Theorem 1.5.1.1

uses 0

Inside \mathcal{O} one has the identity P^+ \mathcal{O} = P^2 by an explicit computation with \zeta + \zeta^{-1} - 2 = -\pi \overline\pi \zeta^{-1}, exhibiting the totally ramified extension at the unique prime above p in the maximal real subfield.

Lemma1.5.1.2

uses 1used by 1✓L∃∀N

Even multiplicity of \pi in a descended generator. If I is a nonzero ideal of \mathcal{O}^+ with I \mathcal{O} = (a) and a \ne 0, then v_\pi(a) is even.

Theorem 1.5.1.1

Lean code for Lemma1.5.1.2●1 theorem

theoremdefined in BernoulliRegular/TotallyRealSubfield/Conjugation.lean

complete

theorem BernoulliRegular.multiplicity_zetaPrime_even_of_map_eq_span.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (K : Type u_1)
  [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (I :
    Ideal
      (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K)))
  (a : NumberField.RingOfIntegers K) (ha : a ≠ 0)
  (hIa :
    Ideal.map
        (algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield K))
          (NumberField.RingOfIntegers K))
        I =
      Ideal.span {a}) :
  Even (multiplicity (⋯.toInteger - 1) a)

theorem BernoulliRegular.multiplicity_zetaPrime_even_of_map_eq_span.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp_odd : p ≠ 2) (K : Type u_1)
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (I :
    Ideal
      (NumberField.RingOfIntegers
        ↥(NumberField.maximalRealSubfield
            K)))
  (a : NumberField.RingOfIntegers K)
  (ha : a ≠ 0)
  (hIa :
    Ideal.map
        (algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield
                K))
          (NumberField.RingOfIntegers K))
        I =
      Ideal.span {a}) :
  Even (multiplicity (⋯.toInteger - 1) a)

If `I · 𝒪_K = (a)` with `a ≠ 0`, then `v_(ζ-1)(a)` is even.

Proof for Lemma 1.5.1.2

uses 0

Let e = v_\pi(a), equivalently the multiplicity with which P = (\pi) appears in the prime factorisation of (a) = I \mathcal{O} in \mathcal{O}. For Dedekind extensions one has v_P(I \mathcal{O}) = e(P/P^+) \cdot v_{P^+}(I), and the ramification index e(P / P^+) = 2 by Theorem 1.5.1.1. Therefore v_\pi(a) = 2 \cdot v_{P^+}(I) is even.

The classification Theorem 1.4.4 is now refined to remove the possible -1.

Theorem1.5.1.3

Statement uses 2

Statement dependency previews

Preview

Theorem 1.4.4

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Pure \zeta-power form of the unit. With I, a, u as above and writing u = (-1)^k \zeta^n, the integer k is necessarily even, so there exists n with u = \zeta^n.

Theorem 1.4.4 Lemma 1.5.1.2

Lean code for Theorem1.5.1.3●1 theorem

theoremdefined in BernoulliRegular/TotallyRealSubfield/FixedAssociate.lean

complete

theorem BernoulliRegular.generator_unit_eq_zeta_pow.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (K : Type u_1) [Field K]
  [NumberField K] [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  {hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta p ℚ K) p}
  (I :
    Ideal
      (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K)))
  (a : NumberField.RingOfIntegers K)
  (u : (NumberField.RingOfIntegers K)ˣ) (ha : a ≠ 0)
  (hIa :
    Ideal.map
        (algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield K))
          (NumberField.RingOfIntegers K))
        I =
      Ideal.span {a})
  (hu : (NumberField.IsCMField.ringOfIntegersComplexConj K) a = ↑u * a)
  (hclass : ∃ n k, u = (-1) ^ k * ⋯.unit ^ n) : ∃ n, u = ⋯.unit ^ n

theorem BernoulliRegular.generator_unit_eq_zeta_pow.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp_odd : p ≠ 2) (K : Type u_1)
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  {hζ :
    IsPrimitiveRoot
      (IsCyclotomicExtension.zeta p ℚ K)
      p}
  (I :
    Ideal
      (NumberField.RingOfIntegers
        ↥(NumberField.maximalRealSubfield
            K)))
  (a : NumberField.RingOfIntegers K)
  (u : (NumberField.RingOfIntegers K)ˣ)
  (ha : a ≠ 0)
  (hIa :
    Ideal.map
        (algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield
                K))
          (NumberField.RingOfIntegers K))
        I =
      Ideal.span {a})
  (hu :
    (NumberField.IsCMField.ringOfIntegersComplexConj
          K)
        a =
      ↑u * a)
  (hclass :
    ∃ n k, u = (-1) ^ k * ⋯.unit ^ n) :
  ∃ n, u = ⋯.unit ^ n

If `u` is classified as a pure `ζ`-power, the possible `-1` factor is absent.

Proof for Theorem 1.5.1.3

uses 0

Suppose for contradiction that k is odd, so u = -\zeta^n. Let e = v_\pi(a) and write a = \pi^e b with \pi \nmid b (Lemma 1.5.1.2 applies and e is even). Conjugation sends \pi to \overline\pi = \gamma \cdot \pi, where the explicit unit \gamma can be computed as \gamma = -\zeta^{p-1} from \overline\zeta = \zeta^{p-1}. Substituting into \overline a = u a and cancelling \pi^e — using that \pi is prime and that \gamma^e \cdot \zeta^e = ((-1) \zeta)^e \cdot \zeta^{(p-1)e - e} simplifies using e even — yields \overline b = u' \cdot b where u' := \zeta^e \cdot u = -\zeta^{e+n}. Reducing modulo the prime P = (\pi) kills \pi and any factor of the form \zeta^m - 1, so \zeta^{e+n} \equiv 1 \pmod P and therefore u' + 1 \equiv 0 \pmod P. On the other hand \overline b \equiv b \pmod P since conjugation is trivial modulo \pi, so b (u' - 1) \equiv 0 \pmod P. Since b \notin P, this forces u' - 1 \in P. Combining u' + 1 \in P and u' - 1 \in P gives 2 \in P, which contradicts p odd (the prime P lies above p, not 2). Therefore k must be even, and (-1)^k = 1.

1.5.2. Constructing the conjugation-fixed associate🔗

Theorem1.5.2.1

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 1.5.2.2

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

There exists b \in \mathcal{O}_{\mathbb{Q}(\zeta_p)} such that (b) = (a) and \overline b = b.

Theorem 1.5.1.3

Lean code for Theorem1.5.2.1●1 theorem

theoremdefined in BernoulliRegular/TotallyRealSubfield/FixedAssociate.lean

complete

theorem BernoulliRegular.exists_conj_fixed_associate_of_classification.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (K : Type u_1)
  [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  {hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta p ℚ K) p}
  (I :
    Ideal
      (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K)))
  (a : NumberField.RingOfIntegers K)
  (u : (NumberField.RingOfIntegers K)ˣ)
  (hIa :
    Ideal.map
        (algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield K))
          (NumberField.RingOfIntegers K))
        I =
      Ideal.span {a})
  (hu : (NumberField.IsCMField.ringOfIntegersComplexConj K) a = ↑u * a)
  (hclass : ∃ n k, u = (-1) ^ k * ⋯.unit ^ n) :
  ∃ b,
    (NumberField.IsCMField.ringOfIntegersComplexConj K) b = b ∧
      Ideal.span {b} = Ideal.span {a}

theorem BernoulliRegular.exists_conj_fixed_associate_of_classification.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp_odd : p ≠ 2) (K : Type u_1)
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  {hζ :
    IsPrimitiveRoot
      (IsCyclotomicExtension.zeta p ℚ K)
      p}
  (I :
    Ideal
      (NumberField.RingOfIntegers
        ↥(NumberField.maximalRealSubfield
            K)))
  (a : NumberField.RingOfIntegers K)
  (u : (NumberField.RingOfIntegers K)ˣ)
  (hIa :
    Ideal.map
        (algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield
                K))
          (NumberField.RingOfIntegers K))
        I =
      Ideal.span {a})
  (hu :
    (NumberField.IsCMField.ringOfIntegersComplexConj
          K)
        a =
      ↑u * a)
  (hclass :
    ∃ n k, u = (-1) ^ k * ⋯.unit ^ n) :
  ∃ b,
    (NumberField.IsCMField.ringOfIntegersComplexConj
            K)
          b =
        b ∧
      Ideal.span {b} = Ideal.span {a}

The extra descent input removes the possible `-1` factor.

Proof for Theorem 1.5.2.1

uses 0

By Theorem 1.5.1.3 write u = \zeta^n. Since p is odd, 2 is invertible modulo p, and the map m \mapsto 2m is a bijection on \mathbb{Z}/p\mathbb{Z}. Choose m with n \equiv 2m \pmod p, so \zeta^n = (\zeta^m)^2. Set b := a \cdot \zeta^m. Then (b) = (a) because \zeta^m \in \mathcal{O}^\times, and using \overline{\zeta^m} = \zeta^{-m} together with \overline a = \zeta^n a = \zeta^{2m} a, \overline b = \overline a \cdot \zeta^{-m} = \zeta^{2m} a \cdot \zeta^{-m} = a \cdot \zeta^m = b.

An algebraic integer of \mathcal{O} fixed by complex conjugation lies in the image of \mathcal{O}^+.

Theorem1.5.2.2

uses 1used by 1✓L∃∀N

If b \in \mathcal{O}_{\mathbb{Q}(\zeta_p)} satisfies \overline b = b, then b lies in the image of \mathcal{O}_{\mathbb{Q}(\zeta_p)^+} \hookrightarrow \mathcal{O}_{\mathbb{Q}(\zeta_p)}.

Theorem 1.5.2.1

Lean code for Theorem1.5.2.2●1 theorem

theoremdefined in BernoulliRegular/TotallyRealSubfield/FixedAssociate.lean

complete

theorem BernoulliRegular.mem_ringOfIntegers_of_conj_eq_self.{u_1} (K : Type u_1)
  [Field K] [NumberField K] [NumberField.IsCMField K]
  (b : NumberField.RingOfIntegers K)
  (hb : (NumberField.IsCMField.ringOfIntegersComplexConj K) b = b) :
  b ∈
    Set.range
      ⇑(algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield K))
          (NumberField.RingOfIntegers K))

theorem BernoulliRegular.mem_ringOfIntegers_of_conj_eq_self.{u_1}
  (K : Type u_1) [Field K] [NumberField K]
  [NumberField.IsCMField K]
  (b : NumberField.RingOfIntegers K)
  (hb :
    (NumberField.IsCMField.ringOfIntegersComplexConj
          K)
        b =
      b) :
  b ∈
    Set.range
      ⇑(algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield
                K))
          (NumberField.RingOfIntegers K))

If `b` is fixed by conjugation, then it comes from `𝒪_{K⁺}`.

Proof for Theorem 1.5.2.2

uses 0

The maximal real subfield is by definition the fixed field of complex conjugation: \mathbb{Q}(\zeta_p)^+ = \mathbb{Q}(\zeta_p)^{\overline{\,\cdot\,}}. An element of \mathcal{O} \subseteq \mathbb{Q}(\zeta_p) fixed by \overline{\,\cdot\,} therefore lies in \mathbb{Q}(\zeta_p)^+, and being an algebraic integer it lies in \mathcal{O}^+.

Combining this with faithful-flat descent gives principality downstairs.

Theorem1.5.2.3

Statement uses 3

Statement dependency previews

Preview

Theorem 1.3.3

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Diekmann Proposition 55 / Washington 4.14. Let I be an ideal of \mathcal{O}_{\mathbb{Q}(\zeta_p)^+}. If the extended ideal I\mathcal{O}_{\mathbb{Q}(\zeta_p)} is principal, then I itself is principal.

Theorem 1.3.3 Theorem 1.5.2.2 Theorem 1.5.2.1

Lean code for Theorem1.5.2.3●1 theorem

theoremdefined in BernoulliRegular/TotallyRealSubfield/ClassGroup.lean

complete

theorem BernoulliRegular.isPrincipal_of_isPrincipal_map_Kplus.{u_1} (p : ℕ)
  [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (K : Type u_1) [Field K]
  [NumberField K] [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (I :
    Ideal
      (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K)))
  (hI :
    Submodule.IsPrincipal
      (Ideal.map
        (algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield K))
          (NumberField.RingOfIntegers K))
        I)) :
  Submodule.IsPrincipal I

theorem BernoulliRegular.isPrincipal_of_isPrincipal_map_Kplus.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp_odd : p ≠ 2) (K : Type u_1)
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (I :
    Ideal
      (NumberField.RingOfIntegers
        ↥(NumberField.maximalRealSubfield
            K)))
  (hI :
    Submodule.IsPrincipal
      (Ideal.map
        (algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield
                K))
          (NumberField.RingOfIntegers K))
        I)) :
  Submodule.IsPrincipal I

**Diekmann Prop. 55** (cf. Washington Thm. 4.14).

If an ideal of `𝒪_{K⁺}` becomes principal after extension to `𝒪_K`, then it
was already principal.

Proof for Theorem 1.5.2.3

uses 0

Write I \mathcal{O} = (a). We may assume a \ne 0, since the case I = 0 is trivial. By Theorem 1.4.1 the ideal I \mathcal{O} is conjugation-fixed, so by Theorem 1.4.2 there is a unit u with \overline a = u a, and by Theorem 1.4.3 this unit satisfies u \overline u = 1. The classification of antisymmetric units (Theorem 1.4.4) gives u = (-1)^k \zeta^n, and Theorem 1.5.1.3 eliminates the -1, so u = \zeta^n for some n. Theorem 1.5.2.1 produces b \in \mathcal{O} with (b) = (a) and \overline b = b, and Theorem 1.5.2.2 gives b = \iota(b_0) for some b_0 \in \mathcal{O}^+. We then have I \mathcal{O} = (b) = (\iota b_0), so Theorem 1.3.3 concludes that I = (b_0) is principal.