Continuity of maps into discrete spaces

A continuous map into a discrete space is locally constant, and this file records three consequences. Pointwise continuous families of equivalences have continuous inverse evaluation when the target space is discrete (TauCeti.continuous_equiv_symm_apply); this supplies continuity of inverse permutation evaluation in TauCeti.WreathProduct.continuous_right_inv and inverse coset translation in Subgroup.continuous_inv_smul_const. A continuous map lifts along any surjection onto a discrete space (TauCeti.exists_continuous_lift), and an injection into a discrete space reflects continuity (TauCeti.continuous_of_injective_comp); these give surjectivity and the descent of cocycle conditions for continuous cochains of discrete modules in TauCeti/RepresentationTheory/Homological/ContCohomology/ShortExact.lean.

theorem TauCeti.continuous_equiv_symm_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology β] {f : α → β ≃ β} (hf : ∀ (b : β), Continuous fun (a : α) => (f a) b) (b : β) : Continuous fun (a : α) => (f a).symm b

Inverse evaluation of a family of equivalences on a discrete space is continuous if every forward evaluation is continuous.

theorem TauCeti.exists_continuous_lift {X : Type u_1} {B : Type u_2} {C : Type u_3} [TopologicalSpace X] [TopologicalSpace B] [TopologicalSpace C] [DiscreteTopology C] {p : B → C} (hp : Function.Surjective p) {f : X → C} (hf : Continuous f) : ∃ (e : X → B), Continuous e ∧ ∀ (x : X), p (e x) = f x

A continuous map lifts along any surjection onto a discrete space. A continuous map into the discrete C is locally constant, so composing it with any set-theoretic section of p is continuous again.

theorem TauCeti.continuous_of_injective_comp {X : Type u_1} {A : Type u_2} {B : Type u_3} [TopologicalSpace X] [TopologicalSpace A] [TopologicalSpace B] [DiscreteTopology B] {f : A → B} (hf : Function.Injective f) {a : X → A} (h : Continuous fun (x : X) => f (a x)) : Continuous a

An injective map into a discrete space reflects continuity. Continuity into the discrete B is local constancy, local constancy descends along an injection, and a locally constant map is continuous.