1.4. Conjugation on principal generators🔗

Let I be an ideal of \mathcal{O}^+ such that I \mathcal{O} = (a) for some a \in \mathcal{O}, and write \overline{\,\cdot\,} for the action of complex conjugation on \mathcal{O}. Because I comes from the real subfield, the extended ideal I \mathcal{O} is fixed by conjugation.

Theorem1.4.1

uses 1used by 1✓L∃∀N

If I is an ideal of \mathcal{O}_{\mathbb{Q}(\zeta_p)^+}, then the extended ideal I\mathcal{O}_{\mathbb{Q}(\zeta_p)} is fixed by complex conjugation.

Definition 1.1.1

Lean code for Theorem1.4.1●1 theorem

theoremdefined in BernoulliRegular/TotallyRealSubfield/Conjugation.lean

complete

theorem BernoulliRegular.ideal_map_conj_eq.{u_1} (K : Type u_1) [Field K]
  [NumberField K] [NumberField.IsCMField K]
  (I :
    Ideal
      (NumberField.RingOfIntegers
        ↥(NumberField.maximalRealSubfield K))) :
  Ideal.map
      (NumberField.IsCMField.ringOfIntegersComplexConj
            K).toRingEquiv.toRingHom
      (Ideal.map
        (algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield K))
          (NumberField.RingOfIntegers K))
        I) =
    Ideal.map
      (algebraMap
        (NumberField.RingOfIntegers
          ↥(NumberField.maximalRealSubfield K))
        (NumberField.RingOfIntegers K))
      I

theorem BernoulliRegular.ideal_map_conj_eq.{u_1}
  (K : Type u_1) [Field K] [NumberField K]
  [NumberField.IsCMField K]
  (I :
    Ideal
      (NumberField.RingOfIntegers
        ↥(NumberField.maximalRealSubfield
            K))) :
  Ideal.map
      (NumberField.IsCMField.ringOfIntegersComplexConj
            K).toRingEquiv.toRingHom
      (Ideal.map
        (algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield
                K))
          (NumberField.RingOfIntegers K))
        I) =
    Ideal.map
      (algebraMap
        (NumberField.RingOfIntegers
          ↥(NumberField.maximalRealSubfield
              K))
        (NumberField.RingOfIntegers K))
      I

Complex conjugation acts trivially on ideals extended from `𝒪_{K⁺}`.

Proof for Theorem 1.4.1

uses 0

Conjugation fixes every element of \mathcal{O}^+ by definition of the maximal real subfield, so it commutes with the algebra map \mathcal{O}^+ \hookrightarrow \mathcal{O}. Functoriality of ideal extension gives \overline{I \mathcal{O}} = \overline{(\iota I)} = \iota I = I \mathcal{O}, where \iota denotes the inclusion.

Hence a and \overline a generate the same principal ideal, so they differ by a unit.

Theorem1.4.2

uses 1used by 1✓L∃∀N

There exists a unit u \in \mathcal{O}_{\mathbb{Q}(\zeta_p)}^\times such that \overline a = u\,a.

Theorem 1.4.1

Lean code for Theorem1.4.2●1 theorem

theoremdefined in BernoulliRegular/TotallyRealSubfield/Conjugation.lean

complete

theorem BernoulliRegular.conj_generator_associated.{u_1} (K : Type u_1)
  [Field K] [NumberField K] [NumberField.IsCMField K]
  (a : NumberField.RingOfIntegers K) (_ha : a ≠ 0)
  (I :
    Ideal
      (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K)))
  (hIa :
    Ideal.map
        (algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield K))
          (NumberField.RingOfIntegers K))
        I =
      Ideal.span {a})
  (hIca :
    Ideal.map
        (algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield K))
          (NumberField.RingOfIntegers K))
        I =
      Ideal.span
        {(NumberField.IsCMField.ringOfIntegersComplexConj K) a}) :
  ∃ u, (NumberField.IsCMField.ringOfIntegersComplexConj K) a = ↑u * a

theorem BernoulliRegular.conj_generator_associated.{u_1}
  (K : Type u_1) [Field K] [NumberField K]
  [NumberField.IsCMField K]
  (a : NumberField.RingOfIntegers K)
  (_ha : a ≠ 0)
  (I :
    Ideal
      (NumberField.RingOfIntegers
        ↥(NumberField.maximalRealSubfield
            K)))
  (hIa :
    Ideal.map
        (algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield
                K))
          (NumberField.RingOfIntegers K))
        I =
      Ideal.span {a})
  (hIca :
    Ideal.map
        (algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield
                K))
          (NumberField.RingOfIntegers K))
        I =
      Ideal.span
        {(NumberField.IsCMField.ringOfIntegersComplexConj
              K)
            a}) :
  ∃ u,
    (NumberField.IsCMField.ringOfIntegersComplexConj
          K)
        a =
      ↑u * a

