feat(data/fun_like): define embedding_like and equiv_like (#10759)

These extend `fun_like` with a proof of injectivity resp. an inverse.

The number of new generic lemmas is quite low at the moment, so their use is more in defining derived classes such as `mul_equiv_class`.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/algebra/group/freiman.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import algebra.big_operators.multiset
-import data.fun_like
+import data.fun_like.basic
 
 /-!
 # Freiman homomorphisms

src/algebra/group/hom.lean

@@ -6,7 +6,7 @@ Authors: Patrick Massot, Kevin Buzzard, Scott Morrison, Johan Commelin, Chris Hu
 -/
 import algebra.group.commute
 import algebra.group_with_zero.defs
-import data.fun_like
+import data.fun_like.basic
 
 /-!
 # monoid and group homomorphisms

src/data/equiv/basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
+import data.fun_like.equiv
 import data.option.basic
 import data.prod
 import data.quot
@@ -86,31 +87,23 @@ namespace equiv
 /-- `perm α` is the type of bijections from `α` to itself. -/
 @[reducible] def perm (α : Sort*) := equiv α α
 
+instance : equiv_like (α ≃ β) α β :=
+{ coe := to_fun, inv := inv_fun, left_inv := left_inv, right_inv := right_inv,
+  coe_injective' := λ e₁ e₂ h₁ h₂, by { cases e₁, cases e₂, congr' } }
+
 instance : has_coe_to_fun (α ≃ β) (λ _, α → β) := ⟨to_fun⟩
 
 @[simp] theorem coe_fn_mk (f : α → β) (g l r) : (equiv.mk f g l r : α → β) = f :=
 rfl
 
 /-- The map `coe_fn : (r ≃ s) → (r → s)` is injective. -/
