isoMk — Mathlib

Lean4
/-- Construct an isomorphism in `SingleFunctors C D A` by giving
level-wise isomorphisms and checking compatibility only in the forward direction. -/
@[simps]
def isoMk (iso : ∀ a, (F.functor a ≅ G.functor a))
    (comm :
      ∀ (n a a' : A) (ha' : n + a = a'),
        (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
          whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom) :
    F ≅ G
    where
  hom :=
    { hom := fun a => (iso a).hom
      comm := comm }
  inv :=
    { hom := fun a => (iso a).inv
      comm := fun n a a' ha' => by
        rw [← cancel_mono (iso a).hom, assoc, assoc, Iso.inv_hom_id, comp_id, comm, ← whiskerRight_comp_assoc,
          Iso.inv_hom_id, whiskerRight_id', id_comp] }
Похожие утверждения