If `(a) = (c(a))`, then `c(a)` differs from `a` by a unit.

Proof for Theorem 1.4.2

uses 0

From I \mathcal{O} = (a) and \overline{I \mathcal{O}} = I \mathcal{O} we have (a) = \overline{(a)} = (\overline a) in \mathcal{O}. Two generators of the same nonzero principal ideal in an integral domain are associates, so \overline a = u a for some u \in \mathcal{O}^\times.

Applying conjugation a second time recovers a, which forces the unit u to be antisymmetric under conjugation.

Theorem1.4.3

uses 1used by 1✓L∃∀N

The unit u satisfies u\,\overline u = 1.

Theorem 1.4.2

Lean code for Theorem1.4.3●1 theorem

theoremdefined in BernoulliRegular/TotallyRealSubfield/Conjugation.lean

complete

theorem BernoulliRegular.conj_unit_mul_eq_one.{u_1} (K : Type u_1) [Field K]
  [NumberField K] [NumberField.IsCMField K]
  (a : NumberField.RingOfIntegers K) (ha : a ≠ 0)
  (u : (NumberField.RingOfIntegers K)ˣ)
  (hu :
    (NumberField.IsCMField.ringOfIntegersComplexConj K) a = ↑u * a) :
  (NumberField.IsCMField.unitsComplexConj K) u * u = 1

theorem BernoulliRegular.conj_unit_mul_eq_one.{u_1}
  (K : Type u_1) [Field K] [NumberField K]
  [NumberField.IsCMField K]
  (a : NumberField.RingOfIntegers K)
  (ha : a ≠ 0)
  (u : (NumberField.RingOfIntegers K)ˣ)
  (hu :
    (NumberField.IsCMField.ringOfIntegersComplexConj
          K)
        a =
      ↑u * a) :
  (NumberField.IsCMField.unitsComplexConj
          K)
        u *
      u =
    1

If `c(a) = u a` with `a ≠ 0`, then `c(u) u = 1`.

Proof for Theorem 1.4.3

uses 0

Apply conjugation to \overline a = u a and use \overline{\overline a} = a: a = \overline{\overline a} = \overline u \cdot \overline a = \overline u \cdot u\,a. Cancelling a \ne 0 in the domain \mathcal{O} gives \overline u \, u = 1.

The next ingredient is the classification of antisymmetric units in a cyclotomic field, sometimes called the Kronecker–Kummer lemma. We use \zeta for \zeta_p and \langle \zeta \rangle for the cyclic group of p-th roots of unity.

Theorem1.4.4

uses 1used by 1✓L∃∀N

If u \in \mathcal{O}_{\mathbb{Q}(\zeta_p)}^\times satisfies u\overline u = 1, then there exist integers k,n such that u = (-1)^k \zeta_p^n.

Theorem 1.4.3

Lean code for Theorem1.4.4●1 theorem

theoremdefined in BernoulliRegular/TotallyRealSubfield/Conjugation.lean

complete

theorem BernoulliRegular.antisymmetric_unit_eq_neg_one_pow_mul_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}
  (u : (NumberField.RingOfIntegers K)ˣ)
  (hu : (NumberField.IsCMField.unitsComplexConj K) u * u = 1) :
  ∃ n k, u = (-1) ^ k * ⋯.unit ^ n

theorem BernoulliRegular.antisymmetric_unit_eq_neg_one_pow_mul_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}
  (u : (NumberField.RingOfIntegers K)ˣ)
  (hu :
    (NumberField.IsCMField.unitsComplexConj
            K)
          u *
        u =
      1) :
  ∃ n k, u = (-1) ^ k * ⋯.unit ^ n

An antisymmetric unit has the form `(-1)^k ζ^n`.

Proof for Theorem 1.4.4

uses 0

Let \sigma : K \hookrightarrow \mathbb{C} be any embedding. Since complex conjugation on K commutes with every embedding, the relation u\overline u = 1 implies |\sigma(u)|^2 = \sigma(u)\overline{\sigma(u)} = 1. Thus every Galois conjugate of u has complex absolute value 1. Kronecker's theorem therefore shows that u is a root of unity. The roots of unity in \mathbb{Q}(\zeta_p) are exactly the elements \{\pm \zeta_p^n : 0 \le n \le p-1\}, because p is odd. Hence there exist integers k,n such that u = (-1)^k \zeta_p^n.