Smooth or analytic manifold… to Sphere

ClassSmooth or analytic manifold (with boundary and corners)#

Typeclass defining manifolds with respect to a model with corners, over a field 𝕜. This definition includes the model with corners I (which might allow boundary, corners, or not, so this class covers both manifolds with boundary and manifolds without boundary), and a smoothness parameter n : ℕ∞ω (where n = 0 means topological manifold, n = ∞ means smooth manifold and n = ω means analytic manifold).

IsManifold.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (M : Type u_4) [TopologicalSpace M]
  [ChartedSpace H M] : Prop

Sources

• Mathlib documentation: IsManifold
• Source of IsManifold in Mathlib/Geometry/Manifold/IsManifold/Basic.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibIsManifold

Uses 7 · Used by 11

Statement usesAssociative algebra over a commutative ring · Completeness · Convex subsets · Homeomorphisms · Infinite sum · Norm of a continuous linear map · Radius of convergence

Used byDisjoint union of manifolds · Jacobi/Leibniz identity · Lie group · Local existence of integral curves · Product of manifolds · Sphere · Uniform time existence · Uniqueness of integral curves · Closed interval · Discrete spaces are 0-manifolds · Whitney embedding theorem

DefinitionSmooth map between manifolds#

ContMDiff I I' n f indicates that the function f : M → M' between manifolds is n times continuously differentiable.

f is n times continuously differentiable if it is continuous and, for any pair of points, it is n times continuously differentiable in the charts around these points. The parameter n belongs to ℕ∞ω (accessible in the ContDiff scope), i.e. it can be a natural number, ∞, or ω, where C^ω corresponds to analytic functions.

ContMDiff.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M]
  {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H']
  (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M']
  (n : WithTop ℕ∞) (f : M → M') : Prop

Sources

• Mathlib documentation: ContMDiff
• Source of ContMDiff in Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibContMDiff

Uses 6 · Used by 9

Statement usesAssociative algebra over a commutative ring · Completeness · Convex subsets · Infinite sum · Norm of a continuous linear map · Radius of convergence

Used byJacobi/Leibniz identity · Lie group · Uniform time existence · Uniqueness of integral curves · Riemannian manifold · Smooth bundle metric · (smooth) pullback vector bundle · (smooth) trivial vector bundle · Whitney embedding theorem

DefinitionSmooth immersion#

f : M → N is a C^n immersion if around each point x ∈ M, there are charts φ and ψ of M and N around x and f x, respectively such that in these charts, f looks like u ↦ (u, 0).

Implicit in this definition is an abstract choice F of a complement of E in E': being an immersion includes a choice of linear isomorphism between E × F and E', which is where the choice of F enters. If you need stronger control over the complement F, use IsImmersionOfComplement instead.

Note that our global choice of complement is a bit stronger than asking f to be an immersion at each x ∈ M w.r.t. potentially varying complements: see isImmersionAt for details.

Manifold.IsImmersion.{u, u_1, u_2, u_7, u_9, u_11, u_13} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {E : Type u_2} {E'' : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'']
  [NormedSpace 𝕜 E''] {H : Type u_7} [TopologicalSpace H] {G : Type u_9} [TopologicalSpace G]
  (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 E'' G) {M : Type u_11} [TopologicalSpace M]
  [ChartedSpace H M] {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] (n : WithTop ℕ∞)
  (f : M → N) : Prop

Sources

• Mathlib documentation: Manifold.IsImmersion
• Source of Manifold.IsImmersion in Mathlib/Geometry/Manifold/Immersion.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibManifold.IsImmersion

Uses 8 · Used by 1

Statement usesAssociative algebra over a commutative ring · Completeness · Convex subsets · Homeomorphisms · Infinite sum · Norm of a continuous linear map · Product of vector spaces · Radius of convergence

Used bySmooth embedding

StructureSmooth embedding#

A C^n map f : M → M' is a smooth C^n embedding if it is a topological embedding and a C^n immersion.

Manifold.IsSmoothEmbedding.{u_1, u_2, u_4, u_6, u_8, u_10, u_12} {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜] {E₁ : Type u_2} {E₃ : Type u_4} [NormedAddCommGroup E₁]
  [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₃] [NormedSpace 𝕜 E₃] {H : Type u_6} {G : Type u_8}
  [TopologicalSpace H] [TopologicalSpace G] (I : ModelWithCorners 𝕜 E₁ H)
  (J : ModelWithCorners 𝕜 E₃ G) {M : Type u_10} {N : Type u_12} [TopologicalSpace M]
  [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] (n : WithTop ℕ∞) (f : M → N) : Prop

Sources

• Mathlib documentation: Manifold.IsSmoothEmbedding
• Source of Manifold.IsSmoothEmbedding in Mathlib/Geometry/Manifold/SmoothEmbedding.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibManifold.IsSmoothEmbedding

Uses 2

Statement usesInduced topology · Smooth immersion

TheoremProduct of manifolds#

The product of two C^n manifolds is naturally a C^n manifold.

IsManifold.prod.{u_5, u_6, u_7, u_8, u_9, u_10, u_11} {n : WithTop ℕ∞} {𝕜 : Type u_5}
  [NontriviallyNormedField 𝕜] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_8} [TopologicalSpace H]
  {I : ModelWithCorners 𝕜 E H} {H' : Type u_9} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  (M : Type u_10) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I n M] (M' : Type u_11)
  [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' n M'] :
  IsManifold (I.prod I') n (M × M')

Sources

• Mathlib documentation: IsManifold.prod
• Source of IsManifold.prod in Mathlib/Geometry/Manifold/IsManifold/Basic.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibIsManifold.prod

Uses 2

Statement usesSmooth or analytic manifold (with boundary and corners)

Proof uses\(C^k\) function

TheoremDisjoint union of manifolds#

The disjoint union of two C^n manifolds modelled on (E, H) is a C^n manifold modelled on (E, H).

IsManifold.disjointUnion.{u_1, u_2, u_3, u_4, u_5} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H]
  {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M]
  [ChartedSpace H M] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M']
  [hM : IsManifold I n M] [hM' : IsManifold I n M'] : IsManifold I n (M ⊕ M')

Sources

• Mathlib documentation: IsManifold.disjointUnion
• Source of IsManifold.disjointUnion in Mathlib/Geometry/Manifold/IsManifold/Basic.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibIsManifold.disjointUnion

Uses 2

Statement usesSmooth or analytic manifold (with boundary and corners)

Proof usesInduced topology

DefinitionInterior of a manifold#

The interior of a manifold M is the set of its interior points.

ModelWithCorners.interior.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H]
  {I : ModelWithCorners 𝕜 E H} (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] : Set M

Sources

• Mathlib documentation: ModelWithCorners.interior
• Source of ModelWithCorners.interior in Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibModelWithCorners.interior

Uses 5

Statement usesAssociative algebra over a commutative ring · Completeness · Continuous function · Convex subsets · Normed vector space over a normed field

DefinitionBoundary of a manifold#

The boundary of a manifold M is the set of its boundary points.

ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H]
  {I : ModelWithCorners 𝕜 E H} (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] : Set M

