Documentation

Mathlib.Geometry.Manifold.LocalDiffeomorph

Local diffeomorphisms between manifolds #

In this file, we define C^n local diffeomorphisms between manifolds.

A C^n map f : M → N is a local diffeomorphism at x iff there are neighbourhoods s and t of x and f x, respectively such that f restricts to a diffeomorphism between s and t. f is called a local diffeomorphism on s iff it is a local diffeomorphism at every x ∈ s, and a local diffeomorphism iff it is a local diffeomorphism on univ.

Main definitions #

Main results #

TODO #

Implementation notes #

This notion of diffeomorphism is needed although there is already a notion of local structomorphism because structomorphisms do not allow the model spaces H and H' of the two manifolds to be different, i.e. for a structomorphism one has to impose H = H' which is often not the case in practice.

Tags #

local diffeomorphism, manifold

structure PartialDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 F G) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] (N : Type u_7) [TopologicalSpace N] [ChartedSpace G N] (n : ℕ∞) extends PartialEquiv :
Type (max u_6 u_7)

A partial diffeomorphism on s is a function f : M → N such that f restricts to a diffeomorphism s → t between open subsets of M and N, respectively. This is an auxiliary definition and should not be used outside of this file.

  • toFun : MN
  • invFun : NM
  • source : Set M
  • target : Set N
  • map_source' : ∀ ⦃x : M⦄, x self.sourceself.toPartialEquiv x self.target
  • map_target' : ∀ ⦃x : N⦄, x self.targetself.invFun x self.source
  • left_inv' : ∀ ⦃x : M⦄, x self.sourceself.invFun (self.toPartialEquiv x) = x
  • right_inv' : ∀ ⦃x : N⦄, x self.targetself.toPartialEquiv (self.invFun x) = x
  • open_source : IsOpen self.source
  • open_target : IsOpen self.target
  • contMDiffOn_toFun : ContMDiffOn I J n (↑self.toPartialEquiv) self.source
  • contMDiffOn_invFun : ContMDiffOn J I n self.invFun self.target
