groupoidOfElements

Mathlib.CategoryTheory.Elements

URI: https://scilib.ai/kg/mathlib#CategoryTheory.groupoidOfElements

Lean4

instance groupoidOfElements {G : Type u} [Groupoid.{v} G] (F : G ⥤ Type w) : Groupoid F.Elements
    where
  inv {p q}
    f :=
    ⟨Groupoid.inv f.val,
      calc
        F.map (Groupoid.inv f.val) q.2 = F.map (Groupoid.inv f.val) (F.map f.val p.2) := by rw [f.2]
        _ = (F.map f.val ≫ F.map (Groupoid.inv f.val)) p.2 := rfl
        _ = p.2 := by
          rw [← F.map_comp]
          simp⟩
  inv_comp
    _ := by
    ext
    simp
  comp_inv
    _ := by
    ext
    simp

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

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

Разделы

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

Аффилиация

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