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

@[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.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

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

The map p' ↦ p /ₛ p' as a homeomorphism: Equiv.constSDiv as a homeomorphism

Equations

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

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

The map p' ↦ p -ᵥ p' as a homeomorphism: Equiv.constVSub as a homeomorphism

Equations

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

@[simp]

theorem Homeomorph.constSDiv_apply {V : Type u_1} {P : Type u_2} [Group V] [TopologicalSpace V] [Torsor V P] [TopologicalSpace P] [IsTopologicalTorsor P] (p x✝ : P) : (constSDiv p) x✝ = p /ₛ x✝

@[simp]

theorem Homeomorph.constVSub_symm_apply {V : Type u_1} {P : Type u_2} [AddGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] (p : P) (x✝ : V) : (constVSub p).symm x✝ = -x✝ +ᵥ p

@[simp]

theorem Homeomorph.constSDiv_symm_apply {V : Type u_1} {P : Type u_2} [Group V] [TopologicalSpace V] [Torsor V P] [TopologicalSpace P] [IsTopologicalTorsor P] (p : P) (x✝ : V) : (constSDiv p).symm x✝ = x✝⁻¹ • p

@[simp]

theorem Homeomorph.constVSub_apply {V : Type u_1} {P : Type u_2} [AddGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] (p x✝ : P) : (constVSub p) x✝ = p -ᵥ x✝

def Homeomorph.pointReflection {V : Type u_4} {P : Type u_5} [AddGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] (p : P) : P ≃ₜ P

Equiv.pointReflection as a homeomorphism

Equations

• Homeomorph.pointReflection p = (Homeomorph.constVSub p).trans (Homeomorph.vaddConst p)

@[simp]

theorem Homeomorph.coe_pointReflection {V : Type u_4} {P : Type u_5} [AddGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] (p : P) : ⇑(pointReflection p) = ⇑(Equiv.pointReflection 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)