Algebraic facts about the topology of uniform convergence

This file contains algebraic compatibility results about the uniform structure of uniform convergence / 𝔖-convergence. They will mostly be useful for defining strong topologies on the space of continuous linear maps between two topological vector spaces.

Main statements

• UniformFun.uniform_group : if G is a uniform group, then α →ᵤ G a uniform group
• UniformOnFun.uniform_group : if G is a uniform group, then for any 𝔖 : Set (Set α), α →ᵤ[𝔖] G a uniform group.
• UniformOnFun.continuousSMul_induced_of_image_bounded : let E be a TVS, 𝔖 : Set (Set α) and H a submodule of α →ᵤ[𝔖] E. If the image of any S ∈ 𝔖 by any u ∈ H is bounded (in the sense of Bornology.IsVonNBounded), then H, equipped with the topology induced from α →ᵤ[𝔖] E, is a TVS.

Implementation notes

Like in Topology/UniformSpace/UniformConvergenceTopology, we use the type aliases UniformFun (denoted α →ᵤ β) and UniformOnFun (denoted α →ᵤ[𝔖] β) for functions from α to β endowed with the structures of uniform convergence and 𝔖-convergence.

TODO

• UniformOnFun.continuousSMul_induced_of_image_bounded unnecessarily asks for 𝔖 to be nonempty and directed. This will be easy to solve once we know that replacing 𝔖 by its noncovering bornology (i.e not what Bornology currently refers to in mathlib) doesn't change the topology.

References

• [N. Bourbaki, General Topology, Chapter X][bourbaki1966]
• [N. Bourbaki, Topological Vector Spaces][bourbaki1987]

Tags

uniform convergence, strong dual

instance instAddMonoidUniformFun {α : Type u_1} {β : Type u_2} [AddMonoid β] : AddMonoid (UniformFun α β)

Equations

• instAddMonoidUniformFun = Pi.addMonoid

instance instMonoidUniformFun {α : Type u_1} {β : Type u_2} [Monoid β] : Monoid (UniformFun α β)

Equations

• instMonoidUniformFun = Pi.monoid

instance instAddMonoidUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [AddMonoid β] : AddMonoid (UniformOnFun α β 𝔖)

Equations

• instAddMonoidUniformOnFun = Pi.addMonoid

instance instMonoidUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Monoid β] : Monoid (UniformOnFun α β 𝔖)

Equations

• instMonoidUniformOnFun = Pi.monoid

instance instAddCommMonoidUniformFun {α : Type u_1} {β : Type u_2} [AddCommMonoid β] : AddCommMonoid (UniformFun α β)

Equations

• instAddCommMonoidUniformFun = Pi.addCommMonoid

instance instCommMonoidUniformFun {α : Type u_1} {β : Type u_2} [CommMonoid β] : CommMonoid (UniformFun α β)

Equations

• instCommMonoidUniformFun = Pi.commMonoid

instance instAddCommMonoidUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [AddCommMonoid β] : AddCommMonoid (UniformOnFun α β 𝔖)

Equations

• instAddCommMonoidUniformOnFun = Pi.addCommMonoid

instance instCommMonoidUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [CommMonoid β] : CommMonoid (UniformOnFun α β 𝔖)

Equations

• instCommMonoidUniformOnFun = Pi.commMonoid

instance instAddGroupUniformFun {α : Type u_1} {β : Type u_2} [AddGroup β] : AddGroup (UniformFun α β)

Equations

• instAddGroupUniformFun = Pi.addGroup

instance instGroupUniformFun {α : Type u_1} {β : Type u_2} [Group β] : Group (UniformFun α β)

Equations

• instGroupUniformFun = Pi.group

instance instAddGroupUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [AddGroup β] : AddGroup (UniformOnFun α β 𝔖)

Equations

• instAddGroupUniformOnFun = Pi.addGroup

instance instGroupUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Group β] : Group (UniformOnFun α β 𝔖)

Equations

• instGroupUniformOnFun = Pi.group

instance instAddCommGroupUniformFun {α : Type u_1} {β : Type u_2} [AddCommGroup β] : AddCommGroup (UniformFun α β)

Equations

• instAddCommGroupUniformFun = Pi.addCommGroup

instance instCommGroupUniformFun {α : Type u_1} {β : Type u_2} [CommGroup β] : CommGroup (UniformFun α β)

Equations

• instCommGroupUniformFun = Pi.commGroup

instance instAddCommGroupUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [AddCommGroup β] : AddCommGroup (UniformOnFun α β 𝔖)

Equations

