Invertible ideals and the Picard group of an order

For an order in a number field, the invertible fractional ideals are precisely the units of its fractional-ideal monoid. Every such ideal is proper, although a proper ideal need not be invertible. The wide Picard group is their quotient by nonzero principal ideals. Mathlib's ClassGroup already forms this quotient for every domain, so the Picard group of an order uses that carrier rather than constructing a second quotient.

References

• G. S. Kopp and J. C. Lagarias, Class Field Theory for Orders of Number Fields, §2.

@[reducible, inline]

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

The wide Picard group of an order: invertible fractional ideals modulo principal ideals. ClassGroup already implements this quotient for every integral domain.

@[reducible, inline]

noncomputable abbrev TauCeti.GlobalNumberFields.NumberFieldOrder.mkPic {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : O.invertibleProperFractionalIdeals →* Pic O

The wide Picard class of an invertible fractional ideal.

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

Every wide Picard class has an invertible fractional-ideal representative.