Products of local diffeomorphisms #
The product of two partial diffeomorphisms has product source and target. Applying this to local representatives shows that the product of two local diffeomorphisms is a local diffeomorphism.
def
PartialDiffeomorph.prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
{E' : Type u_3}
{F : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{H : Type u_6}
{H' : Type u_7}
{G : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace H']
[TopologicalSpace G]
[TopologicalSpace G']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{J' : ModelWithCorners 𝕜 F' G'}
{M : Type u_10}
{M' : Type u_11}
{N : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace N']
[ChartedSpace G' N']
{n : WithTop ℕ∞}
(e : PartialDiffeomorph I I' M M' n)
(f : PartialDiffeomorph J J' N N' n)
:
PartialDiffeomorph (I.prod J) (I'.prod J') (M × N) (M' × N') n
The product of partial diffeomorphisms, on the product of their sources.
Instances For
@[simp]
theorem
PartialDiffeomorph.prod_source
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
{E' : Type u_3}
{F : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{H : Type u_6}
{H' : Type u_7}
{G : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace H']
[TopologicalSpace G]
[TopologicalSpace G']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{J' : ModelWithCorners 𝕜 F' G'}
{M : Type u_10}
{M' : Type u_11}
{N : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace N']
[ChartedSpace G' N']
{n : WithTop ℕ∞}
(e : PartialDiffeomorph I I' M M' n)
(f : PartialDiffeomorph J J' N N' n)
:
The source of a product partial diffeomorphism is the product of its sources.
@[simp]
theorem
PartialDiffeomorph.prod_target
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
{E' : Type u_3}
{F : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{H : Type u_6}
{H' : Type u_7}
{G : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace H']
[TopologicalSpace G]
[TopologicalSpace G']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{J' : ModelWithCorners 𝕜 F' G'}
{M : Type u_10}
{M' : Type u_11}
{N : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace N']
[ChartedSpace G' N']
{n : WithTop ℕ∞}
(e : PartialDiffeomorph I I' M M' n)
(f : PartialDiffeomorph J J' N N' n)
:
The target of a product partial diffeomorphism is the product of its targets.
@[simp]
theorem
PartialDiffeomorph.prod_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
{E' : Type u_3}
{F : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{H : Type u_6}
{H' : Type u_7}
{G : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace H']
[TopologicalSpace G]
[TopologicalSpace G']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{J' : ModelWithCorners 𝕜 F' G'}
{M : Type u_10}
{M' : Type u_11}
{N : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace N']
[ChartedSpace G' N']
{n : WithTop ℕ∞}
(e : PartialDiffeomorph I I' M M' n)
(f : PartialDiffeomorph J J' N N' n)
(z : M × N)
:
A product partial diffeomorphism acts componentwise.
@[simp]
theorem
PartialDiffeomorph.prod_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
{E' : Type u_3}
{F : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{H : Type u_6}
{H' : Type u_7}
{G : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace H']
[TopologicalSpace G]
[TopologicalSpace G']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{J' : ModelWithCorners 𝕜 F' G'}
{M : Type u_10}
{M' : Type u_11}
{N : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace N']
[ChartedSpace G' N']
{n : WithTop ℕ∞}
(e : PartialDiffeomorph I I' M M' n)
(f : PartialDiffeomorph J J' N N' n)
:
The inverse of a product is the product of the inverses.
theorem
IsLocalDiffeomorphAt.prodMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
{E' : Type u_3}
{F : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{H : Type u_6}
{H' : Type u_7}
{G : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace H']
[TopologicalSpace G]
[TopologicalSpace G']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{J' : ModelWithCorners 𝕜 F' G'}
{M : Type u_10}
{M' : Type u_11}
{N : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace N']
[ChartedSpace G' N']
{n : WithTop ℕ∞}
{f : M → M'}
{g : N → N'}
{x : M}
{y : N}
(hf : IsLocalDiffeomorphAt I I' n f x)
(hg : IsLocalDiffeomorphAt J J' n g y)
:
The product map is a local diffeomorphism at a pair of points where its factors are.
theorem
IsLocalDiffeomorph.prodMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
{E' : Type u_3}
{F : Type u_4}
{F' : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{H : Type u_6}
{H' : Type u_7}
{G : Type u_8}
{G' : Type u_9}
[TopologicalSpace H]
[TopologicalSpace H']
[TopologicalSpace G]
[TopologicalSpace G']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{J' : ModelWithCorners 𝕜 F' G'}
{M : Type u_10}
{M' : Type u_11}
{N : Type u_12}
{N' : Type u_13}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace M']
[ChartedSpace H' M']
[TopologicalSpace N]
[ChartedSpace G N]
[TopologicalSpace N']
[ChartedSpace G' N']
{n : WithTop ℕ∞}
{f : M → M'}
{g : N → N'}
(hf : IsLocalDiffeomorph I I' n f)
(hg : IsLocalDiffeomorph J J' n g)
:
IsLocalDiffeomorph (I.prod J) (I'.prod J') n (Prod.map f g)
Products of local diffeomorphisms are local diffeomorphisms.