doc-next-gen

Mathlib.Data.FunLike.Embedding

Module docstring

{"# Typeclass for a type F with an injective map to A ↪ B

This typeclass is primarily for use by embeddings such as RelEmbedding.

Basic usage of EmbeddingLike

A typical type of embeddings should be declared as: ``` structure MyEmbedding (A B : Type*) [MyClass A] [MyClass B] where (toFun : A → B) (injective' : Function.Injective toFun) (map_op' : ∀ (x y : A), toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))

namespace MyEmbedding

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

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

-- This instance is optional if you follow the \"Embedding class\" design below: instance : EmbeddingLike (MyEmbedding A B) A B where injective' := MyEmbedding.injective'

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

/-- Copy of a MyEmbedding with a new toFun equal to the old one. Useful to fix definitional equalities. -/ protected def copy (f : MyEmbedding A B) (f' : A → B) (h : f' = ⇑f) : MyEmbedding A B := { toFun := f' injective' := h.symm ▸ f.injective' mapop' := h.symm ▸ f.mapop' }

end MyEmbedding ```

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

Embedding classes extending EmbeddingLike

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

`` /--MyEmbeddingClass F A Bstates thatFis a type ofMyClass.op-preserving embeddings. You should extend this class when you extendMyEmbedding`. -/ class MyEmbeddingClass (F : Type) (A B : outParam Type) [MyClass A] [MyClass B] [FunLike F A B] extends EmbeddingLike F A B where 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] [MyEmbeddingClass F A B] (f : F) (x y : A) : f (MyClass.op x y) = MyClass.op (f x) (f y) := MyEmbeddingClass.mapop _ _ _

namespace MyEmbedding

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

-- You can replace MyEmbedding.EmbeddingLike with the below instance: instance : MyEmbeddingClass (MyEmbedding A B) A B where injective' := MyEmbedding.injective' mapop := MyEmbedding.mapop'

end MyEmbedding ```

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

``` structure CoolerEmbedding (A B : Type*) [CoolClass A] [CoolClass B] extends MyEmbedding A B where (map_cool' : toFun CoolClass.cool = CoolClass.cool)

class CoolerEmbeddingClass (F : Type) (A B : outParam Type) [CoolClass A] [CoolClass B] [FunLike F A B] extends MyEmbeddingClass F A B where (map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)

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

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

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

instance : CoolerEmbeddingClass (CoolerEmbedding A B) A B where injective' f := f.injective' 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 : MyEmbedding A B) : sorry := sorry lemma do_something {F : Type*} [FunLike F A B] [MyEmbeddingClass F A B] (f : F) : sorry := sorry

This means anything set up for MyEmbeddings will automatically work for CoolerEmbeddingClasses, and defining CoolerEmbeddingClass only takes a constant amount of effort, instead of linearly increasing the work per MyEmbedding-related declaration. "}

EmbeddingLike structure
(F : Sort*) (α β : outParam (Sort*)) [FunLike F α β]
Full source 
/-- The class `EmbeddingLike F α β` expresses that terms of type `F` have an
injective coercion to injective functions `α ↪ β`.
-/
class EmbeddingLike (F : Sort*) (α β : outParam (Sort*)) [FunLike F α β] : Prop where
  /-- The coercion to functions must produce injective functions. -/
  injective' : ∀ f : F, Function.Injective (DFunLike.coe f)
Embedding-like class
Informal description
The class `EmbeddingLike F α β` expresses that terms of type `F` have an injective coercion to injective functions from `α` to `β`. More precisely, for any `f : F`, the function `f : α → β` is injective, and for any `x, y : α`, we have `f x = f y` if and only if `x = y`.
EmbeddingLike.injective theorem
(f : F) : Function.Injective f
Full source 
protected theorem injective (f : F) : Function.Injective f :=
  injective' f
Injectivity of Embedding-like Functions
Informal description
For any term $f$ of type $F$ in the `EmbeddingLike` class, the function $f : \alpha \to \beta$ is injective. That is, for any $x, y \in \alpha$, if $f(x) = f(y)$, then $x = y$.
EmbeddingLike.apply_eq_iff_eq theorem
(f : F) {x y : α} : f x = f y ↔ x = y
Full source 
@[simp]
theorem apply_eq_iff_eq (f : F) {x y : α} : f x = f y ↔ x = y :=
  (EmbeddingLike.injective f).eq_iff
Equality Preservation under Embedding-like Functions
Informal description
For any term $f$ of type $F$ in the `EmbeddingLike` class and any elements $x, y$ of type $\alpha$, the equality $f(x) = f(y)$ holds if and only if $x = y$.
EmbeddingLike.comp_injective theorem
{F : Sort*} [FunLike F β γ] [EmbeddingLike F β γ] (f : α → β) (e : F) : Function.Injective (e ∘ f) ↔ Function.Injective f
Full source 
@[simp]
theorem comp_injective {F : Sort*} [FunLike F β γ] [EmbeddingLike F β γ] (f : α → β) (e : F) :
    Function.InjectiveFunction.Injective (e ∘ f) ↔ Function.Injective f :=
  (EmbeddingLike.injective e).of_comp_iff f
Injectivity of Composition with Embedding
Informal description
Let $F$ be a type with an injective coercion to functions from $\beta$ to $\gamma$ (i.e., $F$ is in the `EmbeddingLike` class). For any function $f : \alpha \to \beta$ and any embedding $e : F$, the composition $e \circ f$ is injective if and only if $f$ is injective. In symbols: $\text{Injective}(e \circ f) \leftrightarrow \text{Injective}(f)$.