Multiplicativity of normalized maximal finite-support divisors #
This module proves the field-generic reduction underlying LM24, Corollary 6.3.7. If every
finite-support divisor of a product in RV̂ factors into finite-support divisors of the two
factors, then the normalized maximal finite-support divisor is multiplicative.
Pairwise greatest-common-divisor existence and the classification of finite-support units remain explicit hypotheses; the statements module discharges both over the real exponents.
theorem
Berarducci.gradedNormalizedMaximalFiniteSupportDivisor_mul_of_factorization
{K : Type v}
[Field K]
[CharZero K]
(hgcd : ∀ (p q : ↥FiniteSupportRing), ∃ (d : ↥FiniteSupportRing), ∀ (e : ↥FiniteSupportRing), e ∣ p ∧ e ∣ q ↔ e ∣ d)
(hunits : ∀ (u : ↥FiniteSupportRing), IsUnit u ↔ ∃ (k : K), k ≠ 0 ∧ u = HahnSeries.Nonpositive.finiteSupportScalarHom k)
(hfactor :
∀ (p : ↥FiniteSupportRing) (B C : DegreeGraded K),
(finiteSupportGradedEmbedding K) p ∣ B * C →
∃ (p₁ : ↥FiniteSupportRing) (p₂ : ↥FiniteSupportRing),
p = p₁ * p₂ ∧ (finiteSupportGradedEmbedding K) p₁ ∣ B ∧ (finiteSupportGradedEmbedding K) p₂ ∣ C)
(B C : DegreeGraded K)
:
The normalized maximal finite-support divisor is multiplicative whenever finite-support divisors of products admit compatible finite-support factorisations.