From 86c29aefdba50b3f33e86e52e3b2f51a0d8f0282 Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Tue, 20 Jun 2023 04:52:54 +0000
Subject: [PATCH] refactor(geometry/manifold/cont_mdiff_map): redefine as
 subtype not structure (#19147)

We have a long-running conversation in mathlib about whether function spaces should be implemented as subtypes or as structures.  This PR proposes to change `cont_mdiff_map`, the type of smooth functions between manifolds `M` and `M'`, from a "structure" implementation to a "subtype" implementation.  It honestly seems pretty painless, even though this is a widely used type -- the only change for users is that the field names are now `val` and `property` rather than `to_fun` and `cont_mdiff_to_fun`.

The motivation is to make it possible to make certain constructions about function spaces generic, so that work for the space of smooth functions can be reused for (for example) the spaces of continuous or differentiable functions.

Notably, in #19146 we introduce a generic construction of a sheaf of functions on a manifold whose object over the open set `U` is the subtype of functions satisfying a "local invariant property".  With this PR, when that construction is applied to the property "smoothness", the resulting sheaf has objects which are *by definition* the types `cont_mdiff_map`.   They then inherit algebraic structures for free, see #19094.
---
 src/geometry/manifold/cont_mdiff_map.lean    | 32 ++++++++++----------
 src/geometry/manifold/derivation_bundle.lean |  4 +--
 src/geometry/manifold/whitney_embedding.lean |  4 +--
 3 files changed, 20 insertions(+), 20 deletions(-)

diff --git a/src/geometry/manifold/cont_mdiff_map.lean b/src/geometry/manifold/cont_mdiff_map.lean
index 1fce5586befc0..9b736749c8f52 100644
--- a/src/geometry/manifold/cont_mdiff_map.lean
+++ b/src/geometry/manifold/cont_mdiff_map.lean
@@ -33,10 +33,7 @@ variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
 (n : ℕ∞)
 
 /-- Bundled `n` times continuously differentiable maps. -/
-@[protect_proj]
-structure cont_mdiff_map :=
-(to_fun                  : M → M')
-(cont_mdiff_to_fun : cont_mdiff I I' n to_fun)
+def cont_mdiff_map := {f : M → M' // cont_mdiff I I' n f}
 
 /-- Bundled smooth maps. -/
 @[reducible] def smooth_map := cont_mdiff_map I I' M M' ⊤
@@ -52,24 +49,27 @@ namespace cont_mdiff_map
 
 variables {I} {I'} {M} {M'} {n}
 
-instance : has_coe_to_fun C^n⟮I, M; I', M'⟯ (λ _, M → M') := ⟨cont_mdiff_map.to_fun⟩
+instance fun_like : fun_like C^n⟮I, M; I', M'⟯ M (λ _, M') :=
+{ coe := subtype.val,
+  coe_injective' := subtype.coe_injective }
+
+protected lemma cont_mdiff (f : C^n⟮I, M; I', M'⟯) :
+  cont_mdiff I I' n f := f.prop
+
+protected lemma smooth (f : C^∞⟮I, M; I', M'⟯) :
+  smooth I I' f := f.prop
+
 instance : has_coe C^n⟮I, M; I', M'⟯ C(M, M') :=
-⟨λ f, ⟨f, f.cont_mdiff_to_fun.continuous⟩⟩
+⟨λ f, ⟨f, f.cont_mdiff.continuous⟩⟩
 
 attribute [to_additive_ignore_args 21] cont_mdiff_map
-  cont_mdiff_map.has_coe_to_fun cont_mdiff_map.continuous_map.has_coe
+  cont_mdiff_map.fun_like cont_mdiff_map.continuous_map.has_coe
 variables {f g : C^n⟮I, M; I', M'⟯}
 
 @[simp] lemma coe_fn_mk (f : M → M') (hf : cont_mdiff I I' n f) :
-  (mk f hf : M → M') = f :=
+  ((by exact subtype.mk f hf : C^n⟮I, M; I', M'⟯) : M → M') = f :=
 rfl
 
-protected lemma cont_mdiff (f : C^n⟮I, M; I', M'⟯) :
-  cont_mdiff I I' n f := f.cont_mdiff_to_fun
-
-protected lemma smooth (f : C^∞⟮I, M; I', M'⟯) :
-  smooth I I' f := f.cont_mdiff_to_fun
-
 lemma coe_inj ⦃f g : C^n⟮I, M; I', M'⟯⦄ (h : (f : M → M') = g) : f = g :=
 by cases f; cases g; cases h; refl
 
@@ -86,8 +86,8 @@ def id : C^n⟮I, M; I, M⟯ := ⟨id, cont_mdiff_id⟩
 
 /-- The composition of smooth maps, as a smooth map. -/
 def comp (f : C^n⟮I', M'; I'', M''⟯) (g : C^n⟮I, M; I', M'⟯) : C^n⟮I, M; I'', M''⟯ :=
-{ to_fun := λ a, f (g a),
-  cont_mdiff_to_fun := f.cont_mdiff_to_fun.comp g.cont_mdiff_to_fun, }
+{ val := λ a, f (g a),
+  property := f.cont_mdiff.comp g.cont_mdiff, }
 
 @[simp] lemma comp_apply (f : C^n⟮I', M'; I'', M''⟯) (g : C^n⟮I, M; I', M'⟯) (x : M) :
   f.comp g x = f (g x) := rfl
diff --git a/src/geometry/manifold/derivation_bundle.lean b/src/geometry/manifold/derivation_bundle.lean
index 7a37e9acc559b..71f103747b268 100644
--- a/src/geometry/manifold/derivation_bundle.lean
+++ b/src/geometry/manifold/derivation_bundle.lean
@@ -42,8 +42,8 @@ variables {𝕜 M}
 
 namespace pointed_smooth_map
 
-instance {x : M} : has_coe_to_fun C^∞⟮I, M; 𝕜⟯⟨x⟩ (λ _, M → 𝕜) :=
-cont_mdiff_map.has_coe_to_fun
+instance fun_like {x : M} : fun_like C^∞⟮I, M; 𝕜⟯⟨x⟩ M (λ _, 𝕜) :=
+cont_mdiff_map.fun_like
 instance {x : M} : comm_ring C^∞⟮I, M; 𝕜⟯⟨x⟩ := smooth_map.comm_ring
 instance {x : M} : algebra 𝕜 C^∞⟮I, M; 𝕜⟯⟨x⟩ := smooth_map.algebra
 instance {x : M} : inhabited C^∞⟮I, M; 𝕜⟯⟨x⟩ := ⟨0⟩
diff --git a/src/geometry/manifold/whitney_embedding.lean b/src/geometry/manifold/whitney_embedding.lean
index 02240f02a1f1a..736ba534e91f6 100644
--- a/src/geometry/manifold/whitney_embedding.lean
+++ b/src/geometry/manifold/whitney_embedding.lean
@@ -50,8 +50,8 @@ include hi
 
 /-- Smooth embedding of `M` into `(E × ℝ) ^ ι`. -/
 def embedding_pi_tangent : C^∞⟮I, M; 𝓘(ℝ, ι → (E × ℝ)), ι → (E × ℝ)⟯ :=
-{ to_fun := λ x i, (f i x • ext_chart_at I (f.c i) x, f i x),
-  cont_mdiff_to_fun := cont_mdiff_pi_space.2 $ λ i,
+{ val := λ x i, (f i x • ext_chart_at I (f.c i) x, f i x),
+  property := cont_mdiff_pi_space.2 $ λ i,
     ((f i).smooth_smul cont_mdiff_on_ext_chart_at).prod_mk_space ((f i).smooth) }
 
 local attribute [simp] lemma embedding_pi_tangent_coe :