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

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

Basic usage of FunLike

A typical type of morphisms should be declared as:

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

namespace MyHom

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

-- This instance is optional if you follow the "morphism class" design below:
instance : FunLike (MyHom A B) A (λ _, B) :=
  { coe := MyHom.toFun, coe_injective' := λ f g h, by cases f; cases g; congr' }

/-- Helper instance for when there's too many metavariables to apply
`FunLike.coe` directly. -/
instance : CoeFun (MyHom A B) (λ _, A → B) := ⟨MyHom.toFun⟩

@[ext] theorem ext {f g : MyHom A B} (h : ∀ x, f x = g x) : f = g := FunLike.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 :=
  { 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 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]
  extends FunLike F A (λ _, B) :=
(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] [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 replace `MyHom.FunLike` with the below instance:
instance : MyHomClass (MyHom A B) A B :=
  { coe := MyHom.toFun,
    coe_injective' := λ f g h, by cases f; cases g; congr',
    map_op := MyHom.map_op' }

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

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

class CoolerHomClass (F : Type*) (A B : outParam <| Type*) [CoolClass A] [CoolClass 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] [CoolerHomClass F A B]
  (f : F) : f CoolClass.cool = CoolClass.cool :=
MyHomClass.map_op

-- You can also replace `MyHom.FunLike` with the below instance:
instance : CoolerHomClass (CoolHom A B) A B :=
  { coe := CoolHom.toFun,
    coe_injective' := λ f g h, by cases f; cases g; congr',
    map_op := CoolHom.map_op',
    map_cool := CoolHom.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 : MyHom A B) : sorry := sorry
lemma do_something {F : Type*} [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.

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

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

  The coercion from F to a function.

• coe_injective' : Function.Injective FunLike.coe

  The coercion to functions must be injective.

The class FunLike F α β expresses that terms of type F have an injective coercion to functions from α to β.

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

FunLike F α β where β depends on a : α

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

Equations

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

theorem FunLike.coe_eq_coe_fn {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : FunLike F α β] : FunLike.coe = fun f => ↑f

theorem FunLike.coe_injective {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : FunLike F α β] : Function.Injective fun f => ↑f

@[simp]

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

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

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

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

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

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

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

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

theorem FunLike.subsingleton_cod {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : FunLike 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 FunLike.congr {F : Sort u_1} {α : Sort u_2} {β : Sort u_3} [i : FunLike F α fun x => β] {f : F} {g : F} {x : α} {y : α} (h₁ : f = g) (h₂ : x = y) : ↑f x = ↑g y

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