1.3. The class-group map and faithful-flat descent🔗

There is a natural extension-of-ideals map \mathrm{Cl}(\mathcal{O}_{\mathbb{Q}(\zeta_p)^+}) \longrightarrow \mathrm{Cl}(\mathcal{O}_{\mathbb{Q}(\zeta_p)}), \qquad [I] \longmapsto [I\,\mathcal{O}_{\mathbb{Q}(\zeta_p)}]. Throughout this chapter we abbreviate \mathcal{O} := \mathcal{O}_{\mathbb{Q}(\zeta_p)} and \mathcal{O}^+ := \mathcal{O}_{\mathbb{Q}(\zeta_p)^+}.

The proof that \hplus \mid h(\mathbb{Q}(\zeta_p)) reduces, by injectivity-implies-divisibility on finite groups, to the statement that an ideal I of \mathcal{O}^+ whose extension I \mathcal{O} is principal is itself principal. The basic descent input is that the ring extension \mathcal{O}^+ \subseteq \mathcal{O} is well-behaved.

Theorem1.3.1

uses 1used by 1✓L∃∀N

The ring of integers \mathcal{O}_{\mathbb{Q}(\zeta_p)} is faithfully flat over \mathcal{O}_{\mathbb{Q}(\zeta_p)^+}.

Definition 1.1.1

Lean code for Theorem1.3.1●1 theorem

theoremdefined in BernoulliRegular/TotallyRealSubfield/ClassGroup.lean

complete

theorem BernoulliRegular.ringOfIntegers_faithfullyFlat_maximalRealSubfield.{u_2}
  (L : Type u_2) [Field L] [NumberField L] :
  Module.FaithfullyFlat
    (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield L))
    (NumberField.RingOfIntegers L)

theorem BernoulliRegular.ringOfIntegers_faithfullyFlat_maximalRealSubfield.{u_2}
  (L : Type u_2) [Field L]
  [NumberField L] :
  Module.FaithfullyFlat
    (NumberField.RingOfIntegers
      ↥(NumberField.maximalRealSubfield
          L))
    (NumberField.RingOfIntegers L)

`𝓞 L` is faithfully flat over `𝓞(L⁺)`.

Proof for Theorem 1.3.1

uses 0

Flatness is automatic: \mathcal{O} is finitely generated and projective as a \mathcal{O}^+-module, because \mathbb{Q}(\zeta_p) / \mathbb{Q}(\zeta_p)^+ is a finite separable extension and the rings of integers form a tower of Dedekind domains. To upgrade flatness to faithful flatness it suffices, by the prime-spectrum criterion, to show that the comap \operatorname{Spec} \mathcal{O} \to \operatorname{Spec} \mathcal{O}^+ is surjective. Given a prime \mathfrak{q} \subseteq \mathcal{O}^+, choose any prime \mathfrak{Q} of \mathcal{O} lying over \mathfrak{q} (such a prime exists by integrality of \mathcal{O} over \mathcal{O}^+); then \mathfrak{Q} maps to \mathfrak{q} under the comap.

Faithful flatness gives the standard extension-contraction identity.

Theorem1.3.2

uses 1used by 1✓L∃∀N

For every ideal J \subseteq \mathcal{O}_{\mathbb{Q}(\zeta_p)^+} one has (J\mathcal{O}_{\mathbb{Q}(\zeta_p)}) \cap \mathcal{O}_{\mathbb{Q}(\zeta_p)^+} = J.

Theorem 1.3.1

Lean code for Theorem1.3.2●1 theorem

theoremdefined in BernoulliRegular/TotallyRealSubfield/ClassGroup.lean

complete

theorem BernoulliRegular.map_comap_eq_ringOfIntegers.{u_2} (L : Type u_2)
  [Field L] [NumberField L]
  (J :
    Ideal
      (NumberField.RingOfIntegers
        ↥(NumberField.maximalRealSubfield L))) :
  Ideal.comap
      (algebraMap
        (NumberField.RingOfIntegers
          ↥(NumberField.maximalRealSubfield L))
        (NumberField.RingOfIntegers L))
      (Ideal.map
        (algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield L))
          (NumberField.RingOfIntegers L))
        J) =
    J