Sources

• Mathlib documentation: ModelWithCorners.boundary
• Source of ModelWithCorners.boundary in Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibModelWithCorners.boundary

Uses 6

Statement usesAssociative algebra over a commutative ring · Closure · Completeness · Continuous function · Convex subsets · Normed vector space over a normed field

AbbreviationTangent bundle#

The tangent bundle to a manifold, as a Sigma type. Defined in terms of Bundle.TotalSpace to be able to put a suitable topology on it.

TangentBundle.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] :
  Type (max u_4 u_2)

Sources

• Mathlib documentation: TangentBundle
• Source of TangentBundle in Mathlib/Geometry/Manifold/IsManifold/Basic.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibTangentBundle

Uses 5 · Used by 5

Statement usesAssociative algebra over a commutative ring · Completeness · Continuous function · Convex subsets · Normed vector space over a normed field

Used byJacobi/Leibniz identity · Local existence of integral curves · Tangent map · Uniform time existence · Uniqueness of integral curves

DefinitionTangent map#

tangentMap I I' f is the derivative of f : M → M' as a map between the tangent bundles TM and TM'.

tangentMap.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M]
  {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H']
  (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M']
  (f : M → M') : TangentBundle I M → TangentBundle I' M'

Sources

• Mathlib documentation: tangentMap
• Source of tangentMap in Mathlib/Geometry/Manifold/MFDeriv/Defs.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibtangentMap

Uses 2

Statement usesContinuous linear map · Tangent bundle

DefinitionPullback of vector fields#

The pullback of a vector field under a map between manifolds. If the derivative of the map is not invertible, then pullback is given the junk value zero.

VectorField.mpullback.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M]
  {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
  (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M']
  (f : M → M') (V : (x : M') → TangentSpace I' x) (x : M) : TangentSpace I x

Sources

• Mathlib documentation: VectorField.mpullback
• Source of VectorField.mpullback in Mathlib/Geometry/Manifold/VectorField/Pullback.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibVectorField.mpullback

Uses 5 · Used by 1

Statement usesAssociative algebra over a commutative ring · Completeness · Continuous linear map · Convex subsets · Normed vector space over a normed field

Used byLie bracket of vector field

DefinitionLie bracket of vector field#

The Lie bracket of two vector fields in a manifold.

VectorField.mlieBracket.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M]
  (V W : (x : M) → TangentSpace I x) (x₀ : M) : TangentSpace I x₀

Sources

• Mathlib documentation: VectorField.mlieBracket
• Source of VectorField.mlieBracket in Mathlib/Geometry/Manifold/VectorField/LieBracket.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibVectorField.mlieBracket

Uses 1 · Used by 1

Statement usesPullback of vector fields

Used byJacobi/Leibniz identity

TheoremJacobi/Leibniz identity#

The Lie bracket of vector fields in manifolds satisfies the Leibniz identity [U, [V, W]] = [[U, V], W] + [V, [U, W]] (also called Jacobi identity).

VectorField.leibniz_identity_mlieBracket.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (minSmoothness 𝕜 3) M] [CompleteSpace E]
  {U V W : (x : M) → TangentSpace I x}
  (hU : ContMDiff I I.tangent (minSmoothness 𝕜 2) fun x => ⟨x, U x⟩)
  (hV : ContMDiff I I.tangent (minSmoothness 𝕜 2) fun x => ⟨x, V x⟩)
  (hW : ContMDiff I I.tangent (minSmoothness 𝕜 2) fun x => ⟨x, W x⟩) :
  VectorField.mlieBracket I U (VectorField.mlieBracket I V W) =
    VectorField.mlieBracket I (VectorField.mlieBracket I U V) W +
      VectorField.mlieBracket I V (VectorField.mlieBracket I U W)

Sources

• Mathlib documentation: VectorField.leibniz_identity_mlieBracket
• Source of VectorField.leibniz_identity_mlieBracket in Mathlib/Geometry/Manifold/VectorField/LieBracket.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibVectorField.leibniz_identity_mlieBracket

Uses 11

Statement usesLie bracket of vector field · Smooth map between manifolds · Smooth or analytic manifold (with boundary and corners) · Tangent bundle · Topological fiber bundle

Proof usesCharacteristic zero · Closure · Cluster point · Generating sets · Ordered ring · The Triangle Inequality

DefinitionIntegral curves#

If v : M → TM is a vector field on M, IsMIntegralCurve γ v means γ : ℝ → M is a global integral curve of v. That is, γ t is tangent to v (γ t) for all t : ℝ.

IsMIntegralCurve.{u_1, u_2, u_3} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3}
  [TopologicalSpace M] [ChartedSpace H M] (γ : ℝ → M) (v : (x : M) → TangentSpace I x) : Prop

Sources

• Mathlib documentation: IsMIntegralCurve
• Source of IsMIntegralCurve in Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibIsMIntegralCurve

Uses 6 · Used by 1

Statement usesAssociative algebra over a commutative ring · Completeness · Continuous linear map · Convex subsets · Normed vector space over a normed field · Topological module

Used byUniform time existence

TheoremLocal existence of integral curves#

Existence of local integral curves for a \(C^1\) vector field on a C^1 manifold without boundary.

exists_isMIntegralCurveAt_of_contMDiffAt_boundaryless.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M]
  [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} (t₀ : ℝ) {x₀ : M} [CompleteSpace E]
  [BoundarylessManifold I M] (hv : ContMDiffAt I I.tangent 1 (fun x => ⟨x, v x⟩) x₀) :
  ∃ γ, γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀

