Typeclass for a type `F` with an injective map to `A ↪ B↪ 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] :=
(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

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

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

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

@[ext] theorem ext {f g : MyEmbedding A B} (h : ∀ x, f x = g x) : f = g := FunLike.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',
  map_op' := h.symm ▸ f.map_op' }

end MyEmbedding
→ B)
(injective' : Function.Injective toFun)
(map_op' : ∀ {x y : A}, toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))

namespace MyEmbedding

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

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

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

@[ext] theorem ext {f g : MyEmbedding A B} (h : ∀ x, f x = g x) : f = g := FunLike.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',
  map_op' := h.symm ▸ f.map_op' }

end MyEmbedding
∀ {x y : A}, toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))

namespace MyEmbedding

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

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

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

@[ext] theorem ext {f g : MyEmbedding A B} (h : ∀ x, f x = g x) : f = g := FunLike.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',
  map_op' := h.symm ▸ f.map_op' }

end MyEmbedding
→ B) := ⟨MyEmbedding.toFun⟩

@[ext] theorem ext {f g : MyEmbedding A B} (h : ∀ x, f x = g x) : f = g := FunLike.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',
  map_op' := h.symm ▸ f.map_op' }

end MyEmbedding
∀ x, f x = g x) : f = g := FunLike.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',
  map_op' := h.symm ▸ f.map_op' }

end MyEmbedding
→ B) (h : f' = ⇑f) : MyEmbedding A B :=
{ toFun := f',
  injective' := h.symm ▸ f.injective',
  map_op' := h.symm ▸ f.map_op' }

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

end MyEmbedding
▸ f.injective',
  map_op' := h.symm ▸ f.map_op' }

end MyEmbedding
▸ f.map_op' }

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:

section

/-- `MyEmbeddingClass F A B` states that `F` is a type of `MyClass.op`-preserving embeddings.
You should extend this class when you extend `MyEmbedding`. -/
class MyEmbeddingClass (F : Type _) (A B : outParam <| Type _) [MyClass A] [MyClass B]
  extends EmbeddingLike F A B :=
(map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y))

end

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

-- You can replace `MyEmbedding.EmbeddingLike` with the below instance:
instance : MyEmbeddingClass (MyEmbedding A B) A B :=
{ coe := MyEmbedding.toFun,
  coe_injective' := λ f g h, by cases f; cases g; congr',
  injective' := MyEmbedding.injective',
  map_op := MyEmbedding.map_op' }

-- [Insert `CoeFun`, `ext` and `copy` here]
∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y))

end

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

-- You can replace `MyEmbedding.EmbeddingLike` with the below instance:
instance : MyEmbeddingClass (MyEmbedding A B) A B :=
{ coe := MyEmbedding.toFun,
  coe_injective' := λ f g h, by cases f; cases g; congr',
  injective' := MyEmbedding.injective',
  map_op := MyEmbedding.map_op' }

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

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

section
set_option old_structure_cmd true

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

end

@[simp] lemma map_cool {F A B : Type _} [CoolClass A] [CoolClass B] [CoolerEmbeddingClass F A B]
  (f : F) : f CoolClass.cool = CoolClass.cool :=
MyEmbeddingClass.map_op

-- You can also replace `MyEmbedding.EmbeddingLike` with the below instance:
instance : CoolerEmbeddingClass (CoolerEmbedding A B) A B :=
{ coe := CoolerEmbedding.toFun,
  coe_injective' := λ f g h, by cases f; cases g; congr',
  injective' := MyEmbedding.injective',
  map_op := CoolerEmbedding.map_op',
  map_cool := CoolerEmbedding.map_cool' }

-- [Insert `CoeFun`, `ext` and `copy` here]
∀ (f : F), f CoolClass.cool = CoolClass.cool)

end

@[simp] lemma map_cool {F A B : Type _} [CoolClass A] [CoolClass B] [CoolerEmbeddingClass F A B]
  (f : F) : f CoolClass.cool = CoolClass.cool :=
MyEmbeddingClass.map_op

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

source

ink

class EmbeddingLike (F : Sort u_1) (α : outParam (Sort u_2)) (β : outParam (Sort u_3)) extends FunLike :

Sort (max(max(max1u_1)u_2)u_3)

The coercion to functions must produce injective functions.
injective' : ∀ (f : F), Function.Injective ↑f

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

Instances

source

ink

theorem EmbeddingLike.injective {F : Sort u_3} {α : Sort u_1} {β : Sort u_2} [i : EmbeddingLike F α β] (f : F) :

Function.Injective ↑f

source

ink

@[simp]

theorem EmbeddingLike.apply_eq_iff_eq {F : Sort u_2} {α : Sort u_3} {β : Sort u_1} [i : EmbeddingLike F α β] (f : F) {x : α} {y : α} :

↑f x = ↑f y ↔ x = y

source

ink

@[simp]

theorem EmbeddingLike.comp_injective {α : Sort u_4} {β : Sort u_2} {γ : Sort u_3} {F : Sort u_1} [inst : EmbeddingLike F β γ] (f : α → β) (e : F) :

Function.Injective (↑e ∘ f) ↔ Function.Injective f

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

Basic usage of EmbeddingLike #

Embedding classes extending EmbeddingLike #

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

Basic usage of `EmbeddingLike` #

Embedding classes extending `EmbeddingLike` #