English
Let R, S1, S2 be commutative semirings and σ a type. For ring hom f : R →+* S1, g : σ → S1, and φ : S1 →+* S2, the evaluation followed by φ equals the evaluation with the composed data: φ ∘ eval₂(f,g) = eval₂(φ ∘ f) (i ↦ φ(g(i))).
Русский
Пусть R, S1, S2 — коммутативные полукольца, σ — множество индексов. Для кольцогомофтр f : R →+* S1, g : σ → S1 и φ : S1 →+* S2 равенство компоновок выполняется: φ ∘ eval₂(f,g) = eval₂(φ ∘ f) (i ↦ φ(g(i))).
LaTeX
$$$\\phi \\circ \\mathrm{eval}_2 f g = \\mathrm{eval}_2(\\phi \\circ f) (\\, i \\mapsto \\phi(g(i)) \\\\).$$
Lean4
@[simp]
theorem comp_eval₂Hom [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₁) (φ : S₁ →+* S₂) :
φ.comp (eval₂Hom f g) = eval₂Hom (φ.comp f) fun i => φ (g i) := by ext <;> simp
