# Typeclass for a type `F` with an injective map to `A ≃ B` #

This typeclass is primarily for use by isomorphisms like `MonoidEquiv` and `LinearEquiv`.

## Basic usage of `EquivLike` #

A typical type of isomorphisms should be declared as:

    structure MyIso (A B : Type*) [MyClass A] [MyClass B] extends Equiv A B where
      (map_op' : ∀ (x y : A), toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))

    namespace MyIso

    variable (A B : Type*) [MyClass A] [MyClass B]

    instance instEquivLike : EquivLike (MyIso A B) A B where
      coe f := f.toFun
      inv f := f.invFun
      left_inv f := f.left_inv
      right_inv f := f.right_inv
      coe_injective' f g h₁ h₂ := by cases f; cases g; congr; exact EquivLike.coe_injective' _ _ h₁ h₂

    @[ext] theorem ext {f g : MyIso A B} (h : ∀ x, f x = g x) : f = g := DFunLike.ext f g h

    /-- Copy of a `MyIso` with a new `toFun` equal to the old one. Useful to fix definitional
    equalities. -/
    protected def copy (f : MyIso A B) (f' : A → B) (f_inv : B → A)
        (h₁ : f' = f) (h₂ : f_inv = f.invFun) : MyIso A B where
      toFun := f'
      invFun := f_inv
      left_inv := h₁.symm ▸ h₂.symm ▸ f.left_inv
      right_inv := h₁.symm ▸ h₂.symm ▸ f.right_inv
      map_op' := h₁.symm ▸ f.map_op'

    end MyIso

This file will then provide a `CoeFun` instance and various extensionality and simp lemmas.

## Isomorphism classes extending `EquivLike` #

The `EquivLike` design provides further benefits if you put in a bit more work. The first step is to extend `EquivLike` to create a class of those types satisfying the axioms of your new type of isomorphisms. Continuing the example above:

    /-- `MyIsoClass F A B` states that `F` is a type of `MyClass.op`-preserving morphisms.
    You should extend this class when you extend `MyIso`. -/
    class MyIsoClass (F : Type*) (A B : outParam Type*) [MyClass A] [MyClass B]
        [EquivLike F A B]
        extends MyHomClass F A B

    namespace MyIso

    variable {A B : Type*} [MyClass A] [MyClass B]

    -- This goes after `MyIsoClass.instEquivLike`:
    instance : MyIsoClass (MyIso A B) A B where
      map_op := MyIso.map_op'

    -- [Insert `ext` and `copy` here]

    end MyIso

The second step is to add instances of your new `MyIsoClass` for all types extending `MyIso`. Typically, you can just declare a new class analogous to `MyIsoClass`:

    structure CoolerIso (A B : Type*) [CoolClass A] [CoolClass B] extends MyIso A B where
      (map_cool' : toFun CoolClass.cool = CoolClass.cool)

    class CoolerIsoClass (F : Type*) (A B : outParam Type*) [CoolClass A] [CoolClass B]
        [EquivLike F A B]
        extends MyIsoClass F A B where
      (map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)

    @[simp] lemma map_cool {F A B : Type*} [CoolClass A] [CoolClass B]
        [EquivLike F A B] [CoolerIsoClass F A B] (f : F) :
        f CoolClass.cool = CoolClass.cool :=
      CoolerIsoClass.map_cool _

    namespace CoolerIso

    variable {A B : Type*} [CoolClass A] [CoolClass B]

    instance : EquivLike (CoolerIso A B) A B where
      coe f := f.toFun
      inv f := f.invFun
      left_inv f := f.left_inv
      right_inv f := f.right_inv
      coe_injective' f g h₁ h₂ := by cases f; cases g; congr; exact EquivLike.coe_injective' _ _ h₁ h₂

    instance : CoolerIsoClass (CoolerIso A B) A B where
      map_op f := f.map_op'
      map_cool f := f.map_cool'

    -- [Insert `ext` and `copy` here]

    end CoolerIso

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 : MyIso A B) : sorry := sorry
    lemma do_something {F : Type*} [EquivLike F A B] [MyIsoClass F A B] (f : F) : sorry := sorry

This means anything set up for `MyIso`s will automatically work for `CoolerIsoClass`es, and defining `CoolerIsoClass` only takes a constant amount of effort, instead of linearly increasing the work per `MyIso`-related declaration.

source
class EquivLike (E : Sort u_1) (α : outParam (Sort u_2)) (β : outParam (Sort u_3)) :
Sort (max (max (max 1 u_1) u_2) u_3)

The class `EquivLike E α β` expresses that terms of type `E` have an injective coercion to bijections between `α` and `β`.

Note that this does not directly extend `FunLike`, nor take `FunLike` as a parameter, so we can state `coe_injective'` in a nicer way.

This typeclass is used in the definition of the isomorphism (or equivalence) typeclasses, such as `ZeroEquivClass`, `MulEquivClass`, `MonoidEquivClass`, ....

- coe : E → α → β

  The coercion to a function in the forward direction.

- inv : E → β → α

  The coercion to a function in the backwards direction.

- left_inv (e : E) : Function.LeftInverse (inv e) (coe e)

  The coercions are left inverses.

- right_inv (e : E) : Function.RightInverse (inv e) (coe e)

  The coercions are right inverses.

- coe_injective' (e g : E) : coe e = coe g → inv e = inv g → e = g

  The two coercions to functions are jointly injective.

Instances

source
theorem EquivLike.inv_injective {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] :
Function.Injective inv
source
@[instance 100]
instance EquivLike.toFunLike {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] :
FunLike E α β
Equations

- EquivLike.toFunLike = { coe := EquivLike.coe, coe_injective' := ⋯ }

source
@[simp]
theorem EquivLike.coe_apply {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] {e : E} {a : α} :
coe e a = e a
source
theorem EquivLike.inv_apply_eq {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] {e : E} {b : β} {a : α} :
inv e b = a ↔ b = e a
source
@[instance 100]
instance EquivLike.toEmbeddingLike {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] :
EmbeddingLike E α β
source
theorem EquivLike.injective {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] (e : E) :
Function.Injective ⇑e
source
theorem EquivLike.surjective {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] (e : E) :
Function.Surjective ⇑e
source
theorem EquivLike.bijective {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] (e : E) :
Function.Bijective ⇑e
source
theorem EquivLike.apply_eq_iff_eq {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] (f : E) {x y : α} :
f x = f y ↔ x = y
source
@[simp]
theorem EquivLike.injective_comp {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [EquivLike E α β] (e : E) (f : β → γ) :
Function.Injective (f ∘ ⇑e) ↔ Function.Injective f
source
@[simp]
theorem EquivLike.surjective_comp {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [EquivLike E α β] (e : E) (f : β → γ) :
Function.Surjective (f ∘ ⇑e) ↔ Function.Surjective f
source
@[simp]
theorem EquivLike.bijective_comp {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [EquivLike E α β] (e : E) (f : β → γ) :
Function.Bijective (f ∘ ⇑e) ↔ Function.Bijective f
source
@[simp]
theorem EquivLike.inv_apply_apply {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] (e : E) (a : α) :
inv e (e a) = a

This lemma is only supposed to be used in the generic context, when working with instances of classes extending `EquivLike`. For concrete isomorphism types such as `Equiv`, you should use `Equiv.symm_apply_apply` or its equivalent.

TODO: define a generic form of `Equiv.symm`.

source
@[simp]
theorem EquivLike.apply_inv_apply {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] (e : E) (b : β) :
e (inv e b) = b

This lemma is only supposed to be used in the generic context, when working with instances of classes extending `EquivLike`. For concrete isomorphism types such as `Equiv`, you should use `Equiv.apply_symm_apply` or its equivalent.

TODO: define a generic form of `Equiv.symm`.

source
@[deprecated EquivLike.inv_apply_eq (since := "2025-06-20")]
theorem EquivLike.inv_apply_eq_iff_eq_apply {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] {e : E} {b : β} {a : α} :
inv e b = a ↔ b = e a
source
theorem EquivLike.comp_injective {F : Sort u_2} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [EquivLike F β γ] (f : α → β) (e : F) :
Function.Injective (⇑e ∘ f) ↔ Function.Injective f
source
@[simp]
theorem EquivLike.comp_surjective {F : Sort u_2} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [EquivLike F β γ] (f : α → β) (e : F) :
Function.Surjective (⇑e ∘ f) ↔ Function.Surjective f
source
@[simp]
theorem EquivLike.comp_bijective {F : Sort u_2} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [EquivLike F β γ] (f : α → β) (e : F) :
Function.Bijective (⇑e ∘ f) ↔ Function.Bijective f
source
theorem EquivLike.subsingleton_dom {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] [Subsingleton α] :
Subsingleton E

This is not an instance to avoid slowing down every single `Subsingleton` typeclass search.