# Documentation

Mathlib.Data.FunLike.Basic

# Typeclass for a type F with an injective map to A → B→ 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
→ 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
∀ {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
→ 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
∀ 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
→ B) (h : f' = ⇑f) : MyHom A B :=
{ toFun := f',
map_op' := h.symm ▸ f.map_op' }

end MyHom
⇑f) : MyHom A B :=
{ toFun := f',
map_op' := h.symm ▸ f.map_op' }

end MyHom
▸ 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]
∀ (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]
∀ (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(max1u_1)u_2)u_3)
• The coercion from F to a function.

coe : F(a : α) → β a
• The coercion to functions must be injective.

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

Instances

### 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_3} {α : Sort u_1} {β : αSort u_2} [i : FunLike F α β] {f : F} {g : F} :
f = g f = g
theorem FunLike.ext' {F : Sort u_3} {α : Sort u_1} {β : αSort u_2} [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_2} {α : Sort u_3} {β : αSort u_1} [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_3} {β : αSort u_2} [i : FunLike F α β] {f : F} {g : F} :
f = g ∀ (x : α), f x = g x
theorem FunLike.congr_fun {F : Sort u_1} {α : Sort u_3} {β : αSort u_2} [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_2} {α : Sort u_3} {β : αSort u_1} [i : FunLike F α β] [inst : ∀ (a : α), Subsingleton (β a)] :

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_3} {α : Sort u_1} {β : Sort u_2} [i : FunLike F α fun x => β] (f : F) {x : α} {y : α} (h₂ : x = y) :
f x = f y