Sources

• Mathlib documentation: exists_isMIntegralCurveAt_of_contMDiffAt_boundaryless
• Source of exists_isMIntegralCurveAt_of_contMDiffAt_boundaryless in Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean
• Mathlib overview: Geometry › Differentiable manifolds

Mathlibexists_isMIntegralCurveAt_of_contMDiffAt_boundaryless

Uses 8

Statement usesSmooth or analytic manifold (with boundary and corners) · Tangent bundle · Topological fiber bundle · Topological module

Proof usesBall · Cauchy-Lipschitz Theorem · Derivative at a point · Differentiable function between normed vector spaces

TheoremUniform time existence#

If there exists ε > 0 such that the local integral curve at each point x : M is defined at least on an open interval Ioo (-ε) ε, then every point on M has a global integral curve passing through it.

See Lemma 9.15, [J.M. Lee (2012)][lee2012].

exists_isMIntegralCurve_of_isMIntegralCurveOn.{u_1, u_2, u_3} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3}
  [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [T2Space M] [BoundarylessManifold I M]
  {v : (x : M) → TangentSpace I x} (hv : ContMDiff I I.tangent 1 fun x => ⟨x, v x⟩) {ε : ℝ}
  (hε : 0 < ε) (h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Set.Ioo (-ε) ε)) (x : M) :
  ∃ γ, γ 0 = x ∧ IsMIntegralCurve γ v

