# Documentation

Mathlib.Data.FunLike.Equiv

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

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

## Basic usage of EquivLike#

A typical type of morphisms should be declared as:

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

namespace MyIso

variables (A B : Type _) [MyClass A] [MyClass B]

-- This instance is optional if you follow the "Isomorphism class" design below:
instance : EquivLike (MyIso A B) A (λ _, B) :=
{ coe := MyIso.toEquiv.toFun,
inv := MyIso.toEquiv.invFun,
left_inv := MyIso.toEquiv.left_inv,
right_inv := MyIso.toEquiv.right_inv,
coe_injective' := λ f g h, by cases f; cases g; congr' }

/-- Helper instance for when there's too many metavariables to apply EquivLike.coe directly. -/
instance : CoeFun (MyIso A B) := FunLike.instCoeFunForAll

@[ext] theorem ext {f g : MyIso A B} (h : ∀ x, f x = g x) : f = g := FunLike.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) : MyIso A B :=
{ toFun := f',
invFun := f_inv,
left_inv := h.symm ▸ f.left_inv,
right_inv := h.symm ▸ f.right_inv,
map_op' := h.symm ▸ f.map_op' }

end MyIso
∀ {x y : A}, toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))

namespace MyIso

variables (A B : Type _) [MyClass A] [MyClass B]

-- This instance is optional if you follow the "Isomorphism class" design below:
instance : EquivLike (MyIso A B) A (λ _, B) :=
{ coe := MyIso.toEquiv.toFun,
inv := MyIso.toEquiv.invFun,
left_inv := MyIso.toEquiv.left_inv,
right_inv := MyIso.toEquiv.right_inv,
coe_injective' := λ f g h, by cases f; cases g; congr' }

/-- Helper instance for when there's too many metavariables to apply EquivLike.coe directly. -/
instance : CoeFun (MyIso A B) := FunLike.instCoeFunForAll

@[ext] theorem ext {f g : MyIso A B} (h : ∀ x, f x = g x) : f = g := FunLike.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) : MyIso A B :=
{ toFun := f',
invFun := f_inv,
left_inv := h.symm ▸ f.left_inv,
right_inv := h.symm ▸ f.right_inv,
map_op' := h.symm ▸ f.map_op' }

end MyIso
∀ x, f x = g x) : f = g := FunLike.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) : MyIso A B :=
{ toFun := f',
invFun := f_inv,
left_inv := h.symm ▸ f.left_inv,
right_inv := h.symm ▸ f.right_inv,
map_op' := h.symm ▸ f.map_op' }

end MyIso
→ B) (f_inv : B → A) (h : f' = ⇑f) : MyIso A B :=
{ toFun := f',
invFun := f_inv,
left_inv := h.symm ▸ f.left_inv,
right_inv := h.symm ▸ f.right_inv,
map_op' := h.symm ▸ f.map_op' }

end MyIso
→ A) (h : f' = ⇑f) : MyIso A B :=
{ toFun := f',
invFun := f_inv,
left_inv := h.symm ▸ f.left_inv,
right_inv := h.symm ▸ f.right_inv,
map_op' := h.symm ▸ f.map_op' }

end MyIso
⇑f) : MyIso A B :=
{ toFun := f',
invFun := f_inv,
left_inv := h.symm ▸ f.left_inv,
right_inv := h.symm ▸ f.right_inv,
map_op' := h.symm ▸ f.map_op' }

end MyIso
▸ f.left_inv,
right_inv := h.symm ▸ f.right_inv,
map_op' := h.symm ▸ f.map_op' }

end MyIso
▸ f.right_inv,
map_op' := h.symm ▸ f.map_op' }

end MyIso
▸ 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]
extends EquivLike F A (λ _, B), MyHomClass F A B

end

