### Nuprl Lemma : free-group-hom

`∀[X:Type]. ∀G:Group{i}. ∀f:X ⟶ |G|.  ∃F:MonHom(free-group(X),G). ∀x:X. ((F free-letter(x)) = (f x) ∈ |G|)`

Proof

Definitions occuring in Statement :  free-letter: `free-letter(x)` free-group: `free-group(X)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T` monoid_hom: `MonHom(M1,M2)` grp: `Group{i}` grp_car: `|g|`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` grp: `Group{i}` mon: `Mon` so_lambda: `λ2x.t[x]` monoid_hom: `MonHom(M1,M2)` free-group: `free-group(X)` grp_car: `|g|` pi1: `fst(t)` so_apply: `x[s]` prop: `ℙ` free-letter: `free-letter(x)` fg-lift: `fg-lift(G;f)` fg-hom: `fg-hom(G;f;w)` top: `Top` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` imon: `IMonoid` and: `P ∧ Q`
Lemmas referenced :  fg-lift_wf monoid_hom_wf free-group_wf all_wf equal_wf grp_car_wf free-letter_wf free-word_wf grp_wf list_accum_cons_lemma list_accum_nil_lemma mon_ident grp_sig_wf monoid_p_wf grp_op_wf grp_id_wf inverse_wf grp_inv_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation dependent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality dependent_functionElimination functionExtensionality applyEquality hypothesis lambdaEquality setElimination rename setEquality because_Cache sqequalRule functionEquality universeEquality isect_memberEquality voidElimination voidEquality productElimination

Latex:
\mforall{}[X:Type].  \mforall{}G:Group\{i\}.  \mforall{}f:X  {}\mrightarrow{}  |G|.    \mexists{}F:MonHom(free-group(X),G).  \mforall{}x:X.  ((F  free-letter(x))  =  (f  x))

Date html generated: 2020_05_20-AM-08_23_13
Last ObjectModification: 2017_01_16-AM-00_26_54

Theory : free!groups

Home Index