chore(geometry/manifold/complex): extract some theory of locally cons…

…tant functions (#16019)

After #16015, I realised that we might as well deduce the rest of the lemmas in the file from the `is_locally_constant` lemma by appealing to general theory about locally constant functions.  I have added three such lemmas to the general theory of locally constant functions:
* `is_locally_constant.apply_eq_of_preconnected_space`
* `is_locally_constant.eq_const`
* `is_locally_constant.exists_eq_const`

All are direct copies of the lemmas for the bundled version (`locally_constant`).  Then I reworked the holomorphic function theory to pass through these, which cuts a few lines from the file.

src/geometry/manifold/complex.lean

@@ -44,24 +44,25 @@ namespace mdifferentiable
 variables {E : Type*} [normed_add_comm_group E] [normed_space ℂ E]
 variables {F : Type*} [normed_add_comm_group F] [normed_space ℂ F] [strict_convex_space ℝ F]
 
-variables {M : Type*} [topological_space M] [charted_space E M]
+variables {M : Type*} [topological_space M] [compact_space M] [charted_space E M]
   [smooth_manifold_with_corners 𝓘(ℂ, E) M]
 
-/-- A holomorphic function on a complex manifold is constant on every compact, preconnected, clopen
-subset. -/
-lemma apply_eq_of_is_compact {s : set M} (hs₁ : is_compact s) (hs₂ : is_preconnected s)
-  (hs₃ : is_clopen s)
-  {f : M → F} (hf : mdifferentiable 𝓘(ℂ, E) 𝓘(ℂ, F) f) {a b : M} (ha : a ∈ s) (hb : b ∈ s) :
-  f a = f b :=
+/-- A holomorphic function on a compact complex manifold is locally constant. -/
+protected lemma is_locally_constant {f : M → F} (hf : mdifferentiable 𝓘(ℂ, E) 𝓘(ℂ, F) f) :
+  is_locally_constant f :=
 begin
+  haveI : locally_connected_space M := charted_space.locally_connected_space E M,
+  apply is_locally_constant.of_constant_on_preconnected_clopens,
+  intros s hs₂ hs₃ a ha b hb,
+  have hs₁ : is_compact s := hs₃.2.is_compact,
   -- for an empty set this fact is trivial
   rcases s.eq_empty_or_nonempty with rfl | hs',
   { exact false.rec _ ha },
   -- otherwise, let `p₀` be a point where the value of `f` has maximal norm
   obtain ⟨p₀, hp₀s, hp₀⟩ := hs₁.exists_forall_ge hs' hf.continuous.norm.continuous_on,
   -- we will show `f` agrees everywhere with `f p₀`
   suffices : s ⊆ {r : M | f r = f p₀} ∩ s,
-  { exact (this ha).1.trans (this hb).1.symm }, clear ha hb a b,
+  { exact (this hb).1.trans (this ha).1.symm }, clear ha hb a b,
   refine hs₂.subset_clopen _ ⟨p₀, hp₀s, ⟨rfl, hp₀s⟩⟩,
   -- closedness of the set of points sent to `f p₀`
   refine ⟨_, (is_closed_singleton.preimage hf.continuous).inter hs₃.2⟩,
@@ -98,33 +99,17 @@ begin
   simpa [local_homeomorph.left_inv _ hq', hp, -norm_eq_abs] using hUf (chart_at E p q) hq,
 end
 
-/-- A holomorphic function on a compact complex manifold is locally constant. -/
-protected lemma is_locally_constant [compact_space M]
-  {f : M → F} (hf : mdifferentiable 𝓘(ℂ, E) 𝓘(ℂ, F) f) :
-  is_locally_constant f :=
-begin
-  haveI : locally_connected_space M := charted_space.locally_connected_space E M,
-  apply is_locally_constant.of_constant_on_preconnected_clopens,
-  intros s hs hs' x hx y hy,
-  exact hf.apply_eq_of_is_compact hs'.2.is_compact hs hs' hy hx,
-end
-
 /-- A holomorphic function on a compact connected complex manifold is constant. -/
-lemma apply_eq_of_compact_space [compact_space M] [preconnected_space M]
+lemma apply_eq_of_compact_space [preconnected_space M]
   {f : M → F} (hf : mdifferentiable 𝓘(ℂ, E) 𝓘(ℂ, F) f) (a b : M) :
   f a = f b :=
-hf.apply_eq_of_is_compact compact_univ is_preconnected_univ is_clopen_univ (set.mem_univ _)
-  (set.mem_univ _)
+hf.is_locally_constant.apply_eq_of_preconnected_space _ _
 
 /-- A holomorphic function on a compact connected complex manifold is the constant function `f ≡ v`,
 for some value `v`. -/
-lemma exists_eq_const_of_compact_space [compact_space M] [preconnected_space M]
+lemma exists_eq_const_of_compact_space [preconnected_space M]
   {f : M → F} (hf : mdifferentiable 𝓘(ℂ, E) 𝓘(ℂ, F) f) :
   ∃ v : F, f = function.const M v :=
-begin
-  casesI is_empty_or_nonempty M,
-  { exact ⟨0, funext $ λ a, h.elim a⟩ },
-  { inhabit M, exact ⟨f default, funext $ λ a, hf.apply_eq_of_compact_space a default⟩ },
-end
+hf.is_locally_constant.exists_eq_const
 
 end mdifferentiable

src/topology/locally_constant/basic.lean

@@ -141,6 +141,23 @@ begin
   { simpa only [inter_empty, not_nonempty_empty, inter_compl_self] using hs }
 end
 
+lemma apply_eq_of_preconnected_space [preconnected_space X]
+  {f : X → Y} (hf : is_locally_constant f) (x y : X) :
+  f x = f y :=
+hf.apply_eq_of_is_preconnected is_preconnected_univ trivial trivial
+
+lemma eq_const [preconnected_space X] {f : X → Y} (hf : is_locally_constant f) (x : X) :
+  f = function.const X (f x) :=
+funext $ λ y, hf.apply_eq_of_preconnected_space y x
+
+lemma exists_eq_const [preconnected_space X] [nonempty Y] {f : X → Y} (hf : is_locally_constant f) :
+  ∃ y, f = function.const X y :=
+begin
+  casesI is_empty_or_nonempty X,
+  { exact ⟨classical.arbitrary Y, funext $ h.elim⟩ },
+  { exact ⟨f (classical.arbitrary X), hf.eq_const _⟩ },
+end
+
 lemma iff_is_const [preconnected_space X] {f : X → Y} :
   is_locally_constant f ↔ ∀ x y, f x = f y :=
 ⟨λ h x y, h.apply_eq_of_is_preconnected is_preconnected_univ trivial trivial, of_constant _⟩