Groupoids #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define groupoid as a typeclass extending category, asserting that all morphisms have inverses.

The instance is_iso.of_groupoid (f : X ⟶ Y) : is_iso f means that you can then write inv f to access the inverse of any morphism f.

groupoid.iso_equiv_hom : (X ≅ Y) ≃ (X ⟶ Y) provides the equivalence between isomorphisms and morphisms in a groupoid.

We provide a (non-instance) constructor groupoid.of_is_iso from an existing category with is_iso f for every f.

See also #

See also category_theory.core for the groupoid of isomorphisms in a category.

source

@[class]

structure category_theory.groupoid (obj : Type u) :

Type (max u (v+1))

to_category : category_theory.category obj
inv : Π {X Y : obj}, (X ⟶ Y) → (Y ⟶ X)
inv_comp' : (∀ {X Y : obj} (f : X ⟶ Y), category_theory.groupoid.inv f ≫ f = 𝟙 Y) . "obviously"
comp_inv' : (∀ {X Y : obj} (f : X ⟶ Y), f ≫ category_theory.groupoid.inv f = 𝟙 X) . "obviously"

A groupoid is a category such that all morphisms are isomorphisms.

Instances of this typeclass

Instances of other typeclasses for category_theory.groupoid

category_theory.groupoid.has_sizeof_inst

source

theorem category_theory.groupoid.inv_comp {obj : Type u} [self : category_theory.groupoid obj] {X Y : obj} (f : X ⟶ Y) :

category_theory.groupoid.inv f ≫ f = 𝟙 Y

source

theorem category_theory.groupoid.comp_inv {obj : Type u} [self : category_theory.groupoid obj] {X Y : obj} (f : X ⟶ Y) :

f ≫ category_theory.groupoid.inv f = 𝟙 X

source

@[reducible]

def category_theory.large_groupoid (C : Type (u+1)) :

Type (u+1)

A large_groupoid is a groupoid where the objects live in Type (u+1) while the morphisms live in Type u.

source

@[reducible]

def category_theory.small_groupoid (C : Type u) :

Type (u+1)

A small_groupoid is a groupoid where the objects and morphisms live in the same universe.

source

@[protected, instance]

def category_theory.is_iso.of_groupoid {C : Type u} [category_theory.groupoid C] {X Y : C} (f : X ⟶ Y) :

category_theory.is_iso f

source

@[simp]

theorem category_theory.groupoid.inv_eq_inv {C : Type u} [category_theory.groupoid C] {X Y : C} (f : X ⟶ Y) :

category_theory.groupoid.inv f = category_theory.inv f

source

@[simp]

theorem category_theory.groupoid.inv_equiv_apply {C : Type u} [category_theory.groupoid C] {X Y : C} (ᾰ : X ⟶ Y) :

⇑category_theory.groupoid.inv_equiv ᾰ = category_theory.groupoid.inv ᾰ

source

def category_theory.groupoid.inv_equiv {C : Type u} [category_theory.groupoid C] {X Y : C} :

(X ⟶ Y) ≃ (Y ⟶ X)

groupoid.inv is involutive.

Equations

category_theory.groupoid.inv_equiv = {to_fun := category_theory.groupoid.inv Y, inv_fun := category_theory.groupoid.inv X, left_inv := _, right_inv := _}

source

@[simp]

theorem category_theory.groupoid.inv_equiv_symm_apply {C : Type u} [category_theory.groupoid C] {X Y : C} (ᾰ : Y ⟶ X) :

⇑(category_theory.groupoid.inv_equiv.symm) ᾰ = category_theory.groupoid.inv ᾰ

source

@[protected, instance]

def category_theory.groupoid_has_involutive_reverse {C : Type u} [category_theory.groupoid C] :

quiver.has_involutive_reverse C

Equations

