refactor(linear_algebra/affine_space/affine_{map,equiv}): add fun_lik…

…e instances (#18575)

Going all the way and defining a new `affine_map_class` class can wait till after the port; but adding `fun_like` makes the port easier.

This has to reorder a few declarations in `affine_equiv.lean`.
The only new declarations are the new instances.

src/linear_algebra/affine_space/affine_equiv.lean

@@ -59,36 +59,15 @@ namespace affine_equiv
 
 include V₁ V₂
 
-instance : has_coe_to_fun (P₁ ≃ᵃ[k] P₂) (λ _, P₁ → P₂) := ⟨λ e, e.to_fun⟩
-
-instance : has_coe (P₁ ≃ᵃ[k] P₂) (P₁ ≃ P₂) := ⟨affine_equiv.to_equiv⟩
-
-variables {k P₁}
-
-@[simp] lemma map_vadd (e : P₁ ≃ᵃ[k] P₂) (p : P₁) (v : V₁) : e (v +ᵥ p) = e.linear v +ᵥ e p :=
-e.map_vadd' p v
-
-@[simp] lemma coe_to_equiv (e : P₁ ≃ᵃ[k] P₂) : ⇑e.to_equiv = e := rfl
-
 /-- Reinterpret an `affine_equiv` as an `affine_map`. -/
-def to_affine_map (e : P₁ ≃ᵃ[k] P₂) : P₁ →ᵃ[k] P₂ := { to_fun := e, .. e }
-
-instance : has_coe (P₁ ≃ᵃ[k] P₂) (P₁ →ᵃ[k] P₂) := ⟨to_affine_map⟩
-
-@[simp] lemma coe_to_affine_map (e : P₁ ≃ᵃ[k] P₂) :
-  (e.to_affine_map : P₁ → P₂) = (e : P₁ → P₂) :=
-rfl
+def to_affine_map (e : P₁ ≃ᵃ[k] P₂) : P₁ →ᵃ[k] P₂ := { .. e }
 
 @[simp] lemma to_affine_map_mk (f : P₁ ≃ P₂) (f' : V₁ ≃ₗ[k] V₂) (h) :
   to_affine_map (mk f f' h) = ⟨f, f', h⟩ :=
 rfl
 
-@[norm_cast, simp] lemma coe_coe (e : P₁ ≃ᵃ[k] P₂) : ((e : P₁ →ᵃ[k] P₂) : P₁ → P₂) = e := rfl
-
 @[simp] lemma linear_to_affine_map (e : P₁ ≃ᵃ[k] P₂) : e.to_affine_map.linear = e.linear := rfl
 
-@[simp] lemma coe_linear (e : P₁ ≃ᵃ[k] P₂) : (e : P₁ →ᵃ[k] P₂).linear = e.linear := rfl
-
 lemma to_affine_map_injective : injective (to_affine_map : (P₁ ≃ᵃ[k] P₂) → (P₁ →ᵃ[k] P₂)) :=
 begin
   rintros ⟨e, el, h⟩ ⟨e', el', h'⟩ H,
@@ -101,11 +80,39 @@ end
   e.to_affine_map = e'.to_affine_map ↔ e = e' :=
 to_affine_map_injective.eq_iff
 
+instance equiv_like : equiv_like (P₁ ≃ᵃ[k] P₂) P₁ P₂ :=
+{ coe := λ f, f.to_fun,
+  inv := λ f, f.inv_fun,
+  left_inv := λ f, f.left_inv,
+  right_inv := λ f, f.right_inv,
+  coe_injective' := λ f g h _, to_affine_map_injective (fun_like.coe_injective h) }
+
+instance : has_coe_to_fun (P₁ ≃ᵃ[k] P₂) (λ _, P₁ → P₂) := fun_like.has_coe_to_fun
+
+instance : has_coe (P₁ ≃ᵃ[k] P₂) (P₁ ≃ P₂) := ⟨affine_equiv.to_equiv⟩
+
+variables {k P₁}
+
+@[simp] lemma map_vadd (e : P₁ ≃ᵃ[k] P₂) (p : P₁) (v : V₁) : e (v +ᵥ p) = e.linear v +ᵥ e p :=
+e.map_vadd' p v
+
+@[simp] lemma coe_to_equiv (e : P₁ ≃ᵃ[k] P₂) : ⇑e.to_equiv = e := rfl
+
+instance : has_coe (P₁ ≃ᵃ[k] P₂) (P₁ →ᵃ[k] P₂) := ⟨to_affine_map⟩
+
+@[simp] lemma coe_to_affine_map (e : P₁ ≃ᵃ[k] P₂) :
+  (e.to_affine_map : P₁ → P₂) = (e : P₁ → P₂) :=
+rfl
+
+@[norm_cast, simp] lemma coe_coe (e : P₁ ≃ᵃ[k] P₂) : ((e : P₁ →ᵃ[k] P₂) : P₁ → P₂) = e := rfl
+
+@[simp] lemma coe_linear (e : P₁ ≃ᵃ[k] P₂) : (e : P₁ →ᵃ[k] P₂).linear = e.linear := rfl
+
 @[ext] lemma ext {e e' : P₁ ≃ᵃ[k] P₂} (h : ∀ x, e x = e' x) : e = e' :=
-to_affine_map_injective $ affine_map.ext h
+fun_like.ext _ _ h
 
 lemma coe_fn_injective : @injective (P₁ ≃ᵃ[k] P₂) (P₁ → P₂) coe_fn :=
-λ e e' H, ext $ congr_fun H
+fun_like.coe_injective
 
 @[simp, norm_cast] lemma coe_fn_inj {e e' : P₁ ≃ᵃ[k] P₂} : (e : P₁ → P₂) = e' ↔ e = e' :=
 coe_fn_injective.eq_iff

src/linear_algebra/affine_space/affine_map.lean

@@ -59,11 +59,24 @@ structure affine_map (k : Type*) {V1 : Type*} (P1 : Type*) {V2 : Type*} (P2 : Ty
 
 notation P1 ` →ᵃ[`:25 k:25 `] `:0 P2:0 := affine_map k P1 P2
 
-instance (k : Type*) {V1 : Type*} (P1 : Type*) {V2 : Type*} (P2 : Type*)
-    [ring k]
-    [add_comm_group V1] [module k V1] [affine_space V1 P1]
-    [add_comm_group V2] [module k V2] [affine_space V2 P2]:
-    has_coe_to_fun (P1 →ᵃ[k] P2) (λ _, P1 → P2) := ⟨affine_map.to_fun⟩
+instance affine_map.fun_like (k : Type*) {V1 : Type*} (P1 : Type*) {V2 : Type*} (P2 : Type*)
+  [ring k]
+  [add_comm_group V1] [module k V1] [affine_space V1 P1]
+  [add_comm_group V2] [module k V2] [affine_space V2 P2]:
+  fun_like (P1 →ᵃ[k] P2) P1 (λ _, P2) :=
+{ coe := affine_map.to_fun,
+  coe_injective' := λ ⟨f, f_linear, f_add⟩ ⟨g, g_linear, g_add⟩ (h : f = g), begin
+    cases (add_torsor.nonempty : nonempty P1) with p,
+    congr' with v,
+    apply vadd_right_cancel (f p),
+    erw [← f_add, h, ← g_add]
+  end }
+
+instance affine_map.has_coe_to_fun (k : Type*) {V1 : Type*} (P1 : Type*) {V2 : Type*} (P2 : Type*)
+  [ring k]
+  [add_comm_group V1] [module k V1] [affine_space V1 P1]
+  [add_comm_group V2] [module k V2] [affine_space V2 P2] :
+  has_coe_to_fun (P1 →ᵃ[k] P2) (λ _, P1 → P2) := fun_like.has_coe_to_fun
 
 namespace linear_map
 
@@ -115,20 +128,12 @@ by conv_rhs { rw [←vsub_vadd p1 p2, map_vadd, vadd_vsub] }
 
 /-- Two affine maps are equal if they coerce to the same function. -/
 @[ext] lemma ext {f g : P1 →ᵃ[k] P2} (h : ∀ p, f p = g p) : f = g :=
-begin
-  rcases f with ⟨f, f_linear, f_add⟩,
-  rcases g with ⟨g, g_linear, g_add⟩,
-  obtain rfl : f = g := funext h,
-  congr' with v,
-  cases (add_torsor.nonempty : nonempty P1) with p,
-  apply vadd_right_cancel (f p),
-  erw [← f_add, ← g_add]
-end
+fun_like.ext _ _ h
 
 lemma ext_iff {f g : P1 →ᵃ[k] P2} : f = g ↔ ∀ p, f p = g p := ⟨λ h p, h ▸ rfl, ext⟩
 
 lemma coe_fn_injective : @function.injective (P1 →ᵃ[k] P2) (P1 → P2) coe_fn :=
-λ f g H, ext $ congr_fun H
+fun_like.coe_injective
 
 protected lemma congr_arg (f : P1 →ᵃ[k] P2) {x y : P1} (h : x = y) : f x = f y :=
 congr_arg _ h

src/topology/algebra/continuous_affine_map.lean

@@ -45,30 +45,34 @@ variables [add_comm_group W] [module R W] [topological_space Q] [add_torsor W Q]
 
 include V W
 
-/-- see Note [function coercion] -/
-instance : has_coe_to_fun (P →A[R] Q) (λ _, P → Q) := ⟨λ f, f.to_affine_map.to_fun⟩
+instance : has_coe (P →A[R] Q) (P →ᵃ[R] Q) :=
+⟨to_affine_map⟩
+
+lemma to_affine_map_injective {f g : P →A[R] Q} (h : (f : P →ᵃ[R] Q) = (g : P →ᵃ[R] Q)) : f = g :=
+by { cases f, cases g, congr' }
+
+instance : continuous_map_class (P →A[R] Q) P Q :=
+{ coe := λ f, f.to_affine_map,
+  coe_injective' := λ f g h, to_affine_map_injective $ fun_like.coe_injective h,
+  map_continuous := cont }
+
+/-- Helper instance for when there's too many metavariables to apply
+`fun_like.has_coe_to_fun` directly. -/
+instance : has_coe_to_fun (P →A[R] Q) (λ _, P → Q) := fun_like.has_coe_to_fun
 
 lemma to_fun_eq_coe (f : P →A[R] Q) : f.to_fun = ⇑f := rfl
 
-lemma coe_injective :
-  @function.injective (P →A[R] Q) (P → Q) coe_fn :=
-begin
-  rintros ⟨⟨f, ⟨f', hf₁, hf₂⟩, hf₀⟩, hf₁⟩ ⟨⟨g, ⟨g', hg₁, hg₂⟩, hg₀⟩, hg₁⟩ h,
-  have : f = g ∧ f' = g', { simpa only using affine_map.coe_fn_injective h, },
-  congr,
-  exacts [this.1, this.2],
-end
+lemma coe_injective : @function.injective (P →A[R] Q) (P → Q) coe_fn :=
+fun_like.coe_injective
 
 @[ext] lemma ext {f g : P →A[R] Q} (h : ∀ x, f x = g x) : f = g :=
-coe_injective $ funext h
+fun_like.ext _ _ h
 
 lemma ext_iff {f g : P →A[R] Q} : f = g ↔ ∀ x, f x = g x :=
-⟨by { rintro rfl x, refl, }, ext⟩
+fun_like.ext_iff
 
-lemma congr_fun {f g : P →A[R] Q} (h : f = g) (x : P) : f x = g x := h ▸ rfl
-
-instance : has_coe (P →A[R] Q) (P →ᵃ[R] Q) :=
-⟨to_affine_map⟩
+lemma congr_fun {f g : P →A[R] Q} (h : f = g) (x : P) : f x = g x :=
+fun_like.congr_fun h _
 
 /-- Forgetting its algebraic properties, a continuous affine map is a continuous map. -/
 def to_continuous_map (f : P →A[R] Q) : C(P, Q) :=
@@ -92,10 +96,6 @@ rfl
   ((f : C(P, Q)) : P → Q) = f :=
 rfl
 
-lemma to_affine_map_injective {f g : P →A[R] Q}
-  (h : (f : P →ᵃ[R] Q) = (g : P →ᵃ[R] Q)) : f = g :=
-by { ext a, exact affine_map.congr_fun h a, }
-
 lemma to_continuous_map_injective {f g : P →A[R] Q}
   (h : (f : C(P, Q)) = (g : C(P, Q))) : f = g :=
 by { ext a, exact continuous_map.congr_fun h a, }