The unit-norm obstruction for ambiguous ideal classes. Equal obstructions yield classes differing by a class represented by an invariant fractional ideal. The representatives can be chosen once, so the fiber argument does not need a preliminary choice-independent description of the obstruction homomorphism.

The unit-norm quotient in a quadratic extension is finite, with a uniform bound depending only on the base-field degree. Squares of base units are norms of their extensions.

noncomputable def CCDN.relativeUnitNorm (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] : (NumberField.RingOfIntegers K)ˣ →* (NumberField.RingOfIntegers F)ˣ

The relative norm N_{K/F} restricted to unit groups of rings of integers.

Equations

• CCDN.relativeUnitNorm F K = Units.map (RingOfIntegers.norm F)

@[reducible, inline]

abbrev CCDN.quadraticUnitNormQuotient (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] : Type u_1

The unit-norm obstruction group: the units of 𝓞 F modulo the relative norms of units of 𝓞 K.

Equations

• CCDN.quadraticUnitNormQuotient F K = ((NumberField.RingOfIntegers F)ˣ ⧸ (CCDN.relativeUnitNorm F K).range)

theorem CCDN.quadraticUnitNormQuotient_finite (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [NumberField F] (hd : Module.finrank F K = 2) : Finite (quadraticUnitNormQuotient F K)

For a quadratic extension K / F of number fields, the unit-norm quotient is finite.

theorem CCDN.quadraticUnitNormQuotient_card_le_degree (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [NumberField F] (hd : Module.finrank F K = 2) : Nat.card (quadraticUnitNormQuotient F K) ≤ 2 ^ Module.finrank ℚ F

For a quadratic extension K / F of number fields, the unit-norm quotient has order at most 2 ^ [F : ℚ].

noncomputable def CCDN.stronglyAmbiguousClassGroup (F : Type u_1) (K : Type u_2) [Field F] [Field K] [NumberField K] [Algebra F K] (σ : Gal(K/F)) : Subgroup (ClassGroup (NumberField.RingOfIntegers K))

Classes represented by invariant invertible fractional ideals.

Equations

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

theorem CCDN.mem_stronglyAmbiguousClassGroup (F : Type u_1) (K : Type u_2) [Field F] [Field K] [NumberField K] [Algebra F K] (σ : Gal(K/F)) (c : ClassGroup (NumberField.RingOfIntegers K)) : c ∈ stronglyAmbiguousClassGroup F K σ ↔ ∃ (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ), (fractionalIdealUnitAction (NumberField.RingOfIntegers.mapAlgEquiv σ).toRingEquiv) I = I ∧ (ClassGroup.mk K) I = c

An ideal class is strongly ambiguous if and only if it is the class of a σ-invariant invertible fractional ideal.

theorem CCDN.equal_unit_obstructions_stronglyAmbiguous (F : Type u_1) (K : Type u_2) [Field F] [Field K] [NumberField F] [NumberField K] [Algebra F K] (hd : Module.finrank F K = 2) (σ : Gal(K/F)) (hσ : σ ≠ 1) (I J : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) (a b : Kˣ) (u v : (NumberField.RingOfIntegers F)ˣ) (hI : (fractionalIdealUnitAction (NumberField.RingOfIntegers.mapAlgEquiv σ).toRingEquiv) I = (toPrincipalIdeal (NumberField.RingOfIntegers K) K) a * I) (hJ : (fractionalIdealUnitAction (NumberField.RingOfIntegers.mapAlgEquiv σ).toRingEquiv) J = (toPrincipalIdeal (NumberField.RingOfIntegers K) K) b * J) (ha : (Algebra.norm F) ↑a = ↑↑u) (hb : (Algebra.norm F) ↑b = ↑↑v) (huv : ↑u = ↑v) : (ClassGroup.mk K) I / (ClassGroup.mk K) J ∈ stronglyAmbiguousClassGroup F K σ

Equality of the concrete unit obstructions places the quotient of two represented classes in the strongly ambiguous subgroup.