Mathlib.Control.EquivFunctor

EquivFunctor structure

(f : Type u₀ → Type u₁)

Full source

/-- 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`.
-/
class EquivFunctor (f : Type u₀ → Type u₁) where
  /-- The action of `f` on isomorphisms. -/
  map : ∀ {α β}, α ≃ β → f α → f β
  /-- `map` of `f` preserves the identity morphism. -/
  map_refl' : ∀ α, map (Equiv.refl α) = @id (f α) := by rfl
  /-- `map` is functorial on equivalences. -/
  map_trans' : ∀ {α β γ} (k : α ≃ β) (h : β ≃ γ), map (k.trans h) = map h ∘ map k := by rfl

Equivalence-preserving functor on types

Informal description

An `EquivFunctor` is a structure that consists of a type constructor `f : Type → Type` equipped with the ability to coherently map equivalences between types to equivalences between the corresponding constructed types. Specifically, for any equivalence `e : α ≃ β`, there is an induced equivalence `mapEquiv e : f α ≃ f β` that satisfies the functoriality laws.

EquivFunctor.mapEquiv definition

: f α ≃ f β

Full source

/-- An `EquivFunctor` in fact takes every equiv to an equiv. -/
def mapEquiv : f α ≃ f β where
  toFun := EquivFunctor.map e
  invFun := EquivFunctor.map e.symm
  left_inv x := by
    convert (congr_fun (EquivFunctor.map_trans' e e.symm) x).symm
    simp
  right_inv y := by
    convert (congr_fun (EquivFunctor.map_trans' e.symm e) y).symm
    simp

Functorial mapping of equivalences

Informal description

Given an equivalence $e : \alpha \simeq \beta$, the function `mapEquiv` constructs an equivalence $f \alpha \simeq f \beta$ by applying the functorial mapping of $f$ to $e$ and its inverse. Specifically, the forward map is `EquivFunctor.map e` and the inverse map is `EquivFunctor.map e.symm`, satisfying the bijection properties.

EquivFunctor.mapEquiv_apply theorem

(x : f α) : mapEquiv f e x = EquivFunctor.map e x

Full source

@[simp]
theorem mapEquiv_apply (x : f α) : mapEquiv f e x = EquivFunctor.map e x :=
  rfl

Functorial Mapping of Equivalence Preserves Application

Informal description

For any equivalence-preserving functor $f$ on types and any equivalence $e : \alpha \simeq \beta$, the application of the mapped equivalence $\text{mapEquiv}\,f\,e$ to an element $x \in f\alpha$ equals the functorial mapping of $e$ applied to $x$, i.e., $(\text{mapEquiv}\,f\,e)(x) = f(e)(x)$.

EquivFunctor.mapEquiv_symm_apply theorem

(y : f β) : (mapEquiv f e).symm y = EquivFunctor.map e.symm y

Full source

theorem mapEquiv_symm_apply (y : f β) : (mapEquiv f e).symm y = EquivFunctor.map e.symm y :=
  rfl

Inverse of Mapped Equivalence via Functorial Action

Informal description

For any equivalence-preserving functor $f$ on types and any equivalence $e : \alpha \simeq \beta$, the inverse of the mapped equivalence $(f e)^{-1} : f \beta \to f \alpha$ applied to an element $y \in f \beta$ equals the functorial mapping of the inverse equivalence $f(e^{-1})$ applied to $y$. That is, $(f e)^{-1}(y) = f(e^{-1})(y)$.

EquivFunctor.mapEquiv_refl theorem

(α) : mapEquiv f (Equiv.refl α) = Equiv.refl (f α)

Full source

@[simp]
theorem mapEquiv_refl (α) : mapEquiv f (Equiv.refl α) = Equiv.refl (f α) := by
 ext; simp [mapEquiv]

Functorial Mapping Preserves Identity Equivalence

Informal description

For any equivalence-preserving functor $f$ on types and any type $\alpha$, the functorial mapping of the identity equivalence $\text{id}_\alpha : \alpha \simeq \alpha$ is equal to the identity equivalence on $f \alpha$, i.e., $f(\text{id}_\alpha) = \text{id}_{f\alpha}$.

EquivFunctor.mapEquiv_symm theorem

: (mapEquiv f e).symm = mapEquiv f e.symm

Full source

@[simp]
theorem mapEquiv_symm : (mapEquiv f e).symm = mapEquiv f e.symm :=
  Equiv.ext <| mapEquiv_symm_apply f e

Inverse of Mapped Equivalence Equals Mapped Inverse

Informal description

For any equivalence-preserving functor $f$ on types and any equivalence $e : \alpha \simeq \beta$, the inverse of the mapped equivalence $(f e)^{-1} : f \beta \simeq f \alpha$ is equal to the functorial mapping of the inverse equivalence $f(e^{-1})$. That is, $(f e)^{-1} = f(e^{-1})$.

EquivFunctor.mapEquiv_trans theorem

{γ : Type u₀} (ab : α ≃ β) (bc : β ≃ γ) : (mapEquiv f ab).trans (mapEquiv f bc) = mapEquiv f (ab.trans bc)

Full source

/-- 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.
-/
@[simp]
theorem mapEquiv_trans {γ : Type u₀} (ab : α ≃ β) (bc : β ≃ γ) :
    (mapEquiv f ab).trans (mapEquiv f bc) = mapEquiv f (ab.trans bc) :=
  Equiv.ext fun x => by simp [mapEquiv, map_trans']

Functoriality of Equivalence Mapping: Composition Preserved Under `mapEquiv`

Informal description

For any type constructor $f$ that is an `EquivFunctor`, and for any equivalences $ab : \alpha \simeq \beta$ and $bc : \beta \simeq \gamma$, the composition of the mapped equivalences $(f \alpha \simeq f \beta) \circ (f \beta \simeq f \gamma)$ is equal to the mapped equivalence of the composition $(\alpha \simeq \gamma)$. In other words, the following equality holds: $$(f_{map}(ab)) \circ (f_{map}(bc)) = f_{map}(ab \circ bc)$$

EquivFunctor.ofLawfulFunctor instance

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

Full source

instance (priority := 100) ofLawfulFunctor (f : Type u₀ → Type u₁) [Functor f] [LawfulFunctor f] :
    EquivFunctor f where
  map {_ _} e := Functor.map e
  map_refl' α := by
    ext
    apply LawfulFunctor.id_map
  map_trans' {α β γ} k h := by
    ext x
    apply LawfulFunctor.comp_map k h x

Lawful Functors as Equivalence-Preserving Functors

Informal description

For any type constructor $f : \text{Type} \to \text{Type}$ that is a lawful functor, $f$ can be equipped with the structure of an `EquivFunctor`, meaning it coherently maps equivalences between types to equivalences between the corresponding constructed types.

EquivFunctor.mapEquiv.injective theorem

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

Full source

theorem mapEquiv.injective (f : Type u₀ → Type u₁)
    [Applicative f] [LawfulApplicative f] {α β : Type u₀}
    (h : ∀ γ, Function.Injective (pure : γ → f γ)) :
      Function.Injective (@EquivFunctor.mapEquiv f _ α β) :=
  fun e₁ e₂ H =>
    Equiv.ext fun x => h β (by simpa [EquivFunctor.map] using Equiv.congr_fun H (pure x))

Injectivity of Equivalence Mapping for Lawful Applicative Functors with Injective Pure

Informal description

Let $f : \text{Type} \to \text{Type}$ be an applicative functor that is lawful, and suppose that for every type $\gamma$, the function $\text{pure} : \gamma \to f \gamma$ is injective. Then the function $\text{mapEquiv} : (\alpha \simeq \beta) \to (f \alpha \simeq f \beta)$ is injective.