Instances For
    theorem PartialDiffeomorph.open_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (self : PartialDiffeomorph I J M N n) :
    IsOpen self.source
    theorem PartialDiffeomorph.open_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (self : PartialDiffeomorph I J M N n) :
    IsOpen self.target
    theorem PartialDiffeomorph.contMDiffOn_toFun {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (self : PartialDiffeomorph I J M N n) :
    ContMDiffOn I J n (↑self.toPartialEquiv) self.source
    theorem PartialDiffeomorph.contMDiffOn_invFun {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (self : PartialDiffeomorph I J M N n) :
    ContMDiffOn J I n self.invFun self.target
    instance instCoeFunPartialDiffeomorphForall {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 F G) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] (N : Type u_7) [TopologicalSpace N] [ChartedSpace G N] (n : ℕ∞) :
    CoeFun (PartialDiffeomorph I J M N n) fun (x : PartialDiffeomorph I J M N n) => MN

    Coercion of a PartialDiffeomorph to function. Note that a PartialDiffeomorph is not DFunLike (like PartialHomeomorph), as toFun doesn't determine invFun outside of target.

    Equations
    def Diffeomorph.toPartialDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h : Diffeomorph I J M N n) :

    A diffeomorphism is a partial diffeomorphism.

    Equations
    • h.toPartialDiffeomorph = { toPartialEquiv := h.toHomeomorph.toPartialEquiv, open_source := , open_target := , contMDiffOn_toFun := , contMDiffOn_invFun := }
    Instances For
      def PartialDiffeomorph.toPartialHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (Φ : PartialDiffeomorph I J M N n) :

      A partial diffeomorphism is also a local homeomorphism.

      Equations
      • Φ.toPartialHomeomorph = { toPartialEquiv := Φ.toPartialEquiv, open_source := , open_target := , continuousOn_toFun := , continuousOn_invFun := }
      Instances For
        def PartialDiffeomorph.symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (Φ : PartialDiffeomorph I J M N n) :

        The inverse of a local diffeomorphism.

        Equations
        • Φ.symm = { toPartialEquiv := Φ.symm, open_source := , open_target := , contMDiffOn_toFun := , contMDiffOn_invFun := }
        Instances For
          theorem PartialDiffeomorph.contMDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (Φ : PartialDiffeomorph I J M N n) :
          ContMDiffOn I J n (↑Φ.toPartialEquiv) Φ.source
          theorem PartialDiffeomorph.mdifferentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (Φ : PartialDiffeomorph I J M N n) (hn : 1 n) :
          MDifferentiableOn I J (↑Φ.toPartialEquiv) Φ.source
          theorem PartialDiffeomorph.mdifferentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (Φ : PartialDiffeomorph I J M N n) (hn : 1 n) {x : M} (hx : x Φ.source) :
          MDifferentiableAt I J (↑Φ.toPartialEquiv) x
          def IsLocalDiffeomorphAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 F G) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (n : ℕ∞) (f : MN) (x : M) :

          f : M → N is called a C^n local diffeomorphism at x iff there exist open sets U ∋ x and V ∋ f x and a diffeomorphism Φ : U → V such that f = Φ on U.

          Equations
          Instances For
            def IsLocalDiffeomorphOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 F G) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (n : ℕ∞) (f : MN) (s : Set M) :

            f : M → N is called a C^n local diffeomorphism on s iff it is a local diffeomorphism at each x : s.

            Equations
            Instances For
              def IsLocalDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 F G) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (n : ℕ∞) (f : MN) :

              f : M → N is a C^n local diffeomorphism iff it is a local diffeomorphism at each x ∈ M.

              Equations
              Instances For
                theorem isLocalDiffeomorphOn_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {f : MN} (s : Set M) :
                IsLocalDiffeomorphOn I J n f s ∀ (x : s), IsLocalDiffeomorphAt I J n f x
                theorem isLocalDiffeomorph_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {f : MN} :
                IsLocalDiffeomorph I J n f ∀ (x : M), IsLocalDiffeomorphAt I J n f x
                theorem isLocalDiffeomorph_iff_isLocalDiffeomorphOn_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {f : MN} :
                theorem IsLocalDiffeomorph.isLocalDiffeomorphOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {f : MN} (hf : IsLocalDiffeomorph I J n f) (s : Set M) :

                Basic properties of local diffeomorphisms #

                theorem IsLocalDiffeomorphAt.contMDiffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {f : MN} {x : M} (hf : IsLocalDiffeomorphAt I J n f x) :
                ContMDiffAt I J n f x

                A C^n local diffeomorphism at x is C^n differentiable at x.

                theorem IsLocalDiffeomorphAt.mdifferentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {f : MN} {x : M} (hf : IsLocalDiffeomorphAt I J n f x) (hn : 1 n) :

                A local diffeomorphism at x is differentiable at x.

                theorem IsLocalDiffeomorphOn.contMDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {f : MN} {s : Set M} (hf : IsLocalDiffeomorphOn I J n f s) :
                ContMDiffOn I J n f s

                A C^n local diffeomorphism on s is C^n on s.

                theorem IsLocalDiffeomorphOn.mdifferentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {f : MN} {s : Set M} (hf : IsLocalDiffeomorphOn I J n f s) (hn : 1 n) :

                A local diffeomorphism on s is differentiable on s.

                theorem IsLocalDiffeomorph.contMDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {f : MN} (hf : IsLocalDiffeomorph I J n f) :
                ContMDiff I J n f

                A C^n local diffeomorphism is C^n.

                theorem IsLocalDiffeomorph.mdifferentiable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {f : MN} (hf : IsLocalDiffeomorph I J n f) (hn : 1 n) :

                A C^n local diffeomorphism is differentiable.

                theorem Diffeomorph.isLocalDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (Φ : Diffeomorph I J M N n) :
                IsLocalDiffeomorph I J n Φ

                A C^n diffeomorphism is a local diffeomorphism.

                theorem IsLocalDiffeomorphOn.isLocalHomeomorphOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {f : MN} {s : Set M} (hf : IsLocalDiffeomorphOn I J n f s) :

                A local diffeomorphism on s is a local homeomorphism on s.

                theorem IsLocalDiffeomorph.isLocalHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {f : MN} (hf : IsLocalDiffeomorph I J n f) :

                A local diffeomorphism is a local homeomorphism.

                theorem IsLocalDiffeomorph.isOpenMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {f : MN} (hf : IsLocalDiffeomorph I J n f) :

                A local diffeomorphism is an open map.

                theorem IsLocalDiffeomorph.isOpen_range {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {f : MN} (hf : IsLocalDiffeomorph I J n f) :

                A local diffeomorphism has open range.

                def IsLocalDiffeomorph.image {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {f : MN} (hf : IsLocalDiffeomorph I J n f) :

                The image of a local diffeomorphism is open.

                Equations
                • hf.image = { carrier := Set.range f, is_open' := }
                Instances For
                  theorem IsLocalDiffeomorph.image_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {f : MN} (hf : IsLocalDiffeomorph I J n f) :
                  hf.image.carrier = Set.range f
                  noncomputable def IslocalDiffeomorph.diffeomorph_of_bijective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {f : MN} (hf : IsLocalDiffeomorph I J n f) (hf' : Function.Bijective f) :
                  Diffeomorph I J M N n

                  A bijective local diffeomorphism is a diffeomorphism.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For