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

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

Instances
    theorem EquivLike.left_inv {E : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (Sort u_3)} [self : EquivLike E α β] (e : E) :

    The coercions are left inverses.

    theorem EquivLike.right_inv {E : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (Sort u_3)} [self : EquivLike E α β] (e : E) :

    The coercions are right inverses.

    theorem EquivLike.coe_injective' {E : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (Sort u_3)} [self : EquivLike E α β] (e : E) (g : E) :

    The two coercions to functions are jointly injective.

    theorem EquivLike.inv_injective {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] :
    Function.Injective EquivLike.inv
    @[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' := }
    @[instance 100]
    instance EquivLike.toEmbeddingLike {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] :
    Equations
    • =
    theorem EquivLike.injective {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] (e : E) :
    theorem EquivLike.surjective {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] (e : E) :
    theorem EquivLike.bijective {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] (e : E) :
    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
    @[simp]
    theorem EquivLike.injective_comp {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [EquivLike E α β] (e : E) (f : βγ) :
    @[simp]
    theorem EquivLike.surjective_comp {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [EquivLike E α β] (e : E) (f : βγ) :
    @[simp]
    theorem EquivLike.bijective_comp {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [EquivLike E α β] (e : E) (f : βγ) :
    @[simp]
    theorem EquivLike.inv_apply_apply {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [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} [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} [EquivLike F β γ] (f : αβ) (e : F) :
    @[simp]
    theorem EquivLike.comp_surjective {F : Sort u_2} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [EquivLike F β γ] (f : αβ) (e : F) :
    @[simp]
    theorem EquivLike.comp_bijective {F : Sort u_2} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [EquivLike F β γ] (f : αβ) (e : F) :
    theorem EquivLike.subsingleton_dom {F : Sort u_2} {β : Sort u_4} {γ : Sort u_5} [EquivLike F β γ] [FunLike F β γ] [Subsingleton β] :

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