The narrow 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 𝔣, and let 𝔣∞ be the modulus with finite part 𝔣 and every real place (NumberFieldOrder.narrowConductorModulus). Taking the narrow Picard class of the contraction J ∩ O of an ideal J of 𝓞 K prime to 𝔣 gives a monoid homomorphism NumberFieldOrder.narrowPicClass to NarrowPic O.

Its kernel consists of the principal ideals β 𝓞 K with a totally positive generator β ∈ O. In particular the ideals with a totally positive generator β ≡ 1 mod 𝔣 die in NarrowPic O, so narrowPicClass factors through the ray class group of 𝔣∞. The result is the congruence description of the narrow Picard group of an order:

NarrowPic 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 totally positive and coprime to 𝔣. Here it is stated as the surjective homomorphism NumberFieldOrder.rayClassToNarrowPic from the ray class group of 𝔣∞, whose kernel is the image of P⁺_{K,O}(𝔣). Since that ray class group is finite, so is NarrowPic O.

Forgetting positivity, rayClassToNarrowPic lies over NumberFieldOrder.rayClassToPic, the corresponding description of the wide Picard group. Surjectivity reduces to that of the wide map and to realizing every principal narrow class, which depends only on the signs of a generator at the real places, by a nonzero algebraic integer congruent to one modulo 𝔣. The latter is weak approximation at the primes dividing 𝔣 together with all real places.

Main definitions

• TauCeti.GlobalNumberFields.NumberFieldOrder.narrowConductorModulus: the conductor of an order together with every real place, as a modulus.
• TauCeti.GlobalNumberFields.NumberFieldOrder.narrowPicClass: the narrow Picard class of the contraction of an ideal of 𝓞 K prime to the conductor.
• TauCeti.GlobalNumberFields.NumberFieldOrder.rayClassToNarrowPic: the surjection from the ray class group of the narrow conductor modulus onto NarrowPic O.

Main results

• TauCeti.GlobalNumberFields.NumberFieldOrder.narrowPicClass_eq_one_iff: an ideal of 𝓞 K prime to the conductor has trivial narrow Picard class exactly when it is generated by a totally positive element of the order.
• TauCeti.GlobalNumberFields.NumberFieldOrder.rayClassToNarrowPic_surjective: every narrow Picard class comes from a ray class of the narrow conductor modulus.
• TauCeti.GlobalNumberFields.NumberFieldOrder.mem_ker_rayClassToNarrowPic: the kernel of rayClassToNarrowPic consists of the ray classes of the ideals generated by totally positive elements of O.
• TauCeti.GlobalNumberFields.NumberFieldOrder.narrowToPic_comp_rayClassToNarrowPic: forgetting positivity, rayClassToNarrowPic lies over rayClassToPic.
• TauCeti.GlobalNumberFields.NumberFieldOrder.finite_narrowPic: the narrow 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 (the quadratic case).

The narrow conductor modulus

noncomputable def TauCeti.GlobalNumberFields.NumberFieldOrder.narrowConductorModulus {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : Modulus K

The conductor of an order as a modulus of K together with every real place. Its ray class group surjects onto the narrow Picard group of the order.

@[simp]

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.narrowConductorModulus_finitePart {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : O.narrowConductorModulus.finitePart = O.conductor

@[simp]

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.mem_narrowConductorModulus_infinitePart {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : w ∈ O.narrowConductorModulus.infinitePart

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.conductorModulus_dvd_narrowConductorModulus {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : O.conductorModulus ∣ O.narrowConductorModulus

The conductor modulus divides the narrow conductor modulus: they have the same finite part, and the latter has more real places.

@[simp]

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.narrowConductorModulus_maximalNumberFieldOrder {K : Type u_1} [Field K] [NumberField K] : (maximalNumberFieldOrder K).narrowConductorModulus = narrowModulus K

The narrow conductor modulus of the maximal order is the narrow modulus.

Narrow Picard classes of ideals prime to the conductor

noncomputable def TauCeti.GlobalNumberFields.NumberFieldOrder.narrowPicClass {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : ↥(integralIdealsPrimeTo O.narrowConductorModulus) →* NarrowPic O

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

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.narrowPicClass_apply {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (J : ↥(integralIdealsPrimeTo O.narrowConductorModulus)) : O.narrowPicClass J = (NarrowPic.mk O) (O.integralIdealsAwayConductorToInvertible (O.integralIdealsAwayConductorEquiv.symm ((integralIdealsPrimeToInclusion ⋯) J)))

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

@[simp]

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.narrowToPic_narrowPicClass {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (J : ↥(integralIdealsPrimeTo O.narrowConductorModulus)) : O.narrowToPic (O.narrowPicClass J) = O.picClass ((integralIdealsPrimeToInclusion ⋯) J)

Forgetting positivity, the narrow Picard class of J is its Picard class.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.narrowPicClass_eq_mkPrincipal {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {J : ↥(integralIdealsPrimeTo O.narrowConductorModulus)} {β : NumberField.RingOfIntegers K} (hβ : β ∈ O.toRingOfIntegers) {x : Kˣ} (hx : ↑x = ↑β) (hJ : ↑J = Ideal.span {β}) : O.narrowPicClass J = (NarrowPic.mkPrincipal O) x

An ideal of 𝓞 K prime to the conductor and generated by an element β of the order has the narrow Picard class of the principal ideal β O.

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

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

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

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

The narrow Picard group as a quotient of a ray class group

noncomputable def TauCeti.GlobalNumberFields.NumberFieldOrder.rayClassToNarrowPic {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : RayClassGroup O.narrowConductorModulus →* NarrowPic O

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

@[simp]

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.rayClassToNarrowPic_idealClass {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (J : ↥(integralIdealsPrimeTo O.narrowConductorModulus)) : O.rayClassToNarrowPic ((idealClass O.narrowConductorModulus) J) = O.narrowPicClass J

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

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.rayClassToNarrowPic_comp_idealClass {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : O.rayClassToNarrowPic.comp (idealClass O.narrowConductorModulus) = O.narrowPicClass

Composing rayClassToNarrowPic with the ray class map gives the narrow Picard class map.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.narrowToPic_comp_rayClassToNarrowPic {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : O.narrowToPic.comp O.rayClassToNarrowPic = O.rayClassToPic.comp (classMap ⋯)

Forgetting positivity. The narrow description of NarrowPic O lies over the description of Pic O: the square formed with narrowToPic and the transition map classMap commutes.

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

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

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

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

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

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

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

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