Continuity of AffineEquiv.constVAdd

Stream: maths

[Michael Rothgang]

I'd like to construct a bi-continuous affine equivalence from constVAdd, but am stuck at proving continuity. The root cause seems to me that constVAdd is defined in terms of VAdd, whereas usual continuity statements are for standard addition. Any ideas how to bridge that gap?

MWE:

import Mathlib
theorem ContinuousAffineEquiv.foo {k P₁ V₁ : Type*} [Ring k]
    [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁]
    [TopologicalSpace P₁] [TopologicalSpace V₁] [ContinuousAdd V₁] (v : V₁) :
    Continuous (AffineEquiv.constVAdd k P₁ v).toFun := by
  -- this is the standard proof, used e.g. in `Homeomorph.add_Left v`
  have : Continuous fun x ↦ v + id x := Continuous.add (continuous_const (y := v)) continuous_id
  simp only [id] at this
  show Continuous fun x ↦ v +ᵥ x
  sorry

[Michael Rothgang]

Broader context, to un-#xy: AmpleSet.lean in sphere-eversion defines what an "ample" subset of e.g. a real vector space is. This includes two lemmas, about ample sets being invariant under ContinuousLinearEquivs and affine translations. Proving invariant under continuous affine equivalences generalises and unifies both --- this requires showing constVAdd induces a continuous affine equivalence.

[Jireh Loreaux]

Are you looking for docs#continuous_const_vadd_iff ?

[Joseph Myers]

You definitely need some hypothesis about the topology on the torsor for this to be true; the MWE above gives the torsor a completely arbitrary topology that might be unrelated to the addition operation or to the topology on the module. (A NormedAddTorsor certainly has good enough topological properties but is also stronger than needed for them.)

[Jireh Loreaux]

We have a class for exactly this: docs#ContinuousConstVAdd

[Michael Rothgang]

Thank you for the input; this was exactly what I needed!