category_theory.groupoid_has_involutive_reverse = {to_has_reverse := {reverse' := λ (X Y : C) (f : X ⟶ Y), category_theory.groupoid.inv f}, inv' := _}

source

@[simp]

theorem category_theory.groupoid.reverse_eq_inv {C : Type u} [category_theory.groupoid C] {X Y : C} (f : X ⟶ Y) :

quiver.reverse f = category_theory.groupoid.inv f

source

@[protected, instance]

def category_theory.functor_map_reverse {C : Type u} [category_theory.groupoid C] {D : Type u_1} [category_theory.groupoid D] (F : C ⥤ D) :

F.to_prefunctor.map_reverse

Equations

category_theory.functor_map_reverse F = {map_reverse' := _}

source

def category_theory.groupoid.iso_equiv_hom {C : Type u} [category_theory.groupoid C] (X Y : C) :

(X ≅ Y) ≃ (X ⟶ Y)

In a groupoid, isomorphisms are equivalent to morphisms.

Equations

category_theory.groupoid.iso_equiv_hom X Y = {to_fun := category_theory.iso.hom Y, inv_fun := λ (f : X ⟶ Y), {hom := f, inv := category_theory.groupoid.inv f, hom_inv_id' := _, inv_hom_id' := _}, left_inv := _, right_inv := _}

source

@[simp]

theorem category_theory.groupoid.inv_functor_obj (C : Type u) [category_theory.groupoid C] (ᾰ : C) :

(category_theory.groupoid.inv_functor C).obj ᾰ = opposite.op ᾰ

source

@[simp]

theorem category_theory.groupoid.inv_functor_map (C : Type u) [category_theory.groupoid C] {X Y : C} (f : X ⟶ Y) :

(category_theory.groupoid.inv_functor C).map f = (category_theory.inv f).op

source

noncomputable def category_theory.groupoid.inv_functor (C : Type u) [category_theory.groupoid C] :

C ⥤ Cᵒᵖ

The functor from a groupoid C to its opposite sending every morphism to its inverse.

Equations

category_theory.groupoid.inv_functor C = {obj := opposite.op C, map := λ {X Y : C} (f : X ⟶ Y), (category_theory.inv f).op, map_id' := _, map_comp' := _}

source

noncomputable def category_theory.groupoid.of_is_iso {C : Type u} [category_theory.category C] (all_is_iso : ∀ {X Y : C} (f : X ⟶ Y), category_theory.is_iso f) :

category_theory.groupoid C

A category where every morphism is_iso is a groupoid.

Equations

category_theory.groupoid.of_is_iso all_is_iso = {to_category := {to_category_struct := category_theory.category.to_category_struct _inst_1, id_comp' := _, comp_id' := _, assoc' := _}, inv := λ (X Y : C) (f : X ⟶ Y), category_theory.inv f, inv_comp' := _, comp_inv' := _}

source

def category_theory.groupoid.of_hom_unique {C : Type u} [category_theory.category C] (all_unique : Π {X Y : C}, unique (X ⟶ Y)) :

category_theory.groupoid C

A category with a unique morphism between any two objects is a groupoid

Equations

category_theory.groupoid.of_hom_unique all_unique = {to_category := {to_category_struct := category_theory.category.to_category_struct _inst_1, id_comp' := _, comp_id' := _, assoc' := _}, inv := λ (X Y : C) (f : X ⟶ Y), inhabited.default, inv_comp' := _, comp_inv' := _}

source

@[protected, instance]

def category_theory.induced_category.groupoid {C : Type u} (D : Type u₂) [category_theory.groupoid D] (F : C → D) :

category_theory.groupoid (category_theory.induced_category D F)

Equations

category_theory.induced_category.groupoid D F = {to_category := {to_category_struct := category_theory.category.to_category_struct (category_theory.induced_category.category F), id_comp' := _, comp_id' := _, assoc' := _}, inv := λ (X Y : category_theory.induced_category D F) (f : X ⟶ Y), category_theory.groupoid.inv f, inv_comp' := _, comp_inv' := _}

source

@[protected, instance]

def category_theory.groupoid_pi {I : Type u} {J : I → Type u₂} [Π (i : I), category_theory.groupoid (J i)] :

category_theory.groupoid (Π (i : I), J i)

Equations

category_theory.groupoid_pi = {to_category := {to_category_struct := category_theory.category.to_category_struct (category_theory.pi (λ (i : I), J i)), id_comp' := _, comp_id' := _, assoc' := _}, inv := λ (x y : Π (i : I), J i) (f : Π (i : I), x i ⟶ y i) (i : I), category_theory.groupoid.inv (f i), inv_comp' := _, comp_inv' := _}

source

@[protected, instance]

def category_theory.groupoid_prod {α : Type u} {β : Type v} [category_theory.groupoid α] [category_theory.groupoid β] :

category_theory.groupoid (α × β)

Equations

category_theory.groupoid_prod = {to_category := {to_category_struct := category_theory.category.to_category_struct (category_theory.prod α β), id_comp' := _, comp_id' := _, assoc' := _}, inv := λ (x y : α × β) (f : x ⟶ y), (category_theory.groupoid.inv f.fst, category_theory.groupoid.inv f.snd), inv_comp' := _, comp_inv' := _}