Theorems · Theorem · group theory

CategoryTheory.Subgroupoid.Map.arrows_iff

∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) (S : CategoryTheory.Subgroupoid C) {c d : D}
  (f : c ⟶ d),
  CategoryTheory.Subgroupoid.Map.Arrows φ hφ S c d f ↔
    ∃ a b g,
      ∃ (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
        f =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp (φ.map g) (CategoryTheory.eqToHom hb))

Defined in

Mathlib.CategoryTheory.Groupoid.Subgroupoid

Cited by

3 results in Mathlib

Foundations

Depth 7 from the axioms · uses propext

Assumes

CategoryTheory.GroupoidCategoryTheory.Groupoid