Functions functorial with respect to equivalences #
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]
- 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
@[simp]
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
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 := _}
@[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
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
@[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 α)
@[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
@[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.
@[protected, instance]
Equations
- equiv_functor.of_is_lawful_functor f = {map := λ (α β : Type u₀) (e : α ≃ β), functor.map ⇑e, map_refl' := _, map_trans' := _}
theorem
equiv_functor.map_equiv.injective
(f : Type u₀ → Type u₁)
[applicative f]
[is_lawful_applicative f]
{α β : Type u₀}
(h : ∀ (γ : Type u₀), function.injective pure) :