Locally constant functions on topological groups

A homomorphism from a topological group whose kernel is open is locally constant. Open kernels are preserved by taking integer multiples of additive homomorphisms.

A locally constant function f : G → A on a topological group is constant near each point, but the neighbourhood on which it is constant depends on the point. On a compact group the dependence disappears: there is a single open subgroup V with f (x * v) = f x for every x : G and every v : V. This file records that subgroup, TauCeti.rightTranslationStabilizer f, and its openness, TauCeti.isOpen_rightTranslationStabilizer.

The proof is the tube lemma. The set of pairs (x, g) with f (x * g) = f x is open, because it is the locus where two locally constant functions of (x, g) agree, and it contains G × {1}; compactness of G produces a single open V ∋ 1 that works for every x at once. Being a subgroup that is a neighbourhood of 1, the stabilizer is then open.

Compactness is the hypothesis the tube lemma consumes, and it is what turns "for each x there is a neighbourhood of 1" into "there is a neighbourhood of 1 that works for every x". Nothing weaker is claimed for the stabilizer: for a non-compact G the argument produces a neighbourhood depending on x and no uniform one, and the statements below about the stabilizer assume G compact.

Uniform local constancy is what makes the coinduced module of locally constant equivariant maps a discrete G-module, its right-translation stabilizers being open.

The tube-lemma step itself needs only a compact set K ⊆ G, not a compact group: TauCeti.exists_isOpen_forall_mem_mul_right_eq is that statement, uniform in the translated point x ∈ K, and the stabilizer's openness is its case K = G.

TauCeti.exists_isOpen_forall_mul_right_eq is the form in which a cochain construction consumes the stabilizer: a continuous family σ : P → G of right translations moves f only locally in the parameter p, uniformly in the point being translated.

theorem TauCeti.isLocallyConstant_character {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [ContinuousMul G] [AddGroup A] {χ : Additive G →+ A} (hχ : IsOpen ↑χ.ker) : IsLocallyConstant fun (g : G) => χ (Additive.ofMul g)

A character with open kernel is locally constant.

theorem TauCeti.isOpen_ker_zsmul {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [ContinuousMul G] [AddCommGroup A] {χ : Additive G →+ A} (hχ : IsOpen ↑χ.ker) (k : ℤ) : IsOpen ↑(k • χ).ker

The kernel of an integer multiple of an additive homomorphism with open kernel is open.

theorem TauCeti.exists_isOpen_forall_mem_mul_right_eq {G : Type u_1} [Mul G] [TopologicalSpace G] [ContinuousMul G] {A : Type u_2} {f : G → A} (hf : IsLocallyConstant f) {K : Set G} (hK : IsCompact K) {P : Type u_3} [TopologicalSpace P] {σ : P → G} (hσ : Continuous σ) (p₀ : P) : ∃ (V : Set P), IsOpen V ∧ p₀ ∈ V ∧ ∀ p ∈ V, ∀ x ∈ K, f (x * σ p) = f (x * σ p₀)

Uniform local constancy on a compact set, in a parameter. For a locally constant f on a space with a continuous multiplication, a compact set K and a continuous family σ : P → G of right translations, every parameter has a neighbourhood on which x ↦ f (x * σ p) does not change at all on K: the neighbourhood is uniform in x ∈ K. No compactness of G is needed, only of K, and no group structure.

def TauCeti.rightTranslationStabilizer {G : Type u_1} [Group G] {A : Type u_2} (f : G → A) : Subgroup G

The right-translation stabilizer of f : G → A: the subgroup of those g with f (x * g) = f x for every x : G. For a locally constant f on a compact group it is open (TauCeti.isOpen_rightTranslationStabilizer), which is the sense in which f is uniformly locally constant.

Equations

• TauCeti.rightTranslationStabilizer f = { carrier := {g : G | ∀ (x : G), f (x * g) = f x}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem TauCeti.mem_rightTranslationStabilizer {G : Type u_1} [Group G] {A : Type u_2} {f : G → A} {g : G} : g ∈ rightTranslationStabilizer f ↔ ∀ (x : G), f (x * g) = f x

theorem TauCeti.isOpen_rightTranslationStabilizer {G : Type u_1} [Group G] {A : Type u_2} [TopologicalSpace G] [ContinuousMul G] [CompactSpace G] {f : G → A} (hf : IsLocallyConstant f) : IsOpen ↑(rightTranslationStabilizer f)

A locally constant function on a compact topological group is uniformly locally constant: its right-translation stabilizer is an open subgroup, so a single open neighbourhood of 1 makes f (x * g) = f x hold for every x simultaneously.

theorem TauCeti.exists_isOpen_forall_mul_right_eq {G : Type u_1} [Group G] {A : Type u_2} [TopologicalSpace G] [ContinuousMul G] [CompactSpace G] {f : G → A} (hf : IsLocallyConstant f) {P : Type u_3} [TopologicalSpace P] {σ : P → G} (hσ : Continuous σ) (p₀ : P) : ∃ (V : Set P), IsOpen V ∧ p₀ ∈ V ∧ ∀ p ∈ V, ∀ (x : G), f (x * σ p) = f (x * σ p₀)

Uniform local constancy in a parameter. For a locally constant f on a compact group and a continuous family σ : P → G of right translations, every parameter has a neighbourhood on which x ↦ f (x * σ p) does not change at all: the neighbourhood is uniform in x. This is the form in which a cochain built by right-translating a locally constant function is proved locally constant in its group arguments.

theorem TauCeti.exists_isOpen_translate₂ {G : Type u_1} [Group G] {A : Type u_2} [TopologicalSpace G] [ContinuousMul G] [CompactSpace G] {N : G × G → A} (hN : IsLocallyConstant N) (g₀ : G) : ∃ (V : Set G), IsOpen V ∧ g₀ ∈ V ∧ ∀ g ∈ V, ∀ (y : G), N (y, y * g) = N (y, y * g₀)

A locally constant function N : G × G → A, evaluated along (y, y * g), is locally constant in g, uniformly in y.

theorem TauCeti.exists_isOpen_translate₃ {G : Type u_1} [Group G] {A : Type u_2} [TopologicalSpace G] [ContinuousMul G] [CompactSpace G] {Q : G × G × G → A} (hQ : IsLocallyConstant Q) (q₀ : G × G) : ∃ (V : Set (G × G)), IsOpen V ∧ q₀ ∈ V ∧ ∀ q ∈ V, ∀ (y : G), Q (y, y * q.1, y * q.1 * q.2) = Q (y, y * q₀.1, y * q₀.1 * q₀.2)

A locally constant function Q : G × G × G → A, evaluated along (y, y * g, y * g * h), is locally constant in (g, h), uniformly in y.