doc-next-gen

Mathlib.Data.FunLike.Basic

Module docstring

{"# 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' mapop' := h.symm ▸ f.mapop'

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 Bstates thatFis a type ofMyClass.op-preserving morphisms. You should extend this class when you extendMyHom`. -/ 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 mapop {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.mapop _ _ _

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

-- [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 mapcool {F A B : Type*} [CoolClass A] [CoolClass B] [FunLike F A B] [CoolerHomClass F A B] (f : F) : f CoolClass.cool = CoolClass.cool := CoolerHomClass.mapcool _

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

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

instance : CoolerHomClass (CoolerHom A B) A B where mapop f := f.mapop' mapcool f := f.mapcool'

-- [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 https://github.com/leanprover-community/mathlib4/pull/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. ","### DFunLike F α β where β depends on a : α ","### FunLike F α β where β does not depend on a : α "}

DFunLike structure
(F : Sort*) (α : outParam (Sort*)) (β : outParam <| α → Sort*)
Full source 
/-- 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`, ....
-/
@[notation_class * toFun Simps.findCoercionArgs]
class DFunLike (F : Sort*) (α : outParam (Sort*)) (β : outParam <| α → Sort*) where
  /-- The coercion from `F` to a function. -/
  coe : F → ∀ a : α, β a
  /-- The coercion to functions must be injective. -/
  coe_injective' : Function.Injective coe
Dependent Function-Like Class
Informal description
The class `DFunLike F α β` indicates that terms of type `F` can be injectively coerced into dependent functions from `α` to `β` (where `β` may depend on elements of `α`). For non-dependent functions, the abbreviation `FunLike F α β` is used. This class is foundational for defining various homomorphism typeclasses such as `ZeroHomClass`, `MulHomClass`, `MonoidHomClass`, etc.
FunLike abbrev
F α β
Full source 
/-- The class `FunLike F α β` (`Fun`ction-`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`, ....
-/
abbrev FunLike F α β := DFunLike F α fun _ => β
Function-Like Class for Non-Dependent Functions
Informal description
The class `FunLike F α β` (Function-Like) expresses that terms of type `F` have an injective coercion to functions from `α$ to $\beta$, where $\beta$ does not depend on elements of $\alpha$. This is the non-dependent version of `DFunLike` and is used in defining various homomorphism typeclasses such as `ZeroHomClass`, `MulHomClass`, `MonoidHomClass`, etc.
DFunLike.hasCoeToFun instance
: CoeFun F (fun _ ↦ ∀ a : α, β a)
Full source 
instance (priority := 100) hasCoeToFun : CoeFun F (fun _ ↦ ∀ a : α, β a) where
  coe := @DFunLike.coe _ _ β _
Canonical Coercion from DFunLike to Dependent Functions
Informal description
For any type `F` that is an instance of `DFunLike F α β`, there exists a canonical coercion from `F` to the type of dependent functions `(a : α) → β a`. This coercion is injective, meaning that if two elements of `F` have the same function behavior, they must be equal.
DFunLike.coe_eq_coe_fn theorem
: (DFunLike.coe (F := F)) = (fun f => ↑f)
Full source 
theorem coe_eq_coe_fn : (DFunLike.coe (F := F)) = (fun f => ↑f) := rfl
Equality of DFunLike.coe and Coercion Operator
Informal description
The coercion function `DFunLike.coe` from type `F` to dependent functions `(a : α) → β a` is equal to the function that simply applies the coercion operator `↑` to elements of `F`.
DFunLike.coe_injective theorem
: Function.Injective (fun f : F ↦ (f : ∀ a : α, β a))
Full source 
theorem coe_injective : Function.Injective (fun f : F ↦ (f : ∀ a : α, β a)) :=
  DFunLike.coe_injective'
Injectivity of Coercion from `DFunLike` to Dependent Functions
Informal description
For any type $F$ with a `DFunLike` instance, the canonical coercion map from $F$ to the type of dependent functions $(a : \alpha) \to \beta a$ is injective. That is, if two elements $f, g : F$ satisfy $(f : \forall a : \alpha, \beta a) = (g : \forall a : \alpha, \beta a)$, then $f = g$.
DFunLike.coe_fn_eq theorem
{f g : F} : (f : ∀ a : α, β a) = (g : ∀ a : α, β a) ↔ f = g
Full source 
@[simp]
theorem coe_fn_eq {f g : F} : (f : ∀ a : α, β a) = (g : ∀ a : α, β a) ↔ f = g :=
  ⟨fun h ↦ DFunLike.coe_injective' h, fun h ↦ by cases h; rfl⟩
Equality of Coerced Functions Implies Equality in `DFunLike` Types
Informal description
For any two elements $f$ and $g$ of type $F$ (where $F$ is a type with a `DFunLike` instance), the equality of their coerced dependent functions $(f : \forall a : \alpha, \beta a) = (g : \forall a : \alpha, \beta a)$ holds if and only if $f = g$ in $F$.
DFunLike.ext' theorem
{f g : F} (h : (f : ∀ a : α, β a) = (g : ∀ a : α, β a)) : f = g
Full source 
theorem ext' {f g : F} (h : (f : ∀ a : α, β a) = (g : ∀ a : α, β a)) : f = g :=
  DFunLike.coe_injective' h
Equality of Coerced Functions Implies Equality in `DFunLike` Types
Informal description
For any two elements $f$ and $g$ of a type $F$ with a `DFunLike` instance, if the coerced dependent functions $(f : \forall a : \alpha, \beta a)$ and $(g : \forall a : \alpha, \beta a)$ are equal, then $f = g$.
DFunLike.ext'_iff theorem
{f g : F} : f = g ↔ (f : ∀ a : α, β a) = (g : ∀ a : α, β a)
Full source 
theorem ext'_iff {f g : F} : f = g ↔ (f : ∀ a : α, β a) = (g : ∀ a : α, β a) :=
  coe_fn_eq.symm
Equivalence of Equality and Coerced Function Equality in `DFunLike` Types
Informal description
For any two elements $f$ and $g$ of a type $F$ with a `DFunLike` instance, the equality $f = g$ holds if and only if their coerced dependent functions $(f : \forall a : \alpha, \beta a)$ and $(g : \forall a : \alpha, \beta a)$ are equal.
DFunLike.ext theorem
(f g : F) (h : ∀ x : α, f x = g x) : f = g
Full source 
theorem ext (f g : F) (h : ∀ x : α, f x = g x) : f = g :=
  DFunLike.coe_injective' (funext h)
Extensionality for Dependent Function-Like Types
Informal description
For any two elements $f$ and $g$ of type $F$ in the `DFunLike` class, if $f(x) = g(x)$ for all $x \in \alpha$, then $f = g$.
DFunLike.ext_iff theorem
{f g : F} : f = g ↔ ∀ x, f x = g x
Full source 
theorem ext_iff {f g : F} : f = g ↔ ∀ x, f x = g x :=
  coe_fn_eq.symm.trans funext_iff
Extensionality Criterion for Dependent Function-Like Types
Informal description
For any two elements $f$ and $g$ of a type $F$ with a `DFunLike` instance, $f = g$ if and only if $f(x) = g(x)$ for all $x \in \alpha$.
DFunLike.congr_fun theorem
{f g : F} (h₁ : f = g) (x : α) : f x = g x
Full source 
protected theorem congr_fun {f g : F} (h₁ : f = g) (x : α) : f x = g x :=
  congr_fun (congr_arg _ h₁) x
Function Equality Implies Pointwise Equality for `DFunLike`
Informal description
For any two elements $f$ and $g$ of type $F$ in the `DFunLike` class, if $f = g$, then for all $x \in \alpha$, the evaluations $f(x)$ and $g(x)$ are equal.
DFunLike.ne_iff theorem
{f g : F} : f ≠ g ↔ ∃ a, f a ≠ g a
Full source 
theorem ne_iff {f g : F} : f ≠ gf ≠ g ↔ ∃ a, f a ≠ g a :=
  ext_iff.not.trans not_forall
Inequality Criterion for Dependent Function-Like Types
Informal description
For any two elements $f$ and $g$ of a type $F$ with a `DFunLike` instance, $f \neq g$ if and only if there exists some $a \in \alpha$ such that $f(a) \neq g(a)$.
DFunLike.exists_ne theorem
{f g : F} (h : f ≠ g) : ∃ x, f x ≠ g x
Full source 
theorem exists_ne {f g : F} (h : f ≠ g) : ∃ x, f x ≠ g x :=
  ne_iff.mp h
Existence of Pointwise Inequality for Function-Like Types
Informal description
For any two distinct elements $f$ and $g$ of a type $F$ with a `DFunLike` instance, there exists some $x \in \alpha$ such that $f(x) \neq g(x)$.
DFunLike.subsingleton_cod theorem
[∀ a, Subsingleton (β a)] : Subsingleton F
Full source 
/-- This is not an instance to avoid slowing down every single `Subsingleton` typeclass search. -/
lemma subsingleton_cod [∀ a, Subsingleton (β a)] : Subsingleton F :=
  ⟨fun _ _ ↦ coe_injective <| Subsingleton.elim _ _⟩
Subsingleton Property of Function-Like Types with Subsingleton Codomains
Informal description
For any type $F$ with a `DFunLike` instance where the codomain $\beta(a)$ is a subsingleton for every $a \in \alpha$, the type $F$ itself is a subsingleton (i.e., all elements of $F$ are equal).
DFunLike.congr theorem
{f g : F} {x y : α} (h₁ : f = g) (h₂ : x = y) : f x = g y
Full source 
protected theorem congr {f g : F} {x y : α} (h₁ : f = g) (h₂ : x = y) : f x = g y :=
  congr (congr_arg _ h₁) h₂
Function-Like Evaluation Congruence: $f = g \land x = y \implies f(x) = g(y)$
Informal description
For any function-like terms $f, g : F$ and elements $x, y : \alpha$, if $f = g$ and $x = y$, then the evaluations satisfy $f(x) = g(y)$.
DFunLike.congr_arg theorem
(f : F) {x y : α} (h₂ : x = y) : f x = f y
Full source 
protected theorem congr_arg (f : F) {x y : α} (h₂ : x = y) : f x = f y :=
  congr_arg _ h₂
Function-Like Argument Congruence: $x = y \implies f(x) = f(y)$
Informal description
For any function-like term $f : F$ and elements $x, y : \alpha$, if $x = y$, then the evaluation of $f$ at $x$ equals the evaluation of $f$ at $y$, i.e., $f(x) = f(y)$.
DFunLike.dite_apply theorem
{P : Prop} [Decidable P] (f : P → F) (g : ¬P → F) (x : α) : (if h : P then f h else g h) x = if h : P then f h x else g h x
Full source 
theorem dite_apply {P : Prop} [Decidable P] (f : P → F) (g : ¬P → F) (x : α) :
    (if h : P then f h else g h) x = if h : P then f h x else g h x := by
  split_ifs <;> rfl
Evaluation of Dependent If-Then-Else Function Application
Informal description
For any proposition \( P \) with a decidable instance, given functions \( f : P \to F \) and \( g : \neg P \to F \), and an element \( x : \alpha \), the evaluation of the dependent if-then-else expression at \( x \) satisfies: \[ \left(\text{if } h : P \text{ then } f h \text{ else } g h\right)(x) = \text{if } h : P \text{ then } f h x \text{ else } g h x. \]
DFunLike.ite_apply theorem
{P : Prop} [Decidable P] (f g : F) (x : α) : (if P then f else g) x = if P then f x else g x
Full source 
theorem ite_apply {P : Prop} [Decidable P] (f g : F) (x : α) :
    (if P then f else g) x = if P then f x else g x :=
  dite_apply _ _ _
Evaluation of If-Then-Else Function Application
Informal description
For any proposition \( P \) with a decidable instance, given function-like terms \( f, g : F \) and an element \( x : \alpha \), the evaluation of the if-then-else expression satisfies: \[ (\text{if } P \text{ then } f \text{ else } g)(x) = \text{if } P \text{ then } f(x) \text{ else } g(x). \]