feat: groups with zero with a smooth division away from zero (#6069)

We have currently (additive or multiplicative) Lie groups but no typeclass to express that division is smooth away from zero in fields. 
This PR adds such a typeclass, modelled on the one we already have in topological spaces.

Author: sgouezel

Mathlib/Geometry/Manifold/Algebra/LieGroup.lean

@@ -48,6 +48,7 @@ the addition and negation operations are smooth. -/
 class LieAddGroup {𝕜 : Type _} [NontriviallyNormedField 𝕜] {H : Type _} [TopologicalSpace H]
     {E : Type _} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (G : Type _)
     [AddGroup G] [TopologicalSpace G] [ChartedSpace H G] extends SmoothAdd I G : Prop where
+  /-- Negation is smooth in an additive Lie group. -/
   smooth_neg : Smooth I I fun a : G => -a
 #align lie_add_group LieAddGroup
 
@@ -58,6 +59,7 @@ the multiplication and inverse operations are smooth. -/
 class LieGroup {𝕜 : Type _} [NontriviallyNormedField 𝕜] {H : Type _} [TopologicalSpace H]
     {E : Type _} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (G : Type _)
     [Group G] [TopologicalSpace G] [ChartedSpace H G] extends SmoothMul I G : Prop where
+  /-- Inversion is smooth in a Lie group. -/
   smooth_inv : Smooth I I fun a : G => a⁻¹
 #align lie_group LieGroup
 
@@ -226,3 +228,118 @@ instance normedSpaceLieAddGroup {𝕜 : Type _} [NontriviallyNormedField 𝕜] {
     [NormedAddCommGroup E] [NormedSpace 𝕜 E] : LieAddGroup 𝓘(𝕜, E) E where
   smooth_neg := contDiff_neg.contMDiff
 #align normed_space_lie_add_group normedSpaceLieAddGroup
+
+section HasSmoothInv
+
+-- See note [Design choices about smooth algebraic structures]
+/-- A smooth manifold with `0` and `Inv` such that `fun x ↦ x⁻¹` is smooth at all nonzero points.
+Any complete normed (semi)field has this property. -/
+class SmoothInv₀ {𝕜 : Type _} [NontriviallyNormedField 𝕜] {H : Type _} [TopologicalSpace H]
+    {E : Type _} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (G : Type _)
+    [Inv G] [Zero G] [TopologicalSpace G] [ChartedSpace H G] : Prop where
+  /-- Inversion is smooth away from `0`. -/
+  smoothAt_inv₀ : ∀ ⦃x : G⦄, x ≠ 0 → SmoothAt I I (fun y ↦ y⁻¹) x
+
+instance {𝕜 : Type _} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] : SmoothInv₀ 𝓘(𝕜) 𝕜 :=
+  { smoothAt_inv₀ := by
+      intro x hx
+      change ContMDiffAt 𝓘(𝕜) 𝓘(𝕜) ⊤ Inv.inv x
+      rw [contMDiffAt_iff_contDiffAt]
+      exact contDiffAt_inv 𝕜 hx }
+
+variable {𝕜 : Type _} [NontriviallyNormedField 𝕜] {H : Type _} [TopologicalSpace H] {E : Type _}
+  [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type _}
+  [TopologicalSpace G] [ChartedSpace H G] [Inv G] [Zero G] [SmoothInv₀ I G] {E' : Type _}
+  [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type _} [TopologicalSpace H']
+  {I' : ModelWithCorners 𝕜 E' H'} {M : Type _} [TopologicalSpace M] [ChartedSpace H' M]
+  {n : ℕ∞} {f g : M → G}
+
+theorem smoothAt_inv₀ {x : G} (hx : x ≠ 0) : SmoothAt I I (fun y ↦ y⁻¹) x :=
+  SmoothInv₀.smoothAt_inv₀ hx
+
+/-- In a manifold with smooth inverse away from `0`, the inverse is continuous away from `0`.
+This is not an instance for technical reasons, see
+note [Design choices about smooth algebraic structures]. -/
+theorem hasContinuousInv₀_of_hasSmoothInv₀ : HasContinuousInv₀ G :=
+  { continuousAt_inv₀ := fun _ hx ↦ (smoothAt_inv₀ I hx).continuousAt }
+
+theorem SmoothOn_inv₀ : SmoothOn I I (Inv.inv : G → G) {0}ᶜ := fun _x hx =>
+  (smoothAt_inv₀ I hx).smoothWithinAt
+
+variable {I}
+
+theorem ContMDiffWithinAt.inv₀ (hf : ContMDiffWithinAt I' I n f s a) (ha : f a ≠ 0) :
+    ContMDiffWithinAt I' I n (fun x => (f x)⁻¹) s a :=
+  (smoothAt_inv₀ I ha).contMDiffAt.comp_contMDiffWithinAt a hf
+
+theorem ContMDiffAt.inv₀ (hf : ContMDiffAt I' I n f a) (ha : f a ≠ 0) :
+    ContMDiffAt I' I n (fun x ↦ (f x)⁻¹) a :=
+  (smoothAt_inv₀ I ha).contMDiffAt.comp a hf
+
+theorem ContMDiff.inv₀ (hf : ContMDiff I' I n f) (h0 : ∀ x, f x ≠ 0) :
+    ContMDiff I' I n (fun x ↦ (f x)⁻¹) :=
+  fun x ↦ ContMDiffAt.inv₀ (hf x) (h0 x)
+
+theorem ContMDiffOn.inv₀ (hf : ContMDiffOn I' I n f s) (h0 : ∀ x ∈ s, f x ≠ 0) :
+    ContMDiffOn I' I n (fun x => (f x)⁻¹) s :=
+  fun x hx ↦ ContMDiffWithinAt.inv₀ (hf x hx) (h0 x hx)
+
+theorem SmoothWithinAt.inv₀ (hf : SmoothWithinAt I' I f s a) (ha : f a ≠ 0) :
+    SmoothWithinAt I' I (fun x => (f x)⁻¹) s a :=
+  ContMDiffWithinAt.inv₀ hf ha
+
+theorem SmoothAt.inv₀ (hf : SmoothAt I' I f a) (ha : f a ≠ 0) :
+    SmoothAt I' I (fun x => (f x)⁻¹) a :=
+  ContMDiffAt.inv₀ hf ha
+
+theorem Smooth.inv₀ (hf : Smooth I' I f) (h0 : ∀ x, f x ≠ 0) : Smooth I' I fun x => (f x)⁻¹ :=
+  ContMDiff.inv₀ hf h0
+
+theorem SmoothOn.inv₀ (hf : SmoothOn I' I f s) (h0 : ∀ x ∈ s, f x ≠ 0) :
+    SmoothOn I' I (fun x => (f x)⁻¹) s :=
+  ContMDiffOn.inv₀ hf h0
+
+end HasSmoothInv
+
+section Div
+
+variable {𝕜 : Type _} [NontriviallyNormedField 𝕜] {H : Type _} [TopologicalSpace H] {E : Type _}
+  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type _}
+  [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [SmoothInv₀ I G] [SmoothMul I G]
+  {E' : Type _} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type _} [TopologicalSpace H']
+  {I' : ModelWithCorners 𝕜 E' H'} {M : Type _} [TopologicalSpace M] [ChartedSpace H' M]
+  {f g : M → G}
+
+theorem ContMDiffWithinAt.div₀
+    (hf : ContMDiffWithinAt I' I n f s a) (hg : ContMDiffWithinAt I' I n g s a) (h₀ : g a ≠ 0) :
+    ContMDiffWithinAt I' I n (f / g) s a := by
+  simpa [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)
+
+theorem ContMDiffOn.div₀ (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s)
+    (h₀ : ∀ x ∈ s, g x ≠ 0) : ContMDiffOn I' I n (f / g) s := by
+  simpa [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)
+
+theorem ContMDiffAt.div₀ (hf : ContMDiffAt I' I n f a) (hg : ContMDiffAt I' I n g a)
+    (h₀ : g a ≠ 0) : ContMDiffAt I' I n (f / g) a := by
+  simpa [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)
+
+theorem ContMDiff.div₀ (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) (h₀ : ∀ x, g x ≠ 0) :
+    ContMDiff I' I n (f / g) := by simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)
+
+theorem SmoothWithinAt.div₀ (hf : SmoothWithinAt I' I f s a)
+    (hg : SmoothWithinAt I' I g s a) (h₀ : g a ≠ 0) : SmoothWithinAt I' I (f / g) s a :=
+  ContMDiffWithinAt.div₀ hf hg h₀
+
+theorem SmoothOn.div₀ (hf : SmoothOn I' I f s) (hg : SmoothOn I' I g s) (h₀ : ∀ x ∈ s, g x ≠ 0) :
+    SmoothOn I' I (f / g) s :=
+  ContMDiffOn.div₀ hf hg h₀
+
+theorem SmoothAt.div₀ (hf : SmoothAt I' I f a) (hg : SmoothAt I' I g a) (h₀ : g a ≠ 0) :
+    SmoothAt I' I (f / g) a :=
+  ContMDiffAt.div₀ hf hg h₀
+
+theorem Smooth.div₀ (hf : Smooth I' I f) (hg : Smooth I' I g) (h₀ : ∀ x, g x ≠ 0) :
+    Smooth I' I (f / g) :=
+  ContMDiff.div₀ hf hg h₀
+
+end Div

Mathlib/Geometry/Manifold/Algebra/Monoid.lean

@@ -469,3 +469,53 @@ instance hasSmoothAddSelf : SmoothAdd 𝓘(𝕜, E) E :=
 #align has_smooth_add_self hasSmoothAddSelf
 
 end
+
+section DivConst
+
+variable {𝕜 : Type _} [NontriviallyNormedField 𝕜] {H : Type _} [TopologicalSpace H] {E : Type _}
+  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H}
+  {G : Type _} [DivInvMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G]
+  {E' : Type _} [NormedAddCommGroup E']
+  [NormedSpace 𝕜 E'] {H' : Type _} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
+  {M : Type _} [TopologicalSpace M] [ChartedSpace H' M]
+
+variable {f : M → G} {s : Set M} {x : M} {n : ℕ∞} (c : G)
+
+@[to_additive]
+theorem ContMDiffWithinAt.div_const (hf : ContMDiffWithinAt I' I n f s x) :
+    ContMDiffWithinAt I' I n (fun x ↦ f x / c) s x := by
+  simpa only [div_eq_mul_inv] using hf.mul contMDiffWithinAt_const
+
+@[to_additive]
+nonrec theorem ContMDiffAt.div_const (hf : ContMDiffAt I' I n f x) :
+    ContMDiffAt I' I n (fun x ↦ f x / c) x :=
+  hf.div_const c
+
+@[to_additive]
+theorem ContMDiffOn.div_const (hf : ContMDiffOn I' I n f s) :
+    ContMDiffOn I' I n (fun x ↦ f x / c) s := fun x hx => (hf x hx).div_const c
+
+@[to_additive]
+theorem ContMDiff.div_const (hf : ContMDiff I' I n f) :
+    ContMDiff I' I n (fun x ↦ f x / c) := fun x => (hf x).div_const c
+
+@[to_additive]
+nonrec theorem SmoothWithinAt.div_const (hf : SmoothWithinAt I' I f s x) :
+  SmoothWithinAt I' I (fun x ↦ f x / c) s x :=
+  hf.div_const c
+
+@[to_additive]
+nonrec theorem SmoothAt.div_const (hf : SmoothAt I' I f x) :
+    SmoothAt I' I (fun x ↦ f x / c) x :=
+  hf.div_const c
+
+@[to_additive]
+nonrec theorem SmoothOn.div_const (hf : SmoothOn I' I f s) :
+    SmoothOn I' I (fun x ↦ f x / c) s :=
+  hf.div_const c
+
+@[to_additive]
+nonrec theorem Smooth.div_const (hf : Smooth I' I f) : Smooth I' I (fun x ↦ f x / c) :=
+  hf.div_const c
+
+end DivConst

Mathlib/Geometry/Manifold/ContMDiff.lean

@@ -238,33 +238,51 @@ def Smooth (f : M → M') :=
   ContMDiff I I' ⊤ f
 #align smooth Smooth
 
-/-! ### Basic properties of smooth functions between manifolds -/
+variable {I I'}
 
+/-! ### Deducing smoothness from higher smoothness -/
 
-variable {I I'}
+theorem ContMDiffWithinAt.of_le (hf : ContMDiffWithinAt I I' n f s x) (le : m ≤ n) :
+    ContMDiffWithinAt I I' m f s x :=
+  ⟨hf.1, hf.2.of_le le⟩
+#align cont_mdiff_within_at.of_le ContMDiffWithinAt.of_le
+
+theorem ContMDiffAt.of_le (hf : ContMDiffAt I I' n f x) (le : m ≤ n) : ContMDiffAt I I' m f x :=
+  ContMDiffWithinAt.of_le hf le
+#align cont_mdiff_at.of_le ContMDiffAt.of_le
+
+theorem ContMDiffOn.of_le (hf : ContMDiffOn I I' n f s) (le : m ≤ n) : ContMDiffOn I I' m f s :=
+  fun x hx => (hf x hx).of_le le
+#align cont_mdiff_on.of_le ContMDiffOn.of_le
+
+theorem ContMDiff.of_le (hf : ContMDiff I I' n f) (le : m ≤ n) : ContMDiff I I' m f := fun x =>
+  (hf x).of_le le
+#align cont_mdiff.of_le ContMDiff.of_le
+
+/-! ### Basic properties of smooth functions between manifolds -/
 
 theorem ContMDiff.smooth (h : ContMDiff I I' ⊤ f) : Smooth I I' f :=
   h
 #align cont_mdiff.smooth ContMDiff.smooth
 
-theorem Smooth.contMDiff (h : Smooth I I' f) : ContMDiff I I' ⊤ f :=
-  h
+theorem Smooth.contMDiff (h : Smooth I I' f) : ContMDiff I I' n f :=
+  h.of_le le_top
 #align smooth.cont_mdiff Smooth.contMDiff
 
 theorem ContMDiffOn.smoothOn (h : ContMDiffOn I I' ⊤ f s) : SmoothOn I I' f s :=
   h
 #align cont_mdiff_on.smooth_on ContMDiffOn.smoothOn
 
-theorem SmoothOn.contMDiffOn (h : SmoothOn I I' f s) : ContMDiffOn I I' ⊤ f s :=
-  h
+theorem SmoothOn.contMDiffOn (h : SmoothOn I I' f s) : ContMDiffOn I I' n f s :=
+  h.of_le le_top
 #align smooth_on.cont_mdiff_on SmoothOn.contMDiffOn
 
 theorem ContMDiffAt.smoothAt (h : ContMDiffAt I I' ⊤ f x) : SmoothAt I I' f x :=
   h
 #align cont_mdiff_at.smooth_at ContMDiffAt.smoothAt
 
-theorem SmoothAt.contMDiffAt (h : SmoothAt I I' f x) : ContMDiffAt I I' ⊤ f x :=
-  h
+theorem SmoothAt.contMDiffAt (h : SmoothAt I I' f x) : ContMDiffAt I I' n f x :=
+  h.of_le le_top
 #align smooth_at.cont_mdiff_at SmoothAt.contMDiffAt
 
 theorem ContMDiffWithinAt.smoothWithinAt (h : ContMDiffWithinAt I I' ⊤ f s x) :
@@ -273,8 +291,8 @@ theorem ContMDiffWithinAt.smoothWithinAt (h : ContMDiffWithinAt I I' ⊤ f s x)
 #align cont_mdiff_within_at.smooth_within_at ContMDiffWithinAt.smoothWithinAt
 
 theorem SmoothWithinAt.contMDiffWithinAt (h : SmoothWithinAt I I' f s x) :
-    ContMDiffWithinAt I I' ⊤ f s x :=
-  h
+    ContMDiffWithinAt I I' n f s x :=
+  h.of_le le_top
 #align smooth_within_at.cont_mdiff_within_at SmoothWithinAt.contMDiffWithinAt
 
 theorem ContMDiff.contMDiffAt (h : ContMDiff I I' n f) : ContMDiffAt I I' n f x :=
@@ -629,25 +647,6 @@ theorem smooth_iff_target :
   contMDiff_iff_target
 #align smooth_iff_target smooth_iff_target
 
-/-! ### Deducing smoothness from higher smoothness -/
-
-theorem ContMDiffWithinAt.of_le (hf : ContMDiffWithinAt I I' n f s x) (le : m ≤ n) :
-    ContMDiffWithinAt I I' m f s x :=
-  ⟨hf.1, hf.2.of_le le⟩
-#align cont_mdiff_within_at.of_le ContMDiffWithinAt.of_le
-
-theorem ContMDiffAt.of_le (hf : ContMDiffAt I I' n f x) (le : m ≤ n) : ContMDiffAt I I' m f x :=
-  ContMDiffWithinAt.of_le hf le
-#align cont_mdiff_at.of_le ContMDiffAt.of_le
-
-theorem ContMDiffOn.of_le (hf : ContMDiffOn I I' n f s) (le : m ≤ n) : ContMDiffOn I I' m f s :=
-  fun x hx => (hf x hx).of_le le
-#align cont_mdiff_on.of_le ContMDiffOn.of_le
-
-theorem ContMDiff.of_le (hf : ContMDiff I I' n f) (le : m ≤ n) : ContMDiff I I' m f := fun x =>
-  (hf x).of_le le
-#align cont_mdiff.of_le ContMDiff.of_le
-
 /-! ### Deducing smoothness from smoothness one step beyond -/
 
 
@@ -2178,4 +2177,3 @@ theorem isLocalStructomorphOn_contDiffGroupoid_iff (f : LocalHomeomorph M M') :
 #align is_local_structomorph_on_cont_diff_groupoid_iff isLocalStructomorphOn_contDiffGroupoid_iff
 
 end
-