Abelianization

Part of the dependency closure of the small undecidable group constructions.

theorem Undecidability.Host.map_d_eq_one_of_commGroup (datum : Thue.StandingDatum) {A : Type u_1} [CommGroup A] (f : (presentationOf datum).Group →* A) : f (PresentedGroup.of 0) = 1

Every homomorphism from the host group to a commutative group kills D.

theorem Undecidability.Host.d_eq_one_in_abelianization (datum : Thue.StandingDatum) : Abelianization.of (PresentedGroup.of 0) = 1

The image of D is trivial in the abelianization of the host group.