2.1 Definitions that might be unnecessary and possibly omitted #191
Description
(2.1 references item 1 of referee report 2)
Some definitions and proofs look unnecessary and therefore lack motivation. In particular,
-
The referee says we could parameterize FreeAlgebra by a class of algebras K rather than by a relation E on terms,
and defines the FreeDomain F[X] as the quotient of Term X by Th K; then the inductive relation ⊢_▹_≈ (and related proofs,
soundness) are unnecessary for the proof of Birkhoff to carry on.(The original proof did what the referee suggests, but we switched to the approach that requires Abel's ⊢_▹_≈ relation because (I think) with the former approach we ran into trouble completing the proof and actually introduced an inconsistency.)
-
Second half of the paper (starting with § on relatively free algebra) is confusing. The referee suggests the following argument:
Define F[X] as T X / ~, where x ~ y iff given any homomorphism f into an element of K, f x = f y (in other words, x ~ y iff (x,y) ∈ Th K). Then, if A is in Mod (Th K), the surjective morphism T A → A factors through T X → F[X], so it remains to show that F[X] ∈ SP K (then, A ∈ HSP K).
F[X] is easily shown to be a sd prod of all algebras in K. However, because of size issues, this product may not exist. Fortunately, it's also a subproduct of the algebras in {T X / Θ}, because any hom factors as an epimorphism followed by a monomorphism, so that x ~ y iff for any epimorphism f into an element of S K, f x = f y.
This argument is close to ours, but might be more understandable (provided it's correct).