Topology on the space of continuous affine maps

This file defines a topology on the space of continuous affine maps between topological affine spaces. This is the coarsest topology satisfying the following two properties:

• For every point p, the evaluation map fun f ↦ f p is continuous.
• The map fun f ↦ f.contLinear is continuous.

@[instance_reducible]

instance ContinuousAffineMap.instTopologicalSpace {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] : TopologicalSpace (P →ᴬ[R] Q)

Equations

• ContinuousAffineMap.instTopologicalSpace = TopologicalSpace.induced (fun (f : P →ᴬ[R] Q) => (⇑f, f.contLinear)) inferInstance

theorem ContinuousAffineMap.continuous_contLinear {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] [IsTopologicalAddGroup W] : Continuous contLinear

instance ContinuousAffineMap.instContinuousEvalConst {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] : ContinuousEvalConst (P →ᴬ[R] Q) P Q

theorem ContinuousAffineMap.continuous_rng {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] {α : Type u_6} [TopologicalSpace α] [IsTopologicalAddGroup W] {f : α → P →ᴬ[R] Q} (h₁ : ∀ (p : P), Continuous fun (x : α) => (f x) p) (h₂ : Continuous fun (x : α) => (f x).contLinear) : Continuous f

theorem ContinuousAffineMap.continuous_rng_iff {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] {α : Type u_6} [TopologicalSpace α] [IsTopologicalAddGroup W] (f : α → P →ᴬ[R] Q) : Continuous f ↔ (∀ (p : P), Continuous fun (x : α) => (f x) p) ∧ Continuous fun (x : α) => (f x).contLinear

theorem ContinuousAffineMap.continuous_rng_of_exists {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] {α : Type u_6} [TopologicalSpace α] [IsTopologicalAddGroup W] [ContinuousSMul R V] {f : α → P →ᴬ[R] Q} (h₁ : ∃ (p : P), Continuous fun (x : α) => (f x) p) (h₂ : Continuous fun (x : α) => (f x).contLinear) : Continuous f

theorem ContinuousAffineMap.continuous_const {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] : Continuous (const R P)

instance ContinuousAffineMap.instIsTopologicalAddTorsor {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] [IsTopologicalAddGroup W] : IsTopologicalAddTorsor (P →ᴬ[R] Q)

instance ContinuousAffineMap.instT0Space {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] [T0Space W] : T0Space (P →ᴬ[R] Q)

instance ContinuousAffineMap.instRegularSpace {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] : RegularSpace (P →ᴬ[R] Q)

instance ContinuousAffineMap.instIsTopologicalAddGroup {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddTorsor P] [IsTopologicalAddGroup W] : IsTopologicalAddGroup (P →ᴬ[R] W)

instance ContinuousAffineMap.instContinuousConstSMul {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddTorsor P] [IsTopologicalAddGroup W] {S : Type u_6} [Monoid S] [DistribMulAction S W] [SMulCommClass R S W] [ContinuousConstSMul S W] : ContinuousConstSMul S (P →ᴬ[R] W)

instance ContinuousAffineMap.instContinuousSMul {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddTorsor P] [IsTopologicalAddGroup W] [ContinuousSMul R W] : ContinuousSMul R (P →ᴬ[R] W)

theorem ContinuousLinearMap.continuous_toContinuousAffineMap {R : Type u_1} {V : Type u_2} {W : Type u_3} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] : Continuous toContinuousAffineMap

def ContinuousAffineMap.decompHomeomorph (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_5) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] : (V →ᴬ[R] Q) ≃ₜ Q × (V →L[R] W)

The space of continuous affine maps from a topological vector space to a topological affine space is homeomorphic to the product of the codomain with the space of continuous linear maps, by taking the value of the affine map at (0 : V) and the linear part.

Equations

• ContinuousAffineMap.decompHomeomorph R V Q = { toEquiv := ContinuousAffineMap.decompEquiv R V Q, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousAffineMap.fst_decompHomeomorph (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_5) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] (f : V →ᴬ[R] Q) : ((decompHomeomorph R V Q) f).1 = f 0

