English
A dilation-like equivalence between a normed space E and a normed torsor P, parametrized by c ∈ P with a nonzero scalar k ∈ 𝕜, is built so that x ↦ k·x +ᵥ c and its inverse x ↦ k⁻¹·(x −ᵥ c) form a continuous, bijective affine correspondence preserving the torsor structure.
Русский
Построено подобие диляции между нормированным пространством E и нормированной торсором P, параметризованное c ∈ P и ненулевым скаляром k ∈ 𝕜: x ↦ k·x +ᵥ c и его обратное x ↦ k⁻¹·(x −ᵥ c) образуют biекциясную аффинную корреспонденцию, сохраняющую структуру торсора.
LaTeX
$$$\text{smulTorsor}(c) : E \simeq_d P\quad (\text{toFun}=\lambda x. k·x+ᵥ c,\; \text{invFun}=\lambda y. k^{-1}·(y-ᵥ c))$$$
Lean4
/-- Scaling by an element `k` of the scalar ring as a `DilationEquiv` with ratio `‖k‖₊`, mapping
from a normed space to a normed torsor over that space sending `0` to `c`. -/
@[simps]
def smulTorsor (c : P) {k : 𝕜} (hk : k ≠ 0) : E ≃ᵈ P
where
toFun := (k • · +ᵥ c)
invFun := k⁻¹ • (· -ᵥ c)
left_inv x := by simp [inv_smul_smul₀ hk]
right_inv p := by simp [smul_inv_smul₀ hk]
edist_eq' :=
⟨‖k‖₊, nnnorm_ne_zero_iff.mpr hk, fun x y ↦
by
rw [show edist (k • x +ᵥ c) (k • y +ᵥ c) = _ from (IsometryEquiv.vaddConst c).isometry ..]
exact edist_smul₀ ..⟩
-- Cannot be @[simp] because `x` and `y` cannot be inferred by `simp`.
