# Functions functorial with respect to equivalences #

An `EquivFunctor` is a function from `Type → Type` equipped with the additional data of coherently mapping equivalences to equivalences.

In categorical language, it is an endofunctor of the "core" of the category `Type`.

source
class EquivFunctor (f : Type u₀ → Type u₁) :
Type (max (u₀ + 1) u₁)

An `EquivFunctor` is only functorial with respect to equivalences.

To construct an `EquivFunctor`, it suffices to supply just the function `f α → f β` from an equivalence `α ≃ β`, and then prove the functor laws. It's then a consequence that this function is part of an equivalence, provided by `EquivFunctor.mapEquiv`.

- map {α β : Type u₀} : α ≃ β → f α → f β

  The action of `f` on isomorphisms.

- map_refl' (α : Type u₀) : map (Equiv.refl α) = id

  `map` of `f` preserves the identity morphism.

- map_trans' {α β γ : Type u₀} (k : α ≃ β) (h : β ≃ γ) : map (k.trans h) = map h ∘ map k

  `map` is functorial on equivalences.

Instances

source
def EquivFunctor.mapEquiv (f : Type u₀ → Type u₁) [EquivFunctor f] {α β : Type u₀} (e : α ≃ β) :
f α ≃ f β

An `EquivFunctor` in fact takes every equiv to an equiv.

Equations

- EquivFunctor.mapEquiv f e = { toFun := EquivFunctor.map e, invFun := EquivFunctor.map e.symm, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem EquivFunctor.mapEquiv_apply (f : Type u₀ → Type u₁) [EquivFunctor f] {α β : Type u₀} (e : α ≃ β) (x : f α) :
(mapEquiv f e) x = map e x
source
theorem EquivFunctor.mapEquiv_symm_apply (f : Type u₀ → Type u₁) [EquivFunctor f] {α β : Type u₀} (e : α ≃ β) (y : f β) :
(mapEquiv f e).symm y = map e.symm y
source
@[simp]
theorem EquivFunctor.mapEquiv_refl (f : Type u₀ → Type u₁) [EquivFunctor f] (α : Type u₀) :
mapEquiv f (Equiv.refl α) = Equiv.refl (f α)
source
@[simp]
theorem EquivFunctor.mapEquiv_symm (f : Type u₀ → Type u₁) [EquivFunctor f] {α β : Type u₀} (e : α ≃ β) :
(mapEquiv f e).symm = mapEquiv f e.symm
source
@[simp]
theorem EquivFunctor.mapEquiv_trans (f : Type u₀ → Type u₁) [EquivFunctor f] {α β γ : Type u₀} (ab : α ≃ β) (bc : β ≃ γ) :
(mapEquiv f ab).trans (mapEquiv f bc) = mapEquiv f (ab.trans bc)

The composition of `mapEquiv`s is carried over the `EquivFunctor`. For plain `Functor`s, this lemma is named `map_map` when applied or `map_comp_map` when not applied.

source
@[instance 100]
instance EquivFunctor.ofLawfulFunctor (f : Type u₀ → Type u₁) [Functor f] [LawfulFunctor f] :
EquivFunctor f
Equations

- EquivFunctor.ofLawfulFunctor f = { map := fun {x x_1 : Type ?u.20} (e : x ≃ x_1) => Functor.map ⇑e, map_refl' := ⋯, map_trans' := ⋯ }

source
theorem EquivFunctor.mapEquiv.injective (f : Type u₀ → Type u₁) [Applicative f] [LawfulApplicative f] {α β : Type u₀} (h : ∀ (γ : Type u₀), Function.Injective pure) :
Function.Injective (mapEquiv f)