-theorem coe_fn_injective : @function.injective (α ≃ β) (α → β) coe_fn
-| ⟨f₁, g₁, l₁, r₁⟩ ⟨f₂, g₂, l₂, r₂⟩ h :=
-  have f₁ = f₂, from h,
-  have g₁ = g₂, from l₁.eq_right_inverse (this.symm ▸ r₂),
-  by simp *
-
-@[simp, norm_cast] protected lemma coe_inj {e₁ e₂ : α ≃ β} : (e₁ : α → β) = e₂ ↔ e₁ = e₂ :=
-coe_fn_injective.eq_iff
-
-@[ext] lemma ext {f g : equiv α β} (H : ∀ x, f x = g x) : f = g :=
-coe_fn_injective (funext H)
-
-protected lemma congr_arg {f : equiv α β} : Π {x x' : α}, x = x' → f x = f x'
-| _ _ rfl := rfl
-
-protected lemma congr_fun {f g : equiv α β} (h : f = g) (x : α) : f x = g x := h ▸ rfl
-
-lemma ext_iff {f g : equiv α β} : f = g ↔ ∀ x, f x = g x :=
-⟨λ h x, h ▸ rfl, ext⟩
+theorem coe_fn_injective : @function.injective (α ≃ β) (α → β) coe_fn := fun_like.coe_injective
+protected lemma coe_inj {e₁ e₂ : α ≃ β} : (e₁ : α → β) = e₂ ↔ e₁ = e₂ := fun_like.coe_fn_eq
+@[ext] lemma ext {f g : equiv α β} (H : ∀ x, f x = g x) : f = g := fun_like.ext f g H
+protected lemma congr_arg {f : equiv α β} {x x' : α} : x = x' → f x = f x' := fun_like.congr_arg f
+protected lemma congr_fun {f g : equiv α β} (h : f = g) (x : α) : f x = g x :=
+fun_like.congr_fun h x
+lemma ext_iff {f g : equiv α β} : f = g ↔ ∀ x, f x = g x := fun_like.ext_iff
 
 @[ext] lemma perm.ext {σ τ : equiv.perm α} (H : ∀ x, σ x = τ x) : σ = τ :=
 equiv.ext H
@@ -151,14 +144,9 @@ lemma to_fun_as_coe (e : α ≃ β) : e.to_fun = e := rfl
 @[simp]
 lemma inv_fun_as_coe (e : α ≃ β) : e.inv_fun = e.symm := rfl
 
-protected theorem injective (e : α ≃ β) : injective e :=
-e.left_inv.injective
-
-protected theorem surjective (e : α ≃ β) : surjective e :=
-e.right_inv.surjective
-
-protected theorem bijective (f : α ≃ β) : bijective f :=
-⟨f.injective, f.surjective⟩
+protected theorem injective (e : α ≃ β) : injective e := equiv_like.injective e
+protected theorem surjective (e : α ≃ β) : surjective e := equiv_like.surjective e
+protected theorem bijective (e : α ≃ β) : bijective e := equiv_like.bijective e
 
 protected theorem subsingleton (e : α ≃ β) [subsingleton β] : subsingleton α :=
 e.injective.subsingleton
@@ -236,8 +224,7 @@ e.left_inv x
 -- `simp` will always rewrite with `equiv.symm_symm` before this has a chance to fire.
 @[simp, nolint simp_nf] theorem symm_symm_apply (f : α ≃ β) (b : α) : f.symm.symm b = f b := rfl
 
-@[simp] theorem apply_eq_iff_eq (f : α ≃ β) {x y : α} : f x = f y ↔ x = y :=
-f.injective.eq_iff
+theorem apply_eq_iff_eq (f : α ≃ β) {x y : α} : f x = f y ↔ x = y := equiv_like.apply_eq_iff_eq f
 
 theorem apply_eq_iff_eq_symm_apply {α β : Sort*} (f : α ≃ β) {x : α} {y : β} :
   f x = y ↔ x = f.symm y :=
@@ -285,23 +272,23 @@ theorem left_inverse_symm (f : equiv α β) : left_inverse f.symm f := f.left_in
 
 theorem right_inverse_symm (f : equiv α β) : function.right_inverse f.symm f := f.right_inv
 
-@[simp] lemma injective_comp (e : α ≃ β) (f : β → γ) : injective (f ∘ e) ↔ injective f :=
-injective.of_comp_iff' f e.bijective
+lemma injective_comp (e : α ≃ β) (f : β → γ) : injective (f ∘ e) ↔ injective f :=
+equiv_like.injective_comp e f
 
-@[simp] lemma comp_injective (f : α → β) (e : β ≃ γ) : injective (e ∘ f) ↔ injective f :=
-e.injective.of_comp_iff f
+lemma comp_injective (f : α → β) (e : β ≃ γ) : injective (e ∘ f) ↔ injective f :=
+equiv_like.comp_injective f e
 
-@[simp] lemma surjective_comp (e : α ≃ β) (f : β → γ) : surjective (f ∘ e) ↔ surjective f :=
-e.surjective.of_comp_iff f
+lemma surjective_comp (e : α ≃ β) (f : β → γ) : surjective (f ∘ e) ↔ surjective f :=
+equiv_like.surjective_comp e f
 
-@[simp] lemma comp_surjective (f : α → β) (e : β ≃ γ) : surjective (e ∘ f) ↔ surjective f :=
-surjective.of_comp_iff' e.bijective f
+lemma comp_surjective (f : α → β) (e : β ≃ γ) : surjective (e ∘ f) ↔ surjective f :=
+equiv_like.comp_surjective f e
 
-@[simp] lemma bijective_comp (e : α ≃ β) (f : β → γ) : bijective (f ∘ e) ↔ bijective f :=
-e.bijective.of_comp_iff f
+lemma bijective_comp (e : α ≃ β) (f : β → γ) : bijective (f ∘ e) ↔ bijective f :=
+equiv_like.bijective_comp e f
 
-@[simp] lemma comp_bijective (f : α → β) (e : β ≃ γ) : bijective (e ∘ f) ↔ bijective f :=
-bijective.of_comp_iff' e.bijective f
+lemma comp_bijective (f : α → β) (e : β ≃ γ) : bijective (e ∘ f) ↔ bijective f :=
+equiv_like.comp_bijective f e
 
 /-- If `α` is equivalent to `β` and `γ` is equivalent to `δ`, then the type of equivalences `α ≃ γ`
 is equivalent to the type of equivalences `β ≃ δ`. -/

src/data/fun_like.lean → src/data/fun_like/basic.lean

@@ -25,7 +25,7 @@ namespace my_hom
 
 variables (A B : Type*) [my_class A] [my_class B]
 
--- This instance is optional if you follow the "Hom class" design below:
+-- This instance is optional if you follow the "morphism class" design below:
 instance : fun_like (my_hom A B) A (λ _, B) :=
 { coe := my_hom.to_fun, coe_injective' := λ f g h, by cases f; cases g; congr' }
 
@@ -48,7 +48,7 @@ end my_hom
 This file will then provide a `has_coe_to_fun` instance and various
 extensionality and simp lemmas.
 
-## Hom classes extending `fun_like`
+## Morphism classes extending `fun_like`
 
 The `fun_like` design provides further benefits if you put in a bit more work.
 The first step is to extend `fun_like` to create a class of those types satisfying
@@ -66,7 +66,7 @@ class my_hom_class (F : Type*) (A B : out_param $ Type*) [my_class A] [my_class
   (f : F) (x y : A) : f (my_class.op x y) = my_class.op (f x) (f y) :=
 my_hom_class.map_op
 
--- You can replace `my_hom.fun_like` with the below instance, or keep both:
+-- You can replace `my_hom.fun_like` with the below instance:
 instance : my_hom_class (my_hom A B) A B :=
 { coe := my_hom.to_fun,
   coe_injective' := λ f g h, by cases f; cases g; congr',

src/data/fun_like/embedding.lean

@@ -0,0 +1,147 @@
+/-
+Copyright (c) 2021 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+
+import data.fun_like.basic
+
+/-!
+# Typeclass for a type `F` with an injective map to `A ↪ B`
+
+This typeclass is primarily for use by embeddings such as `rel_embedding`.
+
+## Basic usage of `embedding_like`
+
+A typical type of embedding should be declared as:
+```
+structure my_embedding (A B : Type*) [my_class A] [my_class B] :=
+(to_fun : A → B)
+(injective' : function.injective to_fun)
+(map_op' : ∀ {x y : A}, to_fun (my_class.op x y) = my_class.op (to_fun x) (to_fun y))
+
+namespace my_embedding
+
+variables (A B : Type*) [my_class A] [my_class B]
+
+-- This instance is optional if you follow the "Embedding class" design below:
+instance : embedding_like (my_embedding A B) A B :=
+{ coe := my_embedding.to_fun,
+  coe_injective' := λ f g h, by cases f; cases g; congr',
+  injective' := my_embedding.injective' }
+
+/-- Helper instance for when there's too many metavariables to directly
+apply `fun_like.to_coe_fn`. -/
+instance : has_coe_to_fun (my_embedding A B) (λ _, A → B) := ⟨my_embedding.to_fun⟩
+
+@[simp] lemma to_fun_eq_coe {f : my_embedding A B} : f.to_fun = (f : A → B) := rfl
+
+@[ext] theorem ext {f g : my_embedding A B} (h : ∀ x, f x = g x) : f = g := fun_like.ext f g h
+
+/-- Copy of a `my_embedding` with a new `to_fun` equal to the old one. Useful to fix definitional
+equalities. -/
+protected def copy (f : my_embedding A B) (f' : A → B) (h : f' = ⇑f) : my_embedding A B :=
+{ to_fun := f',
+  injective' := h.symm ▸ f.injective',
+  map_op' := h.symm ▸ f.map_op' }
+
+end my_embedding
+```
+
+This file will then provide a `has_coe_to_fun` instance and various
+extensionality and simp lemmas.
+
+## Embedding classes extending `embedding_like`
+
+The `embedding_like` design provides further benefits if you put in a bit more work.
+The first step is to extend `embedding_like` to create a class of those types satisfying
+the axioms of your new type of morphisms.
+Continuing the example above:
+
+```
+/-- `my_embedding_class F A B` states that `F` is a type of `my_class.op`-preserving embeddings.
+You should extend this class when you extend `my_embedding`. -/
+class my_embedding_class (F : Type*) (A B : out_param $ Type*) [my_class A] [my_class B]
+  extends embedding_like F A B :=
+(map_op : ∀ (f : F) (x y : A), f (my_class.op x y) = my_class.op (f x) (f y))
+
+@[simp] lemma map_op {F A B : Type*} [my_class A] [my_class B] [my_embedding_class F A B]
+  (f : F) (x y : A) : f (my_class.op x y) = my_class.op (f x) (f y) :=
+my_embedding_class.map_op
+
+-- You can replace `my_embedding.embedding_like` with the below instance:
+instance : my_embedding_class (my_embedding A B) A B :=
+{ coe := my_embedding.to_fun,
+  coe_injective' := λ f g h, by cases f; cases g; congr',
+  injective' := my_embedding.injective',
+  map_op := my_embedding.map_op' }
+
+-- [Insert `has_coe_to_fun`, `to_fun_eq_coe`, `ext` and `copy` here]
+```
+
+The second step is to add instances of your new `my_embedding_class` for all types extending
+`my_embedding`.
+Typically, you can just declare a new class analogous to `my_embedding_class`:
+
+```
+structure cooler_embedding (A B : Type*) [cool_class A] [cool_class B]
+  extends my_embedding A B :=
+(map_cool' : to_fun cool_class.cool = cool_class.cool)
+
+class cooler_embedding_class (F : Type*) (A B : out_param $ Type*) [cool_class A] [cool_class B]
+  extends my_embedding_class F A B :=
+(map_cool : ∀ (f : F), f cool_class.cool = cool_class.cool)
+
+@[simp] lemma map_cool {F A B : Type*} [cool_class A] [cool_class B] [cooler_embedding_class F A B]
+  (f : F) : f cool_class.cool = cool_class.cool :=
+my_embedding_class.map_op
+
+-- You can also replace `my_embedding.embedding_like` with the below instance:
+instance : cool_embedding_class (cool_embedding A B) A B :=
+{ coe := cool_embedding.to_fun,
+  coe_injective' := λ f g h, by cases f; cases g; congr',
+  injective' := my_embedding.injective',
+  map_op := cool_embedding.map_op',
+  map_cool := cool_embedding.map_cool' }
+
+-- [Insert `has_coe_to_fun`, `to_fun_eq_coe`, `ext` and `copy` here]
+```
+
+Then any declaration taking a specific type of morphisms as parameter can instead take the
+class you just defined:
+```
+-- Compare with: lemma do_something (f : my_embedding A B) : sorry := sorry
+lemma do_something {F : Type*} [my_embedding_class F A B] (f : F) : sorry := sorry
+```
+
+This means anything set up for `my_embedding`s will automatically work for `cool_embedding_class`es,
+and defining `cool_embedding_class` only takes a constant amount of effort,
+instead of linearly increasing the work per `my_embedding`-related declaration.
+
+-/
+
+/-- The class `embedding_like F α β` expresses that terms of type `F` have an
+injective coercion to injective functions `α ↪ β`.
+-/
+class embedding_like (F : Sort*) (α β : out_param Sort*)
+  extends fun_like F α (λ _, β) :=
+(injective' : ∀ (f : F), @function.injective α β (coe f))
+
+namespace embedding_like
+
+variables {F α β γ : Sort*} [i : embedding_like F α β]
+
+include i
+
+protected lemma injective (f : F) : function.injective f := injective' f
+
+@[simp] lemma apply_eq_iff_eq (f : F) {x y : α} : f x = f y ↔ x = y :=
+(embedding_like.injective f).eq_iff
+
+omit i
+
+@[simp] lemma comp_injective {F : Sort*} [embedding_like F β γ] (f : α → β) (e : F) :
+  function.injective (e ∘ f) ↔ function.injective f :=
+(embedding_like.injective e).of_comp_iff f
+
+end embedding_like