feat(analysis/normed_space/banach): open mapping theorem for maps between affine spaces (#9540)

Formalized as part of the Sphere Eversion project.

Author: ocfnash

src/analysis/normed_space/banach.lean

@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 import topology.metric_space.baire
 import analysis.normed_space.operator_norm
+import analysis.normed_space.affine_isometry
 
 /-!
 # Banach open mapping theorem
@@ -239,6 +240,17 @@ begin
   exact set.mem_image_of_mem _ (hε this)
 end
 
+lemma open_mapping_affine {P Q : Type*}
+  [metric_space P] [normed_add_torsor E P] [metric_space Q] [normed_add_torsor F Q]
+  {f : P →ᵃ[𝕜] Q} (hf : continuous f) (surj : surjective f) :
+  is_open_map f :=
+begin
+  rw ← affine_map.is_open_map_linear_iff,
+  exact open_mapping
+    { cont := affine_map.continuous_linear_iff.mpr hf, .. f.linear }
+    (f.surjective_iff_linear_surjective.mpr surj),
+end
+
 /-! ### Applications of the Banach open mapping theorem -/
 
 namespace continuous_linear_map

src/linear_algebra/affine_space/affine_map.lean

@@ -293,13 +293,19 @@ include V2
 @[simp] lemma injective_iff_linear_injective (f : P1 →ᵃ[k] P2) :
   function.injective f.linear ↔ function.injective f :=
 begin
-  split; intros hf x y hxy,
-  { rw [← @vsub_eq_zero_iff_eq V1, ← @submodule.mem_bot k V1, ← linear_map.ker_eq_bot.mpr hf,
-      linear_map.mem_ker, affine_map.linear_map_vsub, hxy, vsub_self], },
-  { obtain ⟨p⟩ := (by apply_instance : nonempty P1),
-    have hxy' : (f.linear x) +ᵥ f p = (f.linear y) +ᵥ f p, { rw hxy, },
-    rw [← f.map_vadd, ← f.map_vadd] at hxy',
-    exact (vadd_right_cancel_iff _).mp (hf hxy'), },
+  obtain ⟨p⟩ := (infer_instance : nonempty P1),
+  have h : ⇑f.linear = (equiv.vadd_const (f p)).symm ∘ f ∘ (equiv.vadd_const p),
+  { ext v, simp [f.map_vadd, vadd_vsub_assoc], },
+  rw [h, equiv.comp_injective, equiv.injective_comp],
+end
+
+@[simp] lemma surjective_iff_linear_surjective (f : P1 →ᵃ[k] P2) :
+  function.surjective f.linear ↔ function.surjective f :=
+begin
+  obtain ⟨p⟩ := (infer_instance : nonempty P1),
+  have h : ⇑f.linear = (equiv.vadd_const (f p)).symm ∘ f ∘ (equiv.vadd_const p),
+  { ext v, simp [f.map_vadd, vadd_vsub_assoc], },
+  rw [h, equiv.comp_surjective, equiv.surjective_comp],
 end
 
 omit V2