GCD complexity measure

Defines the GCD complexity of a finite set of elements in a UFD: the sum of the lengths of their factorisations. This serves as the well-founded measure for the inductive step of the close-up construction when n >= 3 generators. Dividing all generators by a common prime strictly decreases the complexity.

noncomputable def gcdComplexity {T : Type u_1} [CommRing T] {R : Subring T} [UniqueFactorizationMonoid ↥R] (s : Finset ↥R) : ℕ

"GCD complexity" of a finite set s in a UFD subring R: the sum over x ∈ s of the number of (normalized) irreducible factors of x. Used as a termination measure in the close-up construction.

Equations

• gcdComplexity s = ∑ x ∈ s, (UniqueFactorizationMonoid.normalizedFactors x).card

noncomputable def gcdComplexityNsub {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (s : Finset ↥R.carrier) : ℕ

gcdComplexity for a finite set in an N-subring, supplying the domain and UFD instances from the N-subring structure.

Equations

• gcdComplexityNsub R s = gcdComplexity s

theorem normalizedFactors_card_inclusion {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R S₁ : NSubring T) (hAext : IsAExtension R S₁) (hle : R.carrier ≤ S₁.carrier) (x : ↥R.carrier) : (UniqueFactorizationMonoid.normalizedFactors ((Subring.inclusion hle) x)).card = (UniqueFactorizationMonoid.normalizedFactors x).card

theorem span_eq_mul_span_image_div {R₀ : Type u_2} [CommRing R₀] [DecidableEq R₀] (p : R₀) (s : Finset R₀) (_hp_dvd : ∀ x ∈ s, p ∣ x) (div_f : R₀ → R₀) (hdiv_spec : ∀ x ∈ s, x = p * div_f x) : Ideal.span ↑s = Ideal.span {p} * Ideal.span ↑(Finset.image div_f s)

theorem prime_mul_span_insert_le {R₀ : Type u_2} [CommRing R₀] [DecidableEq R₀] (q' a : R₀) (rest : Finset R₀) (div_f : R₀ → R₀) (hdiv : ∀ x ∈ rest, x = q' * div_f x) : Ideal.span {q'} * Ideal.span ↑(insert a (Finset.image div_f rest)) ≤ Ideal.span ↑(insert a rest)

theorem nzd_element_in_span_prime {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (q a : ↥R.carrier) (hq_prime : Prime q) (hqa : ¬q ∣ a) (_hM_not_assoc : ∀ (r : T), r ≠ 0 → IsLocalRing.maximalIdeal T ∉ associatedPrimes T (T ⧸ Ideal.span {r})) (t_val : T) (h_at_mem : ↑a * t_val ∈ Ideal.span {↑q}) : ∃ (t' : T), t_val = ↑q * t'

theorem gcdComplexity_div_le {T : Type u_1} [CommRing T] [IsDomain T] {R₀ : Subring T} [UniqueFactorizationMonoid ↥R₀] [DecidableEq ↥R₀] (q : ↥R₀) (hq : Prime q) (s : Finset ↥R₀) (_hq_dvd : ∀ x ∈ s, q ∣ x) (div_f : ↥R₀ → ↥R₀) (hdiv : ∀ x ∈ s, x = q * div_f x) (hinj : Set.InjOn div_f ↑s) : gcdComplexity (Finset.image div_f s) ≤ gcdComplexity s