English
Let R be a commutative semiring and A an R-algebra. If the nonnegative cone of R maps into the image of nonnegative elements of A and s is convex over R, then s is convex over A (under faithful SMul).
Русский
Пусть R — коммутативный полупрерывный полулинейный полюс, A — алгебра над R. Если неотрицательная полупрямота R отображается в образ неотрицательных элементов A и s выпукло относительно R, то s выпукло относительно A (при оговорке о верности тензорного действия).
LaTeX
$$$\text{Ici}(0) \subseteq \text{image}(\text{algebraMap } R A)(\text{Ici}(0)) \wedge \operatorname{Convex}_R(s) \Rightarrow \operatorname{Convex}_A(s).$$$
Lean4
theorem convex_of_nonneg_surjective_algebraMap [FaithfulSMul R A] {s : Set M}
(halg : Set.Ici 0 ⊆ algebraMap R A '' Set.Ici 0) (hs : Convex R s) : Convex A s :=
by
simp only [Convex, StarConvex] at hs ⊢
intro u hu v hv a b ha hb hab
obtain ⟨c, hc1, hc2⟩ := halg ha
obtain ⟨d, hd1, hd2⟩ := halg hb
convert hs hu hv hc1 hd1 _ using 2
· rw [← hc2, algebraMap_smul]
· rw [← hd2, algebraMap_smul]
rw [← hc2, ← hd2, ← algebraMap.coe_add] at hab
exact (FaithfulSMul.algebraMap_eq_one_iff R A).mp hab
