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

This typeclass is primarily for use by homomorphisms like MonoidHom and LinearMap.

There is the "D"ependent version DFunLike and the non-dependent version FunLike.

Basic usage of DFunLike and FunLike

A typical type of morphisms should be declared as:

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

namespace MyHom

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

instance : FunLike (MyHom A B) A B where
  coe := MyHom.toFun
  coe_injective' := fun f g h => by cases f; cases g; congr

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

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

end MyHom

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

Morphism classes extending DFunLike and FunLike

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

/-- `MyHomClass F A B` states that `F` is a type of `MyClass.op`-preserving morphisms.
You should extend this class when you extend `MyHom`. -/
class MyHomClass (F : Type*) (A B : outParam Type*) [MyClass A] [MyClass B]
    [FunLike F A B] : Prop :=
  (map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y))

@[simp]
lemma map_op {F A B : Type*} [MyClass A] [MyClass B] [FunLike F A B] [MyHomClass F A B]
    (f : F) (x y : A) :
    f (MyClass.op x y) = MyClass.op (f x) (f y) :=
  MyHomClass.map_op _ _ _

-- You can add the below instance next to `MyHomClass.instFunLike`:
instance : MyHomClass (MyHom A B) A B where
  map_op := MyHom.map_op'

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

Note that A B are marked as outParam even though they are not purely required to be so due to the FunLike parameter already filling them in. This is required to see through type synonyms, which is important in the category theory library. Also, it appears having them as outParam is slightly faster.

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

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

class CoolerHomClass (F : Type*) (A B : outParam Type*) [CoolClass A] [CoolClass B]
  [FunLike F A B] extends MyHomClass F A B :=
    (map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)

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

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

instance : FunLike (CoolerHom A B) A B where
  coe f := f.toFun
  coe_injective' := fun f g h ↦ by cases f; cases g; congr; apply DFunLike.coe_injective; congr

instance : CoolerHomClass (CoolerHom A B) A B where
  map_op f := f.map_op'
  map_cool f := f.map_cool'

-- [Insert `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 : MyHom A B) : sorry := sorry
lemma do_something {F : Type*} [FunLike F A B] [MyHomClass F A B] (f : F) : sorry :=
  sorry

This means anything set up for MyHoms will automatically work for CoolerHomClasses, and defining CoolerHomClass only takes a constant amount of effort, instead of linearly increasing the work per MyHom-related declaration.

Design rationale

The current form of FunLike was set up in pull request #8386: https://github.com/leanprover-community/mathlib4/pull/8386 We made FunLike unbundled: child classes don't extend FunLike, they take a [FunLike F A B] parameter instead. This suits the instance synthesis algorithm better: it's easy to verify a type does not have a FunLike instance by checking the discrimination tree once instead of searching the entire extends hierarchy.

class DFunLike (F : Sort u_1) (α : outParam (Sort u_2)) (β : outParam (α → Sort u_3)) : Sort (max (max (max 1 u_1) u_2) u_3)

The class DFunLike F α β expresses that terms of type F have an injective coercion to (dependent) functions from α to β.

For non-dependent functions you can also use the abbreviation FunLike.

This typeclass is used in the definition of the homomorphism typeclasses, such as ZeroHomClass, MulHomClass, MonoidHomClass, ....

• coe : F → (a : α) → β a

  The coercion from F to a function.

• coe_injective' : Function.Injective DFunLike.coe

  The coercion to functions must be injective.

theorem DFunLike.coe_injective' {F : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (α → Sort u_3)} [self : DFunLike F α β] : Function.Injective DFunLike.coe

The coercion to functions must be injective.

@[reducible, inline]

abbrev FunLike (F : Sort u_1) (α : Sort u_2) (β : Sort u_3) : Sort (max (max (max 1 u_1) u_2) u_3)

The class FunLike F α β (Function-Like) expresses that terms of type F have an injective coercion to functions from α to β. FunLike is the non-dependent version of DFunLike. This typeclass is used in the definition of the homomorphism typeclasses, such as ZeroHomClass, MulHomClass, MonoidHomClass, ....

Equations

• FunLike F α β = DFunLike F α fun (x : α) => β

DFunLike F α β where β depends on a : α

@[instance 100]

instance DFunLike.hasCoeToFun {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] : CoeFun F fun (x : F) => (a : α) → β a

Equations

• DFunLike.hasCoeToFun = { coe := DFunLike.coe }

theorem DFunLike.coe_eq_coe_fn {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] : DFunLike.coe = fun (f : F) => ⇑f

theorem DFunLike.coe_injective {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] : Function.Injective fun (f : F) => ⇑f

@[simp]

theorem DFunLike.coe_fn_eq {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f : F} {g : F} : ⇑f = ⇑g ↔ f = g

theorem DFunLike.ext' {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f : F} {g : F} (h : ⇑f = ⇑g) : f = g

theorem DFunLike.ext'_iff {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f : F} {g : F} : f = g ↔ ⇑f = ⇑g

theorem DFunLike.ext {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] (f : F) (g : F) (h : ∀ (x : α), f x = g x) : f = g

theorem DFunLike.ext_iff {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f : F} {g : F} : f = g ↔ ∀ (x : α), f x = g x

theorem DFunLike.congr_fun {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f : F} {g : F} (h₁ : f = g) (x : α) : f x = g x

theorem DFunLike.ne_iff {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f : F} {g : F} : f ≠ g ↔ ∃ (a : α), f a ≠ g a

theorem DFunLike.exists_ne {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f : F} {g : F} (h : f ≠ g) : ∃ (x : α), f x ≠ g x

theorem DFunLike.subsingleton_cod {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] [∀ (a : α), Subsingleton (β a)] : Subsingleton F

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

FunLike F α β where β does not depend on a : α

theorem DFunLike.congr {F : Sort u_1} {α : Sort u_2} {β : Sort u_3} [i : FunLike F α β] {f : F} {g : F} {x : α} {y : α} (h₁ : f = g) (h₂ : x = y) : f x = g y

theorem DFunLike.congr_arg {F : Sort u_1} {α : Sort u_2} {β : Sort u_3} [i : FunLike F α β] (f : F) {x : α} {y : α} (h₂ : x = y) : f x = f y