English
If f is an order-embedding Γ → Γ' preserving addition, then embDomain f preserves multiplication: embDomain f (x y) = embDomain f x · embDomain f y for HahnSeries x,y.
Русский
Если f — отображение с сохранением порядка и суммы, то embDomain f сохраняет умножение: embDomain f (x y) = embDomain f x · embDomain f y для HahnSeries x,y.
LaTeX
$$$ embDomain\ f (x \cdot y) = embDomain\ f\ x \cdot embDomain\ f\ y $$$
Lean4
theorem embDomain_mul [NonUnitalNonAssocSemiring R] (f : Γ ↪o Γ') (hf : ∀ x y, f (x + y) = f x + f y)
(x y : HahnSeries Γ R) : embDomain f (x * y) = embDomain f x * embDomain f y :=
by
ext g
by_cases hg : g ∈ Set.range f
· obtain ⟨g, rfl⟩ := hg
simp only [coeff_mul, embDomain_coeff]
trans
∑ ij ∈ (addAntidiagonal x.isPWO_support y.isPWO_support g).map (f.toEmbedding.prodMap f.toEmbedding),
(embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2
· simp
apply sum_subset
· rintro ⟨i, j⟩ hij
simp only [mem_map, mem_addAntidiagonal, Function.Embedding.coe_prodMap, mem_support, Prod.exists] at hij
obtain ⟨i, j, ⟨hx, hy, rfl⟩, rfl, rfl⟩ := hij
simp [hx, hy, hf]
· rintro ⟨_, _⟩ h1 h2
contrapose! h2
obtain ⟨i, _, rfl⟩ := support_embDomain_subset (ne_zero_and_ne_zero_of_mul h2).1
obtain ⟨j, _, rfl⟩ := support_embDomain_subset (ne_zero_and_ne_zero_of_mul h2).2
simp only [mem_map, mem_addAntidiagonal, Function.Embedding.coe_prodMap, mem_support, Prod.exists]
simp only [mem_addAntidiagonal, embDomain_coeff, mem_support, ← hf, OrderEmbedding.eq_iff_eq] at h1
exact ⟨i, j, h1, rfl⟩
· rw [embDomain_notin_range hg, eq_comm]
contrapose! hg
obtain ⟨_, hi, _, hj, rfl⟩ := support_mul_subset_add_support ((mem_support _ _).2 hg)
obtain ⟨i, _, rfl⟩ := support_embDomain_subset hi
obtain ⟨j, _, rfl⟩ := support_embDomain_subset hj
exact ⟨i + j, hf i j⟩
