English
In a topological vector space with separating dual, the group of continuous linear automorphisms of V acts transitively on the set of nonzero vectors: for any nonzero x,y ∈ V there exists a continuous linear equivalence A: V → V with A x = y.
Русский
В топологическом векторном пространстве с разделяющим двойственным группа непрерывных линейных аутоморфизмов V действует транзитивно на множестве ненулевых векторов: для любых ненулевых x,y ∈ V существует непрерывно линейное взаимно однозначное отображение A: V → V с A x = y.
LaTeX
$$$\exists A: V \simeq_L[V] V \quad A x = y$$$
Lean4
/-- In a topological vector space with separating dual, the group of continuous linear equivalences
acts transitively on the set of nonzero vectors: given two nonzero vectors `x` and `y`, there
exists `A : V ≃L[R] V` mapping `x` to `y`. -/
theorem exists_continuousLinearEquiv_apply_eq [ContinuousSMul R V] {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
∃ A : V ≃L[R] V, A x = y :=
by
obtain ⟨G, Gx, Gy⟩ : ∃ G : StrongDual R V, G x = 1 ∧ G y ≠ 0 := exists_eq_one_ne_zero_of_ne_zero_pair hx hy
let A : V ≃L[R] V :=
{ toFun := fun z ↦ z + G z • (y - x)
invFun := fun z ↦ z + ((G y)⁻¹ * G z) • (x - y)
map_add' := fun a b ↦ by simp [add_smul]; abel
map_smul' := by simp [smul_smul]
left_inv := fun z ↦
by
simp only [RingHom.id_apply, smul_eq_mul,
-- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to change `map_smulₛₗ` into `map_smulₛₗ _`
map_add, map_smulₛₗ _, map_sub, Gx, mul_sub, mul_one, add_sub_cancel]
rw [mul_comm (G z), ← mul_assoc, inv_mul_cancel₀ Gy]
simp only [smul_sub, one_mul]
abel
right_inv := fun z ↦ by
-- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to change `map_smulₛₗ` into `map_smulₛₗ _`
simp only [map_add, map_smulₛₗ _, map_mul, map_inv₀, RingHom.id_apply, map_sub, Gx, smul_eq_mul, mul_sub,
mul_one]
rw [mul_comm _ (G y), ← mul_assoc, mul_inv_cancel₀ Gy]
simp only [smul_sub, one_mul, add_sub_cancel]
abel
continuous_toFun := continuous_id.add (G.continuous.smul continuous_const)
continuous_invFun := continuous_id.add ((continuous_const.mul G.continuous).smul continuous_const) }
exact ⟨A, show x + G x • (y - x) = y by simp [Gx]⟩
