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.

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₀), EquivFunctor.map (Equiv.refl α) = id

  map of f preserves the identity morphism.

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

  map is functorial on equivalences.

@[simp]

theorem EquivFunctor.map_refl' {f : Type u₀ → Type u₁} [self : EquivFunctor f] (α : Type u₀) : EquivFunctor.map (Equiv.refl α) = id

map of f preserves the identity morphism.

theorem EquivFunctor.map_trans' {f : Type u₀ → Type u₁} [self : EquivFunctor f] {α : Type u₀} {β : Type u₀} {γ : Type u₀} (k : α ≃ β) (h : β ≃ γ) : EquivFunctor.map (k.trans h) = EquivFunctor.map h ∘ EquivFunctor.map k

map is functorial on equivalences.

def EquivFunctor.mapEquiv (f : Type u₀ → Type u₁) [EquivFunctor f] {α : Type u₀} {β : 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 := ⋯ }

@[simp]

theorem EquivFunctor.mapEquiv_apply (f : Type u₀ → Type u₁) [EquivFunctor f] {α : Type u₀} {β : Type u₀} (e : α ≃ β) (x : f α) : (EquivFunctor.mapEquiv f e) x = EquivFunctor.map e x

theorem EquivFunctor.mapEquiv_symm_apply (f : Type u₀ → Type u₁) [EquivFunctor f] {α : Type u₀} {β : Type u₀} (e : α ≃ β) (y : f β) : (EquivFunctor.mapEquiv f e).symm y = EquivFunctor.map e.symm y

@[simp]

theorem EquivFunctor.mapEquiv_refl (f : Type u₀ → Type u₁) [EquivFunctor f] (α : Type u₀) : EquivFunctor.mapEquiv f (Equiv.refl α) = Equiv.refl (f α)

@[simp]

theorem EquivFunctor.mapEquiv_symm (f : Type u₀ → Type u₁) [EquivFunctor f] {α : Type u₀} {β : Type u₀} (e : α ≃ β) : (EquivFunctor.mapEquiv f e).symm = EquivFunctor.mapEquiv f e.symm

@[simp]

theorem EquivFunctor.mapEquiv_trans (f : Type u₀ → Type u₁) [EquivFunctor f] {α : Type u₀} {β : Type u₀} {γ : Type u₀} (ab : α ≃ β) (bc : β ≃ γ) : (EquivFunctor.mapEquiv f ab).trans (EquivFunctor.mapEquiv f bc) = EquivFunctor.mapEquiv f (ab.trans bc)

The composition of mapEquivs is carried over the EquivFunctor. For plain Functors, this lemma is named map_map when applied or map_comp_map when not applied.

@[instance 100]

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

Equations

• EquivFunctor.ofLawfulFunctor f = { map := fun {α β : Type u₀} (e : α ≃ β) => Functor.map ⇑e, map_refl' := ⋯, map_trans' := ⋯ }

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