feat(analysis/normed_space/affine_isometry, linear_algebra/affine_space/affine_equiv): restrict affine isometry to isometry equivalence (#17522)

The main result in this commit is `affine_subspace.isometry_equiv_map`: Given an affine isometry, each of its affine subspaces is affine isometry equivalent to its image. `isometry_equiv_map` returns this isometry equivalence.

The two other most significant results that are proved on the way are:
- `affine_subspace.equiv_map_of_injective`: Restricts an injective affine map to an affine equivalence of a subspace to its image (used by `isometry_equiv_map`)
- `affine_equiv.of_bijective`: obtain an affine equivalence from a bijective affine map

The construction uses the new definition `affine_equiv.of_bijective` that makes an affine equivalence of a bijective affine map.

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: datokrat

src/analysis/convex/side.lean

@@ -75,7 +75,7 @@ begin
   rcases hfp₁ with ⟨p₁, hp₁, rfl⟩,
   rcases hfp₂ with ⟨p₂, hp₂, rfl⟩,
   refine ⟨p₁, hp₁, p₂, hp₂, _⟩,
-  simp_rw [←linear_map_vsub, (f.injective_iff_linear_injective.2 hf).same_ray_map_iff] at h,
+  simp_rw [←linear_map_vsub, (f.linear_injective_iff.2 hf).same_ray_map_iff] at h,
   exact h
 end
 
@@ -111,7 +111,7 @@ begin
   rcases hfp₁ with ⟨p₁, hp₁, rfl⟩,
   rcases hfp₂ with ⟨p₂, hp₂, rfl⟩,
   refine ⟨p₁, hp₁, p₂, hp₂, _⟩,
-  simp_rw [←linear_map_vsub, (f.injective_iff_linear_injective.2 hf).same_ray_map_iff] at h,
+  simp_rw [←linear_map_vsub, (f.linear_injective_iff.2 hf).same_ray_map_iff] at h,
   exact h
 end
 

src/analysis/normed_space/add_torsor_bases.lean

@@ -33,7 +33,7 @@ include E
 lemma is_open_map_barycentric_coord [nontrivial ι] (b : affine_basis ι 𝕜 P) (i : ι) :
   is_open_map (b.coord i) :=
 affine_map.is_open_map_linear_iff.mp $ (b.coord i).linear.is_open_map_of_finite_dimensional $
-  (b.coord i).surjective_iff_linear_surjective.mpr (b.surjective_coord i)
+  (b.coord i).linear_surjective_iff.mpr (b.surjective_coord i)
 
 variables [finite_dimensional 𝕜 E] (b : affine_basis ι 𝕜 P)
 

src/analysis/normed_space/affine_isometry.lean

@@ -6,6 +6,7 @@ Authors: Heather Macbeth
 import analysis.normed_space.linear_isometry
 import analysis.normed.group.add_torsor
 import analysis.normed_space.basic
+import linear_algebra.affine_space.restrict
 
 /-!
 # Affine isometries
@@ -587,3 +588,54 @@ begin
   rw this,
   simp only [homeomorph.comp_is_open_map_iff, homeomorph.comp_is_open_map_iff'],
 end
+
+local attribute [instance, nolint fails_quickly] affine_subspace.nonempty_map
+
+include V₁
+omit V
+
+namespace affine_subspace
+
+/--
+An affine subspace is isomorphic to its image under an injective affine map.
+This is the affine version of `submodule.equiv_map_of_injective`.
+-/
+@[simps]
+noncomputable def equiv_map_of_injective (E: affine_subspace 𝕜 P₁) [nonempty E]
+  (φ : P₁ →ᵃ[𝕜] P₂) (hφ : function.injective φ) : E ≃ᵃ[𝕜] E.map φ :=
+{ linear :=
+    (E.direction.equiv_map_of_injective φ.linear (φ.linear_injective_iff.mpr hφ)).trans
+      (linear_equiv.of_eq _ _ (affine_subspace.map_direction _ _).symm),
+  map_vadd' := λ p v, subtype.ext $ φ.map_vadd p v,
+  .. equiv.set.image _ (E : set P₁) hφ }
+
+/--
+Restricts an affine isometry to an affine isometry equivalence between a nonempty affine
+subspace `E` and its image.
+
+This is an isometry version of `affine_subspace.equiv_map`, having a stronger premise and a stronger
+conclusion.
+-/
+noncomputable def isometry_equiv_map
+  (φ : P₁ →ᵃⁱ[𝕜] P₂) (E : affine_subspace 𝕜 P₁) [nonempty E] : E ≃ᵃⁱ[𝕜] E.map φ.to_affine_map :=
+⟨E.equiv_map_of_injective φ.to_affine_map φ.injective, (λ _, φ.norm_map _)⟩
+
+@[simp]
+lemma isometry_equiv_map.apply_symm_apply
+  {E : affine_subspace 𝕜 P₁} [nonempty E]
+  {φ : P₁ →ᵃⁱ[𝕜] P₂} (x : E.map φ.to_affine_map) :
+  φ ((E.isometry_equiv_map φ).symm x) = x :=
+congr_arg coe $ (E.isometry_equiv_map φ).apply_symm_apply _
+
+@[simp]
+lemma isometry_equiv_map.coe_apply
+  (φ : P₁ →ᵃⁱ[𝕜] P₂) (E : affine_subspace 𝕜 P₁) [nonempty E] (g: E) :
+  ↑(E.isometry_equiv_map φ g) = φ g := rfl
+
+@[simp]
+lemma isometry_equiv_map.to_affine_map_eq
+  (φ : P₁ →ᵃⁱ[𝕜] P₂) (E : affine_subspace 𝕜 P₁) [nonempty E] :
+  (E.isometry_equiv_map φ).to_affine_map = E.equiv_map_of_injective φ.to_affine_map φ.injective :=
+rfl
+
+end affine_subspace

src/analysis/normed_space/banach.lean

@@ -250,7 +250,7 @@ lemma _root_.affine_map.is_open_map {P Q : Type*}
   is_open_map f :=
 affine_map.is_open_map_linear_iff.mp $ continuous_linear_map.is_open_map
   { cont := affine_map.continuous_linear_iff.mpr hf, .. f.linear }
-  (f.surjective_iff_linear_surjective.mpr surj)
+  (f.linear_surjective_iff.mpr surj)
 
 /-! ### Applications of the Banach open mapping theorem -/
 

src/linear_algebra/affine_space/affine_equiv.lean

@@ -160,6 +160,16 @@ protected lemma bijective (e : P₁ ≃ᵃ[k] P₂) : bijective e := e.to_equiv.
 protected lemma surjective (e : P₁ ≃ᵃ[k] P₂) : surjective e := e.to_equiv.surjective
 protected lemma injective (e : P₁ ≃ᵃ[k] P₂) : injective e := e.to_equiv.injective
 
+/-- Bijective affine maps are affine isomorphisms. -/
+@[simps]
+noncomputable def of_bijective {φ : P₁ →ᵃ[k] P₂} (hφ : function.bijective φ) : P₁ ≃ᵃ[k] P₂ :=
+{ linear := linear_equiv.of_bijective φ.linear (φ.linear_bijective_iff.mpr hφ),
+  map_vadd' := φ.map_vadd,
+  ..(equiv.of_bijective _ hφ) }
+
+lemma of_bijective.symm_eq {φ : P₁ →ᵃ[k] P₂} (hφ : function.bijective φ) :
+  (of_bijective hφ).symm.to_equiv = (equiv.of_bijective _ hφ).symm := rfl
+
 @[simp] lemma range_eq (e : P₁ ≃ᵃ[k] P₂) : range e = univ := e.surjective.range_eq
 
 @[simp] lemma apply_symm_apply (e : P₁ ≃ᵃ[k] P₂) (p : P₂) : e (e.symm p) = p :=

src/linear_algebra/affine_space/affine_map.lean

@@ -328,7 +328,7 @@ instance : monoid (P1 →ᵃ[k] P1) :=
 
 include V2
 
-@[simp] lemma injective_iff_linear_injective (f : P1 →ᵃ[k] P2) :
+@[simp] lemma linear_injective_iff (f : P1 →ᵃ[k] P2) :
   function.injective f.linear ↔ function.injective f :=
 begin
   obtain ⟨p⟩ := (infer_instance : nonempty P1),
@@ -337,7 +337,7 @@ begin
   rw [h, equiv.comp_injective, equiv.injective_comp],
 end
 
-@[simp] lemma surjective_iff_linear_surjective (f : P1 →ᵃ[k] P2) :
+@[simp] lemma linear_surjective_iff (f : P1 →ᵃ[k] P2) :
   function.surjective f.linear ↔ function.surjective f :=
 begin
   obtain ⟨p⟩ := (infer_instance : nonempty P1),
@@ -346,6 +346,10 @@ begin
   rw [h, equiv.comp_surjective, equiv.surjective_comp],
 end
 
+@[simp] lemma linear_bijective_iff (f : P1 →ᵃ[k] P2) :
+  function.bijective f.linear ↔ function.bijective f :=
+and_congr f.linear_injective_iff f.linear_surjective_iff
+
 lemma image_vsub_image {s t : set P1} (f : P1 →ᵃ[k] P2) :
   (f '' s) -ᵥ (f '' t) = f.linear '' (s -ᵥ t) :=
 begin

src/linear_algebra/affine_space/independent.lean

@@ -365,7 +365,7 @@ begin
   rw affine_independent_iff_linear_independent_vsub k p i at hai,
   simp_rw [affine_independent_iff_linear_independent_vsub k (f ∘ p) i, function.comp_app,
     ← f.linear_map_vsub],
-  have hf' : f.linear.ker = ⊥, { rwa [linear_map.ker_eq_bot, f.injective_iff_linear_injective], },
+  have hf' : f.linear.ker = ⊥, { rwa [linear_map.ker_eq_bot, f.linear_injective_iff], },
   exact linear_independent.map' hai f.linear hf',
 end
 

src/linear_algebra/affine_space/restrict.lean

@@ -99,3 +99,9 @@ begin
   obtain ⟨y, hy, rfl⟩ := hx,
   exact ⟨⟨y, hy⟩, rfl⟩,
 end
+
+lemma affine_map.restrict.bijective
+  {E : affine_subspace k P₁} [nonempty E]
+  {φ : P₁ →ᵃ[k] P₂} (hφ : function.injective φ) :
+  function.bijective (φ.restrict (le_refl (E.map φ))) :=
+⟨affine_map.restrict.injective hφ _, affine_map.restrict.surjective _ rfl⟩