Documentation

Mathlib.Data.FunLike.Equiv

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 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

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]

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 (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 β.

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

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

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