Built with
doc-gen4, running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑Ctrl+↓to navigate,
Ctrl+🖱️to focus.
On Mac, use
Cmdinstead of
Ctrl.
/-
Copyright (c) 2021 Anne Baanen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anne Baanen
! This file was ported from Lean 3 source module data.fun_like.equiv
! leanprover-community/mathlib commit f340f229b1f461aa1c8ee11e0a172d0a3b301a4a
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.FunLike.Embedding
/-!
# 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 morphisms should be declared as:
```
structure MyIso (A B : Type _) [MyClass A] [MyClass B]
extends Equiv A B :=
(map_op' : ∀ {x y : A}, toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))
namespace MyIso
variables (A B : Type _) [MyClass A] [MyClass B]
-- This instance is optional if you follow the "Isomorphism class" design below:
instance : EquivLike (MyIso A B) A (λ _, B) :=
{ coe := MyIso.toEquiv.toFun,
inv := MyIso.toEquiv.invFun,
left_inv := MyIso.toEquiv.left_inv,
right_inv := MyIso.toEquiv.right_inv,
coe_injective' := λ f g h, by cases f; cases g; congr' }
/-- Helper instance for when there's too many metavariables to apply `EquivLike.coe` directly. -/
instance : CoeFun (MyIso A B) := FunLike.instCoeFunForAll
@[ext] theorem ext {f g : MyIso A B} (h : ∀ x, f x = g x) : f = g := FunLike.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) : MyIso A B :=
{ toFun := f',
invFun := f_inv,
left_inv := h.symm ▸ f.left_inv,
right_inv := 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]
extends EquivLike F A (λ _, B), MyHomClass F A B
end
-- You can replace `MyIso.EquivLike` with the below instance:
instance : MyIsoClass (MyIso A B) A B :=
{ coe := MyIso.toFun,
inv := MyIso.invFun,
left_inv := MyIso.left_inv,
right_inv := MyIso.right_inv,
coe_injective' := λ f g h, by cases f; cases g; congr',
map_op := MyIso.map_op' }
-- [Insert `CoeFun`, `ext` and `copy` here]
```
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 :=
(map_cool' : toFun CoolClass.cool = CoolClass.cool)
section
set_option old_structure_cmd true
class CoolerIsoClass (F : Type _) (A B : outParam <| Type _) [CoolClass A] [CoolClass B]
extends MyIsoClass 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] [CoolerIsoClass F A B]
(f : F) : f CoolClass.cool = CoolClass.cool :=
CoolerIsoClass.map_cool
instance : CoolerIsoClass (CoolerIso A B) A B :=
{ coe := CoolerIso.toFun,
coe_injective' := λ f g h, by cases f; cases g; congr',
map_op := CoolerIso.map_op',
map_cool := CoolerIso.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 : MyIso A B) : sorry := sorry
lemma do_something {F : Type _} [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 `β`.
This typeclass is used in the definition of the homomorphism typeclasses,
such as `ZeroEquivClass`, `MulEquivClass`, `MonoidEquivClass`, ....
-/
class EquivLike (E : Sort _) (α β : outParam (Sort _)) where
/-- The coercion to a function in the forward direction. -/
coe : E → α → β
/-- The coercion to a function in the backwards direction. -/
inv : E → β → α
/-- The coercions are left inverses. -/
left_inv : ∀ e, Function.LeftInverse: {α : Sort ?u.32} → {β : Sort ?u.31} → (β → α) → (α → β) → Prop
Function.RightInverse: {α : Sort ?u.53} → {β : Sort ?u.52} → (β → α) → (α → β) → Prop
Function.Injective: {α : Sort ?u.155} → {β : Sort ?u.154} → (α → β) → Prop
symm: ∀ {α : Sort ?u.267} {a b : α}, a = b → b = a
symm: ∀ {α : Sort ?u.493} {a b : α}, a = b → b = a
Function.Injective: {α : Sort ?u.739} → {β : Sort ?u.738} → (α → β) → Prop
Function.Surjective: {α : Sort ?u.910} → {β : Sort ?u.909} → (α → β) → Prop
Function.Bijective: {α : Sort ?u.1085} → {β : Sort ?u.1084} → (α → β) → Prop
apply_eq_iff_eq: ∀ (f : E) {x y : α}, ↑f x = ↑f y ↔ x = y
EmbeddingLike.apply_eq_iff_eq: ∀ {F : Sort ?u.1453} {α : Sort ?u.1454} {β : Sort ?u.1452} [i : EmbeddingLike F α β] (f : F) {x y : α},
↑f x = ↑f y ↔ x = y
EquivLike.apply_eq_iff_eq: ∀ {E : Sort u_2} {α : Sort u_3} {β : Sort u_1} [iE : EquivLike E α β] (f : E) {x y : α}, ↑f x = ↑f y ↔ x = y
Function.Injective: {α : Sort ?u.1548} → {β : Sort ?u.1547} → (α → β) → Prop
Function.Injective: {α : Sort ?u.1655} → {β : Sort ?u.1654} → (α → β) → Prop
Function.Surjective: {α : Sort ?u.1797} → {β : Sort ?u.1796} → (α → β) → Prop
Function.Surjective: {α : Sort ?u.1904} → {β : Sort ?u.1903} → (α → β) → Prop
Function.Bijective: {α : Sort ?u.2043} → {β : Sort ?u.2042} → (α → β) → Prop
Function.Bijective: {α : Sort ?u.2150} → {β : Sort ?u.2149} → (α → β) → Prop
EquivLike.inv_apply_apply: ∀ {E : Sort u_2} {α : Sort u_1} {β : Sort u_3} [iE : EquivLike E α β] (e : E) (a : α), inv e (↑e a) = a
EquivLike.apply_inv_apply: ∀ {E : Sort u_2} {α : Sort u_3} {β : Sort u_1} [iE : EquivLike E α β] (e : E) (b : β), ↑e (inv e b) = b
Function.Injective: {α : Sort ?u.2717} → {β : Sort ?u.2716} → (α → β) → Prop
Function.Injective: {α : Sort ?u.2824} → {β : Sort ?u.2823} → (α → β) → Prop
Function.Surjective: {α : Sort ?u.2919} → {β : Sort ?u.2918} → (α → β) → Prop
Function.Surjective: {α : Sort ?u.3026} → {β : Sort ?u.3025} → (α → β) → Prop
Function.Bijective: {α : Sort ?u.3161} → {β : Sort ?u.3160} → (α → β) → Prop
Function.Bijective: {α : Sort ?u.3268} → {β : Sort ?u.3267} → (α → β) → Prop
FunLike.ext: ∀ {F : Sort ?u.3416} {α : Sort ?u.3417} {β : α → Sort ?u.3415} [i : FunLike F α β] (f g : F),
(∀ (x : α), ↑f x = ↑g x) → f = g