Biratio

Stream: Is there code for X?

[Yaël Dillies]

@Joseph Myers, now that we have betweenness, do we have the "biratio" somewhere? I mean $\frac{\bar{AB}}{\bar{AC}}$ for $A, B, C$ points on a line.

[Yaël Dillies]

This would help generalize the Ceva theorem we have in #10632 to all points not aligned with points of the triangle.

[Joseph Myers]

I'm not aware of such a definition in mathlib. I'd be inclined to set it up as an operation that divides two vectors (in a module), yielding a scalar (note that the ring would need to be an explicit argument to this operation), defaulting to 0 if there is not a unique scalar that, acting on one vector, yields the other. (This has no dependence on any kind of order on the ring, but over the reals it yields an appropriate ratio of signed distances.)

[Yaël Dillies]

So it would default to 0 as soon as the $A, B, C$ are not aligned? I quite like that.

[Yaël Dillies]

Do you think we should define the cross-ratio as the ratio of biratios, or rather use the complex numbers definition?

[Joseph Myers]

Cross-ratio is meaningful in any affine space over a field (or indeed in any projective space over a field, but I suspect it may be convenient to use a definition of cross-ratio in affine spaces as part of defining it in projectivization), not just over the reals, so involving complex numbers in the definition seems wrong.

[Oliver Nash]

I suspect the association of cross ratio with complex numbers arises only because $CP^1$ is a popular projective line. It should indeed be defined for four ordered points in a projective line over any field.

[Yaël Dillies]

So defining it using the biratio is too restrictive, right?

[Joseph Myers]

If you define biratio as an operation for dividing vectors in an arbitrary module, that should be fine for defining the affine space version of cross-ratio. I think lots of projective definitions / results will end up wanting both affine/Euclidean versions and general projective versions (affine/Euclidean versions, though less general and sometimes more awkward to state when they need to say e.g. "concurrent or parallel",will help for the common case of applying a projective result in the middle of a Euclidean argument; Euclidean versions of some results using a circle / sphere may also be more convenient in such cases than the ideal general versions of such results that use a conic / quadric in projective space).