The group-theoretic part of quadratic class-group descent. An involution on an elementary abelian two-group has at least the square root of the group's cardinality in fixed points. This is applied to the action of a field involution on two-torsion ideal classes.

noncomputable def CCDN.classGroupTwoTorsionAction (K : Type u_1) [Field K] (σ : K ≃+* K) : ↥(classGroupTwoTorsion K) →* ↥(classGroupTwoTorsion K)

The action of a field automorphism on two-torsion ideal classes.

Equations

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

noncomputable def CCDN.fixedClassGroupTwoTorsion (K : Type u_1) [Field K] (σ : K ≃+* K) : Subgroup ↥(classGroupTwoTorsion K)

Two-torsion classes fixed by the specified field automorphism.

Equations

• CCDN.fixedClassGroupTwoTorsion K σ = (CCDN.classGroupTwoTorsionAction K σ).eqLocus (MonoidHom.id ↥(CCDN.classGroupTwoTorsion K))

@[simp]

theorem CCDN.mem_fixedClassGroupTwoTorsion (K : Type u_1) [Field K] (σ : K ≃+* K) (c : ↥(classGroupTwoTorsion K)) : c ∈ fixedClassGroupTwoTorsion K σ ↔ (ClassGroup.mulEquiv (NumberField.RingOfIntegers.mapRingEquiv σ)) ↑c = ↑c

A two-torsion class lies in the σ-fixed subgroup if and only if σ maps its underlying ideal class to itself.

theorem CCDN.classGroupTwoTorsionCard_le_fixed_square (K : Type u_1) [Field K] [NumberField K] (σ : K ≃+* K) (hσ : Function.Involutive ⇑σ) : classGroupTwoTorsionCard K ≤ Nat.card ↥(fixedClassGroupTwoTorsion K σ) ^ 2

For an involutive automorphism σ of K, the order of the two-torsion subgroup of the class group is at most the square of the order of its σ-fixed subgroup.