Add more examples of functors to witness property combinations

[ScriptRaccoon]

This is a continuation of #305. It adds the four functors below to bring down the number of missing functor combinations. The number is reduced from 87 to only 13.

The forgetful functor from torsion-free abelian groups

First, the PR adds the forgetful functor TorsFreeAb → Ab. It is intended to be an example of a fully faithful functor that does not preserve epis, but it is much more: This brings down the number of missing combinations from 87 to 53. In other words, the functor witnesses 34 combinations (or their duals) that were missing before.

These are:

• essentially injective ∧ ¬preserves coreflexive equalizers [*]
• essentially injective ∧ ¬preserves epimorphisms
• essentially injective ∧ ¬preserves monomorphisms [*]
• essentially injective ∧ ¬preserves reflexive coequalizers
• full ∧ ¬preserves coequalizers
• full ∧ ¬preserves coreflexive equalizers [*]
• full ∧ ¬preserves epimorphisms
• full ∧ ¬preserves equalizers [*]
• full ∧ ¬preserves monomorphisms [*]
• full ∧ ¬preserves reflexive coequalizers
• full on isomorphisms ∧ ¬preserves coequalizers
• full on isomorphisms ∧ ¬preserves coreflexive equalizers [*]
• full on isomorphisms ∧ ¬preserves epimorphisms
• full on isomorphisms ∧ ¬preserves equalizers [*]
• full on isomorphisms ∧ ¬preserves monomorphisms [*]
• full on isomorphisms ∧ ¬preserves reflexive coequalizers
• fully faithful ∧ ¬preserves coequalizers
• fully faithful ∧ ¬preserves coreflexive equalizers [*]
• fully faithful ∧ ¬preserves epimorphisms
• fully faithful ∧ ¬preserves equalizers [*]
• fully faithful ∧ ¬preserves monomorphisms [*]
• fully faithful ∧ ¬preserves reflexive coequalizers
• left-invertible ∧ ¬preserves coequalizers
• left-invertible ∧ ¬preserves coreflexive equalizers [*]
• left-invertible ∧ ¬preserves epimorphisms
• left-invertible ∧ ¬preserves equalizers [*]
• left-invertible ∧ ¬preserves monomorphisms [*]
• left-invertible ∧ ¬preserves reflexive coequalizers
• pseudomonic ∧ ¬preserves coequalizers
• pseudomonic ∧ ¬preserves coreflexive equalizers [*]
• pseudomonic ∧ ¬preserves epimorphisms
• pseudomonic ∧ ¬preserves equalizers [*]
• pseudomonic ∧ ¬preserves monomorphisms [*]
• pseudomonic ∧ ¬preserves reflexive coequalizers

[*] The dual combination is witnessed, which is enough.

All properties of the functor have been decided. To make this easier, the following basic implication has been added:

• fully faithful + right adjoint ==> monadic + left-invertible

The inclusion functor to ordinals

The PR also adds the inclusion functor from IN_∞ to On. It is intended to be an example of a functor that preserves binary products but not terminal objects. Actually, it further brings down the number of missing combinations from 53 to 39. The 14 new witnessed combinations (or their duals) are:

• full ∧ ¬preserves initial objects
• full ∧ ¬preserves terminal objects
• full on isomorphisms ∧ ¬preserves initial objects
• full on isomorphisms ∧ ¬preserves terminal objects
• fully faithful ∧ ¬preserves initial objects
• fully faithful ∧ ¬preserves terminal objects
• left-invertible ∧ ¬preserves initial objects
• left-invertible ∧ ¬preserves terminal objects
• preserves binary coproducts ∧ ¬preserves finite coproducts
• preserves binary coproducts ∧ ¬preserves initial objects
• preserves binary products ∧ ¬preserves finite products
• preserves binary products ∧ ¬preserves terminal objects
• pseudomonic ∧ ¬preserves initial objects
• pseudomonic ∧ ¬preserves terminal objects

All properties of the functor have been decided.

The nerve functor

The nerve functor Cat → sSet provides an example of a fully faithful functor that does not preserve regular epimorphisms. In fact, it brings down the number of missing combinations from 39 to 19. The 20 new witnessed combinations (or their duals) are:

• comonadic ∧ ¬coregular
• comonadic ∧ ¬preserves regular monomorphisms
• conservative ∧ ¬preserves regular epimorphisms
• conservative ∧ ¬preserves regular monomorphisms
• essentially injective ∧ ¬preserves regular epimorphisms
• essentially injective ∧ ¬preserves regular monomorphisms
• faithful ∧ ¬preserves regular epimorphisms
• faithful ∧ ¬preserves regular monomorphisms
• full ∧ ¬preserves regular epimorphisms
• full ∧ ¬preserves regular monomorphisms
• full on isomorphisms ∧ ¬preserves regular epimorphisms
• full on isomorphisms ∧ ¬preserves regular monomorphisms
• fully faithful ∧ ¬preserves regular epimorphisms
• fully faithful ∧ ¬preserves regular monomorphisms
• left-invertible ∧ ¬preserves regular epimorphisms
• left-invertible ∧ ¬preserves regular monomorphisms
• monadic ∧ ¬preserves regular epimorphisms
• monadic ∧ ¬regular
• pseudomonic ∧ ¬preserves regular epimorphisms
• pseudomonic ∧ ¬preserves regular monomorphisms

All properties of the functor have been decided.

Reflectors preserve terminal objects

A result that I wasn't aware of before: any reflector must preserve terminal objects. Dually, any coreflector must preserve initial objects. This brings down the number of missing combinations (without adding new functors) from 19 to just 17.

Stone-Čech compactification functor

The Stone-Čech compactification Top → CompHaus is added as an example of a reflector that does not preserve binary products. This brings down the number from 17 to just 13. The following four new combinations are witnessed (or their dual):

• coreflector ∧ ¬preserves binary coproducts
• coreflector ∧ ¬preserves finite coproducts
• reflector ∧ ¬preserves binary products
• reflector ∧ ¬preserves finite products