Isometries of products of Riemannian manifolds

For the product metric on M × N (TauCeti.Geometry.Manifold.Riemannian.Prod.Basic), the product Φ × Ψ of Riemannian isometries is again a Riemannian isometry. Products of self-isometries give a group homomorphism Isom(M) × Isom(N) → Isom(M × N), injective when both factors are nonempty. Consequently a product of homogeneous Riemannian manifolds is homogeneous: if Isom(M) acts transitively on M and Isom(N) on N, then Isom(M × N) acts transitively on M × N. This is how the product model geometries S² × ℝ and ℍ² × ℝ among Thurston's eight inherit their homogeneity from their factors.

Main definitions

• TauCeti.RiemannianIsometry.prodCongr: the product of two Riemannian isometries.
• TauCeti.RiemannianIsometry.prodCongrHom: the homomorphism Isom(M) × Isom(N) → Isom(M × N).

Main results

• TauCeti.RiemannianIsometry.prodCongrHom_injective: the homomorphism is injective when M and N are nonempty.
• TauCeti.RiemannianIsometry.isPretransitive_prod: a product of homogeneous Riemannian manifolds is homogeneous.

References

• P. Scott, The geometries of 3-manifolds, Bull. London Math. Soc. 15 (1983) 401–487 (the product geometries S² × ℝ and ℍ² × ℝ).

def TauCeti.RiemannianIsometry.prodCongr {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_8} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_9} [TopologicalSpace M'] [ChartedSpace H' M'] [Bundle.RiemannianBundle fun (x : M') => TangentSpace I' x] {F' : Type u_10} [NormedAddCommGroup F'] [NormedSpace ℝ F'] {G' : Type u_11} [TopologicalSpace G'] {J' : ModelWithCorners ℝ F' G'} {N' : Type u_12} [TopologicalSpace N'] [ChartedSpace G' N'] [Bundle.RiemannianBundle fun (y : N') => TangentSpace J' y] (Φ : RiemannianIsometry I I' M M') (Ψ : RiemannianIsometry J J' N N') : RiemannianIsometry (I.prod J) (I'.prod J') (M × N) (M' × N')

The product Φ × Ψ of two Riemannian isometries is a Riemannian isometry between the products, for the product metrics.

@[simp]

theorem TauCeti.RiemannianIsometry.coe_prodCongr {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_8} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_9} [TopologicalSpace M'] [ChartedSpace H' M'] [Bundle.RiemannianBundle fun (x : M') => TangentSpace I' x] {F' : Type u_10} [NormedAddCommGroup F'] [NormedSpace ℝ F'] {G' : Type u_11} [TopologicalSpace G'] {J' : ModelWithCorners ℝ F' G'} {N' : Type u_12} [TopologicalSpace N'] [ChartedSpace G' N'] [Bundle.RiemannianBundle fun (y : N') => TangentSpace J' y] (Φ : RiemannianIsometry I I' M M') (Ψ : RiemannianIsometry J J' N N') : ⇑(Φ.prodCongr Ψ) = Prod.map ⇑Φ ⇑Ψ

theorem TauCeti.RiemannianIsometry.prodCongr_apply {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_8} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_9} [TopologicalSpace M'] [ChartedSpace H' M'] [Bundle.RiemannianBundle fun (x : M') => TangentSpace I' x] {F' : Type u_10} [NormedAddCommGroup F'] [NormedSpace ℝ F'] {G' : Type u_11} [TopologicalSpace G'] {J' : ModelWithCorners ℝ F' G'} {N' : Type u_12} [TopologicalSpace N'] [ChartedSpace G' N'] [Bundle.RiemannianBundle fun (y : N') => TangentSpace J' y] (Φ : RiemannianIsometry I I' M M') (Ψ : RiemannianIsometry J J' N N') (p : M × N) : (Φ.prodCongr Ψ) p = (Φ p.1, Ψ p.2)

@[simp]

theorem TauCeti.RiemannianIsometry.toDiffeomorph_prodCongr {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_8} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_9} [TopologicalSpace M'] [ChartedSpace H' M'] [Bundle.RiemannianBundle fun (x : M') => TangentSpace I' x] {G'' : Type u_13} [TopologicalSpace G''] {J'' : ModelWithCorners ℝ F G''} {N'' : Type u_14} [TopologicalSpace N''] [ChartedSpace G'' N''] [Bundle.RiemannianBundle fun (y : N'') => TangentSpace J'' y] (Φ : RiemannianIsometry I I' M M') (Ψ : RiemannianIsometry J J'' N N'') : (Φ.prodCongr Ψ).toDiffeomorph = Φ.prodCongr Ψ.toDiffeomorph

When N and N' share a model vector space, the underlying diffeomorphism of a product of isometries is Mathlib's product of diffeomorphisms.

@[simp]

theorem TauCeti.RiemannianIsometry.prodCongr_symm {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_8} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_9} [TopologicalSpace M'] [ChartedSpace H' M'] [Bundle.RiemannianBundle fun (x : M') => TangentSpace I' x] {F' : Type u_10} [NormedAddCommGroup F'] [NormedSpace ℝ F'] {G' : Type u_11} [TopologicalSpace G'] {J' : ModelWithCorners ℝ F' G'} {N' : Type u_12} [TopologicalSpace N'] [ChartedSpace G' N'] [Bundle.RiemannianBundle fun (y : N') => TangentSpace J' y] (Φ : RiemannianIsometry I I' M M') (Ψ : RiemannianIsometry J J' N N') : (Φ.prodCongr Ψ).symm = Φ.symm.prodCongr Ψ.symm

The inverse of a product of isometries is the product of the inverses.

@[simp]

theorem TauCeti.RiemannianIsometry.refl_prodCongr_refl {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] : (RiemannianIsometry.refl I M).prodCongr (RiemannianIsometry.refl J N) = RiemannianIsometry.refl (I.prod J) (M × N)

The product of identity isometries is the identity isometry.

def TauCeti.RiemannianIsometry.prodCongrHom {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [TopologicalSpace G] (J : ModelWithCorners ℝ F G) (N : Type u_6) [TopologicalSpace N] [ChartedSpace G N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] : Isom I M × Isom J N →* Isom (I.prod J) (M × N)

Products of isometries give a group homomorphism Isom(M) × Isom(N) → Isom(M × N).

@[simp]

theorem TauCeti.RiemannianIsometry.prodCongrHom_apply {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] (Φ : Isom I M × Isom J N) : (prodCongrHom I M J N) Φ = prodCongr Φ.1 Φ.2

theorem TauCeti.RiemannianIsometry.prodCongrHom_injective {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [Nonempty M] [Nonempty N] : Function.Injective ⇑(prodCongrHom I M J N)

When both factors are nonempty, distinct pairs of isometries give distinct products.

instance TauCeti.RiemannianIsometry.isPretransitive_prod {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [MulAction.IsPretransitive (Isom I M) M] [MulAction.IsPretransitive (Isom J N) N] : MulAction.IsPretransitive (Isom (I.prod J) (M × N)) (M × N)

A product of homogeneous Riemannian manifolds is homogeneous: if the isometry groups of M and of N act transitively, then so does the isometry group of M × N, already through products of isometries.