Coprime integral representatives of cyclotomic pseudo-units

This file proves the denominator-dependent normalization step used in a one-sided Kummer reciprocity argument. Its ideal-theoretic input is the standard Dedekind-domain fact that an ideal class has an integral representative coprime to any prescribed nonzero proper ideal.

The proof is internal to Mathlib's Dedekind-domain API. If J is an integral representative of the inverse class and F is the prescribed ideal, IsDedekindDomain.exists_sup_span_eq supplies x with J * F + (x) = J. Cancelling J shows that (x) * J⁻¹ is both integral and coprime to F.

theorem FractionalIdeal.exists_integral_coprime_principal_multiple {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] (A : (FractionalIdeal (nonZeroDivisors R) K)ˣ) (F : Ideal R) (hF_ne : F ≠ ⊥) (hF_proper : F ≠ ⊤) : ∃ (c : Kˣ) (B : Ideal R) (hB : B ≠ ⊥), (toPrincipalIdeal R K) c * A = (mk0 K) ⟨B, ⋯⟩ ∧ IsCoprime B F

A nonzero fractional ideal can be rescaled by a field unit to an integral ideal coprime to any prescribed nonzero proper ideal.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.exists_coprime_integral_pseudoUnit_normalization {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (hdiv : ∀ (v : FinitePrime (PrimeCyclotomicField p)), ↑p ∣ FractionalIdeal.count (PrimeCyclotomicField p) v (FractionalIdeal.spanSingleton (nonZeroDivisors (NumberField.RingOfIntegers (PrimeCyclotomicField p))) E.kummerPresentation.radicand)) (I : Ideal (NumberField.RingOfIntegers (PrimeCyclotomicField p))) (hI : I ≠ ⊥) : ∃ (c : (PrimeCyclotomicField p)ˣ) (η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (B : Ideal (NumberField.RingOfIntegers (PrimeCyclotomicField p))), η ≠ 0 ∧ (algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) η = E.kummerPresentation.radicand * ↑c ^ p ∧ Ideal.span {η} = B ^ p ∧ IsCoprime (Ideal.span {η}) I ∧ IsCoprime (Ideal.span {η}) (cyclotomicPrime p).asIdeal

A pseudo-unit radicand can be changed by a p-th power so that it is integral and its principal ideal is simultaneously coprime to a prescribed nonzero denominator ideal and to the cyclotomic prime.