theorem BernoulliRegular.map_comap_eq_ringOfIntegers.{u_2}
  (L : Type u_2) [Field L] [NumberField L]
  (J :
    Ideal
      (NumberField.RingOfIntegers
        ↥(NumberField.maximalRealSubfield
            L))) :
  Ideal.comap
      (algebraMap
        (NumberField.RingOfIntegers
          ↥(NumberField.maximalRealSubfield
              L))
        (NumberField.RingOfIntegers L))
      (Ideal.map
        (algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield
                L))
          (NumberField.RingOfIntegers L))
        J) =
    J

Extending and contracting ideals along `𝓞(L⁺) ⊆ 𝓞 L` is the identity.

Proof for Theorem 1.3.2

uses 0

Faithful flatness of \mathcal{O} over \mathcal{O}^+ is equivalent to the statement that the canonical map J \to J \mathcal{O} is injective for every ideal J of \mathcal{O}^+, and more strongly that contracting an extended ideal recovers the original. Concretely, J \mathcal{O} \cap \mathcal{O}^+ \subseteq J holds for any faithfully flat extension by the standard descent fact; the reverse inclusion is automatic.

Consequently, principality of an extended ideal descends as soon as one can exhibit a generator that already lives in the smaller ring of integers.

Theorem1.3.3

uses 1used by 1✓L∃∀N

Let I be an ideal of \mathcal{O}_{\mathbb{Q}(\zeta_p)^+}. If I\mathcal{O}_{\mathbb{Q}(\zeta_p)} = (b) for some element b lying in the image of \mathcal{O}_{\mathbb{Q}(\zeta_p)^+} \hookrightarrow \mathcal{O}_{\mathbb{Q}(\zeta_p)}, say b = \iota(b_0) with b_0 \in \mathcal{O}^+, then I = (b_0); in particular I is principal.

Theorem 1.3.2

Lean code for Theorem1.3.3●1 theorem

theoremdefined in BernoulliRegular/TotallyRealSubfield/ClassGroup.lean

complete

theorem BernoulliRegular.isPrincipal_of_map_eq_span_singleton_of_mem.{u_1}
  (K : Type u_1) [Field K] [NumberField K]
  (I :
    Ideal
      (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K)))
  (b₀ : NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K))
  (hb :
    Ideal.map
        (algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield K))
          (NumberField.RingOfIntegers K))
        I =
      Ideal.span
        {(algebraMap
              (NumberField.RingOfIntegers
                ↥(NumberField.maximalRealSubfield K))
              (NumberField.RingOfIntegers K))
            b₀}) :
  Submodule.IsPrincipal I

theorem BernoulliRegular.isPrincipal_of_map_eq_span_singleton_of_mem.{u_1}
  (K : Type u_1) [Field K] [NumberField K]
  (I :
    Ideal
      (NumberField.RingOfIntegers
        ↥(NumberField.maximalRealSubfield
            K)))
  (b₀ :
    NumberField.RingOfIntegers
      ↥(NumberField.maximalRealSubfield
          K))
  (hb :
    Ideal.map
        (algebraMap
          (NumberField.RingOfIntegers
            ↥(NumberField.maximalRealSubfield
                K))
          (NumberField.RingOfIntegers K))
        I =
      Ideal.span
        {(algebraMap
              (NumberField.RingOfIntegers
                ↥(NumberField.maximalRealSubfield
                    K))
              (NumberField.RingOfIntegers
                K))
            b₀}) :
  Submodule.IsPrincipal I

If `I · 𝒪_K = (b)` with `b` descending from `𝒪_{K⁺}`, then `I` is principal.

Proof for Theorem 1.3.3

uses 0

Write \iota : \mathcal{O}^+ \hookrightarrow \mathcal{O} for the inclusion. We use Theorem 1.3.2 twice. First, applied to I, I = \iota^{-1}(I \mathcal{O}) = \iota^{-1}((b)) = \iota^{-1}((\iota(b_0))). Second, applied to the principal ideal (b_0) \subseteq \mathcal{O}^+, \iota^{-1}((\iota(b_0))) = \iota^{-1}((b_0) \mathcal{O}) = (b_0). Combining the two displays gives I = (b_0).

The remaining work is therefore to start from an arbitrary generator a of I \mathcal{O} upstairs and replace it by an associate fixed by complex conjugation; that associate will then lie in \mathcal{O}^+.