rankCondition_of_strongRankCondition

English

If R has StrongRankCondition, then RankCondition R holds (i.e., le_of_fin_injective applies).

Русский

Если R обладает свойством сильного ранга, то выполняется RankCondition R (то есть применимо неравенство).

LaTeX

$$$\text{RankCondition } R \text{ follows from } \text{StrongRankCondition } R.$$$

Lean4

/-- By the universal property for free modules, any surjective map `(Fin n → R) →ₗ[R] (Fin m → R)`
has an injective splitting `(Fin m → R) →ₗ[R] (Fin n → R)`
from which the strong rank condition gives the necessary inequality for the rank condition.
-/
instance (priority := 100) rankCondition_of_strongRankCondition [StrongRankCondition R] : RankCondition R where
  le_of_fin_surjective f s := le_of_fin_injective R _ (f.splittingOfFunOnFintypeSurjective_injective s)

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