English
The range of mapAlgHom for the identity algebra hom equals the range generated by the identity map on coefficients.
Русский
Диапазон mapAlgHom от тождества гомоморфизма алгебр равен диапазону образа по коэффициентам.
LaTeX
$$$\\mathrm{range}(\\\\mathrm{mapAlgHom} (\\\\mathrm{AlgHom.id} R S_1)).toSubmodule = \\\\mathrm{coeffsIn} σ (\\\\mathrm{RelEmbedding}.instFunLike.coe (\\\\mathrm{range}) )$$$
Lean4
theorem mem_range_map_iff_coeffs_subset {f : R →+* S₁} {x : MvPolynomial σ S₁} :
x ∈ Set.range (MvPolynomial.map f) ↔ (x.coeffs : Set _) ⊆ .range f := by
classical
refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
· obtain ⟨p, rfl⟩ := hx
exact subset_trans (coe_coeffs_map f p) (by simp)
·
induction x using induction_on'' with
| C a =>
by_cases h : a = 0
· subst h
exact ⟨0, by simp⟩
· simp only [coeffs_C, h, reduceIte, Finset.coe_singleton, Set.singleton_subset_iff] at hx
obtain ⟨b, rfl⟩ := hx
exact ⟨C b, by simp⟩
| mul_X p n ih =>
rw [coeffs_mul_X] at hx
obtain ⟨q, rfl⟩ := ih hx
exact ⟨q * X n, by simp⟩
| monomial_add a s p ha hs hp
ih =>
rw [coeffs_add (disjoint_support_monomial ha hs)] at hx
simp only [Finset.coe_union, Set.union_subset_iff] at hx
obtain ⟨q, hq⟩ := ih hx.1
obtain ⟨u, hu⟩ := hp hx.2
exact ⟨q + u, by simp [hq, hu]⟩