• instAddCommGroupUniformOnFun = Pi.addCommGroup

instance instCommGroupUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [CommGroup β] : CommGroup (UniformOnFun α β 𝔖)

Equations

• instCommGroupUniformOnFun = Pi.commGroup

instance instModuleUniformFunInstAddCommMonoidUniformFun {α : Type u_1} {β : Type u_2} {R : Type u_4} [Semiring R] [AddCommMonoid β] [Module R β] : Module R (UniformFun α β)

Equations

• instModuleUniformFunInstAddCommMonoidUniformFun = Pi.module α (fun a => β) R

instance instModuleUniformOnFunInstAddCommMonoidUniformOnFun {α : Type u_1} {β : Type u_2} {R : Type u_4} {𝔖 : Set (Set α)} [Semiring R] [AddCommMonoid β] [Module R β] : Module R (UniformOnFun α β 𝔖)

Equations

• instModuleUniformOnFunInstAddCommMonoidUniformOnFun = Pi.module α (fun a => β) R

@[simp]

theorem UniformFun.zero_apply {α : Type u_1} {β : Type u_2} {x : α} [AddMonoid β] : OfNat.ofNat (UniformFun α β) 0 Zero.toOfNat0 x = 0

@[simp]

theorem UniformFun.one_apply {α : Type u_1} {β : Type u_2} {x : α} [Monoid β] : OfNat.ofNat (UniformFun α β) 1 One.toOfNat1 x = 1

@[simp]

