tensor preserves coequalizers

[Alizter]

We show that tensor products of abelian groups preserve coequalizers. This will be used when defining tensor products of modules.

[jdchristensen]

Since ab_coeq is a special case of ab_cokernel, I would argue that all of these results (functoriality of ab_coeq and preservation of ab_coeq by tensoring) should be proved for cokernels instead, as that would be more general and the proofs would be slightly simpler, since there is only one homomorphism to deal with, not two. We would then add a lemma saying that k $o f $== k $o g iff k $o (-f + g) is homotopic to the constant map, which would let us easily apply the results about cokernels to coequalizers.

(In fact, the result about tensoring should apply to any exact sequence B -> C -> D -> 0, but maybe that's more awkward to prove. Still, the result about cokernels would be closer to this more general result.)

[jdchristensen]

I added ab_tensor_prod_rec', which is close to the expected map (A $-> ab_hom B C) -> (ab_tensor_prod A B $-> C). But any use of ab_hom requires Funext, so results stated using ab_hom are a bit annoying.

[Alizter]

Since ab_coeq is a special case of ab_cokernel, I would argue that all of these results (functoriality of ab_coeq and preservation of ab_coeq by tensoring) should be proved for cokernels instead, as that would be more general and the proofs would be slightly simpler, since there is only one homomorphism to deal with, not two. We would then add a lemma saying that k $o f $== k $o g iff k $o (-f + g) is homotopic to the constant map, which would let us easily apply the results about cokernels to coequalizers.

(In fact, the result about tensoring should apply to any exact sequence B -> C -> D -> 0, but maybe that's more awkward to prove. Still, the result about cokernels would be closer to this more general result.)

This sounds good. I'll see if I can prove the same about cokernels and derive the same results using those.

[jdchristensen]

I'll see if I can prove the same about cokernels and derive the same results using those.

Continuing in this line of thought, functoriality for cokernels should follow from functoriality for quotients and images, so maybe it's best to prove those first (if not already there). Also, maybe the functoriality of the tensor product should be derived from functoriality of coequalizers? OTOH, some of these are so easy that it's probably not worth optimizing too much.

But there's also a different possibility that occurred to me. Right now we're treating the quotient of a group by a normal subgroup as fundamental, and defining other quotients in terms of this. That means that instead of requiring that foo = bar, we require that -bar * foo = mon_unit, which leads to repeated algebraic manipulations. Maybe we should instead take the quotient of a group by a "normal multiplicative relation" (which should be a relation with whatever axioms we need in order for the quotient to be a group). Then coequalizers could be defined directly in terms of that without needing to negate and add homomorphisms, and cokernels would be a special case of coequalizers. This would also simplify the algebra involving tensor products.

(As an orthogonal comment, right now we require a subgroup to be represented by an h-prop valued function, but since we set-truncate the quotient, we could allow quotienting by a more general predicate, which would avoid needing to strip truncations and apply tr everywhere.)

[Alizter]

I'll see if I can prove the same about cokernels and derive the same results using those.

Continuing in this line of thought, functoriality for cokernels should follow from functoriality for quotients and images, so maybe it's best to prove those first (if not already there). Also, maybe the functoriality of the tensor product should be derived from functoriality of coequalizers? OTOH, some of these are so easy that it's probably not worth optimizing too much.

I'm not sure if it is best to do that now. It seems a bit tedious.

But there's also a different possibility that occurred to me. Right now we're treating the quotient of a group by a normal subgroup as fundamental, and defining other quotients in terms of this. That means that instead of requiring that foo = bar, we require that -bar * foo = mon_unit, which leads to repeated algebraic manipulations. Maybe we should instead take the quotient of a group by a "normal multiplicative relation" (which should be a relation with whatever axioms we need in order for the quotient to be a group). Then coequalizers could be defined directly in terms of that without needing to negate and add homomorphisms, and cokernels would be a special case of coequalizers. This would also simplify the algebra involving tensor products.

I believe we already do this. In QuotientGroup.v we have CongruenceQuotient and it is the passage from a normal subgroup to a congruence that introduces those ugly -bar * foo terms. I guess it becomes an issue of hooking everything up. Could you create an issue with this and I will try to experiment when I have some time.

(As an orthogonal comment, right now we require a subgroup to be represented by an h-prop valued function, but since we set-truncate the quotient, we could allow quotienting by a more general predicate, which would avoid needing to strip truncations and apply tr everywhere.)

That might be possible, but I don't think it is too difficult to do truncation elimination for the time being.

[jdchristensen]

I believe we already do this. In QuotientGroup.v we have CongruenceQuotient

Ah, yes, that's exactly what I'm thinking of, and it's in fact much simpler than the definition of a normal subgroup (but is equivalent when you take R x y to mean -x * y is in the subgroup.

That might be possible, but I don't think it is too difficult to do truncation elimination for the time being.

Well, it turns out that the hypothesis that R be truncated in the Section defining the congruence quotient is never used, so it can simply be deleted. So if we directly use the congruence quotient to define the coequalizer, I think we'll benefit in this way as well. I guess that given f, g : A $-> B, we should define R b b' to be { a : A & f a = b * g a = b' }.

If we do that, it's not clear whether to define the cokernel as the coequalizer against the zero map, or to keep the cokernel as the quotient by the image subgroup.

I'll create an issue.

[Alizter]

I think it would be good to redefine the cokernel as a congruence quotient too since that actually suffers from the extra truncation we do. This is why Jarl has introduced images and cokernels of emebeddings.

[jdchristensen]

I think it would be good to redefine the cokernel as a congruence quotient too since that actually suffers from the extra truncation we do. This is why Jarl has introduced images and cokernels of emebeddings.

I agree that we should redefine the cokernel as a congruence quotient, but I think we should do it indirectly. Either we make the cokernel a special case of the coequalizer, or we keep it as a special case of the quotient by a subgroup, but generalize that set-up to allow subgroups whose predicates are non-truncated.

It seems like for many purposes working with subgroups defined by non-truncated predicates will be smoother. But a few results about subgroups wouldn't be true in that generality. We could consider dropping the requirement that subgroups use truncated predicates, and adding that as a side condition only for the results that need it. Forming the quotient wouldn't need it, and by default we could define the image of a homomorphism to be the non-truncated version, so we wouldn't need Jarl's special versions of images and cokernels.

[Alizter]

@jdchristensen Are you happy with merging this for the time being? I'll create an issue about showing functionality earlier on, but for now this is good to have. It will allow us to experiment with module tensor products atleast.

[jdchristensen]

I guess it's ok to merge this as is, as long as various issues get created so we don't forget the improvements suggested here. There's already #2035 that covers some of the discussion above. We at least need an issue about functoriality as well. Maybe more, not sure.

[Alizter]

OK I will give it some more time so that we can create the issues first.

[Alizter]

I've created #2067 which I believe was the only issue left to address here. I am therefore merging.