English
For finsupp versions in RankCondition rings, if f : Finsupp α R → Finsupp β R is surjective, then card β ≤ card α.
Русский
Для версий Finsupp в кольцах с RankCondition: если f: Finsupp α R → Finsupp β R сюръективно, тогда |β| ≤ |α|.
LaTeX
$$$\text{If } f:\mathrm{Finsupp}(\alpha, R) \to_\mathrm{lin} \mathrm{Finsupp}(\beta, R) \text{ is surjective, then } |\beta| \le |\alpha|.$$$
Lean4
theorem card_le_of_surjective' [RankCondition R] {α β : Type*} [Fintype α] [Fintype β] (f : (α →₀ R) →ₗ[R] β →₀ R)
(i : Surjective f) : Fintype.card β ≤ Fintype.card α :=
by
let P := Finsupp.linearEquivFunOnFinite R R β
let Q := (Finsupp.linearEquivFunOnFinite R R α).symm
exact card_le_of_surjective R ((P.toLinearMap.comp f).comp Q.toLinearMap) ((P.surjective.comp i).comp Q.surjective)
