LM24 principal-factor invariance statements

This module states LM24, Lemmas 6.3.1--6.3.2. The first lemma concerns the multiplicative RV quotient and the paper's set P of principal RV classes. The second concerns the full degree-graded ring RV̂ and the principal graded subring P̂. In both cases multiplication by a nonzero principal factor preserves the normalized maximal finite-support divisor.

The RV notation p(B) is represented by applying the full graded normalization to the canonical graded image of B. The proofs use Berarducci multiplicativity and finite-support greatest-common divisors.

theorem Berarducci.maximalFiniteSupportDivisor_rv_mul_principal {K : Type v} [Field K] [CharZero K] (B C : HahnDegreeRV K) (hC : IsPrincipalRV C) (hC0 : C ≠ 0) : gradedNormalizedMaximalFiniteSupportDivisor ((HahnSeries.Nonpositive.degreeValuation K).rvInitialFormHom (B * C)) = gradedNormalizedMaximalFiniteSupportDivisor ((HahnSeries.Nonpositive.degreeValuation K).rvInitialFormHom B)

LM24, Lemma 6.3.1: multiplying an RV class by a nonzero principal RV class does not change its normalized maximal finite-support divisor.

theorem Berarducci.maximalFiniteSupportDivisor_mul_principal {K : Type v} [Field K] [CharZero K] (B C : DegreeGraded K) (hC : IsPrincipalGraded C) (hC0 : C ≠ 0) : gradedNormalizedMaximalFiniteSupportDivisor (B * C) = gradedNormalizedMaximalFiniteSupportDivisor B

LM24, Lemma 6.3.2: multiplying a full graded element by a nonzero element of the principal graded subring does not change its normalized maximal finite-support divisor.