inv_fun_map — Mathlib

English

Second formulation of inverse-map for morphisms under equivalence.

Русский

Вторая формулировка отображения обратного функторa для морфизмов в рамках эквивалентности.

LaTeX

$$$e.inverse.map (e.functor.map f) = e.unitInv.app X \\;\\circ \\; f \\;\\circ \\; e.unit.app Y$$$

Lean4

@[reassoc, simp]
theorem inv_fun_map (e : C ≌ D) (X Y : C) (f : X ⟶ Y) :
    e.inverse.map (e.functor.map f) = e.unitInv.app X ≫ f ≫ e.unit.app Y :=
  (NatIso.naturality_1 e.unitIso f).symm

Похожие утверждения