Topological torsors of additive groups

This file defines topological torsors of additive groups, that is, torsors where +ᵥ and -ᵥ are continuous.

class IsTopologicalAddTorsor {V : Type u_1} (P : Type u_2) [AddGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] extends ContinuousVAdd V P : Prop

A topological torsor over a topological additive group is a torsor where +ᵥ and -ᵥ are continuous.

• continuous_vadd : Continuous fun (p : V × P) => p.1 +ᵥ p.2
• continuous_vsub : Continuous fun (x : P × P) => x.1 -ᵥ x.2

theorem Filter.Tendsto.vsub {V : Type u_1} {P : Type u_2} {α : Type u_3} [AddGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] {l : Filter α} {f g : α → P} {x y : P} (hf : Tendsto f l (nhds x)) (hg : Tendsto g l (nhds y)) : Tendsto (f -ᵥ g) l (nhds (x -ᵥ y))

theorem Continuous.vsub {V : Type u_1} {P : Type u_2} {α : Type u_3} [AddGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [TopologicalSpace α] {f g : α → P} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : α) => f x -ᵥ g x

theorem ContinuousAt.vsub {V : Type u_1} {P : Type u_2} {α : Type u_3} [AddGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [TopologicalSpace α] {f g : α → P} {x : α} (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun (x : α) => f x -ᵥ g x) x

theorem ContinuousWithinAt.vsub {V : Type u_1} {P : Type u_2} {α : Type u_3} [AddGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [TopologicalSpace α] {f g : α → P} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) : ContinuousWithinAt (fun (x : α) => f x -ᵥ g x) s x

theorem ContinuousOn.vsub {V : Type u_1} {P : Type u_2} {α : Type u_3} [AddGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [TopologicalSpace α] {f g : α → P} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun (x : α) => f x -ᵥ g x) s

theorem IsTopologicalAddTorsor.to_isTopologicalAddGroup (V : Type u_1) (P : Type u_2) [AddGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] : IsTopologicalAddGroup V

The underlying group of a topological torsor is a topological group. This is not an instance, as P cannot be inferred.

def Homeomorph.vaddConst {V : Type u_1} {P : Type u_2} [AddGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] (p : P) : V ≃ₜ P

The map v ↦ v +ᵥ p as a homeomorphism between V and P.

Equations

• Homeomorph.vaddConst p = { toEquiv := Equiv.vaddConst p, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.vaddConst_symm_apply {V : Type u_1} {P : Type u_2} [AddGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] (p p' : P) : (vaddConst p).symm p' = p' -ᵥ p

@[simp]

theorem Homeomorph.vaddConst_apply {V : Type u_1} {P : Type u_2} [AddGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] (p : P) (v : V) : (vaddConst p) v = v +ᵥ p

theorem IsClosed.vadd_right_of_isCompact {V : Type u_1} {P : Type u_2} [AddGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] {s : Set V} {t : Set P} (hs : IsClosed s) (ht : IsCompact t) : IsClosed (s +ᵥ t)

instance instIsTopologicalAddTorsor {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : IsTopologicalAddTorsor G

instance instIsTopologicalAddTorsorProd {V : Type u_1} {W : Type u_2} {P : Type u_3} {Q : Type u_4} [AddCommGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [AddCommGroup W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor Q] : IsTopologicalAddTorsor (P × Q)

instance instIsTopologicalAddTorsorForall {ι : Type u_1} {V : ι → Type u_2} {P : ι → Type u_3} [(i : ι) → AddCommGroup (V i)] [(i : ι) → TopologicalSpace (V i)] [(i : ι) → AddTorsor (V i) (P i)] [(i : ι) → TopologicalSpace (P i)] [∀ (i : ι), IsTopologicalAddTorsor (P i)] : IsTopologicalAddTorsor ((i : ι) → P i)