Factoring a product of conjugate primes in a Dedekind domain

Let R be a Dedekind domain carrying a ring endomorphism σ, and let S be a finite set of nonzero primes of R on which σ acts involutively. This file characterizes the ideals A with A * σ A = ∏ p ∈ S, p as exactly the products over the transversals of σ on S. When σ additionally has no fixed points on S, so that S splits into conjugate pairs {p, σ p}, it also proves that there are exactly 2 ^ (#S / 2) such ideals, one for each choice of a prime from each conjugate pair. Fixed-point-freeness is needed only for this count.

The count is what makes such factorizations a source of many ideals with a prescribed conjugate product: taking S to be a set of primes above rational primes that split into conjugate pairs, the theorem produces exactly 2 ^ (#S / 2) ideals A with A · σA the prescribed ideal. The argument is the interplay of two facts: a divisor of a product of distinct primes is the product of a subset of them (TauCeti.exists_subset_finset_prod_eq_of_dvd), and the transversals of a fixed-point-free involution are counted by TauCeti.ncard_setOf_isInvolutionTransversal.

References

The existence half of the count is exists_transversal_family in the formalization kim-em/erdos-unit-distance, written for Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture, where it is stated as the lower bound 2 ^ (#S / 2) ≤ #G for a family G of such ideals. The induction on S that strips off one conjugate pair at a time is taken from there; it is carried out here on the transversals rather than on the ideals, which turns the bound into the exact count and separates the combinatorics from the arithmetic.

Main results

• TauCeti.mul_map_eq_prod_iff: A * σ A = ∏ p ∈ S, p exactly when A is the product over a transversal of σ on S.
• TauCeti.ncard_setOf_mul_map_eq_prod: there are exactly 2 ^ (#S / 2) such A.

theorem TauCeti.mul_map_eq_prod_iff {R : Type u_1} {F : Type u_2} [CommRing R] [IsDedekindDomain R] [FunLike F R R] [RingHomClass F R R] {σ : F} {S : Finset (Ideal R)} (hprime : ∀ p ∈ S, p.IsPrime) (hbot : ∀ p ∈ S, p ≠ ⊥) (hmaps : ∀ p ∈ S, Ideal.map σ p ∈ S) (hinvol : ∀ p ∈ S, Ideal.map σ (Ideal.map σ p) = p) {A : Ideal R} : A * Ideal.map σ A = ∏ p ∈ S, p ↔ ∃ (T : Finset (Ideal R)), IsInvolutionTransversal (Ideal.map σ) S T ∧ A = ∏ p ∈ T, p

The conjugate factorizations of a product of paired primes. If a ring endomorphism σ acts involutively on a finite set S of nonzero primes, then the ideals A with A * σ A = ∏ p ∈ S, p are exactly the products over the transversals of σ on S.

theorem TauCeti.ncard_setOf_mul_map_eq_prod {R : Type u_1} {F : Type u_2} [CommRing R] [IsDedekindDomain R] [FunLike F R R] [RingHomClass F R R] {σ : F} {S : Finset (Ideal R)} (hprime : ∀ p ∈ S, p.IsPrime) (hbot : ∀ p ∈ S, p ≠ ⊥) (hmaps : ∀ p ∈ S, Ideal.map σ p ∈ S) (hinvol : ∀ p ∈ S, Ideal.map σ (Ideal.map σ p) = p) (hfree : ∀ p ∈ S, Ideal.map σ p ≠ p) : {A : Ideal R | A * Ideal.map σ A = ∏ p ∈ S, p}.ncard = 2 ^ (S.card / 2)

The conjugate factorization count. If a ring endomorphism σ acts involutively and without fixed points on a finite set S of nonzero primes, then there are exactly 2 ^ (#S / 2) factorizations A * σ A = ∏ p ∈ S, p, one for each choice of a prime from each conjugate pair.