sheafCongr — Mathlib

Lean4
/-- The equivalence of sheaf categories. -/
def sheafCongr : Sheaf J A ≌ Sheaf K A
    where
  functor := sheafCongr.functor J K e A
  inverse := sheafCongr.inverse J K e A
  unitIso := sheafCongr.unitIso J K e A
  counitIso := sheafCongr.counitIso J K e A
  functor_unitIso_comp
    X := by
    ext
    simp only [id_obj, sheafCongr.functor_obj_val_obj, comp_obj, Sheaf.comp_val, NatTrans.comp_app,
      sheafCongr.inverse_obj_val_obj, Opposite.unop_op, sheafCongr.functor_map_val_app,
      sheafCongr.unitIso_hom_app_val_app, sheafCongr.counitIso_hom_app_val_app, sheafCongr.functor_obj_val_map,
      Quiver.Hom.unop_op, Sheaf.id_val, NatTrans.id_app]
    simp [← Functor.map_comp, ← op_comp]
Похожие утверждения