WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Riemannian manifold

Revision #1543 → #2473 · back to history

modifiedRiemannian manifold (informal)8f489a8ac27e
FieldFrom #1543To #2473
mathlib.decl—IsRiemannianManifold
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Manifold.Riemannian.Basic
note—`IsRiemannianManifold I M` is the Prop-valued typeclass registering the Riemannian-manifold predicate on a manifold equipped with an emetric structure and a Riemannian bundle on its tangent bundle.
status—formalized
modifiedRiemannian metric (informal)a54850aeefc7
FieldFrom #1543To #2473
mathlib.decl—Bundle.ContMDiffRiemannianMetric
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Manifold.VectorBundle.Riemannian
note—`ContMDiffRiemannianMetric IB n F E` is a family of inner products on the fibers of a vector bundle varying `C^n`-smoothly with the base point; applied to the tangent bundle it is exactly a Riemannian metric.
status—formalized
modifiedTheorema Egregium33041a26c564
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Gaussian curvature of surfaces is not formalized in Mathlib, so Theorema Egregium is absent.
status—not_formalized
modifiedLocal isometry (surfaces)c2055187b47b
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No definition of local isometry between Riemannian manifolds/surfaces exists in Mathlib; only the metric-space `Isometry` predicate is available.
status—not_formalized
modifiedIntrinsic/extrinsic propertya713aeb65d6a
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no notion of intrinsic vs extrinsic property of a surface.
status—not_formalized
modifiedRiemannian metric and Riemannian manifolde5873192f9b0
FieldFrom #1543To #2473
anchor.snippetassigns to eachA Riemannian metric
mathlib.decl—Bundle.RiemannianMetric
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.VectorBundle.Riemannian
note—Anchor tightened to point to the definitional sentence.
note_annotation—`Bundle.RiemannianMetric E` gives a family of inner products on the fibers of a vector bundle (and `IsRiemannianManifold` packages the manifold-level assertion).
provenanceai-agent1ai-moderated
status—formalized
modifiedMetric components in coordinatesc9d2a2980add
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib's Riemannian metrics are coordinate-free bilinear forms on fibers; the classical `g_{ij}` coordinate components are not defined.
status—not_formalized
modifiedContinuous/smooth Riemannian metric31459bcceb44
FieldFrom #1543To #2473
mathlib.decl—IsContMDiffRiemannianBundle
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Manifold.VectorBundle.Riemannian
note—`IsContinuousRiemannianBundle` and `IsContMDiffRiemannianBundle` express, respectively, that the inner product on fibers varies continuously / `C^n`-smoothly with the base point.
status—formalized
modifiedMusical isomorphism7d805eedbdd5
FieldFrom #1543To #2473
mathlib.decl—InnerProductSpace.toDual
mathlib.match_kind—special_case
mathlib.module—Mathlib.Analysis.InnerProductSpace.Dual
note—The pointwise `InnerProductSpace.toDual` gives the fiberwise flat isomorphism of a Hilbert space with its dual, but the bundle-level musical isomorphism between the tangent and cotangent bundles is not built in Mathlib.
status—partial
modifiedIsometry944442fb5605
FieldFrom #1543To #2473
anchor.snippeta diffeomorphismAn isometry is a function between Riemannian manifolds which preserves all of the structure of Riemannian manifolds
mathlib.decl—Isometry
mathlib.match_kind—generalization
mathlib.module—Mathlib.Topology.MetricSpace.Isometry
note—Anchor changed to the primary definitional sentence; the previous snippet 'a diffeomorphism' was too generic.
note_annotation—Mathlib's `Isometry` for (pseudo)emetric spaces applies at the level of the induced distance, but there is no dedicated `RiemannianIsometry` preserving the smooth structure and the metric tensor.
provenanceai-agent1ai-moderated
status—partial
modifiedLocal isometry7cbcb2601679
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No local-isometry notion for Riemannian manifolds is present in Mathlib.
status—not_formalized
modifiedRiemannian volume formc4194010724b
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Riemannian volume form on an oriented Riemannian manifold is not defined in Mathlib; only the pointwise `Orientation.volumeForm` on a single inner product space exists.
status—not_formalized
modifiedEuclidean metricbf6af90d7432
FieldFrom #1543To #2473
mathlib.decl—riemannianMetricVectorSpace
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Manifold.Riemannian.Basic
note—`riemannianMetricVectorSpace F` is the canonical Riemannian metric on an inner product space given by its inner product on each tangent space, and `EuclideanSpace` is the standard inner-product model.
status—formalized
modifiedRiemannian submanifolddbd786d7968d
FieldFrom #1543To #2473
anchor.snippetis a Riemannian metric onis said to be a Riemannian submanifold
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Anchor sharpened to the defining phrase.
note_annotation—Riemannian submanifolds and the induced metric are not formalized.
provenanceai-agent1ai-moderated
status—not_formalized
modifiedRound metric on the sphere11c8cae37637
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The round Riemannian metric on the sphere is not defined in Mathlib.
status—not_formalized
modifiedEllipsoid as submanifoldb73e482cfb25
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Ellipsoids as Riemannian submanifolds are not in Mathlib.
status—not_formalized
modifiedGraph of smooth function85ba61b72989
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The graph of a smooth function as an embedded Riemannian submanifold is not treated in Mathlib.
status—not_formalized
modifiedCovering space inherits metric08cb80b46618
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib does not construct a Riemannian metric on a smooth covering space by pullback.
status—not_formalized
modifiedIsometric immersion/embeddinge5ed66c3c8cf
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Isometric immersions/embeddings between Riemannian manifolds are not defined in Mathlib.
status—not_formalized
modifiedProduct Riemannian metric169c939d49f8
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The product Riemannian metric on a product of Riemannian manifolds is not constructed in Mathlib.
status—not_formalized
modifiedFlat torusc8404234c778
FieldFrom #1543To #2473
anchor.snippetthe product Riemannian manifoldis called the flat torus
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Anchor tightened to the naming phrase.
note_annotation—The flat torus as a Riemannian manifold is not present in Mathlib.
provenanceai-agent1ai-moderated
status—not_formalized
modifiedPositive combinations of metricsedcae84901d7
FieldFrom #1543To #2473
anchor.snippetare any positive smooth functions onis another Riemannian metric on
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Anchor moved to the conclusion of the proposition.
note_annotation—No lemma stating that positive linear combinations of Riemannian metrics remain Riemannian is in Mathlib.
provenanceai-agent1ai-moderated
status—not_formalized
modifiedExistence of Riemannian metric40ba7cadcc2f
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib only constructs the canonical Riemannian metric on inner product spaces; the general existence result for arbitrary smooth manifolds (via partitions of unity) is not there.
status—not_formalized
modifiedNash embedding theorem9739c3853f35
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Nash embedding theorem is not in Mathlib.
status—not_formalized
modifiedAdmissible curve and lengthb7b2cc5ecf22
FieldFrom #1543To #2473
mathlib.decl—Manifold.pathELength
mathlib.match_kind—generalization
mathlib.module—Mathlib.Geometry.Manifold.Riemannian.PathELength
note—`Manifold.pathELength` gives the length integral of a `C^1` path in a manifold whose tangent spaces have an `ENorm`; piecewise-smooth admissible curves are subsumed as `C^1` paths.
status—partial
modifiedRiemannian distance is a metric6a1a9fe3536b
FieldFrom #1543To #2473
mathlib.decl—EMetricSpace.ofRiemannianMetric
mathlib.match_kind—generalization
mathlib.module—Mathlib.Geometry.Manifold.Riemannian.Basic
note—`EMetricSpace.ofRiemannianMetric` builds an emetric space structure whose topology agrees with the manifold's, using `riemannianEDist`; positivity/triangle inequality are proved but only an `ℝ≥0∞`-valued distance is provided.
status—partial
modifiedDiameter49115a34eab4
FieldFrom #1543To #2473
mathlib.decl—Metric.diam
mathlib.match_kind—generalization
mathlib.module—Mathlib.Topology.MetricSpace.Bounded
note—`Metric.diam` is defined for arbitrary (pseudo)metric spaces, subsuming the diameter of a Riemannian manifold under its induced distance.
status—formalized
modifiedCompactness iff finite diameter (complete)f00e371f344e
FieldFrom #1543To #2473
anchor.snippetIfis complete, then it is compact if and only if it has finite diameter
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Anchor sharpened from the generic 'If' to the actual proposition text.
note_annotation—The Riemannian statement 'complete ∧ finite diameter ↔ compact' (invoking Hopf–Rinow) is not in Mathlib.
provenanceai-agent1ai-moderated
status—not_formalized
modifiedAffine connection3a218351b067
FieldFrom #1543To #2473
mathlib.decl—CovariantDerivative
mathlib.match_kind—generalization
mathlib.module—Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
note—`CovariantDerivative I F V` is a bundled Koszul connection on a vector bundle; taking `V = TangentSpace I` recovers an affine connection on a manifold.
status—formalized
modifiedCovariant derivative7a3f66b1d0c3
FieldFrom #1543To #2473
mathlib.decl—CovariantDerivative
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
note—`CovariantDerivative` is Mathlib's bundled covariant-derivative structure on a vector bundle over a manifold.
status—formalized
modifiedMetric-preserving connectionddd759c2b339
FieldFrom #1543To #2473
mathlib.decl—CovariantDerivative.IsMetricCompatible
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
note—`CovariantDerivative.IsMetricCompatible cov` states that a connection on a Riemannian bundle preserves the metric (its `derivMetricTensor` vanishes).
status—formalized
modifiedTorsion-free connection240091057396
FieldFrom #1543To #2473
mathlib.decl—CovariantDerivative.torsion_eq_zero_iff
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
note—Mathlib defines `CovariantDerivative.torsion` on the tangent bundle and characterizes torsion-freeness via `torsion_eq_zero_iff` (⇔ `∇_X Y - ∇_Y X = [X,Y]`).
status—formalized
modifiedLevi-Civita connection existence/uniqueness2dfcff3c05eb
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Although metric-compatibility and torsion-freeness are defined, existence/uniqueness of the Levi-Civita connection is not proved in Mathlib.
status—not_formalized
modifiedVector field along a curve6ee36a88f485
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No definition of a smooth vector field along a curve in a manifold appears in Mathlib.
status—not_formalized
modifiedExtension of vector field along curve8924133b91ba
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No notion of extending a vector field along a curve is in Mathlib.
status—not_formalized
modifiedCovariant derivative along a curve0409620e858c
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The existence/uniqueness of the covariant derivative operator along a curve is not formalized.
status—not_formalized
modifiedGeodesicdb343c134220
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Geodesics on Riemannian manifolds are not defined in Mathlib.
status—not_formalized
modifiedExistence and uniqueness of geodesicsf88ba9f8e0b4
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The local existence and uniqueness of geodesics is not in Mathlib.
status—not_formalized
modifiedMaximal geodesic8080b5e738c4
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Maximal geodesics are not defined in Mathlib.
status—not_formalized
modifiedShortest curves are geodesics0d8cf058dc88
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The result identifying length-minimizing curves with geodesics is absent from Mathlib.
status—not_formalized
modifiedGeodesics in the Euclidean plane1aef34fa098e
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Without a geodesic definition, the identification of Euclidean geodesics as affine lines is not in Mathlib.
status—not_formalized
modifiedGeodesics on the sphere8714e64bc491
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The identification of great circles as sphere geodesics is not formalized.
status—not_formalized
modifiedGeodesically complete1878b5dc0353
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Geodesic completeness is not defined in Mathlib.
status—not_formalized
modifiedHopf–Rinow theorem495aa58e4b6f
FieldFrom #1543To #2473
anchor.snippetLetThe Hopf–Rinow theorem characterizes geodesically complete manifolds
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Anchor moved from the generic 'Let' to the theorem's characterizing sentence.
note_annotation—The Hopf–Rinow theorem is not in Mathlib.
provenanceai-agent1ai-moderated
status—not_formalized
modifiedParallel vector fielde3c779515c3d
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Parallel vector fields along a curve are not defined in Mathlib.
status—not_formalized
modifiedParallel transport315bdcc1d773
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Parallel transport is not defined in Mathlib (the file `CovariantDerivative/Metric.lean` even notes it as a TODO).
status—not_formalized
modifiedRiemann curvature tensor32d0d2eb4d30
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Riemann curvature tensor is not defined in Mathlib.
status—not_formalized
modifiedVanishing curvature iff locally Euclidean7234eca45be6
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized: neither the curvature tensor nor local Riemannian isometries are in Mathlib.
status—not_formalized
modifiedRicci curvature tensor8b8f9fa879d9
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Ricci curvature tensor is not defined in Mathlib.
status—not_formalized
modifiedEinstein metric / Einstein manifold339fbf46408c
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Einstein manifolds are not defined in Mathlib.
status—not_formalized
modifiedConstant curvature4f09d256d55e
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Sectional and constant curvatures are not defined in Mathlib.
status—not_formalized
modifiedConstant curvature implies Einsteinf781e34fc019
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib: prerequisites (constant curvature, Einstein) are missing.
status—not_formalized
modifiedRiemannian space form4f56a1bbdf6b
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Riemannian space forms are not defined in Mathlib.
status—not_formalized
modifiedKilling–Hopf theorem2d19f141a247
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Killing–Hopf classification of space forms is not in Mathlib.
status—not_formalized
modifiedLeft-invariant metric on Lie groupfff138786d08
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Left-invariant Riemannian metrics on Lie groups are not constructed in Mathlib.
status—not_formalized
modifiedBi-invariant metric existence67212202f752
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The characterization of Lie groups admitting a bi-invariant metric is not in Mathlib.
status—not_formalized
modifiedHomogeneous Riemannian manifold6092325a24c6
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Homogeneous Riemannian manifolds are not defined in Mathlib.
status—not_formalized
modifiedHomogeneous implies geodesically complete6a594da2c18c
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not in Mathlib: homogeneity, geodesic completeness, and scalar curvature are all missing.
status—not_formalized
modifiedClassification of homogeneous Riemannian manifolds8cdd0bcab58d
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Lie-theoretic classification of homogeneous Riemannian manifolds is not in Mathlib.
status—not_formalized
modifiedSymmetric Riemannian manifoldbee20dd180e2
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Riemannian symmetric spaces are not defined in Mathlib.
status—not_formalized
modifiedCartan: locally symmetric implies symmetrica220e1650d32
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Cartan's local-to-global theorem for symmetric spaces is not in Mathlib.
status—not_formalized
modifiedBerger's holonomy classification35015a6ed188
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Berger's holonomy classification is not in Mathlib (no holonomy group is defined).
status—not_formalized
modifiedWeak/strong Riemannian metricd640181d4a27
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Weak vs strong Riemannian metrics on infinite-dimensional manifolds are not treated in Mathlib.
status—not_formalized
modifiedHilbert space strong metricfa761a441e63
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—This infinite-dimensional example is not in Mathlib.
status—not_formalized
modifiedL² weak metric on diffeomorphism groupc69f0fa06343
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The L² weak metric on a diffeomorphism group is not in Mathlib.
status—not_formalized
modifiedStrong metric separates points2bac47e40d4b
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not formalized in Mathlib.
status—not_formalized
modifiedVanishing geodesic distance for weak metric01b99036b8ed
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Michor–Mumford vanishing-distance phenomenon is not in Mathlib.
status—not_formalized
modifiedHopf–Rinow (strong, infinite-dim)c588a1456cac
FieldFrom #1543To #2473
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The infinite-dimensional Hopf–Rinow theorem is not in Mathlib.
status—not_formalized
addedTangent spacef04702763945
addedInduced norm from Riemannian metric31c58ce06b92
addedRiemannian volume form preserved by orientation-preserving isometries836600fa9d42
addedVolume of a compact Riemannian manifold67dda7dbfa32
addedPullback Riemannian metric088ac3ef31b2
addedn-sphere as embedded submanifoldaa675f6f96b1
addedProduct of Euclidean lines is Euclideanc52bd26a56c3
addedRiemannian distance functione593089dd0b6
addedWhitney embedding gives a Riemannian metric1ad1560317a4
addedConstant curvature: Ricci and scalar formulas14e86172a622
addedLeft-invariant metrics have constant scalar curvatured3757d495633
addedBi-invariant metrics have nonnegative sectional curvature5750c71c47bb
addedSymmetric spaces are homogeneous0823302e73ae