English
Nontrivial commutative semirings satisfy the rank condition; in particular, if the semiring is a ring, the strong rank condition holds.
Русский
Не тривиальные коммутативные полуприроды удовлетворяют условию ранга; в частности, если полуприрода является кольцом, выполняется сильное условие ранга.
LaTeX
$$$\text{RankCondition}(R)\text{ holds for all nontrivial } R \text{ with } R\text{ commutative semiring.}$$$
Lean4
/-- Nontrivial commutative semirings `R` satisfy the rank condition.
If `R` is moreover a ring, then it satisfies the strong rank condition, see
`commRing_strongRankCondition`. It is unclear whether this generalizes to semirings. -/
instance (priority := 100) rankCondition_of_nontrivial_of_commSemiring {R : Type*} [CommSemiring R] [Nontrivial R] :
RankCondition R where
le_of_fin_surjective {n m} f
hf := by
by_contra! lt
let p : (Fin m → R) →ₗ[R] Fin n → R := .funLeft R R (Fin.castLE lt.le)
have hp : Surjective p := LinearMap.funLeft_surjective_of_injective _ _ _ (Fin.castLE_injective lt.le)
have ⟨g, eq⟩ := (p ∘ₗ f).exists_rightInverse_of_surjective (LinearMap.range_eq_top.mpr <| hp.comp hf)
let e := Matrix.toLinAlgEquiv' (R := R) (n := Fin n).symm
apply_fun e at eq
rw [← Module.End.mul_eq_comp, ← Module.End.one_eq_id, map_mul, map_one,
Matrix.mul_eq_one_comm_of_equiv (Equiv.refl _), ← map_mul, ← map_one e, e.injective.eq_iff] at eq
have : Injective p := (p.coe_comp f ▸ LinearMap.injective_of_comp_eq_id _ _ eq).of_comp_right hf
have ⟨⟨i, lt⟩, eq⟩ := injective_comp_right_iff_surjective.mp this ⟨n, lt⟩
exact lt.ne congr($eq)
