Kernels and images in Algebra

[jamesmckinna]

Discussing @Taneb 's most recent comments on PR #1767 , it is clear that we are (also!) missing some fairly crucial definitions from the Algebra library/hierarchy: ie given a XHomomorphism h, define

• kernel, ie via the property InKernel = λ x → h x ≈ 0 (suitably interpreted)
• image, ie via the property InImage = λ y → ∃ x → h x ≈ y

together with their evident closure properties as substructures, cf. issue #1899 .

Note also that while we have definitions of structures (but not yet bundles! #1960) defining IsXMonomorphism and IsXIsomorphism based on Function.Definitions.Injective and Function.Definitions.Core2.Surjective, these might better (best?) be rephrased/proved equivalent to, properties involving the kernel and image, eg.

• IsXMonomorphism h iff ∀ {x} → InKernel h x → x ≈ 0, etc.

[JacquesCarette]

There's a whole bunch of 'evident' constructions from universal algebra that are missing, with the above listing a few.

It's a dangerous rabbit hole... I think Yasmine implemented 12 constructions, but found more than 30 in the literature.

[jamesmckinna]

30 of what, exactly? And which 12 were implemented?

[jamesmckinna]

Regarding whether this is a "dangerous rabbit hole", I've already argued (#1899 ) that we at least need these two concepts, and hence the characterisation of mono/surjective homomorphisms by the corresponding (short) exact sequences.

What is unsatisfying about the properties in #1767 is that they are not phrased in such terms, but without their being already present in the library, it's perhaps easy to see how such mathematically less 'efficient' formulations can come about.

[JacquesCarette]

30 constructions from the universal algebra literature (viewed very broadly). A quick overview on slide 21 of Yasmine Sharoda's PhD defense slides. Some of them are detailed in Chapter 3 of her thesis; chapter 9 lists the ones that are implemented. (I may have had the numbers a tiny bit off, memory is funny that way).

[jamesmckinna]

Apologies for not taking the trouble to go back to Yasmine's thesis for chapter-and verse...
... I was intrigued to see the kernel presented there not as a subset of the carrier, on which the homomorphism is annihilated (suitably interpreted), but rather as the equivalence relation on the carrier induced by having equal images. The former emphasises the kernel as a suitable 'ideal' substructure (with quotients by such things then requiring an additional definition), while the latter defines the quotient structure directly. Food for thought! cf. #1899

[JacquesCarette]

And apologies to take 3 weeks to reply!

As you know, 'subset' is not so well behaved in MLTT and, looking around, the direct relation can be defined much more widely (and was found in textbooks that worries about such things), so we adopted that one.

[jamesmckinna]

Another one to punt until after v2.0, I think ;-)

[jamesmckinna]

This issue, and the discussion, is substantially a duplicate of #1899 , so closing this in favour of leaving that one open... moreover the definition of kernel given here is less general than that given by the equivalence relation above (but obviously equivalent in the presence of (Is)AbelianGroup structure...)