Mathlib.Topology.Algebra.Equicontinuity

Module docstring

{"# Algebra-related equicontinuity criterions "}

equicontinuous_of_equicontinuousAt_one theorem

 {ι G M hom : Type*} [TopologicalSpace G] [UniformSpace M] [Group G] [Group M] [IsTopologicalGroup G] [IsUniformGroup M]
  [FunLike hom G M] [MonoidHomClass hom G M] (F : ι → hom) (hf : EquicontinuousAt ((↑) ∘ F) (1 : G)) :
  Equicontinuous ((↑) ∘ F)

Full source

@[to_additive]
theorem equicontinuous_of_equicontinuousAt_one {ι G M hom : Type*} [TopologicalSpace G]
    [UniformSpace M] [Group G] [Group M] [IsTopologicalGroup G] [IsUniformGroup M]
    [FunLike hom G M] [MonoidHomClass hom G M] (F : ι → hom)
    (hf : EquicontinuousAt ((↑) ∘ F) (1 : G)) :
    Equicontinuous ((↑) ∘ F) := by
  rw [equicontinuous_iff_continuous]
  rw [equicontinuousAt_iff_continuousAt] at hf
  let φ : G →* (ι →ᵤ M) :=
    { toFun := swap ((↑) ∘ F)
      map_one' := by dsimp [UniformFun]; ext; exact map_one _
      map_mul' := fun a b => by dsimp [UniformFun]; ext; exact map_mul _ _ _ }
  exact continuous_of_continuousAt_one φ hf

Equicontinuity of Homomorphism Family from Pointwise Equicontinuity at Identity

Informal description

Let $G$ be a topological group and $M$ be a uniform group. Let $\{F_i\}_{i \in \iota}$ be a family of monoid homomorphisms from $G$ to $M$. If the family $\{F_i\}_{i \in \iota}$ is equicontinuous at the identity element $1 \in G$, then it is equicontinuous on $G$.

uniformEquicontinuous_of_equicontinuousAt_one theorem

 {ι G M hom : Type*} [UniformSpace G] [UniformSpace M] [Group G] [Group M] [IsUniformGroup G] [IsUniformGroup M]
  [FunLike hom G M] [MonoidHomClass hom G M] (F : ι → hom) (hf : EquicontinuousAt ((↑) ∘ F) (1 : G)) :
  UniformEquicontinuous ((↑) ∘ F)

Full source

@[to_additive]
theorem uniformEquicontinuous_of_equicontinuousAt_one {ι G M hom : Type*} [UniformSpace G]
    [UniformSpace M] [Group G] [Group M] [IsUniformGroup G] [IsUniformGroup M]
    [FunLike hom G M] [MonoidHomClass hom G M]
    (F : ι → hom) (hf : EquicontinuousAt ((↑) ∘ F) (1 : G)) :
    UniformEquicontinuous ((↑) ∘ F) := by
  rw [uniformEquicontinuous_iff_uniformContinuous]
  rw [equicontinuousAt_iff_continuousAt] at hf
  let φ : G →* (ι →ᵤ M) :=
    { toFun := swap ((↑) ∘ F)
      map_one' := by dsimp [UniformFun]; ext; exact map_one _
      map_mul' := fun a b => by dsimp [UniformFun]; ext; exact map_mul _ _ _ }
  exact uniformContinuous_of_continuousAt_one φ hf

Uniform equicontinuity of homomorphisms from equicontinuity at identity

Informal description

Let $G$ and $M$ be groups equipped with uniform structures such that they are uniform groups, and let $\{F_i : G \to M\}_{i \in \iota}$ be a family of group homomorphisms. If the family $\{F_i\}$ is equicontinuous at the identity element $1 \in G$, then it is uniformly equicontinuous.