The algebraic starting point of the class-group application. Classes killed by two have nonzero integral representatives whose squares are principal. A principal square determines its ideal uniquely; thus generators chosen for distinct classes are distinct. The norm assertion uses the absolute value: a signed field norm need not be positive.

theorem CCDN.ideal_class_eq_of_square_generators_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] (I J : ↥(nonZeroDivisors (Ideal R))) {β γ : R} (hI : ↑I ^ 2 = Ideal.span {β}) (hJ : ↑J ^ 2 = Ideal.span {γ}) (hβγ : β = γ) : ClassGroup.mk0 I = ClassGroup.mk0 J

Two nonzero integral ideals whose squares are generated by the same element are equal, hence have the same ideal class.

noncomputable def CCDN.classGroupTwoTorsion (K : Type u_1) [Field K] : Subgroup (ClassGroup (NumberField.RingOfIntegers K))

The subgroup of the ideal class group killed by two.

Equations

• CCDN.classGroupTwoTorsion K = (powMonoidHom 2).ker

@[simp]

theorem CCDN.mem_classGroupTwoTorsion (K : Type u_1) [Field K] (c : ClassGroup (NumberField.RingOfIntegers K)) : c ∈ classGroupTwoTorsion K ↔ c ^ 2 = 1

An ideal class lies in the two-torsion subgroup if and only if its square is trivial.

noncomputable def CCDN.classGroupTwoTorsionCard (K : Type u_1) [Field K] : ℕ

The order h₂(K) of the two-torsion subgroup of the class group of K, the quantity bounded in CCDN Theorem 6.

Equations

• CCDN.classGroupTwoTorsionCard K = Nat.card ↥(CCDN.classGroupTwoTorsion K)

theorem CCDN.classGroupTwoTorsionCard_le_classNumber (K : Type u_1) [Field K] [NumberField K] : classGroupTwoTorsionCard K ≤ NumberField.classNumber K

The order of the two-torsion subgroup of the class group is at most the class number.

theorem CCDN.generator_absolute_norm_of_ideal_square (K : Type u_1) [Field K] [NumberField K] (I : Ideal (NumberField.RingOfIntegers K)) {β : NumberField.RingOfIntegers K} (hI : I ^ 2 = Ideal.span {β}) : ((Algebra.norm ℤ) β).natAbs = Ideal.absNorm I ^ 2

If I ^ 2 = (β), then the absolute norm |N(β)| equals N(I) ^ 2.

theorem CCDN.exists_two_torsion_integral_square_representative (K : Type u_1) [Field K] [NumberField K] (c : ↥(classGroupTwoTorsion K)) : ∃ (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) (β : NumberField.RingOfIntegers K), ClassGroup.mk0 I = ↑c ∧ β ≠ 0 ∧ ↑I ^ 2 = Ideal.span {β} ∧ ((Algebra.norm ℤ) β).natAbs = Ideal.absNorm ↑I ^ 2 ∧ ↑(Ideal.absNorm ↑I) ≤ (4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K * (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K * √|↑(NumberField.discr K)|)

Every two-torsion class has a nonzero integral representative within the usual Minkowski ideal-norm bound, with a nonzero generator of its square and the resulting exact absolute norm identity.