MATH.19:5 - Archetypal Grounding

MATH.19:5.1 - Choose the intermediate equality that proves injectivity

Let f:A->B and g:B->A satisfy g(f(a))=a for every a in A. Prove that f is injective.

Work backward from injectivity: choose arbitrary a,b in A and assume f(a)=f(b). The required conclusion is a=b. The given identity involves g(f(a)), so work forward by applying g to the assumed equality:

g(f(a))=g(f(b)).

Substitute the two given identities to obtain a=b. The intermediate equality connects the assumption to the goal; no larger theory is needed.

Now replace the given identity by f(g(b))=b for every b in B. The same proof cannot simplify g(f(a)). What it does supply is surjectivity of f: for an arbitrary b, choose a=g(b), then f(a)=b.

For a concrete separating case, take A={0,1}, B={*}, f(0)=f(1)=*, and g(*)=0. The changed identity holds, but f is not injective. The failure identifies which composite was required and produces the useful conclusion that remains. MATH.18 can use these two composites when comparing descriptions.

MATH.19:5.2 - Discover the lemma needed to repeat a composition

Let f and g be maps X->X with f composed with g equal to g composed with f. Write composition as juxtaposition, with fg meaning apply g first and then f. Define f^0=id and f^(n+1)=f^n f, and similarly for g. Prove:

(fg)^n=f^n g^n

for every natural n.

The base n=0 holds. At the next step, the proposed induction hypothesis gives:

(fg)^(n+1)=f^n g^n f g.

The target is f^(n+1)g^(n+1). The difference exposes a missing lemma: g^n f=f g^n. This states precisely how to move f past the repeated g.

Prove that lemma by induction. At n=0 both sides are f. If it holds at n, then:

g^(n+1)f=g^n g f=g^n f g=f g^n g=f g^(n+1).

The second equality uses gf=fg; the third uses the lemma’s induction hypothesis. Return to the original step:

f^n g^n f g=f^n f g^n g=f^(n+1)g^(n+1).

The two inductions now have separate proved responsibilities. MATH.4 supplies their general induction method; the present work found which additional statement makes the main step possible.

Remove the commutation premise. On integers, f(x)=x+1 and g(x)=2x give (fg)^2(0)=3, while f^2 g^2(0)=2. The theorem has become false. Retaining the premise or retaining the actual interleaved composition are different useful responses; continuing the old rearrangement would lose the result needed by the calculation.

MATH.19:5.3 - Generalize a parameter to make the proof close

Suppose a finite list is built as [] or x::xs. Define append ++ in the usual way, with []++a=a and (x::xs)++a=x::(xs++a). Let [x] denote the one-element list.

Define reversal by R([])=[] and R(x::xs)=R(xs)++[x]. A second construction carries an accumulator:

T([],a)=a,

T(x::xs,a)=T(xs,x::a).

The wanted result is T(xs,[])=R(xs). Induction on xs with only this statement stalls: the recursive call uses accumulator x::[], while the hypothesis concerns [].

Generalize to every accumulator a:

T(xs,a)=R(xs)++a.

The empty-list case gives a=[]++a. For a nonempty list, the generalized induction hypothesis gives:

T(x::xs,a)=T(xs,x::a)=R(xs)++(x::a).

Using x::a=[x]++a and associativity of append, this equals (R(xs)++[x])++a=R(x::xs)++a. Append associativity itself follows by induction on its first list: the empty case is the defining rule, and the nonempty case reduces after the common leading element to the induction hypothesis.

Setting a=[] recovers the original target, using append’s right-identity law. That law also follows from the same two formation cases. On [1,2,3], the accumulator states [], [1], [2,1], [3,2,1] make the changed parameter visible.

The proof establishes equality of the two list results. A claim that one implementation uses less time or storage additionally depends on its list representation and execution model. Those are computational questions for the obtained construction.