The narrow Picard group of a number-field order

The narrow Picard group identifies invertible fractional ideals only when they differ by a principal ideal with a totally positive generator. Forgetting positivity gives a canonical surjection onto the wide Picard group. The same construction for the maximal order is the narrow class group; here the fractional ideals belong to an arbitrary order and only its invertible ideals enter the quotient.

References

• G. S. Kopp and J. C. Lagarias, Class Field Theory for Orders of Number Fields, §2.
• TauCeti/NumberTheory/NumberField/NarrowClassGroup/Basic.lean, for the maximal-order quotient and its forgetful map; the construction here adapts that API to arbitrary orders.

noncomputable def TauCeti.GlobalNumberFields.NumberFieldOrder.narrowPrincipal {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : Subgroup O.invertibleProperFractionalIdeals

The subgroup of invertible fractional ideals generated by totally positive field elements.

@[simp]

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.mem_narrowPrincipal_iff {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {I : O.invertibleProperFractionalIdeals} : I ∈ O.narrowPrincipal ↔ ∃ (x : Kˣ), NumberField.IsTotallyPositive ↑x ∧ (toPrincipalIdeal (↥O.toSubalgebra) K) x = I

An invertible fractional ideal is narrowly principal precisely when it has a totally positive generator in the ambient field.

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

The narrow Picard group of an order: invertible fractional ideals modulo those with a totally positive principal generator.

@[instance_reducible]

noncomputable instance TauCeti.GlobalNumberFields.instCommGroupNarrowPic {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : CommGroup (NarrowPic O)

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

The narrow Picard class of an invertible fractional ideal.

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

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

@[simp]

theorem TauCeti.GlobalNumberFields.NarrowPic.mk_eq_one_iff {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {I : O.invertibleProperFractionalIdeals} : (mk O) I = 1 ↔ I ∈ O.narrowPrincipal

An invertible fractional ideal has trivial narrow class exactly when it has a totally positive principal generator.

@[simp]

theorem TauCeti.GlobalNumberFields.NarrowPic.mk_eq_mk_iff {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {I J : O.invertibleProperFractionalIdeals} : (mk O) I = (mk O) J ↔ ∃ P ∈ O.narrowPrincipal, I * P = J

Two invertible fractional ideals have the same narrow Picard class exactly when they differ by a principal ideal with a totally positive generator.

noncomputable def TauCeti.GlobalNumberFields.NarrowPic.lift {K : Type u_1} [Field K] [NumberField K] {M : Type u_2} [Monoid M] (O : NumberFieldOrder K) (φ : O.invertibleProperFractionalIdeals →* M) (h : O.narrowPrincipal ≤ φ.ker) : NarrowPic O →* M

A homomorphism on invertible ideals that kills the narrowly principal ideals descends to the narrow Picard group.

@[simp]

theorem TauCeti.GlobalNumberFields.NarrowPic.lift_mk {K : Type u_1} [Field K] [NumberField K] {M : Type u_2} [Monoid M] (O : NumberFieldOrder K) (φ : O.invertibleProperFractionalIdeals →* M) (h : O.narrowPrincipal ≤ φ.ker) (I : O.invertibleProperFractionalIdeals) : (lift O φ h) ((mk O) I) = φ I

The descended homomorphism agrees with the original one on ideal classes.

theorem TauCeti.GlobalNumberFields.NarrowPic.lift_unique {K : Type u_1} [Field K] [NumberField K] {M : Type u_2} [Monoid M] (O : NumberFieldOrder K) (φ : O.invertibleProperFractionalIdeals →* M) (h : O.narrowPrincipal ≤ φ.ker) (ψ : NarrowPic O →* M) (hψ : ∀ (I : O.invertibleProperFractionalIdeals), ψ ((mk O) I) = φ I) : ψ = lift O φ h

A homomorphism out of the narrow Picard group is determined by its values on the classes of invertible fractional ideals.

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

The narrow class of the principal fractional ideal generated by a nonzero field element.

@[simp]

theorem TauCeti.GlobalNumberFields.NarrowPic.mkPrincipal_apply {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (x : Kˣ) : (mkPrincipal O) x = (mk O) ((toPrincipalIdeal (↥O.toSubalgebra) K) x)

The narrow principal class is the class of the corresponding principal fractional ideal.

theorem TauCeti.GlobalNumberFields.NarrowPic.mkPrincipal_eq_one_iff {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {x : Kˣ} : (mkPrincipal O) x = 1 ↔ ∃ (w : (↥O.toSubalgebra)ˣ), NumberField.IsTotallyPositive (w • ↑x)

A principal narrow Picard class is trivial exactly when an order unit rescales its generator to a totally positive element.

theorem TauCeti.GlobalNumberFields.NarrowPic.mkPrincipal_eq_one_of_isTotallyPositive {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {x : Kˣ} (hx : NumberField.IsTotallyPositive ↑x) : (mkPrincipal O) x = 1

A totally positive element generates the trivial narrow Picard class.

theorem TauCeti.GlobalNumberFields.NarrowPic.mkPrincipal_sq {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (x : Kˣ) : (mkPrincipal O) x ^ 2 = 1

Every principal narrow Picard class has order dividing two, since a square is totally positive at every real place.

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

Forgetting the positivity condition gives the canonical map from the narrow to the wide Picard group of an order.

@[simp]

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.narrowToPic_mk {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (I : O.invertibleProperFractionalIdeals) : O.narrowToPic ((NarrowPic.mk O) I) = O.mkPic I

On an invertible fractional ideal, the forgetful map gives its wide Picard class.

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

Every wide Picard class has a narrow Picard preimage.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.narrowToPic_mkPrincipal {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (x : Kˣ) : O.narrowToPic ((NarrowPic.mkPrincipal O) x) = 1

The narrow class of a principal ideal maps to the trivial wide Picard class.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.narrowToPic_mk_eq_one_iff {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {I : O.invertibleProperFractionalIdeals} : O.narrowToPic ((NarrowPic.mk O) I) = 1 ↔ ∃ (x : Kˣ), (toPrincipalIdeal (↥O.toSubalgebra) K) x = I

A representative maps to the trivial wide Picard class precisely when it is principal.

theorem TauCeti.GlobalNumberFields.NumberFieldOrder.narrowToPic_ker {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) : O.narrowToPic.ker = (NarrowPic.mkPrincipal O).range

The kernel of the forgetful map consists exactly of narrow classes of principal ideals.