feat: port Geometry.Manifold.ContMdiffMap (#5436)

Mathlib.lean

@@ -1816,6 +1816,7 @@ import Mathlib.Geometry.Manifold.BumpFunction
 import Mathlib.Geometry.Manifold.ChartedSpace
 import Mathlib.Geometry.Manifold.ConformalGroupoid
 import Mathlib.Geometry.Manifold.ContMDiff
+import Mathlib.Geometry.Manifold.ContMDiffMap
 import Mathlib.Geometry.Manifold.Instances.Real
 import Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
 import Mathlib.Geometry.Manifold.LocalInvariantProperties

Mathlib/Geometry/Manifold/ContMDiffMap.lean

@@ -0,0 +1,139 @@
+/-
+Copyright © 2020 Nicolò Cavalleri. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nicolò Cavalleri
+
+! This file was ported from Lean 3 source module geometry.manifold.cont_mdiff_map
+! leanprover-community/mathlib commit 86c29aefdba50b3f33e86e52e3b2f51a0d8f0282
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Geometry.Manifold.ContMDiff
+import Mathlib.Topology.ContinuousFunction.Basic
+
+/-!
+# Smooth bundled map
+
+In this file we define the type `cont_mdiff_map` of `n` times continuously differentiable
+bundled maps.
+-/
+
+variable {𝕜 : Type _} [NontriviallyNormedField 𝕜] {E : Type _} [NormedAddCommGroup E]
+  [NormedSpace 𝕜 E] {E' : Type _} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type _}
+  [TopologicalSpace H] {H' : Type _} [TopologicalSpace H'] (I : ModelWithCorners 𝕜 E H)
+  (I' : ModelWithCorners 𝕜 E' H') (M : Type _) [TopologicalSpace M] [ChartedSpace H M] (M' : Type _)
+  [TopologicalSpace M'] [ChartedSpace H' M'] {E'' : Type _} [NormedAddCommGroup E'']
+  [NormedSpace 𝕜 E''] {H'' : Type _} [TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''}
+  {M'' : Type _} [TopologicalSpace M''] [ChartedSpace H'' M'']
+  -- declare a manifold `N` over the pair `(F, G)`.
+  {F : Type _}
+  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type _} [TopologicalSpace G]
+  {J : ModelWithCorners 𝕜 F G} {N : Type _} [TopologicalSpace N] [ChartedSpace G N] (n : ℕ∞)
+
+/-- Bundled `n` times continuously differentiable maps. -/
+def ContMDiffMap :=
+  { f : M → M' // ContMDiff I I' n f }
+#align cont_mdiff_map ContMDiffMap
+
+/-- Bundled smooth maps. -/
+@[reducible]
+def SmoothMap :=
+  ContMDiffMap I I' M M' ⊤
+#align smooth_map SmoothMap
+
+scoped[Manifold] notation "C^" n "⟮" I ", " M "; " I' ", " M' "⟯" => ContMDiffMap I I' M M' n
+
+scoped[Manifold]
+  notation "C^" n "⟮" I ", " M "; " k "⟯" => ContMDiffMap I (modelWithCornersSelf k k) M k n
+
+open scoped Manifold
+
+namespace ContMDiffMap
+
+variable {I} {I'} {M} {M'} {n}
+
+instance funLike : FunLike C^n⟮I, M; I', M'⟯ M fun _ => M' where
+  coe := Subtype.val
+  coe_injective' := Subtype.coe_injective
+#align cont_mdiff_map.fun_like ContMDiffMap.funLike
+
+protected theorem contMDiff (f : C^n⟮I, M; I', M'⟯) : ContMDiff I I' n f :=
+  f.prop
+#align cont_mdiff_map.cont_mdiff ContMDiffMap.contMDiff
+
+protected theorem smooth (f : C^∞⟮I, M; I', M'⟯) : Smooth I I' f :=
+  f.prop
+#align cont_mdiff_map.smooth ContMDiffMap.smooth
+
+-- porting note: use generic instance instead
+-- instance : Coe C^n⟮I, M; I', M'⟯ C(M, M') :=
+--   ⟨fun f => ⟨f, f.contMDiff.continuous⟩⟩
+
+-- attribute [to_additive_ignore_args 21] ContMDiffMap ContMDiffMap.funLike
+--   ContMDiffMap.ContinuousMap.hasCoe
+
+variable {f g : C^n⟮I, M; I', M'⟯}
+
+@[simp]
+theorem coeFn_mk (f : M → M') (hf : ContMDiff I I' n f) :
+    FunLike.coe (F := C^n⟮I, M; I', M'⟯) ⟨f, hf⟩ = f :=
+  rfl
+#align cont_mdiff_map.coe_fn_mk ContMDiffMap.coeFn_mk
+
+theorem coe_injective ⦃f g : C^n⟮I, M; I', M'⟯⦄ (h : (f : M → M') = g) : f = g :=
+  FunLike.ext' h
+#align cont_mdiff_map.coe_inj ContMDiffMap.coe_injective
+
+@[ext]
+theorem ext (h : ∀ x, f x = g x) : f = g := FunLike.ext _ _ h
+#align cont_mdiff_map.ext ContMDiffMap.ext
+
+instance : ContinuousMapClass C^n⟮I, M; I', M'⟯ M M' where
+  map_continuous f := f.contMDiff.continuous
+
+/-- The identity as a smooth map. -/
+nonrec def id : C^n⟮I, M; I, M⟯ :=
+  ⟨id, contMDiff_id⟩
+#align cont_mdiff_map.id ContMDiffMap.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''⟯ where
+  val a := f (g a)
+  property := f.contMDiff.comp g.contMDiff
+#align cont_mdiff_map.comp ContMDiffMap.comp
+
+@[simp]
+theorem 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
+#align cont_mdiff_map.comp_apply ContMDiffMap.comp_apply
+
+instance [Inhabited M'] : Inhabited C^n⟮I, M; I', M'⟯ :=
+  ⟨⟨fun _ => default, contMDiff_const⟩⟩
+
+/-- Constant map as a smooth map -/
+def const (y : M') : C^n⟮I, M; I', M'⟯ :=
+  ⟨fun _ => y, contMDiff_const⟩
+#align cont_mdiff_map.const ContMDiffMap.const
+
+/-- The first projection of a product, as a smooth map. -/
+def fst : C^n⟮I.prod I', M × M'; I, M⟯ :=
+  ⟨Prod.fst, contMDiff_fst⟩
+#align cont_mdiff_map.fst ContMDiffMap.fst
+
+/-- The second projection of a product, as a smooth map. -/
+def snd : C^n⟮I.prod I', M × M'; I', M'⟯ :=
+  ⟨Prod.snd, contMDiff_snd⟩
+#align cont_mdiff_map.snd ContMDiffMap.snd
+
+/-- Given two smooth maps `f` and `g`, this is the smooth map `x ↦ (f x, g x)`. -/
+def prodMk (f : C^n⟮J, N; I, M⟯) (g : C^n⟮J, N; I', M'⟯) : C^n⟮J, N; I.prod I', M × M'⟯ :=
+  ⟨fun x => (f x, g x), f.2.prod_mk g.2⟩
+#align cont_mdiff_map.prod_mk ContMDiffMap.prodMk
+
+end ContMDiffMap
+
+instance ContinuousLinearMap.hasCoeToContMDiffMap :
+    Coe (E →L[𝕜] E') C^n⟮𝓘(𝕜, E), E; 𝓘(𝕜, E'), E'⟯ :=
+  ⟨fun f => ⟨f, f.contMDiff⟩⟩
+#align continuous_linear_map.has_coe_to_cont_mdiff_map ContinuousLinearMap.hasCoeToContMDiffMap

Mathlib/Topology/ContinuousFunction/Basic.lean

@@ -68,10 +68,10 @@ theorem map_continuousWithinAt (f : F) (s : Set α) (a : α) : ContinuousWithinA
   (map_continuous f).continuousWithinAt
 #align map_continuous_within_at map_continuousWithinAt
 
-instance : CoeTC F C(α, β) :=
-  ⟨fun f =>
-    { toFun := f
-      continuous_toFun := map_continuous f }⟩
+/-- Coerce a bundled morphism with a `ContinuousMapClass` instance to a `ContinuousMap`. -/
+@[coe] def toContinuousMap (f : F) : C(α, β) := ⟨f, map_continuous f⟩
+
+instance : CoeTC F C(α, β) := ⟨toContinuousMap⟩
 
 end ContinuousMapClass
 
@@ -88,7 +88,6 @@ instance toContinuousMapClass : ContinuousMapClass C(α, β) α β where
   coe_injective' f g h := by cases f; cases g; congr
   map_continuous := ContinuousMap.continuous_toFun
 
-
 /- Porting note: Probably not needed anymore
 /-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
 directly. -/

Mathlib/Topology/ContinuousFunction/Ideals.lean

@@ -263,7 +263,7 @@ theorem idealOfSet_ofIdeal_eq_closure (I : Ideal C(X, 𝕜)) :
     · refine' ⟨0, _, fun x hx => False.elim hx⟩
       convert I.zero_mem
       ext
-      simp only [comp_apply, zero_apply, coe_mk, map_zero]
+      simp only [comp_apply, zero_apply, ContinuousMap.coe_coe, map_zero]
     · rintro s₁ s₂ hs ⟨g, hI, hgt⟩; exact ⟨g, hI, fun x hx => hgt x (hs hx)⟩
     · rintro s₁ s₂ ⟨g₁, hI₁, hgt₁⟩ ⟨g₂, hI₂, hgt₂⟩
       refine' ⟨g₁ + g₂, _, fun x hx => _⟩
@@ -286,7 +286,8 @@ theorem idealOfSet_ofIdeal_eq_closure (I : Ideal C(X, 𝕜)) :
             pow_pos (norm_pos_iff.mpr hx.1) 2⟩⟩
       convert I.mul_mem_left (star g) hI
       ext
-      simp only [comp_apply, coe_mk, algebraMapClm_toFun, map_pow, mul_apply, star_apply, star_def]
+      simp only [comp_apply, ContinuousMap.coe_coe, coe_mk, algebraMapClm_toFun, map_pow,
+        mul_apply, star_apply, star_def]
       simp only [normSq_eq_def', IsROrC.conj_mul, ofReal_pow]
       rfl
   /- Get the function `g'` which is guaranteed to exist above. By the extreme value theorem and
@@ -302,7 +303,7 @@ theorem idealOfSet_ofIdeal_eq_closure (I : Ideal C(X, 𝕜)) :
   refine' ⟨g * g', _, hg, hgc.mono hgc'⟩
   convert I.mul_mem_left ((algebraMapClm ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g) hI'
   ext
-  simp only [algebraMapClm_coe, comp_apply, mul_apply, coe_mk, map_mul]
+  simp only [algebraMapClm_coe, comp_apply, mul_apply, ContinuousMap.coe_coe, map_mul]
 #align continuous_map.ideal_of_set_of_ideal_eq_closure ContinuousMap.idealOfSet_ofIdeal_eq_closure
 
 theorem idealOfSet_ofIdeal_isClosed {I : Ideal C(X, 𝕜)} (hI : IsClosed (I : Set C(X, 𝕜))) :

Mathlib/Topology/ContinuousFunction/ZeroAtInfty.lean

@@ -425,7 +425,7 @@ instance (priority := 100) instBoundedContinuousMapClass : BoundedContinuousMapC
     map_bounded := fun f => ZeroAtInftyContinuousMap.bounded f }
 
 /-- Construct a bounded continuous function from a continuous function vanishing at infinity. -/
-@[simps]
+@[simps!]
 def toBcf (f : C₀(α, β)) : α →ᵇ β :=
   ⟨f, map_bounded f⟩
 #align zero_at_infty_continuous_map.to_bcf ZeroAtInftyContinuousMap.toBcf