The two-torsion in the strongly ambiguous class group is bounded by base-field two-torsion and the finite set of ramified primes. The cover comes from the proved invariant-ideal factorization.

Ideal-class notation for finite products of nonzero integral ideals. The value at the zero ideal is set to one only to make the indexing function total; multiplicativity below explicitly requires nonzero ideals.

noncomputable def CCDN.integralIdealClass {R : Type u_1} [CommRing R] [IsDedekindDomain R] (I : Ideal R) : ClassGroup R

The ideal class of an integral ideal, with the zero ideal sent to the trivial class.

Equations

• CCDN.integralIdealClass I = if h : I = 0 then 1 else ClassGroup.mk0 ⟨I, ⋯⟩

theorem CCDN.integralIdealClass_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] : integralIdealClass 1 = 1

The unit ideal has trivial ideal class.

@[simp]

theorem CCDN.integralIdealClass_top {R : Type u_1} [CommRing R] [IsDedekindDomain R] : integralIdealClass ⊤ = 1

The top ideal has trivial ideal class.

theorem CCDN.stronglyAmbiguousTwoTorsion_card_le_discriminant_primes (F : Type u_1) (K : Type u_2) [Field F] [Field K] [NumberField F] [NumberField K] [Algebra F K] [FiniteDimensional F K] (hd : Module.finrank F K = 2) (σ : Gal(K/F)) (hσ : σ ≠ 1) : Nat.card ↥(stronglyAmbiguousTwoTorsion F K σ) ≤ classGroupTwoTorsionCard F * 2 ^ (Module.finrank ℚ K * (NumberField.discr K).natAbs.primeFactors.card)

A fully constructed discriminant-prime cover gives the strongly ambiguous two-torsion estimate.