From ffe70020059f75e529bdf2230a3699ed4b43e7ae Mon Sep 17 00:00:00 2001
From: laughinggas <ashvni.n@gmail.com>
Date: Thu, 19 May 2022 17:11:58 +0000
Subject: [PATCH] feat(topology/locally_constant): Characteristic functions on
 clopen sets are locally constant (#11708)

Gives an API for characteristic functions on clopen sets, `char_fn`, which are locally constant functions.



Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
---
 src/algebra/indicator_function.lean        | 13 +++++++
 src/topology/locally_constant/algebra.lean | 23 ++++++++++++
 src/topology/locally_constant/basic.lean   | 43 ++++++++++++++++++++++
 3 files changed, 79 insertions(+)

diff --git a/src/algebra/indicator_function.lean b/src/algebra/indicator_function.lean
index 2762a65b1b36b..b423494f2cdfb 100644
--- a/src/algebra/indicator_function.lean
+++ b/src/algebra/indicator_function.lean
@@ -459,6 +459,19 @@ begin
   simp [indicator_apply, ← ite_and],
 end
 
+variables (M) [nontrivial M]
+
+lemma indicator_eq_zero_iff_not_mem {U : set α} {x : α} :
+  indicator U 1 x = (0 : M) ↔ x ∉ U :=
+by { classical, simp [indicator_apply, imp_false] }
+
+lemma indicator_eq_one_iff_mem {U : set α} {x : α} :
+  indicator U 1 x = (1 : M) ↔ x ∈ U :=
+by { classical, simp [indicator_apply, imp_false] }
+
+lemma indicator_one_inj {U V : set α} (h : indicator U (1 : α → M) = indicator V 1) : U = V :=
+by { ext, simp_rw [← indicator_eq_one_iff_mem M, h] }
+
 end mul_zero_one_class
 
 section order
diff --git a/src/topology/locally_constant/algebra.lean b/src/topology/locally_constant/algebra.lean
index e811f342f3805..a0133730791e7 100644
--- a/src/topology/locally_constant/algebra.lean
+++ b/src/topology/locally_constant/algebra.lean
@@ -72,6 +72,29 @@ instance [mul_zero_class Y] : mul_zero_class (locally_constant X Y) :=
 instance [mul_zero_one_class Y] : mul_zero_one_class (locally_constant X Y) :=
 { .. locally_constant.mul_zero_class, .. locally_constant.mul_one_class }
 
+section char_fn
+
+variables (Y) [mul_zero_one_class Y] {U V : set X}
+
+/-- Characteristic functions are locally constant functions taking `x : X` to `1` if `x ∈ U`,
+  where `U` is a clopen set, and `0` otherwise. -/
+noncomputable def char_fn (hU : is_clopen U) : locally_constant X Y := indicator 1 hU
+
+lemma coe_char_fn (hU : is_clopen U) : (char_fn Y hU : X → Y) = set.indicator U 1 :=
+rfl
+
+lemma char_fn_eq_one [nontrivial Y] (x : X) (hU : is_clopen U) :
+  char_fn Y hU x = (1 : Y) ↔ x ∈ U := set.indicator_eq_one_iff_mem _
+
+lemma char_fn_eq_zero [nontrivial Y] (x : X) (hU : is_clopen U) :
+  char_fn Y hU x = (0 : Y) ↔ x ∉ U := set.indicator_eq_zero_iff_not_mem _
+
+lemma char_fn_inj [nontrivial Y] (hU : is_clopen U) (hV : is_clopen V)
+  (h : char_fn Y hU = char_fn Y hV) : U = V :=
+set.indicator_one_inj Y $ coe_inj.mpr h
+
+end char_fn
+
 @[to_additive] instance [has_div Y] : has_div (locally_constant X Y) :=
 { div := λ f g, ⟨f / g, f.is_locally_constant.div g.is_locally_constant⟩ }
 
diff --git a/src/topology/locally_constant/basic.lean b/src/topology/locally_constant/basic.lean
index 3ce3b11d4c509..061d0cad2b922 100644
--- a/src/topology/locally_constant/basic.lean
+++ b/src/topology/locally_constant/basic.lean
@@ -426,4 +426,47 @@ lemma coe_desc {X α β : Type*} [topological_space X] (f : X → α) (g : α 
 
 end desc
 
+section indicator
+variables {R : Type*} [has_one R] {U : set X} (f : locally_constant X R)
+open_locale classical
+
+/-- Given a clopen set `U` and a locally constant function `f`, `locally_constant.mul_indicator`
+  returns the locally constant function that is `f` on `U` and `1` otherwise. -/
+@[to_additive /-" Given a clopen set `U` and a locally constant function `f`,
+  `locally_constant.indicator` returns the locally constant function that is `f` on `U` and `0`
+  otherwise. "-/, simps]
+noncomputable def mul_indicator (hU : is_clopen U) :
+  locally_constant X R :=
+{ to_fun := set.mul_indicator U f,
+  is_locally_constant :=
+    begin
+      rw is_locally_constant.iff_exists_open, rintros x,
+      obtain ⟨V, hV, hx, h'⟩ := (is_locally_constant.iff_exists_open _).1 f.is_locally_constant x,
+      by_cases x ∈ U,
+      { refine ⟨U ∩ V, is_open.inter hU.1 hV, set.mem_inter h hx, _⟩, rintros y hy,
+        rw set.mem_inter_iff at hy, rw [set.mul_indicator_of_mem hy.1, set.mul_indicator_of_mem h],
+        apply h' y hy.2, },
+      { rw ←set.mem_compl_iff at h, refine ⟨Uᶜ, (is_clopen.compl hU).1, h, _⟩,
+        rintros y hy, rw set.mem_compl_iff at h, rw set.mem_compl_iff at hy,
+        simp [h, hy], },
+    end, }
+
+variables (a : X)
+
+@[to_additive]
+theorem mul_indicator_apply_eq_if (hU : is_clopen U) :
+  mul_indicator f hU a = if a ∈ U then f a else 1 :=
+set.mul_indicator_apply U f a
+
+variables {a}
+
+@[to_additive]
+theorem mul_indicator_of_mem (hU : is_clopen U) (h : a ∈ U) : f.mul_indicator hU a = f a :=
+by{ rw mul_indicator_apply, apply set.mul_indicator_of_mem h, }
+
+@[to_additive]
+theorem mul_indicator_of_not_mem (hU : is_clopen U) (h : a ∉ U) : f.mul_indicator hU a = 1 :=
+by{ rw mul_indicator_apply, apply set.mul_indicator_of_not_mem h, }
+
+end indicator
 end locally_constant