The signature map on the units of a number field

The signature of a unit records its sign under each real embedding K →+* ℝ, as a class in the sign group ℝˣ ⧸ (posSubgroup ℝ) (the positive units of ℝ form an index-2 subgroup, so each factor is the two-element sign group).

We build it first on the full multiplicative group Kˣ — fieldUnitSignature, whose kernel is the totally positive units totallyPositiveUnits — and then restrict along (𝓞 K)ˣ → Kˣ to the arithmetic unit group to obtain unitSignature, whose kernel is the totally positive integer units.

The integer-unit signature is the archimedean input to the narrow class group Cl⁺(K) (Layer 3 of the multiquadratic roadmap): the cokernel of the signature — the full sign group modulo the signatures realized by units — is what contributes the kernel of the surjection Cl⁺(K) → Cl(K) between the narrow and ordinary class groups, and the 2-rank of Cl⁺(K) is what the t - 1 genus-theory formula computes for a real quadratic field.

Main definitions and results

• NumberField.fieldUnitSignature: the signature homomorphism on Kˣ, with fieldUnitSignature_ker computing its kernel as totallyPositiveUnits.
• NumberField.unitSignature: the signature homomorphism on (𝓞 K)ˣ, the restriction of fieldUnitSignature, with unitSignature_ker its kernel totallyPositiveIntegerUnits (defined in TotallyPositive.lean).

noncomputable def NumberField.fieldUnitSignature {K : Type u_1} [Field K] : Kˣ →* { w : InfinitePlace K // w.IsReal } → ℝˣ ⧸ Units.posSubgroup ℝ

The signature homomorphism on Kˣ: u is sent, at each real infinite place w, to the class of its image Units.map (embedding_of_isReal w) u in the sign group ℝˣ ⧸ (posSubgroup ℝ).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NumberField.fieldUnitSignature_apply {K : Type u_1} [Field K] (u : Kˣ) (w : { w : InfinitePlace K // w.IsReal }) : fieldUnitSignature u w = ↑((Units.map ↑(InfinitePlace.embedding_of_isReal ⋯)) u)

Componentwise evaluation of the field-unit signature.

theorem NumberField.fieldUnitSignature_ker {K : Type u_1} [Field K] : fieldUnitSignature.ker = totallyPositiveUnits

The kernel of the field-unit signature is exactly the subgroup of totally positive units.

@[simp]

theorem NumberField.fieldUnitSignature_eq_one_iff {K : Type u_1} [Field K] {u : Kˣ} : fieldUnitSignature u = 1 ↔ IsTotallyPositive ↑u

A unit has trivial field signature exactly when it is totally positive.

noncomputable def NumberField.unitSignature {K : Type u_1} [Field K] : (RingOfIntegers K)ˣ →* { w : InfinitePlace K // w.IsReal } → ℝˣ ⧸ Units.posSubgroup ℝ

The signature homomorphism on the integer units (𝓞 K)ˣ, the restriction of fieldUnitSignature along the inclusion (𝓞 K)ˣ → Kˣ.

Equations

• NumberField.unitSignature = NumberField.fieldUnitSignature.comp (Units.map ↑(algebraMap (NumberField.RingOfIntegers K) K))

@[simp]

theorem NumberField.unitSignature_apply {K : Type u_1} [Field K] (u : (RingOfIntegers K)ˣ) (w : { w : InfinitePlace K // w.IsReal }) : unitSignature u w = ↑((Units.map ↑(InfinitePlace.embedding_of_isReal ⋯)) ((Units.map ↑(algebraMap (RingOfIntegers K) K)) u))

Componentwise evaluation of the integer-unit signature: the class, in the sign group, of the image of u under the real embedding w composed with (𝓞 K) → K.

theorem NumberField.unitSignature_eq_fieldUnitSignature {K : Type u_1} [Field K] (u : (RingOfIntegers K)ˣ) : unitSignature u = fieldUnitSignature ((Units.map ↑(algebraMap (RingOfIntegers K) K)) u)

The signature of an integer unit is the field-unit signature of its image in Kˣ.

@[simp]

theorem NumberField.unitSignature_eq_one_iff {K : Type u_1} [Field K] {u : (RingOfIntegers K)ˣ} : unitSignature u = 1 ↔ IsTotallyPositive ((algebraMap (RingOfIntegers K) K) ↑u)

An integer unit has trivial signature exactly when its image in K is totally positive.

theorem NumberField.unitSignature_ker {K : Type u_1} [Field K] : unitSignature.ker = totallyPositiveIntegerUnits

The kernel of the integer-unit signature is exactly the totally positive integer units.