mrange_mapRangeAddMonoidHom — Mathlib

English

Kernel of the coordinatewise mapRange.addMonoidHom equals the comap of the kernels of each coordinate map.

Русский

Ядро отображения mapRange.addMonoidHom на координатном уровне равно предобразованию ядер каждого координатного отображения.

LaTeX

$$$\\ker(\\mathrm{mapRange}.addMonoidHom f) = (\\mathrm{AddSubmonoid.pi}\\; Set.univ (\\lambda i, \\ker(f_i))).\\mathrm{comap}\\; \\mathrm{coeFnAddMonoidHom}$$$

Lean4

theorem mrange_mapRangeAddMonoidHom (f : ∀ i, β₁ i →+ β₂ i) :
    AddMonoidHom.mrange (mapRange.addMonoidHom f) =
      (AddSubmonoid.pi Set.univ (fun i ↦ AddMonoidHom.mrange (f i))).comap coeFnAddMonoidHom :=
  by
  classical
  ext x
  simp only [AddSubmonoid.mem_comap, coeFnAddMonoidHom_apply]
  refine ⟨fun ⟨y, hy⟩ i hi ↦ ?_, fun h ↦ ?_⟩
  · simp [← hy]
  · choose g hg using fun i => h i (Set.mem_univ _)
    use DFinsupp.mk x.support (g ·)
    ext i
    simp only [Finset.coe_sort_coe, mapRange.addMonoidHom_apply, mapRange_apply]
    by_cases mem : i ∈ x.support
    · rw [mk_of_mem mem, hg]
    · rw [DFinsupp.notMem_support_iff.mp mem, mk_of_notMem mem, map_zero]

Похожие утверждения