mathlib3 documentation

logic.equiv.functor

Functor and bifunctors can be applied to equivs. #

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

We define

def functor.map_equiv (f : Type u → Type v) [functor f] [is_lawful_functor f] :
  α ≃ β → f α ≃ f β

and

def bifunctor.map_equiv (F : Type u → Type v → Type w) [bifunctor F] [is_lawful_bifunctor F] :
  α ≃ β → α' ≃ β' → F α α' ≃ F β β'
source
def functor.map_equiv {α β : Type u} (f : Type u → Type v) [functor f] [is_lawful_functor f] (h : α ≃ β) :
f α ≃ f β

Apply a functor to an equiv.

Equations
source
@[simp]
theorem functor.map_equiv_apply {α β : Type u} (f : Type u → Type v) [functor f] [is_lawful_functor f] (h : α ≃ β) (x : f α) :
⇑(functor.map_equiv f h) x = ⇑h <$> x
source
@[simp]
theorem functor.map_equiv_symm_apply {α β : Type u} (f : Type u → Type v) [functor f] [is_lawful_functor f] (h : α ≃ β) (y : f β) :
⇑((functor.map_equiv f h).symm) y = ⇑(h.symm) <$> y
source
@[simp]
theorem functor.map_equiv_refl {α : Type u} (f : Type u → Type v) [functor f] [is_lawful_functor f] :
functor.map_equiv f (equiv.refl α) = equiv.refl (f α)
source
def bifunctor.map_equiv {α β : Type u} {α' β' : Type v} (F : Type u → Type v → Type w) [bifunctor F] [is_lawful_bifunctor F] (h : α ≃ β) (h' : α' ≃ β') :
F α α' ≃ F β β'

Apply a bifunctor to a pair of equivs.

Equations
source
@[simp]
theorem bifunctor.map_equiv_apply {α β : Type u} {α' β' : Type v} (F : Type u → Type v → Type w) [bifunctor F] [is_lawful_bifunctor F] (h : α ≃ β) (h' : α' ≃ β') (x : F α α') :
⇑(bifunctor.map_equiv F h h') x = bifunctor.bimap ⇑h ⇑h' x
source
@[simp]
theorem bifunctor.map_equiv_symm_apply {α β : Type u} {α' β' : Type v} (F : Type u → Type v → Type w) [bifunctor F] [is_lawful_bifunctor F] (h : α ≃ β) (h' : α' ≃ β') (y : F β β') :
⇑((bifunctor.map_equiv F h h').symm) y = bifunctor.bimap ⇑(h.symm) ⇑(h'.symm) y
source
@[simp]
theorem bifunctor.map_equiv_refl_refl {α : Type u} {α' : Type v} (F : Type u → Type v → Type w) [bifunctor F] [is_lawful_bifunctor F] :
bifunctor.map_equiv F (equiv.refl α) (equiv.refl α') = equiv.refl (F α α')