inv

Mathlib.CategoryTheory.Quotient

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Quotient.inv

Lean4

/-- Inverse of a map in the quotient category of a groupoid. -/
protected def inv {X Y : Quotient r} (f : X ⟶ Y) : Y ⟶ X :=
  Quot.liftOn f (fun f' => Quot.mk _ (Groupoid.inv f'))
    (fun _ _ con => by
      rcases con with ⟨_, f, g, _, hfg⟩
      have := Quot.sound <| CompClosure.intro (Groupoid.inv g) f g (Groupoid.inv f) hfg
      simp only [Groupoid.inv_eq_inv, IsIso.hom_inv_id, Category.comp_id, IsIso.inv_hom_id_assoc] at this
      simp only [Groupoid.inv_eq_inv, IsIso.inv_comp, Category.assoc]
      repeat rw [← comp_mk]
      rw [this])

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru