Merge branch 'master' into feature/graph-walk-getvert-range

Author: SnirBroshi

Mathlib.lean

@@ -1679,6 +1679,7 @@ import Mathlib.Analysis.Convex.Uniform
 import Mathlib.Analysis.Convex.Visible
 import Mathlib.Analysis.Convolution
 import Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
+import Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
 import Mathlib.Analysis.Distribution.FourierSchwartz
 import Mathlib.Analysis.Distribution.SchwartzSpace
 import Mathlib.Analysis.Fourier.AddCircle
@@ -1706,6 +1707,7 @@ import Mathlib.Analysis.InnerProductSpace.Convex
 import Mathlib.Analysis.InnerProductSpace.Defs
 import Mathlib.Analysis.InnerProductSpace.Dual
 import Mathlib.Analysis.InnerProductSpace.EuclideanDist
+import Mathlib.Analysis.InnerProductSpace.GramMatrix
 import Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
 import Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
 import Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
@@ -2884,6 +2886,7 @@ import Mathlib.CategoryTheory.Triangulated.TriangleShift
 import Mathlib.CategoryTheory.Triangulated.Triangulated
 import Mathlib.CategoryTheory.Triangulated.Yoneda
 import Mathlib.CategoryTheory.Types.Basic
+import Mathlib.CategoryTheory.Types.Monomorphisms
 import Mathlib.CategoryTheory.Types.Set
 import Mathlib.CategoryTheory.UnivLE
 import Mathlib.CategoryTheory.Whiskering
@@ -5585,6 +5588,7 @@ import Mathlib.RingTheory.Grassmannian
 import Mathlib.RingTheory.HahnSeries.Addition
 import Mathlib.RingTheory.HahnSeries.Basic
 import Mathlib.RingTheory.HahnSeries.HEval
+import Mathlib.RingTheory.HahnSeries.HahnEmbedding
 import Mathlib.RingTheory.HahnSeries.Lex
 import Mathlib.RingTheory.HahnSeries.Multiplication
 import Mathlib.RingTheory.HahnSeries.PowerSeries

Mathlib/Algebra/Algebra/Equiv.lean

@@ -817,3 +817,25 @@ def ULift.algEquiv {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Alge
     ULift.{w} A ≃ₐ[R] A where
   __ := ULift.ringEquiv
   commutes' _ := rfl
+
+/-- If an `R`-algebra `A` is isomorphic to `R` as `R`-module, then the canonical map `R → A` is an
+equivalence of `R`-algebras.
+
+Note that if `e : R ≃ₗ[R] A` is the linear equivalence, then this is not the same as the equivalence
+of algebras provided here unless `e 1 = 1`. -/
+@[simps] def LinearEquiv.algEquivOfRing
+    {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A]
+    (e : R ≃ₗ[R] A) : R ≃ₐ[R] A where
+  __ := Algebra.ofId R A
+  invFun x := e.symm (e 1 * x)
+  left_inv x := calc
+    e.symm (e 1 * (algebraMap R A) x)
+      = e.symm (x • e 1) := by rw [Algebra.smul_def, mul_comm]
+    _ = x := by rw [map_smul, e.symm_apply_apply, smul_eq_mul, mul_one]
+  right_inv x := calc
+    (algebraMap R A) (e.symm (e 1 * x))
+      = (algebraMap R A) (e.symm (e 1 * x)) * e (e.symm 1 • 1) := by
+          rw [smul_eq_mul, mul_one, e.apply_symm_apply, mul_one]
+    _ = x := by rw [map_smul, Algebra.smul_def, mul_left_comm, ← Algebra.smul_def _ (e 1),
+          ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply, ← mul_assoc, ← Algebra.smul_def,
+          ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply, one_mul]

Mathlib/Algebra/Category/Ring/Instances.lean

@@ -26,8 +26,7 @@ instance localization_unit_isIso' (R : CommRingCat) :
 
 theorem IsLocalization.epi {R : Type*} [CommRing R] (M : Submonoid R) (S : Type _) [CommRing S]
     [Algebra R S] [IsLocalization M S] : Epi (CommRingCat.ofHom <| algebraMap R S) :=
-  ⟨fun {T} _ _ h => CommRingCat.hom_ext <|
-    @IsLocalization.ringHom_ext R _ M S _ _ T _ _ _ _ (congrArg CommRingCat.Hom.hom h)⟩
+  ⟨fun _ _ h => CommRingCat.hom_ext <| ringHom_ext M congr(($h).hom)⟩
 
 instance Localization.epi {R : Type*} [CommRing R] (M : Submonoid R) :
     Epi (CommRingCat.ofHom <| algebraMap R <| Localization M) :=

Mathlib/Algebra/Order/Module/HahnEmbedding.lean

@@ -28,7 +28,7 @@ under `ArchimedeanClass.closedBall K c`. The embeddings from these submodules ar
 `HahnEmbedding.Seed K M R`.
 
 By setting `K = ℚ` and `R = ℝ`, the condition can be trivially satisfied, leading
-to a proof of the classic Hahn embedding theorem. (TODO: implement this)
+to a proof of the classic Hahn embedding theorem. (See `hahnEmbedding_isOrderedAddMonoid`)
 
 ## Main theorem
 

Mathlib/AlgebraicGeometry/StructureSheaf.lean

@@ -523,14 +523,11 @@ def stalkIso (x : PrimeSpectrum.Top R) :
     rw [← this, ← hs, const_apply, localizationToStalk_mk']
     refine (structureSheaf R).presheaf.germ_ext V hxV (homOfLE hg) iVU ?_
     rw [← hs, res_const']
-  inv_hom_id := CommRingCat.hom_ext <|
-    @IsLocalization.ringHom_ext R _ x.asIdeal.primeCompl (Localization.AtPrime x.asIdeal) _ _
-      (Localization.AtPrime x.asIdeal) _ _
-      (RingHom.comp (stalkToFiberRingHom R x).hom (localizationToStalk R x).hom)
-      (RingHom.id (Localization.AtPrime _)) <| by
-        ext f
-        rw [RingHom.comp_apply, RingHom.comp_apply, localizationToStalk_of,
-          stalkToFiberRingHom_toStalk, RingHom.comp_apply, RingHom.id_apply]
+  inv_hom_id := CommRingCat.hom_ext <| IsLocalization.ringHom_ext x.asIdeal.primeCompl <| by
+    ext f
+    rw [CommRingCat.hom_comp, CommRingCat.hom_id,
+      RingHom.comp_apply, RingHom.comp_apply, localizationToStalk_of,
+      stalkToFiberRingHom_toStalk, RingHom.comp_apply, RingHom.id_apply]
 
 instance (x : PrimeSpectrum R) : IsIso (stalkToFiberRingHom R x) :=
   (stalkIso R x).isIso_hom

Mathlib/Analysis/Analytic/IsolatedZeros.lean

@@ -342,8 +342,8 @@ theorem AnalyticAt.map_nhdsNE {x : 𝕜} {f : 𝕜 → E} (hfx : AnalyticAt 𝕜
 Preimages of codiscrete sets: if `f` is analytic on a neighbourhood of `U` and not locally constant,
 then the preimage of any subset codiscrete within `f '' U` is codiscrete within `U`.
 
-See `AnalyticOnNhd.preimage_zero_codiscreteWithin` for the special case that `s` is the complement
-of zero. Applications might want to use the theorem `Filter.codiscreteWithin.mono`.
+See `AnalyticOnNhd.preimage_zero_mem_codiscreteWithin` for the special case that `s` is the
+complement of zero. Applications might want to use the theorem `Filter.codiscreteWithin.mono`.
 -/
 theorem AnalyticOnNhd.preimage_mem_codiscreteWithin {U : Set 𝕜} {s : Set E} {f : 𝕜 → E}
     (hfU : AnalyticOnNhd 𝕜 f U) (h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x))

Mathlib/Analysis/Calculus/TangentCone.lean

@@ -591,22 +591,25 @@ end Normed
 section RealNormed
 variable [NormedAddCommGroup G] [NormedSpace ℝ G]
 
-/-- In a real vector space, a convex set with nonempty interior is a set of unique
-differentiability at every point of its closure. -/
-theorem uniqueDiffWithinAt_convex {s : Set G} (conv : Convex ℝ s) (hs : (interior s).Nonempty)
-    {x : G} (hx : x ∈ closure s) : UniqueDiffWithinAt ℝ s x := by
+theorem Convex.span_tangentConeAt {s : Set G} (conv : Convex ℝ s) (hs : (interior s).Nonempty)
+    {x : G} (hx : x ∈ closure s) : Submodule.span ℝ (tangentConeAt ℝ s x) = ⊤ := by
   rcases hs with ⟨y, hy⟩
   suffices y - x ∈ interior (tangentConeAt ℝ s x) by
-    refine ⟨Dense.of_closure ?_, hx⟩
-    simp [(Submodule.span ℝ (tangentConeAt ℝ s x)).eq_top_of_nonempty_interior'
-        ⟨y - x, interior_mono Submodule.subset_span this⟩]
+    apply (Submodule.span ℝ (tangentConeAt ℝ s x)).eq_top_of_nonempty_interior'
+    exact ⟨y - x, interior_mono Submodule.subset_span this⟩
   rw [mem_interior_iff_mem_nhds]
   replace hy : interior s ∈ 𝓝 y := IsOpen.mem_nhds isOpen_interior hy
   apply mem_of_superset ((isOpenMap_sub_right x).image_mem_nhds hy)
   rintro _ ⟨z, zs, rfl⟩
   refine mem_tangentConeAt_of_openSegment_subset (Subset.trans ?_ interior_subset)
   exact conv.openSegment_closure_interior_subset_interior hx zs
 
+/-- In a real vector space, a convex set with nonempty interior is a set of unique
+differentiability at every point of its closure. -/
+theorem uniqueDiffWithinAt_convex {s : Set G} (conv : Convex ℝ s) (hs : (interior s).Nonempty)
+    {x : G} (hx : x ∈ closure s) : UniqueDiffWithinAt ℝ s x := by
+  simp [uniqueDiffWithinAt_iff, conv.span_tangentConeAt hs hx, hx]
+
 /-- In a real vector space, a convex set with nonempty interior is a set of unique
 differentiability. -/
 theorem uniqueDiffOn_convex {s : Set G} (conv : Convex ℝ s) (hs : (interior s).Nonempty) :

Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

@@ -0,0 +1,162 @@
+/-
+Copyright (c) 2023 Anatole Dedecker. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anatole Dedecker, Luigi Massacci
+-/
+
+import Mathlib.Analysis.Calculus.ContDiff.Defs
+import Mathlib.Topology.ContinuousMap.Bounded.Normed
+import Mathlib.Topology.Sets.Compacts
+
+/-!
+# Continuously differentiable functions supported in a given compact set
+
+This file develops the basic theory of bundled `n`-times continuously differentiable functions
+with support contained in a given compact set.
+
+Given `n : ℕ∞` and a compact subset `K` of a normed space `E`, we consider the type of bundled
+functions `f : E → F` (where `F` is a normed vector space) such that:
+
+- `f` is `n`-times continuously differentiable: `ContDiff ℝ n f`.
+- `f` vanishes outside of a compact set: `EqOn f 0 Kᶜ`.
+
+The main reason this exists as a bundled type is to be endowed with its natural locally convex
+topology (namely, uniform convergence of `f` and its derivative up to order `n`).
+Taking the locally convex inductive limit of these as `K` varies yields the natural topology on test
+functions, used to define distributions. While most of distribution theory cares only about `C^∞`
+functions, we also want to endow the space of `C^n` test functions with its natural topology.
+Indeed, distributions of order less than `n` are precisely those which extend continuously to this
+larger space of test functions.
+
+## Main definitions
+
+- `ContDiffMapSupportedIn E F n K`: the type of bundled `n`-times continuously differentiable
+  functions `E → F` which vanish outside of `K`.
+- `ContDiffMapSupportedIn.iteratedFDerivₗ'`: wraps `iteratedFDeriv` into a `𝕜`-linear map on
+  `ContDiffMapSupportedIn E F n K`, as a map into
+  `ContDiffMapSupportedIn E (E [×i]→L[ℝ] F) (n-i) K`.
+
+## Main statements
+
+TODO:
+- `ContDiffMapSupportedIn.instIsUniformAddGroup` and
+  `ContDiffMapSupportedIn.instLocallyConvexSpace`: `ContDiffMapSupportedIn` is a locally convex
+  topological vector space.
+
+## Notation
+
+- `𝓓^{n}_{K}(E, F)`:  the space of `n`-times continuously differentiable functions `E → F`
+  which vanish outside of `K`.
+- `𝓓_{K}(E, F)`:  the space of smooth (infinitely differentiable) functions `E → F`
+  which vanish outside of `K`, i.e. `𝓓^{⊤}_{K}(E, F)`.
+
+## Implementation details
+
+The technical choice of spelling `EqOn f 0 Kᶜ` in the definition, as opposed to `tsupport f ⊆ K`
+is to make rewriting `f x` to `0` easier when `x ∉ K`.
+
+## Tags
+
+distributions
+-/
+
+open TopologicalSpace SeminormFamily Set Function Seminorm UniformSpace
+open scoped BoundedContinuousFunction Topology NNReal
+
+variable (𝕜 E F : Type*) [NontriviallyNormedField 𝕜]
+  [NormedAddCommGroup E] [NormedSpace ℝ E]
+  [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F]
+  {n : ℕ∞} {K : Compacts E}
+
+/-- The type of bundled `n`-times continuously differentiable maps which vanish outside of a fixed
+compact set `K`. -/
+structure ContDiffMapSupportedIn (n : ℕ∞) (K : Compacts E) : Type _ where
+  /-- The underlying function. Use coercion instead. -/
+  protected toFun : E → F
+  protected contDiff' : ContDiff ℝ n toFun
+  protected zero_on_compl' : EqOn toFun 0 Kᶜ
+
+/-- Notation for the space of bundled `n`-times continuously differentiable
+functions with support in a compact set `K`. -/
+scoped[Distributions] notation "𝓓^{" n "}_{"K"}(" E ", " F ")" =>
+  ContDiffMapSupportedIn E F n K
+
+/-- Notation for the space of bundled smooth (inifinitely differentiable)
+functions with support in a compact set `K`. -/
+scoped[Distributions] notation "𝓓_{"K"}(" E ", " F ")" =>
+  ContDiffMapSupportedIn E F ⊤ K
+
+open Distributions
+
+/-- `ContDiffMapSupportedInClass B E F n K` states that `B` is a type of bundled `n`-times
+continously differentiable functions with support in the compact set `K`. -/
+class ContDiffMapSupportedInClass (B : Type*) (E F : outParam <| Type*)
+    [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F]
+    (n : outParam ℕ∞) (K : outParam <| Compacts E)
+    extends FunLike B E F where
+  map_contDiff (f : B) : ContDiff ℝ n f
+  map_zero_on_compl (f : B) : EqOn f 0 Kᶜ
+
+open ContDiffMapSupportedInClass
+
+instance (B : Type*) (E F : outParam <| Type*)
+    [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F]
+    (n : outParam ℕ∞) (K : outParam <| Compacts E)
+    [ContDiffMapSupportedInClass B E F n K] :
+    ContinuousMapClass B E F where
+  map_continuous f := (map_contDiff f).continuous
+
+instance (B : Type*) (E F : outParam <| Type*)
+    [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F]
+    (n : outParam ℕ∞) (K : outParam <| Compacts E)
+    [ContDiffMapSupportedInClass B E F n K] :
+    BoundedContinuousMapClass B E F where
+  map_bounded f := by
+    have := HasCompactSupport.intro K.isCompact (map_zero_on_compl f)
+    rcases (map_continuous f).bounded_above_of_compact_support this with ⟨C, hC⟩
+    exact map_bounded (BoundedContinuousFunction.ofNormedAddCommGroup f (map_continuous f) C hC)
+
+namespace ContDiffMapSupportedIn
+
+instance toContDiffMapSupportedInClass :
+    ContDiffMapSupportedInClass 𝓓^{n}_{K}(E, F) E F n K where
+  coe f := f.toFun
+  coe_injective' f g h := by cases f; cases g; congr
+  map_contDiff f := f.contDiff'
+  map_zero_on_compl f := f.zero_on_compl'
+
+variable {E F}
+
+protected theorem contDiff (f : 𝓓^{n}_{K}(E, F)) : ContDiff ℝ n f := map_contDiff f
+protected theorem zero_on_compl (f : 𝓓^{n}_{K}(E, F)) : EqOn f 0 Kᶜ := map_zero_on_compl f
+protected theorem compact_supp (f : 𝓓^{n}_{K}(E, F)) : HasCompactSupport f :=
+  .intro K.isCompact (map_zero_on_compl f)
+
+@[simp]
+theorem toFun_eq_coe {f : 𝓓^{n}_{K}(E, F)} : f.toFun = (f : E → F) :=
+  rfl
+
+/-- See note [custom simps projection]. -/
+def Simps.apply (f : 𝓓^{n}_{K}(E, F)) : E → F := f
+
+initialize_simps_projections ContDiffMapSupportedIn (toFun → apply)
+
+@[ext]
+theorem ext {f g : 𝓓^{n}_{K}(E, F)} (h : ∀ a, f a = g a) : f = g :=
+  DFunLike.ext _ _ h
+
+/-- Copy of a `ContDiffMapSupportedIn` with a new `toFun` equal to the old one. Useful to fix
+definitional equalities. -/
+protected def copy (f : 𝓓^{n}_{K}(E, F)) (f' : E → F) (h : f' = f) : 𝓓^{n}_{K}(E, F) where
+  toFun := f'
+  contDiff' := h.symm ▸ f.contDiff
+  zero_on_compl' := h.symm ▸ f.zero_on_compl
+
+@[simp]
+theorem coe_copy (f : 𝓓^{n}_{K}(E, F)) (f' : E → F) (h : f' = f) : ⇑(f.copy f' h) = f' :=
+  rfl
+
+theorem copy_eq (f : 𝓓^{n}_{K}(E, F)) (f' : E → F) (h : f' = f) : f.copy f' h = f :=
+  DFunLike.ext' h
+
+end ContDiffMapSupportedIn