-
Notifications
You must be signed in to change notification settings - Fork 273
/
Functor.lean
95 lines (74 loc) · 2.75 KB
/
Functor.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
/-
Copyright (c) 2019 Johan Commelin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin, Simon Hudon, Scott Morrison
-/
import Mathlib.Control.Bifunctor
import Mathlib.Logic.Equiv.Defs
#align_import logic.equiv.functor from "leanprover-community/mathlib"@"9407b03373c8cd201df99d6bc5514fc2db44054f"
/-!
# Functor and bifunctors can be applied to `Equiv`s.
We define
```lean
def Functor.mapEquiv (f : Type u → Type v) [Functor f] [LawfulFunctor f] :
α ≃ β → f α ≃ f β
```
and
```lean
def Bifunctor.mapEquiv (F : Type u → Type v → Type w) [Bifunctor F] [LawfulBifunctor F] :
α ≃ β → α' ≃ β' → F α α' ≃ F β β'
```
-/
universe u v w
variable {α β : Type u}
open Equiv
namespace Functor
variable (f : Type u → Type v) [Functor f] [LawfulFunctor f]
/-- Apply a functor to an `Equiv`. -/
def mapEquiv (h : α ≃ β) : f α ≃ f β where
toFun := map h
invFun := map h.symm
left_inv x := by simp [map_map]
right_inv x := by simp [map_map]
#align functor.map_equiv Functor.mapEquiv
@[simp]
theorem mapEquiv_apply (h : α ≃ β) (x : f α) : (mapEquiv f h : f α ≃ f β) x = map h x :=
rfl
#align functor.map_equiv_apply Functor.mapEquiv_apply
@[simp]
theorem mapEquiv_symm_apply (h : α ≃ β) (y : f β) :
(mapEquiv f h : f α ≃ f β).symm y = map h.symm y :=
rfl
#align functor.map_equiv_symm_apply Functor.mapEquiv_symm_apply
@[simp]
theorem mapEquiv_refl : mapEquiv f (Equiv.refl α) = Equiv.refl (f α) := by
ext x
simp only [mapEquiv_apply, refl_apply]
exact LawfulFunctor.id_map x
#align functor.map_equiv_refl Functor.mapEquiv_refl
end Functor
namespace Bifunctor
variable {α' β' : Type v} (F : Type u → Type v → Type w) [Bifunctor F] [LawfulBifunctor F]
/-- Apply a bifunctor to a pair of `Equiv`s. -/
def mapEquiv (h : α ≃ β) (h' : α' ≃ β') : F α α' ≃ F β β' where
toFun := bimap h h'
invFun := bimap h.symm h'.symm
left_inv x := by simp [bimap_bimap, id_bimap]
right_inv x := by simp [bimap_bimap, id_bimap]
#align bifunctor.map_equiv Bifunctor.mapEquiv
@[simp]
theorem mapEquiv_apply (h : α ≃ β) (h' : α' ≃ β') (x : F α α') :
(mapEquiv F h h' : F α α' ≃ F β β') x = bimap h h' x :=
rfl
#align bifunctor.map_equiv_apply Bifunctor.mapEquiv_apply
@[simp]
theorem mapEquiv_symm_apply (h : α ≃ β) (h' : α' ≃ β') (y : F β β') :
(mapEquiv F h h' : F α α' ≃ F β β').symm y = bimap h.symm h'.symm y :=
rfl
#align bifunctor.map_equiv_symm_apply Bifunctor.mapEquiv_symm_apply
@[simp]
theorem mapEquiv_refl_refl : mapEquiv F (Equiv.refl α) (Equiv.refl α') = Equiv.refl (F α α') := by
ext x
simp [id_bimap]
#align bifunctor.map_equiv_refl_refl Bifunctor.mapEquiv_refl_refl
end Bifunctor