Typeclass for a type F
with an injective map to A ≃ B
#
This typeclass is primarily for use by isomorphisms like MonoidEquiv
and LinearEquiv
.
Basic usage of EquivLike
#
A typical type of isomorphisms should be declared as:
structure MyIso (A B : Type*) [MyClass A] [MyClass B] extends Equiv A B where
(map_op' : ∀ (x y : A), toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))
namespace MyIso
variable (A B : Type*) [MyClass A] [MyClass B]
instance instEquivLike : EquivLike (MyIso A B) A B where
coe f := f.toFun
inv f := f.invFun
left_inv f := f.left_inv
right_inv f := f.right_inv
coe_injective' f g h₁ h₂ := by cases f; cases g; congr; exact EquivLike.coe_injective' _ _ h₁ h₂
@[ext] theorem ext {f g : MyIso A B} (h : ∀ x, f x = g x) : f = g := DFunLike.ext f g h
/-- Copy of a `MyIso` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : MyIso A B) (f' : A → B) (f_inv : B → A)
(h₁ : f' = f) (h₂ : f_inv = f.invFun) : MyIso A B where
toFun := f'
invFun := f_inv
left_inv := h₁.symm ▸ h₂.symm ▸ f.left_inv
right_inv := h₁.symm ▸ h₂.symm ▸ f.right_inv
map_op' := h₁.symm ▸ f.map_op'
end MyIso
This file will then provide a CoeFun
instance and various
extensionality and simp lemmas.
Isomorphism classes extending EquivLike
#
The EquivLike
design provides further benefits if you put in a bit more work.
The first step is to extend EquivLike
to create a class of those types satisfying
the axioms of your new type of isomorphisms.
Continuing the example above:
/-- `MyIsoClass F A B` states that `F` is a type of `MyClass.op`-preserving morphisms.
You should extend this class when you extend `MyIso`. -/
class MyIsoClass (F : Type*) (A B : outParam Type*) [MyClass A] [MyClass B]
[EquivLike F A B]
extends MyHomClass F A B
namespace MyIso
variable {A B : Type*} [MyClass A] [MyClass B]
-- This goes after `MyIsoClass.instEquivLike`:
instance : MyIsoClass (MyIso A B) A B where
map_op := MyIso.map_op'
-- [Insert `ext` and `copy` here]
end MyIso
The second step is to add instances of your new MyIsoClass
for all types extending MyIso
.
Typically, you can just declare a new class analogous to MyIsoClass
:
structure CoolerIso (A B : Type*) [CoolClass A] [CoolClass B] extends MyIso A B where
(map_cool' : toFun CoolClass.cool = CoolClass.cool)
class CoolerIsoClass (F : Type*) (A B : outParam Type*) [CoolClass A] [CoolClass B]
[EquivLike F A B]
extends MyIsoClass F A B where
(map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)
@[simp] lemma map_cool {F A B : Type*} [CoolClass A] [CoolClass B]
[EquivLike F A B] [CoolerIsoClass F A B] (f : F) :
f CoolClass.cool = CoolClass.cool :=
CoolerIsoClass.map_cool _
namespace CoolerIso
variable {A B : Type*} [CoolClass A] [CoolClass B]
instance : EquivLike (CoolerIso A B) A B where
coe f := f.toFun
inv f := f.invFun
left_inv f := f.left_inv
right_inv f := f.right_inv
coe_injective' f g h₁ h₂ := by cases f; cases g; congr; exact EquivLike.coe_injective' _ _ h₁ h₂
instance : CoolerIsoClass (CoolerIso A B) A B where
map_op f := f.map_op'
map_cool f := f.map_cool'
-- [Insert `ext` and `copy` here]
end CoolerIso
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 : MyIso A B) : sorry := sorry
lemma do_something {F : Type*} [EquivLike F A B] [MyIsoClass F A B] (f : F) : sorry := sorry
This means anything set up for MyIso
s will automatically work for CoolerIsoClass
es,
and defining CoolerIsoClass
only takes a constant amount of effort,
instead of linearly increasing the work per MyIso
-related declaration.
The class EquivLike E α β
expresses that terms of type E
have an
injective coercion to bijections between α
and β
.
Note that this does not directly extend FunLike
, nor take FunLike
as a parameter,
so we can state coe_injective'
in a nicer way.
This typeclass is used in the definition of the isomorphism (or equivalence) typeclasses,
such as ZeroEquivClass
, MulEquivClass
, MonoidEquivClass
, ....
- coe : E → α → β
The coercion to a function in the forward direction.
- inv : E → β → α
The coercion to a function in the backwards direction.
- left_inv (e : E) : Function.LeftInverse (inv e) (coe e)
The coercions are left inverses.
- right_inv (e : E) : Function.RightInverse (inv e) (coe e)
The coercions are right inverses.
The two coercions to functions are jointly injective.
Instances
This lemma is only supposed to be used in the generic context, when working with instances
of classes extending EquivLike
.
For concrete isomorphism types such as Equiv
, you should use Equiv.symm_apply_apply
or its equivalent.
TODO: define a generic form of Equiv.symm
.
This lemma is only supposed to be used in the generic context, when working with instances
of classes extending EquivLike
.
For concrete isomorphism types such as Equiv
, you should use Equiv.apply_symm_apply
or its equivalent.
TODO: define a generic form of Equiv.symm
.
This is not an instance to avoid slowing down every single Subsingleton
typeclass search.