# mathlib3documentation

data.fun_like.equiv

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This typeclass is primarily for use by isomorphisms like monoid_equiv and linear_equiv.

## Basic usage of equiv_like#

A typical type of morphisms should be declared as:

structure my_iso (A B : Type*) [my_class A] [my_class B]
extends equiv A B :=
(map_op' : ∀ {x y : A}, to_fun (my_class.op x y) = my_class.op (to_fun x) (to_fun y))

namespace my_iso

variables (A B : Type*) [my_class A] [my_class B]

-- This instance is optional if you follow the "Isomorphism class" design below:
instance : equiv_like (my_iso A B) A (λ _, B) :=
{ coe := my_iso.to_equiv.to_fun,
inv := my_iso.to_equiv.inv_fun,
left_inv := my_iso.to_equiv.left_inv,
right_inv := my_iso.to_equiv.right_inv,
coe_injective' := λ f g h, by cases f; cases g; congr' }

/-- Helper instance for when there's too many metavariables to apply equiv_like.coe directly. -/
instance : has_coe_to_fun (my_iso A B) := to_fun.to_coe_fn

@[simp] lemma to_fun_eq_coe {f : my_iso A B} : f.to_fun = (f : A → B) := rfl

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

/-- Copy of a my_iso with a new to_fun equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : my_iso A B) (f' : A → B) (f_inv : B → A) (h : f' = ⇑f) : my_iso A B :=
{ to_fun := f',
inv_fun := f_inv,
left_inv := h.symm ▸ f.left_inv,
right_inv := h.symm ▸ f.right_inv,
map_op' := h.symm ▸ f.map_op' }

end my_iso


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

## Isomorphism classes extending equiv_like#

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

section
set_option old_structure_cmd true

/-- my_iso_class F A B states that F is a type of my_class.op-preserving morphisms.
You should extend this class when you extend my_iso. -/
class my_iso_class (F : Type*) (A B : out_param $Type*) [my_class A] [my_class B] extends equiv_like F A (λ _, B), my_hom_class F A B. end -- You can replace my_iso.equiv_like with the below instance: instance : my_iso_class (my_iso A B) A B := { coe := my_iso.to_fun, inv := my_iso.inv_fun, left_inv := my_iso.left_inv, right_inv := my_iso.right_inv, coe_injective' := λ f g h, by cases f; cases g; congr', map_op := my_iso.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_iso_class for all types extending my_iso. Typically, you can just declare a new class analogous to my_iso_class: structure cooler_iso (A B : Type*) [cool_class A] [cool_class B] extends my_iso A B := (map_cool' : to_fun cool_class.cool = cool_class.cool) section set_option old_structure_cmd true class cooler_iso_class (F : Type*) (A B : out_param$ Type*) [cool_class A] [cool_class B]
extends my_iso_class F A B :=
(map_cool : ∀ (f : F), f cool_class.cool = cool_class.cool)

end

@[simp] lemma map_cool {F A B : Type*} [cool_class A] [cool_class B] [cooler_iso_class F A B]
(f : F) : f cool_class.cool = cool_class.cool :=
my_iso_class.map_op

-- You can also replace my_iso.equiv_like with the below instance:
instance : cool_iso_class (cool_iso A B) A B :=
{ coe := cool_iso.to_fun,
coe_injective' := λ f g h, by cases f; cases g; congr',
map_op := cool_iso.map_op',
map_cool := cool_iso.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_iso A B) : sorry := sorry
lemma do_something {F : Type*} [my_iso_class F A B] (f : F) : sorry := sorry


This means anything set up for my_isos will automatically work for cool_iso_classes, and defining cool_iso_class only takes a constant amount of effort, instead of linearly increasing the work per my_iso-related declaration.

@[class]
structure equiv_like (E : Sort u_1) (α : out_param (Sort u_2)) (β : out_param (Sort u_3)) :
Sort (max 1 (imax u_1 u_2 u_3) (imax u_1 u_3 u_2))
• coe : E α β
• inv : E β α
• left_inv : (e : E),
• right_inv : (e : E),
• coe_injective' : (e g : E), e = g

The class equiv_like 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 zero_equiv_class, mul_equiv_class, monoid_equiv_class, ....

Instances of this typeclass
Instances of other typeclasses for equiv_like
• equiv_like.has_sizeof_inst
theorem equiv_like.inv_injective {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [iE : α β] :
@[protected, instance]
def equiv_like.to_embedding_like {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [iE : α β] :
β
Equations
@[protected]
theorem equiv_like.injective {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [iE : α β] (e : E) :
@[protected]
theorem equiv_like.surjective {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [iE : α β] (e : E) :
@[protected]
theorem equiv_like.bijective {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [iE : α β] (e : E) :
theorem equiv_like.apply_eq_iff_eq {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [iE : α β] (f : E) {x y : α} :
f x = f y x = y
@[simp]
theorem equiv_like.injective_comp {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [iE : α β] (e : E) (f : β γ) :
@[simp]
theorem equiv_like.surjective_comp {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [iE : α β] (e : E) (f : β γ) :
@[simp]
theorem equiv_like.bijective_comp {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [iE : α β] (e : E) (f : β γ) :
@[simp]
theorem equiv_like.inv_apply_apply {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [iE : α β] (e : E) (a : α) :
(e a) = a

This lemma is only supposed to be used in the generic context, when working with instances of classes extending equiv_like. 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 equiv_like.apply_inv_apply {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [iE : α β] (e : E) (b : β) :
e b) = b

This lemma is only supposed to be used in the generic context, when working with instances of classes extending equiv_like. 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 equiv_like.comp_injective {F : Sort u_2} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [iF : β γ] (f : α β) (e : F) :
@[simp]
theorem equiv_like.comp_surjective {F : Sort u_2} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [iF : β γ] (f : α β) (e : F) :
@[simp]
theorem equiv_like.comp_bijective {F : Sort u_2} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [iF : β γ] (f : α β) (e : F) :
theorem equiv_like.subsingleton_dom {F : Sort u_2} {β : Sort u_4} {γ : Sort u_5} [iF : β γ] [subsingleton β] :

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