English
A ring satisfies the strong rank condition if and only if, for every n, any linear map (Fin(n+1) → R) → Fin n → R is not injective.
Русский
Кольцо удовлетворяет сильному условию ранга тогда и только тогда, когда для любого n любая линейная карта (Fin(n+1) → R) → Fin n → R не инъективна.
LaTeX
$$$ StrongRankCondition\; R \iff \forall n:\mathbb{N},\; f:(\mathrm{Fin}(n+1)\to R) \to_\mathrm{lin} (\mathrm{Fin}~n\to R),\; \neg\mathrm{Injective}(f). $$$
Lean4
/-- A ring satisfies the strong rank condition if and only if, for all `n : ℕ`, any linear map
`(Fin (n + 1) → R) →ₗ[R] (Fin n → R)` is not injective. -/
theorem strongRankCondition_iff_succ :
StrongRankCondition R ↔ ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Function.Injective f :=
by
refine ⟨fun h n => fun f hf => ?_, fun h => ⟨@fun n m f hf => ?_⟩⟩
· letI : StrongRankCondition R := h
exact Nat.not_succ_le_self n (le_of_fin_injective R f hf)
· by_contra H
exact
h m (f.comp (Function.ExtendByZero.linearMap R (Fin.castLE (not_le.1 H))))
(hf.comp (Function.extend_injective (Fin.strictMono_castLE _).injective _))
