Affine space over vector span

Stream: Is there code for X?

[Yaël Dillies]

@Joseph Myers, do we have affine_space (vector_span 𝕜 s) (affine_span 𝕜 s) anywhere? Or am I supposed to get it from an affine_span s.direction s instance for s : affine_subspace 𝕜 E? I remember seeing such an instance somewhere, but I can't find it anymore.

[Joseph Myers]

You're expected to get it from docs#affine_subspace.to_add_torsor (which is only locally an instance to avoid a loop with docs#add_torsor.nonempty), yes.

That instance loop could be avoided (and thus docs#affine_subspace.to_add_torsor made globally an instance) by allowing docs#add_torsor to be empty and putting nonempty hypotheses on those uses that require them, as previously discussed. That would be convenient for most uses, but maybe less so for your use, since you want a different instance and docs#vector_span is not defeq to the direction of the affine span.

It would probably be possible also to refactor things if desired so that docs#direction_affine_span does become true by defeq, if that's useful to make the general instance for affine subspaces give you the instance you want. I think the existing docs#vector_span definition (in relation to docs#submodule.span) is useful as a lemma, but doesn't need to be defeq, and likewise the existing definition of docs#span_points is useful as a lemma relating the affine and vector spans, but also doesn't need to be the definition of docs#affine_span by defeq (and where anything abuses that defeq, we should make sure there are affine_span equivalents of any span_points lemmas and remove the defeq abuse).