ualib / agda-algebras

The Agda Universal Algebra Library (html docs available at the url below)
https://ualib.github.io/agda-algebras/
Creative Commons Attribution Share Alike 4.0 International
29 stars 7 forks source link

Issues related to finding an algebra in S (P ๐’ฆ) which is the domain of an epimorphism onto ๐‘จ #200

Closed williamdemeo closed 2 years ago

williamdemeo commented 2 years ago

I'm combining the following into one issue because they all have roughly the same response, which is that finding an F in S (P K) that is the domain of an epimorphism onto an arbitrary algebra in Mod (Th K) proved exceedingly difficult. It was the hardest part of the proof. The suggestions below all seem to point out that (in theory) it's easy to see the F's they suggest are in S (P K). However, proving this formally is hard.

  1. Review 2 (point 1). The second half of the paper (starting with ยง on relatively free algebra) is confusing. The reviewer was hoping for the following argument:

    • Define ๐”ฝ[X] as ๐‘ป(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 ๐’ฆ). Then, if ๐‘จ is in Mod (Th ๐’ฆ), the surjective morphism ๐‘ป(A) โ†’ ๐‘จ factors through ๐‘ป(X) โ†’ ๐”ฝ[X], so it remains to show that ๐”ฝ[X] โˆˆ S (P ๐’ฆ) (then, ๐‘จ โˆˆ HSP ๐’ฆ).
    • ๐”ฝ[X] is easily shown to be a sd prod of all algebras in ๐’ฆ. However, because of size issues, this product may not exist. Fortunately, it's also a subproduct of the algebras in { ๐‘ป(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 ๐’ฆ, f x = f y.
  2. Review 2 (point 12).

    Let ๐‘จ โˆˆ ๐’ฆโบ; it suffices to find an algebra ๐‘ญ โˆˆ S (P ๐’ฆ) such that ๐‘จ is a homomorphic image of ๐‘ญ, as this will show that ๐‘จ โˆˆ H (S (P ๐’ฆ)) = ๐’ฆ.

    Why can't we conclude the proof here by choosing ๐‘ญ = ๐”ฝ[A], since we already showed that ๐‘จ is an homomorphic image of ๐”ฝ[A] before ยง6 and that ๐”ฝ[A] โˆˆ S (P ๐’ฆ) (in the ยง on relatively free algebra in theory)?

  3. Review 2 (point 14).

    Let ๐‘ช be the product of all algebras in S ๐’ฆ, so that ๐‘ช โˆˆ P (S ๐’ฆ).

    Can we comment on the reason we chose a different route from the mathematical proof that we describe informally? (see also: comment on the universe hierarchy).

JacquesCarette commented 2 years ago

Sounds like all of this should be done in referee comments indeed - and maybe future work for a journal version?

williamdemeo commented 2 years ago

Actually, I labeled them incorrectly. All three points were made by the same referee. (The "weak accept" ...I guess s/he really didn't like our proof very much :roll_eyes: )

williamdemeo commented 2 years ago

Sounds like all of this should be done in referee comments indeed - and maybe future work for a journal version?

Yes, good idea.

williamdemeo commented 2 years ago

done