-- You can replace MyIso.EquivLike with the below instance:
instance : MyIsoClass (MyIso A B) A B :=
{ coe := MyIso.toFun,
inv := MyIso.invFun,
left_inv := MyIso.left_inv,
right_inv := MyIso.right_inv,
coe_injective' := λ f g h, by cases f; cases g; congr',
map_op := MyIso.map_op' }

-- [Insert CoeFun, ext and copy here]

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 :=
(map_cool' : toFun CoolClass.cool = CoolClass.cool)

section
set_option old_structure_cmd true

class CoolerIsoClass (F : Type _) (A B : outParam <| Type _) [CoolClass A] [CoolClass B]
extends MyIsoClass F A B :=
(map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)

end

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

instance : CoolerIsoClass (CoolerIso A B) A B :=
{ coe := CoolerIso.toFun,
coe_injective' := λ f g h, by cases f; cases g; congr',
map_op := CoolerIso.map_op',
map_cool := CoolerIso.map_cool' }

-- [Insert CoeFun, ext and copy here]
∀ (f : F), f CoolClass.cool = CoolClass.cool)

end

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

instance : CoolerIsoClass (CoolerIso A B) A B :=
{ coe := CoolerIso.toFun,
coe_injective' := λ f g h, by cases f; cases g; congr',
map_op := CoolerIso.map_op',
map_cool := CoolerIso.map_cool' }

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

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

class EquivLike (E : Sort u_1) (α : outParam (Sort u_2)) (β : outParam (Sort u_3)) :
Sort (max(max(max1u_1)u_2)u_3)
• The coercion to a function in the forward direction.

coe : Eαβ
• The coercion to a function in the backwards direction.

inv : Eβα
• The coercions are left inverses.

left_inv : ∀ (e : E), Function.LeftInverse (inv e) (coe e)
• The coercions are right inverses.

right_inv : ∀ (e : E), Function.RightInverse (inv e) (coe e)
• If two coercions to functions are jointly injective.

coe_injective' : ∀ (e g : E), coe e = coe ginv e = inv ge = g

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

This typeclass is used in the definition of the homomorphism typeclasses, such as ZeroEquivClass, MulEquivClass, MonoidEquivClass, ....

Instances
theorem EquivLike.inv_injective {E : Sort u_1} {α : Sort u_3} {β : Sort u_2} [iE : EquivLike E α β] :
Function.Injective EquivLike.inv
instance EquivLike.toEmbeddingLike {E : Sort u_1} {α : Sort u_2} {β : Sort u_3} [iE : EquivLike E α β] :
Equations
theorem EquivLike.injective {E : Sort u_3} {α : Sort u_1} {β : Sort u_2} [iE : EquivLike E α β] (e : E) :
theorem EquivLike.surjective {E : Sort u_3} {α : Sort u_1} {β : Sort u_2} [iE : EquivLike E α β] (e : E) :
theorem EquivLike.bijective {E : Sort u_3} {α : Sort u_1} {β : Sort u_2} [iE : EquivLike E α β] (e : E) :
theorem EquivLike.apply_eq_iff_eq {E : Sort u_2} {α : Sort u_3} {β : Sort u_1} [iE : EquivLike E α β] (f : E) {x : α} {y : α} :
f x = f y x = y
@[simp]
theorem EquivLike.injective_comp {E : Sort u_4} {α : Sort u_1} {β : Sort u_3} {γ : Sort u_2} [iE : EquivLike E α β] (e : E) (f : βγ) :
@[simp]
theorem EquivLike.surjective_comp {E : Sort u_4} {α : Sort u_1} {β : Sort u_3} {γ : Sort u_2} [iE : EquivLike E α β] (e : E) (f : βγ) :
@[simp]
theorem EquivLike.bijective_comp {E : Sort u_4} {α : Sort u_1} {β : Sort u_3} {γ : Sort u_2} [iE : EquivLike E α β] (e : E) (f : βγ) :
@[simp]
theorem EquivLike.inv_apply_apply {E : Sort u_2} {α : Sort u_1} {β : Sort u_3} [iE : EquivLike E α β] (e : E) (a : α) :
EquivLike.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.

@[simp]
theorem EquivLike.apply_inv_apply {E : Sort u_2} {α : Sort u_3} {β : Sort u_1} [iE : EquivLike E α β] (e : E) (b : β) :
e () = 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.

theorem EquivLike.comp_injective {F : Sort u_4} {α : Sort u_1} {β : Sort u_3} {γ : Sort u_2} [iF : EquivLike F β γ] (f : αβ) (e : F) :
@[simp]
theorem EquivLike.comp_surjective {F : Sort u_4} {α : Sort u_1} {β : Sort u_3} {γ : Sort u_2} [iF : EquivLike F β γ] (f : αβ) (e : F) :
@[simp]
theorem EquivLike.comp_bijective {F : Sort u_4} {α : Sort u_1} {β : Sort u_3} {γ : Sort u_2} [iF : EquivLike F β γ] (f : αβ) (e : F) :
theorem EquivLike.subsingleton_dom {F : Sort u_2} {β : Sort u_1} {γ : Sort u_3} [iF : EquivLike F β γ] [inst : ] :

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