A cardinal bound for fixed two-torsion classes in terms of strongly ambiguous classes and the unit-norm quotient. This is the obstruction-fiber part of genus theory; the ramified-ideal estimate for the strongly ambiguous subgroup is a separate step.

structure CCDN.AmbiguousClassWitness (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)) : Type (max u_1 u_2)

Witness data for an ambiguous ideal class c (one fixed by σ): an invertible fractional ideal representing c, a scalar comparing it with its conjugate, and a base unit equal to the relative norm of that scalar.

• ideal : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ

  An invertible fractional ideal representing the class.

• scalar : Kˣ

  The scalar comparing the conjugate of ideal with ideal.

• baseUnit : (NumberField.RingOfIntegers F)ˣ

  A unit of 𝓞 F equal to the relative norm of scalar.

• class_eq : (ClassGroup.mk K) self.ideal = c

  The fractional ideal ideal represents the class c.

• scalar_eq : (fractionalIdealUnitAction (NumberField.RingOfIntegers.mapAlgEquiv σ).toRingEquiv) self.ideal = (toPrincipalIdeal (NumberField.RingOfIntegers K) K) self.scalar * self.ideal

  The conjugate of ideal under σ is the principal ideal of scalar times ideal.

• norm_eq : (Algebra.norm F) ↑self.scalar = ↑↑self.baseUnit

  The relative norm of scalar is the base unit baseUnit.

@[reducible, inline]

noncomputable abbrev CCDN.stronglyAmbiguousTwoTorsion (F : Type u_1) (K : Type u_2) [Field F] [Field K] [NumberField K] [Algebra F K] (σ : Gal(K/F)) : Subgroup ↥(stronglyAmbiguousClassGroup F K σ)

The two-torsion subgroup of the strongly ambiguous subgroup.

Equations

• CCDN.stronglyAmbiguousTwoTorsion F K σ = (powMonoidHom 2).ker

theorem CCDN.classGroupTwoTorsionCard_le_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) : classGroupTwoTorsionCard K ≤ (Nat.card ↥(stronglyAmbiguousTwoTorsion F K σ) * 2 ^ Module.finrank ℚ F) ^ 2

The quadratic two-torsion count is reduced to the strongly ambiguous subgroup, with a proved degree-only unit factor.