### Nuprl Lemma : fg-lift_wf

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

Proof

Definitions occuring in Statement :  fg-lift: `fg-lift(G;f)` free-letter: `free-letter(x)` free-group: `free-group(X)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` set: `{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]` member: `t ∈ T` all: `∀x:A. B[x]` grp: `Group{i}` mon: `Mon` fg-lift: `fg-lift(G;f)` monoid_hom: `MonHom(M1,M2)` free-group: `free-group(X)` grp_car: `|g|` pi1: `fst(t)` subtype_rel: `A ⊆r B` uimplies: `b supposing a` grp_op: `*` pi2: `snd(t)` infix_ap: `x f y` prop: `ℙ` free-word: `free-word(X)` implies: `P `` Q` cand: `A c∧ B` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` squash: `↓T` true: `True` guard: `{T}` equiv_rel: `EquivRel(T;x,y.E[x; y])` refl: `Refl(T;x,y.E[x; y])` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` free-append: `w + w'` free-letter: `free-letter(x)` fg-hom: `fg-hom(G;f;w)` top: `Top` imon: `IMonoid` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  grp_car_wf grp_wf fg-hom_wf free-group_wf grp_hom_formation grp_subtype_igrp monoid_hom_p_wf word-equiv-equiv list_wf word-equiv_wf equal-wf-base equal_wf squash_wf true_wf free-append_wf subtype_quotient fg-hom-append iff_weakening_equal free-word_wf quotient-member-eq 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 all_wf free-letter_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation dependent_set_memberEquality sqequalHypSubstitution hypothesis functionEquality cumulativity hypothesisEquality extract_by_obid isectElimination thin setElimination rename sqequalRule lambdaEquality dependent_functionElimination axiomEquality equalityTransitivity equalitySymmetry because_Cache universeEquality functionExtensionality applyEquality independent_isectElimination unionEquality promote_hyp independent_pairFormation pointwiseFunctionality pertypeElimination productElimination independent_functionElimination productEquality imageElimination natural_numberEquality imageMemberEquality baseClosed isect_memberEquality voidElimination voidEquality setEquality

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

Date html generated: 2017_10_05-AM-00_45_30
Last ObjectModification: 2017_07_28-AM-09_18_54

Theory : free!groups

Home Index