@[simp]

theorem ContinuousAffineMap.snd_decompHomeomorph (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_5) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] (f : V →ᴬ[R] Q) : ((decompHomeomorph R V Q) f).2 = f.contLinear

@[simp]

theorem ContinuousAffineMap.decompHomeomorph_symm_apply (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_5) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] (p : Q × (V →L[R] W)) (x : V) : ((decompHomeomorph R V Q).symm p) x = p.2 x +ᵥ p.1

@[simp]

theorem ContinuousAffineMap.decompHomeomorph_symm_contLinear (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_5) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] (p : Q × (V →L[R] W)) : ((decompHomeomorph R V Q).symm p).contLinear = p.2

def ContinuousAffineMap.decompContinuousLinearEquiv (R : Type u_1) (V : Type u_2) (W : Type u_3) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] : (V →ᴬ[R] W) ≃L[R] W × (V →L[R] W)

The space of continuous affine maps between topological vector spaces is isomorphic (as a topological vector space) to the product of the codomain with the space of continuous linear maps, by taking the value of the affine map at (0 : V) and the linear part.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousAffineMap.fst_decompContinuousLinearEquiv (R : Type u_1) (V : Type u_2) (W : Type u_3) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] (f : V →ᴬ[R] W) : ((decompContinuousLinearEquiv R V W) f).1 = f 0

@[simp]

theorem ContinuousAffineMap.snd_decompContinuousLinearEquiv (R : Type u_1) (V : Type u_2) (W : Type u_3) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] (f : V →ᴬ[R] W) : ((decompContinuousLinearEquiv R V W) f).2 = f.contLinear

@[simp]

theorem ContinuousAffineMap.decompContinuousLinearEquiv_symm_apply (R : Type u_1) (V : Type u_2) (W : Type u_3) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] (p : W × (V →L[R] W)) (x : V) : ((decompContinuousLinearEquiv R V W).symm p) x = p.2 x +ᵥ p.1

@[simp]

theorem ContinuousAffineMap.decompContinuousLinearEquiv_symm_contLinear (R : Type u_1) (V : Type u_2) (W : Type u_3) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] (p : W × (V →L[R] W)) : ((decompContinuousLinearEquiv R V W).symm p).contLinear = p.2

def ContinuousAffineMap.decompContinuousAffineEquiv (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_5) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] [IsTopologicalAddTorsor Q] : (V →ᴬ[R] Q) ≃ᴬ[R] Q × (V →L[R] W)

The space of continuous affine maps from a topological vector space to a topological affine space is isomorphic (as a topological affine space) to the product of the codomain with the space of continuous linear maps, by taking the value of the affine map at (0 : V) and the linear part.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousAffineMap.fst_decompContinuousAffineEquiv (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_5) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] [IsTopologicalAddTorsor Q] (f : V →ᴬ[R] Q) : ((decompContinuousAffineEquiv R V Q) f).1 = f 0

@[simp]

theorem ContinuousAffineMap.snd_decompContinuousAffineEquiv (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_5) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] [IsTopologicalAddTorsor Q] (f : V →ᴬ[R] Q) : ((decompContinuousAffineEquiv R V Q) f).2 = f.contLinear

@[simp]

theorem ContinuousAffineMap.decompContinuousAffineEquiv_symm_apply (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_5) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] [IsTopologicalAddTorsor Q] (p : Q × (V →L[R] W)) (x : V) : ((decompContinuousAffineEquiv R V Q).symm p) x = p.2 x +ᵥ p.1

@[simp]

theorem ContinuousAffineMap.decompContinuousAffineEquiv_symm_contLinear (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_5) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] [IsTopologicalAddTorsor Q] (p : Q × (V →L[R] W)) : ((decompContinuousAffineEquiv R V Q).symm p).contLinear = p.2