Better name for `AffineSubspace.mk'`?

Stream: mathlib4

[Jovan Gerbscheid]

I'd like it if AffineSubspace.mk' had a more descriptive name.

There are 2 main ways of making an AffineSubspace: either, given a set of points, construct the affineSpan, or, given a point p : P and a subspace direction : Submodule k V, construct the AffineSubspace.mk' p direction, which is the image of direction under fun v ↦ v +ᵥ p.

I'd suggest something like Submodule.affineTranslation, Submodule.embedAffine, Submodule.toAffine, AffineSubspace.ofSubmodule.

There is also Submodule.toAffineSubspace, which is the special case P = V and p = 0.

[Antoine Chambert-Loir]

Something in the namespace Submodule, for example Submodule.vadd, would allow to use dot notation and write write W.vadd p.

[Jovan Gerbscheid]

That seems nice.

The instance Nonempty (W.vadd p) is still missing, but with that we will get an instance for NormedAddTorsor V (W.vadd p).

[Jovan Gerbscheid]

Hmm, calling it Submodule.vadd leads to the confusing lemma name Submodule.vadd_mem_vadd (hv : v ∈ s) : v +ᵥ p ∈ s.vadd p.

What about Submodule.shifted?

Or do we follow in the footsteps of docs#Set.vsub_mem_vsub, and use the +ᵥ notation for Submodule.vadd?

[Jovan Gerbscheid]

Right, I've made a PR renaming it to Submodule.shift #23546

[Johan Commelin]

Thanks. Could you please run scripts/add_deprecations.sh?

[Yaël Dillies]

Can we completely remove it instead? I believe AffineSubspace.mk' p s = p +ᵥ s.toAffineSubspace, and both these operations feel more fundamental than AffineSubspace.mk'

[Jovan Gerbscheid]

Submodule.toAffineSubspace requires that P = V, although this could be generalized.

[Jovan Gerbscheid]

Additionally, there is no instance of HVAdd doing what you want it to do. If it were, then we could use it in the definition of AffineSubspace.Parallel:

def Parallel (s₁ s₂ : AffineSubspace k P) : Prop :=
  ∃ v : V, s₂ = s₁.map (constVAdd k P v)

[Jovan Gerbscheid]

@Yaël Dillies, the problem with that idea is that the only way to embed a linear subspace into an affice space is by providing a base point. Do you think that AffineSubspace.mk' should be called Submodule.toAffineSubspace instead?

[Yaël Dillies]

Yes, I realised that now. I agree that Submodule.toAffineSubspace would be a better name for AffineSpace.mk'. Then the current Submodule.toAffineSubspace would become Submodule.toAffineSubspace 0, which I guess is not so bad? cc @Joseph Myers

[Joseph Myers]

The name shift or notation at least has the benefit over toAffineSubspace of providing a reasonably short name for a common operation.

[Jovan Gerbscheid]

But whatever mk' gets renamed to, should we replace the current .toAffineSubspace by .mk' 0?

[Jovan Gerbscheid]

Johan Commelin said:

Thanks. Could you please run scripts/add_deprecations.sh?

Done

[Jovan Gerbscheid]

Could #23546 get another review? I'm still not 100% convinced Submodule.shift is the best name, maybe Submodule.toAffine is better?

[Jovan Gerbscheid]

I recently found that I want another funtion with a similar flavour to AffineSubspace.mk' to exist: a function lifting a ContinuousLinearMap to a ContinuousAffineMap, by providing a corresponding function on the affine spaces and showing it is compatible (i.e. map_vadd'). I think this should be named analogously to AffineSubspace.mk', so either ContinuousLinearMap.shift, or ContinuousLinearMap.toAffine. Or maybe just the name affine?