theorem 13.63 Constant rank theorem
open in the book ·
parts/02-mathematical-methods/11-manifolds-tensors-curvature.tex:2925
· p. 487
Rests on
-
depends_on
corollary A.292
Inverse function theorem
¶
-
depends_on
proposition 7.104
Chain rule in several variables
¶
-
depends_on
definition 7.13
Composite function
¶
- depends_on definition 7.9 Real function ¶
-
depends_on
definition 7.99
Differentiability at a point
¶
-
depends_on
definition 7.16
Limit
¶
- depends_on definition 7.2 Absolute value ¶
- depends_on definition 7.9 Real function ¶ ↺
-
depends_on
definition 5.37
Linear transformation
¶
- depends_on definition 4.33 Vector space ¶
- depends_on equation 6.12 eq:top-euclidean-metric ¶
-
depends_on
definition 7.16
Limit
¶
-
depends_on
definition 7.102
Differential of a function
¶
- depends_on definition 7.99 Differentiability at a point ¶ ↺
-
depends_on
definition 7.97
Partial derivative; gradient
¶
- depends_on definition 7.26 Derivative of a function at a point ¶
- depends_on definition 5.15 Basis ¶
- proves proof ch:05-real-analysis@proof-63 ¶
-
depends_on
definition 7.13
Composite function
¶
-
depends_on
theorem A.286
Implicit function theorem
¶
- depends_on definition 7.99 Differentiability at a point ¶ ↺
- depends_on proposition 7.104 Chain rule in several variables ¶ ↺
-
depends_on
theorem 7.100
$C^{1}$ implies differentiable
¶
-
depends_on
definition 7.98
Functions of class $C^{1}$
¶
- depends_on definition 7.20 Continuity at a point ¶
- depends_on definition 7.97 Partial derivative; gradient ¶ ↺
- depends_on definition 7.99 Differentiability at a point ¶ ↺
- depends_on theorem 7.35 Mean value theorem ¶
- proves proof ch:05-real-analysis@proof-62 ¶
-
depends_on
definition 7.98
Functions of class $C^{1}$
¶
- proves proof app:A-long-proofs@proof-185 ¶
- proves proof app:A-long-proofs@proof-186 ¶
-
depends_on
proposition 7.104
Chain rule in several variables
¶
- depends_on definition 7.98 Functions of class $C^{1}$ ¶ ↺
- depends_on theorem A.286 Implicit function theorem ¶ ↺
- proves proof ch:11-manifolds-tensors-curvature@proof-12 ¶
Supports
- depends_on corollary 13.64 The image of a constant-rank map, locally ¶
-
depends_on
lemma A.533
The orbit map has constant rank $d$
¶
- depends_on proposition A.534 Every orbit is an embedded copy of $G$ ¶
-
depends_on
proposition A.535
Existence of a slice
¶
-
depends_on
lemma A.536
A slice is a chart domain downstairs
¶
- depends_on theorem A.537 The smooth structure on the orbit space ¶
- depends_on remark A.542 Where each hypothesis is spent ¶
-
depends_on
lemma A.536
A slice is a chart domain downstairs
¶
-
depends_on
lemma A.538
Submersions have smooth local sections
¶
-
depends_on
proposition A.539
Universal property
¶
- depends_on corollary A.540 Uniqueness of the smooth structure ¶
-
depends_on
proposition A.539
Universal property
¶
-
depends_on
theorem 13.67
Quotient manifold theorem
¶
-
depends_on
example 13.68
Why each hypothesis is there
¶
- depends_on remark A.542 Where each hypothesis is spent ¶ ↺
-
depends_on
proposition A.566
The isotropy group acts, and the quotient is
smooth
¶
-
depends_on
proposition A.570
Existence and uniqueness of the reduced form
¶
- depends_on proposition A.571 Invariant Hamiltonians descend with their flows ¶
-
depends_on
proposition A.570
Existence and uniqueness of the reduced form
¶
-
depends_on
theorem A.563
Marsden–Weinstein reduction
¶
- depends_on example A.573 The abelian case, and eliminating a cyclic coordinate ¶
- depends_on example A.572 Rotational reduction of the central-force problem ¶
-
depends_on
example 13.68
Why each hypothesis is there
¶
Neighborhood
Every logical edge within two steps of this node.
- declared and complete
- partly declared
- a check failed
- not graded
- declared in the source
- inferred from structure
Edges
| type | direction | node | provenance | where |
|---|---|---|---|---|
depends_on |
→ | Inverse function theorem | declared | parts/02-mathematical-methods/11-manifolds-tensors-curvature.tex:2938 |
depends_on |
→ | Functions of class $C^{1}$ | declared | parts/02-mathematical-methods/11-manifolds-tensors-curvature.tex:2938 |
depends_on |
→ | Implicit function theorem | declared | parts/02-mathematical-methods/11-manifolds-tensors-curvature.tex:2938 |
depends_on |
← | The image of a constant-rank map, locally | declared | parts/02-mathematical-methods/11-manifolds-tensors-curvature.tex:3002 |
depends_on |
← | The orbit map has constant rank $d$ | declared | appendices/A-long-proofs.tex:26013 |
depends_on |
← | Submersions have smooth local sections | declared | appendices/A-long-proofs.tex:26279 |
depends_on |
← | Quotient manifold theorem | declared | parts/02-mathematical-methods/11-manifolds-tensors-curvature.tex:3082 |
proves |
← | ch:11-manifolds-tensors-curvature@proof-12 | declared | parts/02-mathematical-methods/11-manifolds-tensors-curvature.tex:2941 |