Step
*
of Lemma
omral_alg_umap_unique
∀g:OCMon. ∀a:CDRng. ∀n:algebra{i:l}(a). ∀f:|g| ⟶ n.car. ∀f':algebra_hom(a; omral_alg(g;a); n).
(((f' o (λk:|g|. inj(k,1))) = f ∈ (|g| ⟶ n.car))
⇒ (f' = alg_umap(n,f) ∈ (|omral(g;a)| ⟶ n.car)))
BY
{ (Auto THEN New [`ps'] Ext⋅ THEN Auto) }
1
1. g : OCMon
2. a : CDRng
3. n : algebra{i:l}(a)
4. f : |g| ⟶ n.car
5. f' : algebra_hom(a; omral_alg(g;a); n)
6. (f' o (λk:|g|. inj(k,1))) = f ∈ (|g| ⟶ n.car)
7. ps : |omral(g;a)|
⊢ (f' ps) = (alg_umap(n,f) ps) ∈ n.car
Latex:
Latex:
\mforall{}g:OCMon. \mforall{}a:CDRng. \mforall{}n:algebra\{i:l\}(a). \mforall{}f:|g| {}\mrightarrow{} n.car. \mforall{}f':algebra\_hom(a; omral\_alg(g;a); n).
(((f' o (\mlambda{}k:|g|. inj(k,1))) = f) {}\mRightarrow{} (f' = alg\_umap(n,f)))
By
Latex:
(Auto THEN New [`ps'] Ext\mcdot{} THEN Auto)
Home
Index