commaMapEquivalenceInverse — Mathlib

Lean4
/-- The inverse functor establishing the equivalence `StructuredArrow.commaMapEquivalence`. -/
@[simps]
def commaMapEquivalenceInverse [IsIso β] (X : Comma L' R') :
    Comma (map₂ (𝟙 _) α) (map₂ X.hom (inv β)) ⥤ StructuredArrow X (Comma.map α β)
    where
  obj
    Y :=
    mk (Y := ⟨Y.left.right, Y.right.right, Y.hom.right⟩)
      ⟨by exact Y.left.hom, by exact Y.right.hom, by
        simpa using congrFun (congrArg CategoryStruct.comp (StructuredArrow.w Y.hom)) (β.app Y.right.right)⟩
  map {Y Z}
    f :=
    homMk ⟨by exact f.left.right, by exact f.right.right, by exact congrArg CommaMorphism.right f.w⟩
      (by
        ext <;>
          simp only [Comma.map_obj_right, Comma.map_obj_left, Functor.const_obj_obj, mk_left, mk_right, mk_hom_eq_self,
            Comma.comp_left, Comma.map_map_left, w]
        · simp only [Comma.map_obj_right, Comma.comp_right, Comma.map_map_right, w])
  map_id X := by ext <;> rfl
  map_comp f g := by ext <;> rfl
Похожие утверждения