The Picard group of an order as a quotient of a ray class group

Let O be an order in a number field K with conductor 𝔣. Contraction J ↦ J ∩ O identifies the nonzero ideals of 𝓞 K coprime to 𝔣 with the nonzero ideals of O coprime to 𝔣, and the latter are invertible (NumberFieldOrder.integralIdealsAwayConductorEquiv). Taking Picard classes gives a monoid homomorphism NumberFieldOrder.picClass from the ideals of 𝓞 K prime to the conductor modulus to Pic O.

Its kernel consists of the principal ideals β 𝓞 K with a generator β ∈ O: in that case the contraction is β O, because β is a unit modulo 𝔣 already in O. In particular the ideals with a generator β ≡ 1 mod 𝔣 die in Pic O, so picClass factors through the ray class group of the conductor. The result is the congruence description of the Picard group of an order:

Pic O ≃ I_K(𝔣) / P_{K,O}(𝔣),

where I_K(𝔣) is the group of fractional ideals of 𝓞 K prime to 𝔣 and P_{K,O}(𝔣) is its subgroup generated by the principal ideals β 𝓞 K with β ∈ O coprime to 𝔣. Here it is stated as the surjective homomorphism NumberFieldOrder.rayClassToPic from the ray class group of 𝔣, whose kernel is the image of P_{K,O}(𝔣). Since the ray class group is finite, so is Pic O.

Main definitions

• TauCeti.GlobalNumberFields.NumberFieldOrder.picClass: the Picard class of the contraction of an ideal of 𝓞 K prime to the conductor.
• TauCeti.GlobalNumberFields.NumberFieldOrder.rayClassToPic: the surjection from the ray class group of the conductor onto Pic O.

Main results

• TauCeti.GlobalNumberFields.NumberFieldOrder.picClass_eq_one_iff: an ideal of 𝓞 K prime to the conductor has trivial Picard class exactly when it is generated by an element of O.
• TauCeti.GlobalNumberFields.NumberFieldOrder.rayClassToPic_surjective: every Picard class comes from a ray class of the conductor.
• TauCeti.GlobalNumberFields.NumberFieldOrder.mem_ker_rayClassToPic: the kernel of rayClassToPic consists of the ray classes of the ideals generated by elements of O.
• TauCeti.GlobalNumberFields.NumberFieldOrder.finite_pic: the Picard group of an order is finite.

References

• G. S. Kopp and J. C. Lagarias, Class Field Theory for Orders of Number Fields, §2.
• D. A. Cox, Primes of the Form x² + ny², §7, Propositions 7.20 and 7.22 (the quadratic case).
• J. Neukirch, Algebraic Number Theory, Chapter I, §12.

noncomputable def TauCeti.GlobalNumberFields.NumberFieldOrder.picClass {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : ↥(integralIdealsPrimeTo O.conductorModulus) →* Pic O

The Picard class of an ideal J of 𝓞 K prime to the conductor: the class in Pic O of its contraction J ∩ O, an invertible ideal of O.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.picClass_apply {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (J : ↥(integralIdealsPrimeTo O.conductorModulus)) : O.picClass J = O.mkPic (O.integralIdealsAwayConductorToInvertible (O.integralIdealsAwayConductorEquiv.symm J))

The Picard class of J is the class of its contraction to the order.

@[simp]

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.picClass_integralIdealsAwayConductorEquiv {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (I : ↥O.integralIdealsAwayConductor) : O.picClass (O.integralIdealsAwayConductorEquiv I) = O.mkPic (O.integralIdealsAwayConductorToInvertible I)

The Picard class of the extension to 𝓞 K of an ideal of O coprime to the conductor is the class of the ideal itself.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.picClass_surjective {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : Function.Surjective ⇑O.picClass

Every class of Pic O is the Picard class of an ideal of 𝓞 K prime to the conductor.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.coe_integralIdealsAwayConductorToInvertible_eq_spanSingleton {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {I : ↥O.integralIdealsAwayConductor} {β : NumberField.RingOfIntegers K} (hβ : β ∈ O.toRingOfIntegers) (hI : ↑(O.integralIdealsAwayConductorEquiv I) = Ideal.span {β}) : ↑(O.integralIdealsAwayConductorToInvertible I) = (FractionalIdeal.spanSingleton (nonZeroDivisors ↥O.toSubalgebra)) ↑β

The contraction of a principal ideal with a generator in the order. If the extension to 𝓞 K of an ideal I of O coprime to the conductor is generated by an element β of the order, then I is the principal fractional ideal β O.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.picClass_eq_one_iff {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (J : ↥(integralIdealsPrimeTo O.conductorModulus)) : O.picClass J = 1 ↔ ∃ β ∈ O.toRingOfIntegers, ↑J = Ideal.span {β}

The kernel of the Picard class map. An ideal of 𝓞 K prime to the conductor has trivial Picard class exactly when it is generated by an element of the order.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.picClass_eq_one_of_idealClass_eq_one {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (J : ↥(integralIdealsPrimeTo O.conductorModulus)) (hJ : (idealClass O.conductorModulus) J = 1) : O.picClass J = 1

An ideal of 𝓞 K with trivial ray class modulo the conductor has trivial Picard class: it is generated by an element congruent to one modulo the conductor, and such an element lies in the order.

noncomputable def TauCeti.GlobalNumberFields.NumberFieldOrder.rayClassToPic {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : RayClassGroup O.conductorModulus →* Pic O

The Picard group of an order as a quotient of a ray class group. The homomorphism from the ray class group of the conductor onto Pic O sending the ray class of an ideal J of 𝓞 K prime to the conductor to the Picard class of its contraction J ∩ O.

@[simp]

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.rayClassToPic_idealClass {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (J : ↥(integralIdealsPrimeTo O.conductorModulus)) : O.rayClassToPic ((idealClass O.conductorModulus) J) = O.picClass J

The ray class of J maps to the Picard class of its contraction to the order.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.rayClassToPic_comp_idealClass {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : O.rayClassToPic.comp (idealClass O.conductorModulus) = O.picClass

Composing rayClassToPic with the ray class map gives the Picard class map.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.rayClassToPic_surjective {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : Function.Surjective ⇑O.rayClassToPic

Every Picard class comes from a ray class of the conductor.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.mem_ker_rayClassToPic {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {c : RayClassGroup O.conductorModulus} : c ∈ O.rayClassToPic.ker ↔ ∃ (J : ↥(integralIdealsPrimeTo O.conductorModulus)), (idealClass O.conductorModulus) J = c ∧ ∃ β ∈ O.toRingOfIntegers, ↑J = Ideal.span {β}

The congruence description of the Picard group. A ray class of the conductor maps to the trivial Picard class exactly when it is the ray class of an ideal of 𝓞 K generated by an element of the order.

instance TauCeti.GlobalNumberFields.NumberFieldOrder.finite_pic {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : Finite (Pic O)

The Picard group of an order is finite, being a quotient of the finite ray class group of its conductor.