Lie groups #
A Lie group is a group that is also a C^n manifold, in which the group operations of
multiplication and inversion are C^n maps. Regularity of the group multiplication means that
multiplication is a C^n mapping of the product manifold G × G into G.
Note that, since a manifold here is not second-countable and Hausdorff a Lie group here is not guaranteed to be second-countable (even though it can be proved it is Hausdorff). Note also that Lie groups here are not necessarily finite dimensional.
Main definitions #
LieAddGroup I G: a Lie additive group whereGis a manifold on the model with cornersI.LieGroup I G: a Lie multiplicative group whereGis a manifold on the model with cornersI.ContMDiffInv₀: typeclass forC^nmanifolds with0andInvsuch that inversion isC^nmap at each non-zero point. This includes complete normed fields and (multiplicative) Lie groups.
Main results #
ContMDiff.inv,ContMDiff.divand variants: point-wise inversion and division of mapsM → GisC^n.ContMDiff.inv₀and variants: ifContMDiffInv₀ I n N, point-wise inversion ofC^nmapsf : M → NisC^nat all points at whichfdoesn't vanish.ContMDiff.div₀and variants: if alsoContMDiffMul I n N(i.e.,Nis a Lie group except possibly for smoothness of inversion at0), similar results hold for point-wise division.instNormedSpaceLieAddGroup: a normed vector space over a nontrivially normed field is an additive Lie group.Instances/UnitsOfNormedAlgebrashows that the group of units of a complete normed𝕜-algebra is a multiplicative Lie group.
Implementation notes #
A priori, a Lie group here is a manifold with corners.
The definition of Lie group cannot require I : ModelWithCorners 𝕜 E E with the same space as the
model space and as the model vector space, as one might hope, because in the product situation,
the model space is ModelProd E E' and the model vector space is E × E', which are not the same,
so the definition does not apply. Hence the definition should be more general, allowing
I : ModelWithCorners 𝕜 E H.
class
LieAddGroup
{𝕜 : 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)
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H G]
extends ContMDiffAdd I n G :
An additive Lie group is a group and a C^n manifold at the same time in which
the addition and negation operations are C^n.
- compatible {e e' : PartialHomeomorph G H} : e ∈ atlas H G → e' ∈ atlas H G → e.symm.trans e' ∈ contDiffGroupoid n I
- contMDiff_add : ContMDiff (I.prod I) I n fun (p : G × G) => p.1 + p.2
Negation is smooth in an additive Lie group.
Instances
class
LieGroup
{𝕜 : 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]
extends ContMDiffMul I n G :
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.
- compatible {e e' : PartialHomeomorph G H} : e ∈ atlas H G → e' ∈ atlas H G → e.symm.trans e' ∈ contDiffGroupoid n I
- contMDiff_mul : ContMDiff (I.prod I) I n fun (p : G × G) => p.1 * p.2
Inversion is smooth in a Lie group.
Instances
Smoothness of inversion, negation, division and subtraction #
Let f : M → G be a C^n function into a Lie group, then f is point-wise
invertible with smooth inverse f. If f and g are two such functions, the quotient
f / g (i.e., the point-wise product of f and the point-wise inverse of g) is also C^n.
theorem
LieGroup.of_le
{𝕜 : 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]
{m n : WithTop ℕ∞}
(hmn : m ≤ n)
[h : LieGroup I n G]
:
LieGroup I m G
theorem
LieAddGroup.of_le
{𝕜 : 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]
[AddGroup G]
{m n : WithTop ℕ∞}
(hmn : m ≤ n)
[h : LieAddGroup I n G]
:
LieAddGroup I m G
instance
instLieGroupOfSomeENatTopOfLEInfty
{𝕜 : 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]
{a : WithTop ℕ∞}
[LieGroup I (↑⊤) G]
[h : ENat.LEInfty a]
:
LieGroup I a G
instance
instLieAddGroupOfSomeENatTopOfLEInfty
{𝕜 : 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]
[AddGroup G]
{a : WithTop ℕ∞}
[LieAddGroup I (↑⊤) G]
[h : ENat.LEInfty a]
:
LieAddGroup I a G
instance
instLieGroupOfTopWithTopENat
{𝕜 : 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]
{a : WithTop ℕ∞}
[LieGroup I ⊤ G]
:
LieGroup I a G
instance
instLieAddGroupOfTopWithTopENat
{𝕜 : 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]
[AddGroup G]
{a : WithTop ℕ∞}
[LieAddGroup I ⊤ G]
:
LieAddGroup I a G
instance
instLieGroupOfNatWithTopENatOfIsTopologicalGroup
{𝕜 : 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]
[IsTopologicalGroup G]
:
LieGroup I 0 G
instance
instLieAddGroupOfNatWithTopENatOfIsTopologicalAddGroup
{𝕜 : 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]
[AddGroup G]
[IsTopologicalAddGroup G]
:
LieAddGroup I 0 G
instance
instLieGroupOfNatWithTopENat
{𝕜 : 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]
[LieGroup I 2 G]
:
LieGroup I 1 G
instance
instLieAddGroupOfNatWithTopENat
{𝕜 : 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]
[AddGroup G]
[LieAddGroup I 2 G]
:
LieAddGroup I 1 G
theorem
contMDiff_inv
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I n G]
:
In a Lie group, inversion is C^n.
theorem
contMDiff_neg
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I n G]
:
In an additive Lie group, inversion is a smooth map.
theorem
topologicalGroup_of_lieGroup
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I n G]
:
A Lie group is a topological group. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].
theorem
topologicalAddGroup_of_lieAddGroup
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I n G]
:
An additive Lie group is an additive topological group. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].
theorem
ContMDiffWithinAt.inv
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
{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]
[LieGroup I n G]
{f : M → G}
{s : Set M}
{x₀ : M}
(hf : ContMDiffWithinAt I' I n f s x₀)
:
ContMDiffWithinAt I' I n (fun (x : M) => (f x)⁻¹) s x₀
theorem
ContMDiffWithinAt.neg
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
{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]
[LieAddGroup I n G]
{f : M → G}
{s : Set M}
{x₀ : M}
(hf : ContMDiffWithinAt I' I n f s x₀)
:
ContMDiffWithinAt I' I n (fun (x : M) => -f x) s x₀
theorem
ContMDiffAt.inv
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
{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]
[LieGroup I n G]
{f : M → G}
{x₀ : M}
(hf : ContMDiffAt I' I n f x₀)
:
ContMDiffAt I' I n (fun (x : M) => (f x)⁻¹) x₀
theorem
ContMDiffAt.neg
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
{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]
[LieAddGroup I n G]
{f : M → G}
{x₀ : M}
(hf : ContMDiffAt I' I n f x₀)
:
ContMDiffAt I' I n (fun (x : M) => -f x) x₀
theorem
ContMDiffOn.inv
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
{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]
[LieGroup I n G]
{f : M → G}
{s : Set M}
(hf : ContMDiffOn I' I n f s)
:
ContMDiffOn I' I n (fun (x : M) => (f x)⁻¹) s
theorem
ContMDiffOn.neg
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
{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]
[LieAddGroup I n G]
{f : M → G}
{s : Set M}
(hf : ContMDiffOn I' I n f s)
:
ContMDiffOn I' I n (fun (x : M) => -f x) s
theorem
ContMDiff.inv
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
{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]
[LieGroup I n G]
{f : M → G}
(hf : ContMDiff I' I n f)
:
theorem
ContMDiff.neg
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
{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]
[LieAddGroup I n G]
{f : M → G}
(hf : ContMDiff I' I n f)
:
theorem
ContMDiffWithinAt.div
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
{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]
[LieGroup I n G]
{f g : M → G}
{s : Set M}
{x₀ : M}
(hf : ContMDiffWithinAt I' I n f s x₀)
(hg : ContMDiffWithinAt I' I n g s x₀)
:
ContMDiffWithinAt I' I n (fun (x : M) => f x / g x) s x₀
theorem
ContMDiffWithinAt.sub
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
{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]
[LieAddGroup I n G]
{f g : M → G}
{s : Set M}
{x₀ : M}
(hf : ContMDiffWithinAt I' I n f s x₀)
(hg : ContMDiffWithinAt I' I n g s x₀)
:
ContMDiffWithinAt I' I n (fun (x : M) => f x - g x) s x₀
theorem
ContMDiffAt.div
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
{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]
[LieGroup I n G]
{f g : M → G}
{x₀ : M}
(hf : ContMDiffAt I' I n f x₀)
(hg : ContMDiffAt I' I n g x₀)
:
ContMDiffAt I' I n (fun (x : M) => f x / g x) x₀
theorem
ContMDiffAt.sub
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
{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]
[LieAddGroup I n G]
{f g : M → G}
{x₀ : M}
(hf : ContMDiffAt I' I n f x₀)
(hg : ContMDiffAt I' I n g x₀)
:
ContMDiffAt I' I n (fun (x : M) => f x - g x) x₀
theorem
ContMDiffOn.div
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
{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]
[LieGroup I n G]
{f g : M → G}
{s : Set M}
(hf : ContMDiffOn I' I n f s)
(hg : ContMDiffOn I' I n g s)
:
ContMDiffOn I' I n (fun (x : M) => f x / g x) s
theorem
ContMDiffOn.sub
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
{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]
[LieAddGroup I n G]
{f g : M → G}
{s : Set M}
(hf : ContMDiffOn I' I n f s)
(hg : ContMDiffOn I' I n g s)
:
ContMDiffOn I' I n (fun (x : M) => f x - g x) s
theorem
ContMDiff.div
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
{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]
[LieGroup I n G]
{f g : M → G}
(hf : ContMDiff I' I n f)
(hg : ContMDiff I' I n g)
:
theorem
ContMDiff.sub
{𝕜 : 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}
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
{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]
[LieAddGroup I n G]
{f g : M → G}
(hf : ContMDiff I' I n f)
(hg : ContMDiff I' I n g)
:
Binary product of Lie groups
instance
Prod.instLieGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{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]
[LieGroup I n G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{G' : Type u_7}
[TopologicalSpace G']
[ChartedSpace H' G']
[Group G']
[LieGroup I' n G']
:
instance
Prod.instLieAddGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{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]
[AddGroup G]
[LieAddGroup I n G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{G' : Type u_7}
[TopologicalSpace G']
[ChartedSpace H' G']
[AddGroup G']
[LieAddGroup I' n G']
:
LieAddGroup (I.prod I') n (G × G')
Normed spaces are Lie groups #
instance
instNormedSpaceLieAddGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
:
LieAddGroup (modelWithCornersSelf 𝕜 E) n E
C^n manifolds with C^n inversion away from zero #
Typeclass for C^n manifolds with 0 and Inv such that inversion is C^n at all non-zero
points. (This includes multiplicative Lie groups, but also complete normed semifields.)
Point-wise inversion is C^n when the function/denominator is non-zero.
class
ContMDiffInv₀
{𝕜 : 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)
[Inv G]
[Zero G]
[TopologicalSpace G]
[ChartedSpace H G]
:
A C^n manifold with 0 and Inv such that fun x ↦ x⁻¹ is C^n at all nonzero points.
Any complete normed (semi)field has this property.
- contMDiffAt_inv₀ ⦃x : G⦄ : x ≠ 0 → ContMDiffAt I I n (fun (y : G) => y⁻¹) x
Inversion is
C^naway from0.
Instances
instance
instContMDiffInv₀ModelWithCornersSelf
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
:
ContMDiffInv₀ (modelWithCornersSelf 𝕜 𝕜) n 𝕜
theorem
ContMDiffInv₀.of_le
{𝕜 : 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]
[Inv G]
[Zero G]
{m n : WithTop ℕ∞}
(hmn : m ≤ n)
[h : ContMDiffInv₀ I n G]
:
ContMDiffInv₀ I m G
instance
instContMDiffInv₀OfSomeENatTopOfLEInfty
{𝕜 : 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]
[Inv G]
[Zero G]
{a : WithTop ℕ∞}
[ContMDiffInv₀ I (↑⊤) G]
[h : ENat.LEInfty a]
:
ContMDiffInv₀ I a G
instance
instContMDiffInv₀OfTopWithTopENat
{𝕜 : 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]
[Inv G]
[Zero G]
{a : WithTop ℕ∞}
[ContMDiffInv₀ I ⊤ G]
:
ContMDiffInv₀ I a G
instance
instContMDiffInv₀OfNatWithTopENatOfHasContinuousInv₀
{𝕜 : 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]
[Inv G]
[Zero G]
[HasContinuousInv₀ G]
:
ContMDiffInv₀ I 0 G
instance
instContMDiffInv₀OfNatWithTopENat
{𝕜 : 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]
[Inv G]
[Zero G]
[ContMDiffInv₀ I 2 G]
:
ContMDiffInv₀ I 1 G
theorem
contMDiffAt_inv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{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]
[Inv G]
[Zero G]
[ContMDiffInv₀ I n G]
{x : G}
(hx : x ≠ 0)
:
ContMDiffAt I I n (fun (y : G) => y⁻¹) x
theorem
hasContinuousInv₀_of_hasContMDiffInv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{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]
[Inv G]
[Zero G]
[ContMDiffInv₀ I n G]
:
In a manifold with C^n inverse away from 0, the inverse is continuous away from 0.
This is not an instance for technical reasons, see
note [Design choices about smooth algebraic structures].
theorem
contMDiffOn_inv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{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]
[Inv G]
[Zero G]
[ContMDiffInv₀ I n G]
:
ContMDiffOn I I n Inv.inv {0}ᶜ
theorem
ContMDiffWithinAt.inv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{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]
[Inv G]
[Zero G]
{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 → G}
[ContMDiffInv₀ I n G]
{s : Set M}
{a : M}
(hf : ContMDiffWithinAt I' I n f s a)
(ha : f a ≠ 0)
:
ContMDiffWithinAt I' I n (fun (x : M) => (f x)⁻¹) s a
theorem
ContMDiffAt.inv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{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]
[Inv G]
[Zero G]
{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 → G}
[ContMDiffInv₀ I n G]
{a : M}
(hf : ContMDiffAt I' I n f a)
(ha : f a ≠ 0)
:
ContMDiffAt I' I n (fun (x : M) => (f x)⁻¹) a
theorem
ContMDiff.inv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{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]
[Inv G]
[Zero G]
{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 → G}
[ContMDiffInv₀ I n G]
(hf : ContMDiff I' I n f)
(h0 : ∀ (x : M), f x ≠ 0)
:
theorem
ContMDiffOn.inv₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{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]
[Inv G]
[Zero G]
{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 → G}
[ContMDiffInv₀ I n G]
{s : Set M}
(hf : ContMDiffOn I' I n f s)
(h0 : ∀ x ∈ s, f x ≠ 0)
:
ContMDiffOn I' I n (fun (x : M) => (f x)⁻¹) s
Point-wise division of C^n functions #
If [ContMDiffMul I n N] and [ContMDiffInv₀ I n N], point-wise division of C^n
functions f : M → N is C^n whenever the denominator is non-zero.
(This includes N being a completely normed field.)
theorem
ContMDiffWithinAt.div₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{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]
[GroupWithZero G]
[ContMDiffInv₀ I n G]
[ContMDiffMul I n G]
{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 g : M → G}
{s : Set M}
{a : M}
(hf : ContMDiffWithinAt I' I n f s a)
(hg : ContMDiffWithinAt I' I n g s a)
(h₀ : g a ≠ 0)
:
ContMDiffWithinAt I' I n (f / g) s a
theorem
ContMDiffOn.div₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{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]
[GroupWithZero G]
[ContMDiffInv₀ I n G]
[ContMDiffMul I n G]
{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 g : M → G}
{s : Set M}
(hf : ContMDiffOn I' I n f s)
(hg : ContMDiffOn I' I n g s)
(h₀ : ∀ x ∈ s, g x ≠ 0)
:
ContMDiffOn I' I n (f / g) s
theorem
ContMDiffAt.div₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{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]
[GroupWithZero G]
[ContMDiffInv₀ I n G]
[ContMDiffMul I n G]
{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 g : M → G}
{a : M}
(hf : ContMDiffAt I' I n f a)
(hg : ContMDiffAt I' I n g a)
(h₀ : g a ≠ 0)
:
ContMDiffAt I' I n (f / g) a
theorem
ContMDiff.div₀
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{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]
[GroupWithZero G]
[ContMDiffInv₀ I n G]
[ContMDiffMul I n G]
{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 g : M → G}
(hf : ContMDiff I' I n f)
(hg : ContMDiff I' I n g)
(h₀ : ∀ (x : M), g x ≠ 0)
: