Topological torsors of groups

This file defines topological torsors of additive and multiplicative groups, that is, torsors where +ᵥ and -ᵥ resp. • and /ₛ are continuous.

class IsTopologicalAddTorsor {V : Type u_1} [AddGroup V] [TopologicalSpace V] (P : Type u_2) [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

class IsTopologicalTorsor {V : Type u_1} [Group V] [TopologicalSpace V] (P : Type u_2) [Torsor V P] [TopologicalSpace P] extends ContinuousSMul V P : Prop

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

• continuous_smul : Continuous fun (p : V × P) => p.1 • p.2
• continuous_sdiv : Continuous fun (x : P × P) => x.1 /ₛ x.2

theorem Filter.Tendsto.sdiv {V : Type u_1} {P : Type u_2} {α : Type u_3} [Group V] [TopologicalSpace V] [Torsor V P] [TopologicalSpace P] [IsTopologicalTorsor 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 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.sdiv {V : Type u_1} {P : Type u_2} {α : Type u_3} [Group V] [TopologicalSpace V] [Torsor V P] [TopologicalSpace P] [IsTopologicalTorsor P] [TopologicalSpace α] {f g : α → P} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : α) => f x /ₛ g x

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.sdiv {V : Type u_1} {P : Type u_2} {α : Type u_3} [Group V] [TopologicalSpace V] [Torsor V P] [TopologicalSpace P] [IsTopologicalTorsor P] [TopologicalSpace α] {f g : α → P} {x : α} (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun (x : α) => f x /ₛ g x) 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.sdiv {V : Type u_1} {P : Type u_2} {α : Type u_3} [Group V] [TopologicalSpace V] [Torsor V P] [TopologicalSpace P] [IsTopologicalTorsor 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 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.sdiv {V : Type u_1} {P : Type u_2} {α : Type u_3} [Group V] [TopologicalSpace V] [Torsor V P] [TopologicalSpace P] [IsTopologicalTorsor P] [TopologicalSpace α] {f g : α → P} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun (x : α) => f x /ₛ g x) s

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 IsTopologicalTorsor.to_isTopologicalGroup (V : Type u_1) (P : Type u_2) [Group V] [TopologicalSpace V] [Torsor V P] [TopologicalSpace P] [IsTopologicalTorsor P] : IsTopologicalGroup V

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

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 additive torsor is a topological additive group. This is not an instance, as P cannot be inferred.

def Homeomorph.smulConst {V : Type u_1} {P : Type u_2} [Group V] [TopologicalSpace V] [Torsor V P] [TopologicalSpace P] [IsTopologicalTorsor P] (p : P) : V ≃ₜ P

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

Equations

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

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_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

@[simp]

theorem Homeomorph.smulConst_apply {V : Type u_1} {P : Type u_2} [Group V] [TopologicalSpace V] [Torsor V P] [TopologicalSpace P] [IsTopologicalTorsor P] (p : P) (v : V) : (smulConst p) v = v • p

@[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.smulConst_symm_apply {V : Type u_1} {P : Type u_2} [Group V] [TopologicalSpace V] [Torsor V P] [TopologicalSpace P] [IsTopologicalTorsor P] (p p' : P) : (smulConst p).symm p' = p' /ₛ p

instance instIsTopologicalTorsor {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : IsTopologicalTorsor G

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

instance instIsTopologicalTorsorProd {V : Type u_1} {W : Type u_2} {P : Type u_3} {Q : Type u_4} [CommGroup V] [TopologicalSpace V] [Torsor V P] [TopologicalSpace P] [IsTopologicalTorsor P] [CommGroup W] [TopologicalSpace W] [Torsor W Q] [TopologicalSpace Q] [IsTopologicalTorsor Q] : IsTopologicalTorsor (P × Q)

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 instIsTopologicalTorsorForall {ι : Type u_1} {V : ι → Type u_2} {P : ι → Type u_3} [(i : ι) → CommGroup (V i)] [(i : ι) → TopologicalSpace (V i)] [(i : ι) → Torsor (V i) (P i)] [(i : ι) → TopologicalSpace (P i)] [∀ (i : ι), IsTopologicalTorsor (P i)] : IsTopologicalTorsor ((i : ι) → P i)

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)