On locally spherical polytopes of type {5, 3, 5}

There are only finitely many locally projective regular polytopes of type {5, 3, 5}. They are covered by a locally spherical polytope whose automorphism group is J1×J1×L2(19)J1×J1×L2(19), where J1J1 is the first Janko group, of order 175560, and L2(19)L2(19) is the projective special linear group of order 3420. This polytope is minimal, in the sense that any other polytope that covers all locally projective polytopes of type {5, 3, 5} must in turn cover this one.