MATH.18:4.3 - Establish what the interpretation preserves and reflects

For the consequence being transferred, follow its construction or argument through the interpretation. Establish that the required operations remain applicable and that each used equality or relation remains valid.

Distinguish the two directions. Preservation takes a source consequence to a target consequence. Reflection takes an interpreted target consequence back to the source. To use a target calculation as the source answer, obtain the required recovery and reflection argument.

For operations composed as maps, an object assignment F also assigns F(f):F(A) -> F(B) to each source map f:A -> B. To translate a sequence stage by stage, establish:

F(g∘f)=F(g)∘F(f) and F(id_A)=id_F(A).

Such an assignment is a functor. Fix source objects A and B. To recover maps, determine which target maps F(A) -> F(B) have counterparts A -> B. To recover an equality, take two source maps f,g:A -> B and determine whether F(f)=F(g) implies f=g. The equality test concerns maps with these same endpoints. Recovery of the objects themselves is a further question, handled in :4.4.

Formal-theory branch. When the intended result is transport of theorems, give the translation of the relevant syntax and logic. Establish the interpreted axioms and justify the inference rules used by the theorem. Comparing collections of models through maps supplies a different mathematical result until its connection to this theorem-translation claim is established.

A failed preservation or reflection equation is useful. Work its inputs far enough to show what answer or construction changes. Then restrict the claim, enrich the interpretation or keep the accounts distinct for that purpose.