Module docstring
{"# 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 leftinv f := f.leftinv rightinv f := f.rightinv coeinjective' f g h₁ h₂ := by cases f; cases g; congr; exact EquivLike.coeinjective' _ _ 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) (finv : B → A)
(h₁ : f' = f) (h₂ : finv = f.invFun) : MyIso A B where
toFun := f'
invFun := finv
leftinv := h₁.symm ▸ h₂.symm ▸ f.leftinv
rightinv := h₁.symm ▸ h₂.symm ▸ f.rightinv
mapop' := 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 Bstates thatFis a type ofMyClass.op-preserving morphisms.
You should extend this class when you extendMyIso`. -/
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
mapop := MyIso.mapop'
-- [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 mapcool {F A B : Type*} [CoolClass A] [CoolClass B] [EquivLike F A B] [CoolerIsoClass F A B] (f : F) : f CoolClass.cool = CoolClass.cool := CoolerIsoClass.mapcool _
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 leftinv f := f.leftinv rightinv f := f.rightinv coeinjective' f g h₁ h₂ := by cases f; cases g; congr; exact EquivLike.coeinjective' _ _ h₁ h₂
instance : CoolerIsoClass (CoolerIso A B) A B where mapop f := f.mapop' mapcool f := f.mapcool'
-- [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 MyIsos will automatically work for CoolerIsoClasses,
and defining CoolerIsoClass only takes a constant amount of effort,
instead of linearly increasing the work per MyIso-related declaration.
"}