Support, range and composition of HahnSeries.embDomain

Extending the domain of a Hahn series along an order embedding f : Γ ↪o Γ' moves each coefficient from g to f g. Mathlib records that the support of embDomain f x is contained in the image of the support of x. This file records that it is equal to that image, that a Hahn series on Γ' lies in the range of embDomain f exactly when its support lies in the range of f, and that extending along two embeddings in turn is extending along their composite.

These are the facts used to identify the image of a Laurent series under a change of exponent group, such as X ↦ X ^ d on ℤ, or ℤ → ℚ, k ↦ k / n into rational exponents. The range characterization has the shape of the HahnSeries.mem_range_embDomain_iff proposed for Mathlib in mathlib4 PR #42313.

Main results

• HahnSeries.support_embDomain: (embDomain f x).support = f '' x.support.
• HahnSeries.mem_range_embDomain_iff: x ∈ Set.range (embDomain f) ↔ x.support ⊆ Set.range f.
• HahnSeries.embDomain_embDomain: embDomain g (embDomain f x) = embDomain (f.trans g) x.

@[simp]

theorem HahnSeries.support_embDomain {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_4} [PartialOrder Γ] [PartialOrder Γ'] [Zero R] (f : Γ ↪o Γ') (x : HahnSeries Γ R) : (embDomain f x).support = ⇑f '' x.support

The support of embDomain f x is the image of the support of x.

theorem HahnSeries.mem_range_embDomain_iff {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_4} [PartialOrder Γ] [PartialOrder Γ'] [Zero R] {f : Γ ↪o Γ'} {x : HahnSeries Γ' R} : x ∈ Set.range (embDomain f) ↔ x.support ⊆ Set.range ⇑f

A Hahn series lies in the range of embDomain f exactly when its support lies in the range of f.

theorem HahnSeries.embDomain_embDomain {Γ : Type u_1} {Γ' : Type u_2} {Γ'' : Type u_3} {R : Type u_4} [PartialOrder Γ] [PartialOrder Γ'] [PartialOrder Γ''] [Zero R] (f : Γ ↪o Γ') (g : Γ' ↪o Γ'') (x : HahnSeries Γ R) : embDomain g (embDomain f x) = embDomain (RelEmbedding.trans f g) x

Extending the domain along f and then along g is extending it along f.trans g.