feat(RingTheory/HahnSeries): embDomain as OrderAddMonoidHom; orderTop of embDomain (#29421)

These will be used in #27268 Hahn embedding theorem

Author: wwylele

Mathlib/RingTheory/HahnSeries/Basic.lean

@@ -484,6 +484,21 @@ theorem embDomain_injective {f : Γ ↪o Γ'} :
   have xyg := xy (f g)
   rwa [embDomain_coeff, embDomain_coeff] at xyg
 
+@[simp]
+theorem orderTop_embDomain {Γ : Type*} [LinearOrder Γ] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} :
+    (embDomain f x).orderTop = WithTop.map f x.orderTop := by
+  obtain rfl | hx := eq_or_ne x 0
+  · simp
+  rw [← WithTop.coe_untop x.orderTop (by simpa using hx), WithTop.map_coe]
+  apply orderTop_eq_of_le
+  · simpa using coeff_orderTop_ne (by simp)
+  intro y hy
+  obtain ⟨z, hz, rfl⟩ :=
+    (Set.mem_image _ _ _).mp <| Set.mem_of_subset_of_mem support_embDomain_subset hy
+  rw [OrderEmbedding.le_iff_le, WithTop.untop_le_iff]
+  apply orderTop_le_of_coeff_ne_zero
+  simpa using hz
+
 end Domain
 
 end Zero

Mathlib/RingTheory/HahnSeries/Lex.lean

@@ -353,4 +353,47 @@ end Archimedean
 
 end OrderedGroup
 
+section EmbDomain
+variable [PartialOrder R] {Γ' : Type*} [LinearOrder Γ'] (f : Γ ↪o Γ')
+
+/-- `HahnSeries.embDomain` as an `OrderEmbedding`. -/
+@[simps]
+noncomputable
+def embDomainOrderEmbedding [Zero R] : Lex (HahnSeries Γ R) ↪o Lex (HahnSeries Γ' R) where
+  toFun a := toLex (embDomain f (ofLex a))
+  inj' := toLex.injective.comp (embDomain_injective.comp (ofLex.injective))
+  map_rel_iff' {a b} := by
+    simp_rw [le_iff_lt_or_eq, lt_iff]
+    simp only [Function.Embedding.coeFn_mk, ofLex_toLex, EmbeddingLike.apply_eq_iff_eq]
+    constructor
+    · rintro (⟨i, hj, hi⟩ | heq)
+      · have himem : i ∈ Set.range f := by
+          contrapose! hi
+          simp [embDomain_notin_range hi]
+        obtain ⟨k, rfl⟩ := himem
+        refine Or.inl ⟨k, fun j hjk ↦ ?_, by simpa using hi⟩
+        simpa using hj (f j) (f.lt_iff_lt.mpr hjk)
+      · exact Or.inr <| embDomain_injective.comp (ofLex.injective) heq
+    · rintro (⟨i, hj, hi⟩ | rfl)
+      · refine Or.inl ⟨f i, fun k hki ↦ ?_, by simpa using hi⟩
+        by_cases hkmem : k ∈ Set.range f
+        · obtain ⟨j', rfl⟩ := hkmem
+          simpa using hj _ <| f.lt_iff_lt.mp hki
+        · simp_rw [embDomain_notin_range hkmem]
+      · simp
+
+/-- `HahnSeries.embDomain` as an `OrderAddMonoidHom`. -/
+@[simps]
+noncomputable
+def embDomainOrderAddMonoidHom [AddMonoid R] : Lex (HahnSeries Γ R) →+o Lex (HahnSeries Γ' R) where
+  __ := (embDomainOrderEmbedding f).toOrderHom
+  map_zero' := by simp
+  map_add' := by simp [embDomainOrderEmbedding, embDomain_add]
+
+theorem embDomainOrderAddMonoidHom_injective [AddMonoid R] :
+    Function.Injective (embDomainOrderAddMonoidHom f (R := R)) :=
+  (embDomainOrderEmbedding f).injective
+
+end EmbDomain
+
 end HahnSeries