Factorisations over a divisible exponent subgroup

This file defines the factorisation objects in LM24, Theorem 6.5.7. The coefficient scalar is retained explicitly: the printed product omits it, and therefore does not represent a nonunit constant series. A nonpositive subgroup exponent represents the monomial factor, while a list represents the finite family of almost irreducible factors.

The normalized finite-support factor and the monomial exponent have separate uniqueness predicates. No uniqueness is asserted for the list of almost irreducible or irreducible factors.

def HahnSeries.Nonpositive.IsAlmostIrreducibleFactorization {H : AddSubgroup ℝ} {K : Type v} [Field K] (b : Nonpositive (↥H) K) (k : Kˣ) (p : ConstantTermOneFiniteSupport) (x : ↥(exponentMonoid ↥H)) (factors : List (Nonpositive (↥H) K)) : Prop

A corrected LM24, Theorem 6.5.7 factorisation: a nonzero coefficient scalar, a normalized finite-support factor, a coefficient-one monomial, and finitely many almost irreducible factors with infinite support.

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.Nonpositive.isAlmostIrreducibleFactorization_iff {H : AddSubgroup ℝ} {K : Type v} [Field K] (b : Nonpositive (↥H) K) (k : Kˣ) (p : ConstantTermOneFiniteSupport) (x : ↥(exponentMonoid ↥H)) (factors : List (Nonpositive (↥H) K)) : b.IsAlmostIrreducibleFactorization k p x factors ↔ b = C ↑k * ↑↑p * ↑(finiteSupportMonomial x) * factors.prod ∧ ∀ c ∈ factors, c.IsAlmostIrreducible ∧ (↑c).support.Infinite

Characterization of an almost-irreducible factorisation over an exponent subgroup.

def HahnSeries.Nonpositive.IsUniqueNormalizedHFactor {H : AddSubgroup ℝ} {K : Type v} [Field K] (b : Nonpositive (↥H) K) (p : ConstantTermOneFiniteSupport) : Prop

The normalized finite-support factor is unique among all corrected almost-irreducible factorisations of the same series.

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.Nonpositive.isUniqueNormalizedHFactor_iff {H : AddSubgroup ℝ} {K : Type v} [Field K] (b : Nonpositive (↥H) K) (p : ConstantTermOneFiniteSupport) : b.IsUniqueNormalizedHFactor p ↔ ∀ (k : Kˣ) (q : ConstantTermOneFiniteSupport) (x : ↥(exponentMonoid ↥H)) (factors : List (Nonpositive (↥H) K)), b.IsAlmostIrreducibleFactorization k q x factors → q = p

Characterization of uniqueness of the normalized finite-support factor.

def HahnSeries.Nonpositive.IsIrreducibleSubgroupFactorization {H : AddSubgroup ℝ} {K : Type v} [Field K] (b : Nonpositive (↥H) K) (k : Kˣ) (p : ConstantTermOneFiniteSupport) (x : ↥(exponentMonoid ↥H)) (factors : List (Nonpositive (↥H) K)) : Prop

The strengthened factorisation in LM24, Theorem 6.5.7, in which every infinite-support factor is irreducible rather than merely almost irreducible.

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.Nonpositive.isIrreducibleSubgroupFactorization_iff {H : AddSubgroup ℝ} {K : Type v} [Field K] (b : Nonpositive (↥H) K) (k : Kˣ) (p : ConstantTermOneFiniteSupport) (x : ↥(exponentMonoid ↥H)) (factors : List (Nonpositive (↥H) K)) : b.IsIrreducibleSubgroupFactorization k p x factors ↔ b = C ↑k * ↑↑p * ↑(finiteSupportMonomial x) * factors.prod ∧ ∀ c ∈ factors, Irreducible c ∧ (↑c).support.Infinite

Characterization of an irreducible infinite-support factorisation over an exponent subgroup.

theorem HahnSeries.Nonpositive.IsIrreducibleSubgroupFactorization.isAlmostIrreducibleFactorization {H : AddSubgroup ℝ} {K : Type v} [Field K] {b : Nonpositive (↥H) K} {k : Kˣ} {p : ConstantTermOneFiniteSupport} {x : ↥(exponentMonoid ↥H)} {factors : List (Nonpositive (↥H) K)} (h : b.IsIrreducibleSubgroupFactorization k p x factors) : b.IsAlmostIrreducibleFactorization k p x factors

An irreducible subgroup factorisation is, in particular, an almost-irreducible factorisation with the same data.

def HahnSeries.Nonpositive.IsUniqueIrreducibleFactorizationExponent {H : AddSubgroup ℝ} {K : Type v} [Field K] (b : Nonpositive (↥H) K) (x : ↥(exponentMonoid ↥H)) : Prop

The monomial exponent is unique among all irreducible subgroup factorisations of the same series.

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.Nonpositive.isUniqueIrreducibleFactorizationExponent_iff {H : AddSubgroup ℝ} {K : Type v} [Field K] (b : Nonpositive (↥H) K) (x : ↥(exponentMonoid ↥H)) : b.IsUniqueIrreducibleFactorizationExponent x ↔ ∀ (k : Kˣ) (p : ConstantTermOneFiniteSupport) (y : ↥(exponentMonoid ↥H)) (factors : List (Nonpositive (↥H) K)), b.IsIrreducibleSubgroupFactorization k p y factors → y = x

Characterization of uniqueness of the monomial exponent in irreducible subgroup factorisations.