Sources

• Mathlib documentation: exists_isMIntegralCurve_of_isMIntegralCurveOn
• Source of exists_isMIntegralCurve_of_isMIntegralCurveOn in Mathlib/Geometry/Manifold/IntegralCurve/UniformTime.lean
• Mathlib overview: Geometry › Differentiable manifolds

Mathlibexists_isMIntegralCurve_of_isMIntegralCurveOn

Uses 9

Statement usesHausdorff space · Integral curves · Smooth map between manifolds · Smooth or analytic manifold (with boundary and corners) · Tangent bundle · Topological fiber bundle

Proof usesCharacteristic zero · Ordered ring · Uniqueness of integral curves

TheoremUniqueness of integral curves#

Mathlib states this as isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless.

isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M]
  [IsManifold I 1 M] {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ : ℝ} [T2Space M] {a b : ℝ}
  [BoundarylessManifold I M] (ht₀ : t₀ ∈ Set.Ioo a b)
  (hv : ContMDiff I I.tangent 1 fun x => ⟨x, v x⟩) (hγ : IsMIntegralCurveOn γ v (Set.Ioo a b))
  (hγ' : IsMIntegralCurveOn γ' v (Set.Ioo a b)) (h : γ t₀ = γ' t₀) : Set.EqOn γ γ' (Set.Ioo a b)

Sources

• Mathlib documentation: isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless
• Source of isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless in Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibisMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless

Uses 10 · Used by 1

Statement usesHausdorff space · Smooth map between manifolds · Smooth or analytic manifold (with boundary and corners) · Tangent bundle · Topological fiber bundle · Topological module

Proof usesClosure · Derivative at a point · Field \(\R\) of real numbers · Order topology

Used byUniform time existence

ClassLie group#

A (multiplicative) Lie group is a group and a C^n manifold at the same time in which the multiplication and inverse operations are C^n.

LieGroup.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2}
  [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (G : Type u_4) [Group G] [TopologicalSpace G]
  [ChartedSpace H G] : Prop

Sources

• Mathlib documentation: LieGroup
• Source of LieGroup in Mathlib/Geometry/Manifold/Algebra/LieGroup.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibLieGroup

Uses 2 · Used by 1

Statement usesSmooth map between manifolds · Smooth or analytic manifold (with boundary and corners)

Used byGeneral linear group as a Lie group

AbbreviationLie algebra of a Lie group#

The Lie algebra of a Lie group, i.e., its tangent space at the identity. We use the word GroupLieAlgebra instead of LieAlgebra as the latter is taken as a generic class.

GroupLieAlgebra.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2}
  [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  (I : ModelWithCorners 𝕜 E H) (G : Type u_4) [TopologicalSpace G] [ChartedSpace H G] [Group G] :
  Type u_3

Sources

• Mathlib documentation: GroupLieAlgebra
• Source of GroupLieAlgebra in Mathlib/Geometry/Manifold/GroupLieAlgebra.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibGroupLieAlgebra

Uses 5

Statement usesAssociative algebra over a commutative ring · Completeness · Continuous function · Convex subsets · Normed vector space over a normed field

TheoremSphere#

The unit sphere in an n + 1-dimensional inner product space E is an analytic manifold, modelled on the Euclidean space of dimension n.

EuclideanSpace.instIsManifoldSphere.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] :
  IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ ↑(Metric.sphere 0 1)

Sources

• Mathlib documentation: EuclideanSpace.instIsManifoldSphere
• Source of EuclideanSpace.instIsManifoldSphere in Mathlib/Geometry/Manifold/Instances/Sphere.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibEuclideanSpace.instIsManifoldSphere

Uses 14

Statement usesCardinal · Inner product space, over \(R\) or \(C\) · Linear independence · Norms \(\lVert\cdot\rVert_p\) on \(\R^n\) and \(\C^n\) · Smooth or analytic manifold (with boundary and corners)

Proof uses\(C^k\) function · Characteristic zero · Compactness in terms of filters · Existence of orthonormal basis · Finite-dimensionality · Ordered ring · Orthogonal projection · Topological ring · Topology on a normed vector space

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.