Conjugate-transversal ideal families in a Dedekind domain

Let σ be a ring automorphism of a Dedekind domain R and S a finite set of nonzero prime ideals, packaged as IsDedekindDomain.HeightOneSpectrum R, on which σ acts as a fixed-point-free involution. Pairing each prime with its conjugate σ p ≠ p, the product of one prime from each pair gives many ideals A, each satisfying A * σ A = ∏ p ∈ S, p.asIdeal.

This is the combinatorial core behind counting the ideals 𝔄 with 𝔄 · σ 𝔄 a fixed product of split primes — the engine of the prime-splitting layer of the multiquadratic roadmap.

Main results

• TauCeti.DedekindDomain.exists_transversal_family: the family of ≥ 2 ^ (S.card / 2) ideals.

Provenance

Migrated from kim-em/erdos-unit-distance, the formalization of L. Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture, where it counted the conjugate-product ideals over primes p ≡ 1 (mod 4) in a concrete CM field.

theorem TauCeti.DedekindDomain.exists_transversal_family {R : Type u_1} [CommRing R] [IsDedekindDomain R] (σ : R ≃+* R) (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) (hinv : ∀ p ∈ S, (IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv σ) p ∈ S) (hinvol : ∀ p ∈ S, (IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv σ) ((IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv σ) p) = p) (hfree : ∀ p ∈ S, (IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv σ) p ≠ p) : ∃ (G : Finset (Ideal R)), 2 ^ (S.card / 2) ≤ G.card ∧ ∀ A ∈ G, A * Ideal.map σ A = ∏ p ∈ S, p.asIdeal

Conjugate-transversal ideal family. For a fixed-point-free involution σ of a finite set S of height-one primes of a Dedekind domain, there are at least 2 ^ (S.card / 2) ideals A with A * σ A = ∏ p ∈ S, p.asIdeal.