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.

source

@[class]

structure equiv_functor (f : Type u₀ → Type u₁) :

Type (max (u₀+1) u₁)

map : Π {α β : Type ?}, α ≃ β → f α → f β
map_refl' : (∀ (α : Type ?), equiv_functor.map (equiv.refl α) = id) . "obviously"
map_trans' : (∀ {α β γ : Type ?} (k : α ≃ β) (h : β ≃ γ), equiv_functor.map (k.trans h) = equiv_functor.map h ∘ equiv_functor.map k) . "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

source

@[simp]

theorem equiv_functor.map_refl {f : Type u₀ → Type u₁} [self : equiv_functor f] (α : Type u₀) :

equiv_functor.map (equiv.refl α) = id

source

theorem equiv_functor.map_trans {f : Type u₀ → Type u₁} [self : equiv_functor f] {α β γ : Type u₀} (k : α ≃ β) (h : β ≃ γ) :

equiv_functor.map (k.trans h) = equiv_functor.map h ∘ equiv_functor.map k

source

def equiv_functor.map_equiv (f : Type u₀ → Type u₁) [equiv_functor f] {α β : Type u₀} (e : α ≃ β) :

f α ≃ f β

An equiv_functor in fact takes every equiv to an equiv.

Equations

equiv_functor.map_equiv f e = {to_fun := equiv_functor.map e, inv_fun := equiv_functor.map e.symm, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv_functor.map_equiv_apply (f : Type u₀ → Type u₁) [equiv_functor f] {α β : Type u₀} (e : α ≃ β) (x : f α) :

⇑(equiv_functor.map_equiv f e) x = equiv_functor.map e x

source

theorem equiv_functor.map_equiv_symm_apply (f : Type u₀ → Type u₁) [equiv_functor f] {α β : Type u₀} (e : α ≃ β) (y : f β) :

⇑((equiv_functor.map_equiv f e).symm) y = equiv_functor.map e.symm y

source

@[simp]

theorem equiv_functor.map_equiv_refl (f : Type u₀ → Type u₁) [equiv_functor f] (α : Type u₀) :

equiv_functor.map_equiv f (equiv.refl α) = equiv.refl (f α)

source

@[simp]

theorem equiv_functor.map_equiv_symm (f : Type u₀ → Type u₁) [equiv_functor f] {α β : Type u₀} (e : α ≃ β) :

(equiv_functor.map_equiv f e).symm = equiv_functor.map_equiv f e.symm

source

@[simp]

theorem equiv_functor.map_equiv_trans (f : Type u₀ → Type u₁) [equiv_functor f] {α β γ : Type u₀} (ab : α ≃ β) (bc : β ≃ γ) :

(equiv_functor.map_equiv f ab).trans (equiv_functor.map_equiv f bc) = equiv_functor.map_equiv f (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.

source

@[protected, instance]

def equiv_functor.of_is_lawful_functor (f : Type u₀ → Type u₁) [functor f] [is_lawful_functor f] :

equiv_functor f

Equations

equiv_functor.of_is_lawful_functor f = {map := λ (α β : Type u₀) (e : α ≃ β), functor.map ⇑e, map_refl' := _, map_trans' := _}

source

theorem equiv_functor.map_equiv.injective (f : Type u₀ → Type u₁) [applicative f] [is_lawful_applicative f] {α β : Type u₀} (h : ∀ (γ : Type u₀), function.injective has_pure.pure) :

function.injective (equiv_functor.map_equiv f)