supported_comap_lmapDomain — Mathlib

English

There is a linear equivalence between the supported submodule on s and the finsupps on s.

Русский

Существует линейное эквивалентное отображение между поддерживаемым подмодулем на s и отображениями FinSupp на s.

LaTeX

$$$\mathrm{supportedEquivFinsupp}(M,R,s) : \mathrm{supported}(M,R,s) \simeq_\,R \,(s \to_0 M)$$$

Lean4

theorem supported_comap_lmapDomain (f : α → α') (s : Set α') :
    supported M R (f ⁻¹' s) ≤ (supported M R s).comap (lmapDomain M R f) := by
  classical
  intro l (hl : (l.support : Set α) ⊆ f ⁻¹' s)
  change ↑(mapDomain f l).support ⊆ s
  rw [← Set.image_subset_iff, ← Finset.coe_image] at hl
  exact Set.Subset.trans mapDomain_support hl

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