theorem UniformOnFun.zero_apply {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {x : α} [AddMonoid β] : OfNat.ofNat (UniformOnFun α β 𝔖) 0 Zero.toOfNat0 x = 0

@[simp]

theorem UniformOnFun.one_apply {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {x : α} [Monoid β] : OfNat.ofNat (UniformOnFun α β 𝔖) 1 One.toOfNat1 x = 1

@[simp]

theorem UniformFun.add_apply {α : Type u_1} {β : Type u_2} {f : UniformFun α β} {g : UniformFun α β} {x : α} [AddMonoid β] : (UniformFun α β + UniformFun α β) (UniformFun α β) instHAdd f g x = f x + g x

@[simp]

theorem UniformFun.mul_apply {α : Type u_1} {β : Type u_2} {f : UniformFun α β} {g : UniformFun α β} {x : α} [Monoid β] : (UniformFun α β * UniformFun α β) (UniformFun α β) instHMul f g x = f x * g x

@[simp]

theorem UniformOnFun.add_apply {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {f : UniformOnFun α β 𝔖} {g : UniformOnFun α β 𝔖} {x : α} [AddMonoid β] : (UniformOnFun α β 𝔖 + UniformOnFun α β 𝔖) (UniformOnFun α β 𝔖) instHAdd f g x = f x + g x

@[simp]

theorem UniformOnFun.mul_apply {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {f : UniformOnFun α β 𝔖} {g : UniformOnFun α β 𝔖} {x : α} [Monoid β] : (UniformOnFun α β 𝔖 * UniformOnFun α β 𝔖) (UniformOnFun α β 𝔖) instHMul f g x = f x * g x

@[simp]

theorem UniformFun.neg_apply {α : Type u_1} {β : Type u_2} {f : UniformFun α β} {x : α} [AddGroup β] : (-UniformFun α β) NegZeroClass.toNeg f x = -f x

@[simp]

theorem UniformFun.inv_apply {α : Type u_1} {β : Type u_2} {f : UniformFun α β} {x : α} [Group β] : (UniformFun α β)⁻¹ InvOneClass.toInv f x = (f x)⁻¹

@[simp]

theorem UniformOnFun.neg_apply {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {f : UniformOnFun α β 𝔖} {x : α} [AddGroup β] : (-UniformOnFun α β 𝔖) NegZeroClass.toNeg f x = -f x

@[simp]

theorem UniformOnFun.inv_apply {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {f : UniformOnFun α β 𝔖} {x : α} [Group β] : (UniformOnFun α β 𝔖)⁻¹ InvOneClass.toInv f x = (f x)⁻¹

@[simp]

theorem UniformFun.sub_apply {α : Type u_1} {β : Type u_2} {f : UniformFun α β} {g : UniformFun α β} {x : α} [AddGroup β] : (UniformFun α β - UniformFun α β) (UniformFun α β) instHSub f g x = f x - g x

@[simp]

theorem UniformFun.div_apply {α : Type u_1} {β : Type u_2} {f : UniformFun α β} {g : UniformFun α β} {x : α} [Group β] : (UniformFun α β / UniformFun α β) (UniformFun α β) instHDiv f g x = f x / g x

@[simp]

theorem UniformOnFun.sub_apply {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {f : UniformOnFun α β 𝔖} {g : UniformOnFun α β 𝔖} {x : α} [AddGroup β] : (UniformOnFun α β 𝔖 - UniformOnFun α β 𝔖) (UniformOnFun α β 𝔖) instHSub f g x = f x - g x

@[simp]

theorem UniformOnFun.div_apply {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {f : UniformOnFun α β 𝔖} {g : UniformOnFun α β 𝔖} {x : α} [Group β] : (UniformOnFun α β 𝔖 / UniformOnFun α β 𝔖) (UniformOnFun α β 𝔖) instHDiv f g x = f x / g x

theorem instUniformAddGroupUniformFunUniformSpaceInstAddGroupUniformFun.proof_1 {α : Type u_1} {G : Type u_2} [AddGroup G] [UniformSpace G] [UniformAddGroup G] : UniformAddGroup (UniformFun α G)

instance instUniformAddGroupUniformFunUniformSpaceInstAddGroupUniformFun {α : Type u_1} {G : Type u_2} [AddGroup G] [UniformSpace G] [UniformAddGroup G] : UniformAddGroup (UniformFun α G)

If G is a uniform additive group, then α →ᵤ G is a uniform additive group as well.

Equations

• @instUniformAddGroupUniformFunUniformSpaceInstAddGroupUniformFun = @instUniformAddGroupUniformFunUniformSpaceInstAddGroupUniformFun.proof_1

instance instUniformGroupUniformFunUniformSpaceInstGroupUniformFun {α : Type u_1} {G : Type u_2} [Group G] [UniformSpace G] [UniformGroup G] : UniformGroup (UniformFun α G)

If G is a uniform group, then α →ᵤ G is a uniform group as well.

Equations

• @instUniformGroupUniformFunUniformSpaceInstGroupUniformFun = @instUniformGroupUniformFunUniformSpaceInstGroupUniformFun.proof_1

theorem UniformFun.hasBasis_nhds_zero_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [AddGroup G] [UniformSpace G] [UniformAddGroup G] {p : ι → Prop} {b : ι → Set G} (h : Filter.HasBasis (nhds 0) p b) : Filter.HasBasis (nhds 0) p fun i => {f | ∀ (x : α), f x ∈ b i}

theorem UniformFun.hasBasis_nhds_one_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [Group G] [UniformSpace G] [UniformGroup G] {p : ι → Prop} {b : ι → Set G} (h : Filter.HasBasis (nhds 1) p b) : Filter.HasBasis (nhds 1) p fun i => {f | ∀ (x : α), f x ∈ b i}

theorem UniformFun.hasBasis_nhds_zero {α : Type u_1} {G : Type u_2} [AddGroup G] [UniformSpace G] [UniformAddGroup G] : Filter.HasBasis (nhds 0) (fun V => V ∈ nhds 0) fun V => {f | ∀ (x : α), f x ∈ V}

theorem UniformFun.hasBasis_nhds_one {α : Type u_1} {G : Type u_2} [Group G] [UniformSpace G] [UniformGroup G] : Filter.HasBasis (nhds 1) (fun V => V ∈ nhds 1) fun V => {f | ∀ (x : α), f x ∈ V}

theorem instUniformAddGroupUniformOnFunUniformSpaceInstAddGroupUniformOnFun.proof_1 {α : Type u_1} {G : Type u_2} [AddGroup G] {𝔖 : Set (Set α)} [UniformSpace G] [UniformAddGroup G] : UniformAddGroup (UniformOnFun α G 𝔖)

instance instUniformAddGroupUniformOnFunUniformSpaceInstAddGroupUniformOnFun {α : Type u_1} {G : Type u_2} [AddGroup G] {𝔖 : Set (Set α)} [UniformSpace G] [UniformAddGroup G] : UniformAddGroup (UniformOnFun α G 𝔖)

Let 𝔖 : Set (Set α). If G is a uniform additive group, then α →ᵤ[𝔖] G is a uniform additive group as well.

Equations

• @instUniformAddGroupUniformOnFunUniformSpaceInstAddGroupUniformOnFun = @instUniformAddGroupUniformOnFunUniformSpaceInstAddGroupUniformOnFun.proof_1

instance instUniformGroupUniformOnFunUniformSpaceInstGroupUniformOnFun {α : Type u_1} {G : Type u_2} [Group G] {𝔖 : Set (Set α)} [UniformSpace G] [UniformGroup G] : UniformGroup (UniformOnFun α G 𝔖)

Let 𝔖 : Set (Set α). If G is a uniform group, then α →ᵤ[𝔖] G is a uniform group as well.

Equations

• @instUniformGroupUniformOnFunUniformSpaceInstGroupUniformOnFun = @instUniformGroupUniformOnFunUniformSpaceInstGroupUniformOnFun.proof_1

theorem UniformOnFun.hasBasis_nhds_zero_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [AddGroup G] [UniformSpace G] [UniformAddGroup G] (𝔖 : Set (Set α)) (h𝔖₁ : Set.Nonempty 𝔖) (h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖) {p : ι → Prop} {b : ι → Set G} (h : Filter.HasBasis (nhds 0) p b) : Filter.HasBasis (nhds 0) (fun Si => Si.fst ∈ 𝔖 ∧ p Si.snd) fun Si => {f | ∀ (x : α), x ∈ Si.fst → f x ∈ b Si.snd}

theorem UniformOnFun.hasBasis_nhds_one_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [Group G] [UniformSpace G] [UniformGroup G] (𝔖 : Set (Set α)) (h𝔖₁ : Set.Nonempty 𝔖) (h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖) {p : ι → Prop} {b : ι → Set G} (h : Filter.HasBasis (nhds 1) p b) : Filter.HasBasis (nhds 1) (fun Si => Si.fst ∈ 𝔖 ∧ p Si.snd) fun Si => {f | ∀ (x : α), x ∈ Si.fst → f x ∈ b Si.snd}

theorem UniformOnFun.hasBasis_nhds_zero {α : Type u_1} {G : Type u_2} [AddGroup G] [UniformSpace G] [UniformAddGroup G] (𝔖 : Set (Set α)) (h𝔖₁ : Set.Nonempty 𝔖) (h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖) : Filter.HasBasis (nhds 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ nhds 0) fun SV => {f | ∀ (x : α), x ∈ SV.fst → f x ∈ SV.snd}

theorem UniformOnFun.hasBasis_nhds_one {α : Type u_1} {G : Type u_2} [Group G] [UniformSpace G] [UniformGroup G] (𝔖 : Set (Set α)) (h𝔖₁ : Set.Nonempty 𝔖) (h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖) : Filter.HasBasis (nhds 1) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ nhds 1) fun SV => {f | ∀ (x : α), x ∈ SV.fst → f x ∈ SV.snd}

theorem UniformOnFun.continuousSMul_induced_of_image_bounded (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) (H : Type u_4) {hom : Type u_5} [NormedField 𝕜] [AddCommGroup H] [Module 𝕜 H] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace H] [UniformSpace E] [UniformAddGroup E] [ContinuousSMul 𝕜 E] {𝔖 : Set (Set α)} [LinearMapClass hom 𝕜 H (UniformOnFun α E 𝔖)] (h𝔖₁ : Set.Nonempty 𝔖) (h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖) (φ : hom) (hφ : Inducing ↑φ) (h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)) : ContinuousSMul 𝕜 H

Let E be a TVS, 𝔖 : Set (Set α) and H a submodule of α →ᵤ[𝔖] E. If the image of any S ∈ 𝔖 by any u ∈ H is bounded (in the sense of Bornology.IsVonNBounded), then H, equipped with the topology of 𝔖-convergence, is a TVS.

For convenience, we don't literally ask for H : Submodule (α →ᵤ[𝔖] E). Instead, we prove the result for any vector space H equipped with a linear inducing to α →ᵤ[𝔖] E, which is often easier to use. We also state the Submodule version as UniformOnFun.continuousSMul_submodule_of_image_bounded.

theorem UniformOnFun.continuousSMul_submodule_of_image_bounded (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [UniformSpace E] [UniformAddGroup E] [ContinuousSMul 𝕜 E] {𝔖 : Set (Set α)} (h𝔖₁ : Set.Nonempty 𝔖) (h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖) (H : Submodule 𝕜 (UniformOnFun α E 𝔖)) (h : ∀ (u : UniformOnFun α E 𝔖), u ∈ H → ∀ (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (u '' s)) : ContinuousSMul 𝕜 { x // x ∈ H }

Let E be a TVS, 𝔖 : Set (Set α) and H a submodule of α →ᵤ[𝔖] E. If the image of any S ∈ 𝔖 by any u ∈ H is bounded (in the sense of Bornology.IsVonNBounded), then H, equipped with the topology of 𝔖-convergence, is a TVS.

If you have a hard time using this lemma, try the one above instead.