# mathlib3documentation

control.equiv_functor

# Functions functorial with respect to equivalences #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

An equiv_functor 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.

@[class]
structure equiv_functor (f : Type u₀ Type u₁) :
Type (max (u₀+1) u₁)
• map : Π {α β : Type ?}, α β f α f β
• map_refl' : ( (α : Type ?), . "obviously"
• map_trans' : ( {α β γ : Type ?} (k : α β) (h : β γ), . "obviously"

An equiv_functor is only functorial with respect to equivalences.

To construct an equiv_functor, 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 equiv_functor.map_equiv.

Instances of this typeclass
Instances of other typeclasses for equiv_functor
• equiv_functor.has_sizeof_inst
@[simp]
theorem equiv_functor.map_refl {f : Type u₀ Type u₁} [self : equiv_functor f] (α : Type u₀) :
theorem equiv_functor.map_trans {f : Type u₀ Type u₁} [self : equiv_functor f] {α β γ : Type u₀} (k : α β) (h : β γ) :
def equiv_functor.map_equiv (f : Type u₀ Type u₁) {α β : Type u₀} (e : α β) :
f α f β

An equiv_functor in fact takes every equiv to an equiv.

Equations
@[simp]
theorem equiv_functor.map_equiv_apply (f : Type u₀ Type u₁) {α β : Type u₀} (e : α β) (x : f α) :
x =
theorem equiv_functor.map_equiv_symm_apply (f : Type u₀ Type u₁) {α β : Type u₀} (e : α β) (y : f β) :
e).symm) y =
@[simp]
theorem equiv_functor.map_equiv_refl (f : Type u₀ Type u₁) (α : Type u₀) :
= equiv.refl (f α)
@[simp]
theorem equiv_functor.map_equiv_symm (f : Type u₀ Type u₁) {α β : Type u₀} (e : α β) :
@[simp]
theorem equiv_functor.map_equiv_trans (f : Type u₀ Type u₁) {α β γ : Type u₀} (ab : α β) (bc : β γ) :
ab).trans bc) = (ab.trans bc)

The composition of map_equivs is carried over the equiv_functor. For plain functors, this lemma is named map_map when applied or map_comp_map when not applied.

@[protected, instance]
Equations
theorem equiv_functor.map_equiv.injective (f : Type u₀ Type u₁) [applicative f] {α β : Type u₀} (h : (γ : Type u₀), ) :