Primality of reduced Hahn integer-part series #
LM24's reduction at the leading Archimedean class transfers primality from a real-exponent Hahn series to a reduced element of a cardinal-bounded Hahn integer part. Polynomiality of the real-exponent series ring supplies this primality without a finite-degree hypothesis.
theorem
HahnSeries.Nonpositive.isPrimal_of_orderIso_real
{G : Type u_1}
{K : Type u_2}
[LinearOrder G]
[AddCommGroup G]
[IsOrderedAddMonoid G]
[Field K]
[CharZero K]
(e : G ≃+o ℝ)
(a : Nonpositive G K)
:
IsPrimal a
A nonpositive Hahn series whose exponent group is order-isomorphic to ℝ is primal.
theorem
HahnSeries.Nonpositive.isPrimal_of_isReduced_of_leadingClass_orderIso_real
{K : Type u_1}
{G : Type u_2}
{R : Type u_3}
{κ : Cardinal.{u_2}}
[DivisionRing K]
[LinearOrder K]
[IsOrderedRing K]
[Archimedean K]
[AddCommGroup G]
[LinearOrder G]
[IsOrderedAddMonoid G]
[Module K G]
[IsOrderedModule K G]
[Field R]
[CharZero R]
[Fact (Cardinal.aleph0 < κ)]
[Fact κ.IsRegular]
(u : HahnEmbedding.ArchimedeanStrata K G)
(Z : Subring R)
(b : ↥(cardSuppLTTruncationIntegerPart Z))
(hb0 : (CardSuppLTTruncationIntegerPart.toNonpositiveRingHom Z) b ≠ 0)
(horder : (↑((CardSuppLTTruncationIntegerPart.toNonpositiveRingHom Z) b)).order ≠ 0)
(hbReduced : ((CardSuppLTTruncationIntegerPart.toNonpositiveRingHom Z) b).IsReduced)
(hA2 :
LM24.AssumptionA2AtFiniteClass κ Z (((CardSuppLTTruncationIntegerPart.toNonpositiveRingHom Z) b).leadingClass horder))
(e : ↥(u.stratum (((CardSuppLTTruncationIntegerPart.toNonpositiveRingHom Z) b).leadingClass horder)) ≃+o ℝ)
:
IsPrimal b
A nonzero reduced bounded Hahn integer-part series is primal under the leading-class Archimedean hypotheses.