Mathlib.CategoryTheory.Groupoid

CategoryTheory.Groupoid structure

(obj : Type u) : Type max u (v + 1) extends Category.{v} obj

Full source

/-- A `Groupoid` is a category such that all morphisms are isomorphisms. -/
class Groupoid (obj : Type u) : Type max u (v + 1) extends Category.{v} obj where
  /-- The inverse morphism -/
  inv : ∀ {X Y : obj}, (X ⟶ Y) → (Y ⟶ X)
  /-- `inv f` composed `f` is the identity -/
  inv_comp : ∀ {X Y : obj} (f : X ⟶ Y), comp (inv f) f = id Y := by aesop_cat
  /-- `f` composed with `inv f` is the identity -/
  comp_inv : ∀ {X Y : obj} (f : X ⟶ Y), comp f (inv f) = id X := by aesop_cat

Groupoid

Informal description

A groupoid is a category in which every morphism is an isomorphism. That is, for any morphism $f: X \to Y$, there exists an inverse morphism $f^{-1}: Y \to X$ such that $f \circ f^{-1} = \text{id}_Y$ and $f^{-1} \circ f = \text{id}_X$.

CategoryTheory.LargeGroupoid abbrev

(C : Type (u + 1)) : Type (u + 1)

Full source

/-- A `LargeGroupoid` is a groupoid
where the objects live in `Type (u+1)` while the morphisms live in `Type u`.
-/
abbrev LargeGroupoid (C : Type (u + 1)) : Type (u + 1) :=
  Groupoid.{u} C

Large Groupoid (Objects in Higher Universe)

Informal description

A *large groupoid* is a groupoid where the objects are of type `Type (u+1)` (i.e., they live in a higher universe level) while the morphisms are of type `Type u`.

CategoryTheory.SmallGroupoid abbrev

(C : Type u) : Type (u + 1)

Full source

/-- A `SmallGroupoid` is a groupoid
where the objects and morphisms live in the same universe.
-/
abbrev SmallGroupoid (C : Type u) : Type (u + 1) :=
  Groupoid.{u} C

Small Groupoid (Same Universe for Objects and Morphisms)

Informal description

A small groupoid is a groupoid where both the objects and morphisms are in the same universe level $u$. That is, it is a category where every morphism is an isomorphism, and the type of objects $C$ and the type of morphisms both live in the same universe level $u$.

CategoryTheory.IsIso.of_groupoid instance

(f : X ⟶ Y) : IsIso f

Full source

instance (priority := 100) IsIso.of_groupoid (f : X ⟶ Y) : IsIso f :=
  ⟨⟨Groupoid.inv f, Groupoid.comp_inv f, Groupoid.inv_comp f⟩⟩

Every Morphism in a Groupoid is an Isomorphism

Informal description

For any morphism $f : X \to Y$ in a groupoid, $f$ is an isomorphism.

CategoryTheory.Groupoid.inv_eq_inv theorem

(f : X ⟶ Y) : Groupoid.inv f = CategoryTheory.inv f

Full source

@[simp]
theorem Groupoid.inv_eq_inv (f : X ⟶ Y) : Groupoid.inv f = CategoryTheory.inv f :=
  IsIso.eq_inv_of_hom_inv_id <| Groupoid.comp_inv f

Equality of Groupoid and Categorical Inverses

Informal description

For any morphism $f : X \to Y$ in a groupoid, the inverse morphism defined by the groupoid structure equals the categorical inverse of $f$, i.e., $\text{Groupoid.inv}(f) = \text{inv}(f)$.

CategoryTheory.Groupoid.invEquiv definition

: (X ⟶ Y) ≃ (Y ⟶ X)

Full source

/-- `Groupoid.inv` is involutive. -/
@[simps]
def Groupoid.invEquiv : (X ⟶ Y) ≃ (Y ⟶ X) :=
  ⟨Groupoid.inv, Groupoid.inv, fun f => by simp, fun f => by simp⟩

Equivalence between morphisms and their inverses in a groupoid

Informal description

The equivalence between morphisms $X \to Y$ and morphisms $Y \to X$ in a groupoid, where each morphism is mapped to its inverse. Specifically, this is a bijection that sends any morphism $f: X \to Y$ to its inverse $f^{-1}: Y \to X$, and vice versa, satisfying $f^{-1} \circ f = \text{id}_X$ and $f \circ f^{-1} = \text{id}_Y$.

CategoryTheory.groupoidHasInvolutiveReverse instance

: Quiver.HasInvolutiveReverse C

Full source

instance (priority := 100) groupoidHasInvolutiveReverse : Quiver.HasInvolutiveReverse C where
  reverse' f := Groupoid.inv f
  inv' f := by
    dsimp [Quiver.reverse]
    simp

Involutive Reverse Operation in Groupoids

Informal description

For any groupoid $C$, the category $C$ has an involutive reverse operation on morphisms, where the reverse of a morphism is its inverse.

CategoryTheory.Groupoid.reverse_eq_inv theorem

(f : X ⟶ Y) : Quiver.reverse f = Groupoid.inv f

Full source

@[simp]
theorem Groupoid.reverse_eq_inv (f : X ⟶ Y) : Quiver.reverse f = Groupoid.inv f :=
  rfl

Reverse Equals Inverse in Groupoids

Informal description

For any morphism $f: X \to Y$ in a groupoid, the reverse of $f$ (denoted $\text{reverse}(f)$) is equal to the inverse of $f$ (denoted $f^{-1}$), i.e., $\text{reverse}(f) = f^{-1}$.

CategoryTheory.functorMapReverse instance

{D : Type*} [Groupoid D] (F : C ⥤ D) : F.toPrefunctor.MapReverse

Full source

instance functorMapReverse {D : Type*} [Groupoid D] (F : C ⥤ D) : F.toPrefunctor.MapReverse where
  map_reverse' f := by
    simp only [Quiver.reverse, Quiver.HasReverse.reverse', Groupoid.inv_eq_inv,
      Functor.map_inv]

Functor Preserves Reverse Operation in Groupoids

Informal description

For any functor $F \colon \mathcal{C} \to \mathcal{D}$ where $\mathcal{D}$ is a groupoid, the functor $F$ preserves the reverse operation on morphisms. That is, the reverse of $F(f)$ is equal to $F$ applied to the reverse of $f$.

CategoryTheory.Groupoid.isoEquivHom definition

: (X ≅ Y) ≃ (X ⟶ Y)

Full source

/-- In a groupoid, isomorphisms are equivalent to morphisms. -/
@[simps!]
def Groupoid.isoEquivHom : (X ≅ Y) ≃ (X ⟶ Y) where
  toFun := Iso.hom
  invFun f := ⟨f, Groupoid.inv f, (by simp), (by simp)⟩
  left_inv _ := Iso.ext rfl
  right_inv _ := rfl

Equivalence between isomorphisms and morphisms in a groupoid

Informal description

The equivalence between isomorphisms $X \cong Y$ and morphisms $X \longrightarrow Y$ in a groupoid, where the forward direction extracts the underlying morphism from an isomorphism, and the backward direction constructs an isomorphism from any morphism by using its inverse (which exists because the category is a groupoid).

CategoryTheory.Groupoid.invFunctor definition

: C ⥤ Cᵒᵖ

Full source

/-- The functor from a groupoid `C` to its opposite sending every morphism to its inverse. -/
@[simps]
noncomputable def Groupoid.invFunctor : C ⥤ Cᵒᵖ where
  obj := Opposite.op
  map {_ _} f := (inv f).op

Inverse functor to the opposite category

Informal description

The functor from a groupoid $C$ to its opposite category $C^{\mathrm{op}}$ which sends each object $X$ to $\mathrm{op}(X)$ and each morphism $f: X \to Y$ to the opposite of its inverse $f^{-1}: Y \to X$.

CategoryTheory.IsGroupoid structure

(C : Type u) [Category.{v} C]

Full source

/-- A Prop-valued typeclass asserting that a given category is a groupoid. -/
class IsGroupoid (C : Type u) [Category.{v} C] : Prop where
  all_isIso {X Y : C} (f : X ⟶ Y) : IsIso f := by infer_instance

Groupoid property of a category

Informal description

A property-valued typeclass stating that a given category $ C $ is a groupoid, meaning every morphism in $ C $ is an isomorphism.

CategoryTheory.instIsGroupoid instance

{C : Type u} [Groupoid.{v} C] : IsGroupoid C

Full source

noncomputable instance {C : Type u} [Groupoid.{v} C] : IsGroupoid C where

Groupoids Have All Morphisms Invertible

Informal description

For any groupoid $C$, every morphism in $C$ is an isomorphism.

CategoryTheory.Groupoid.ofIsGroupoid definition

[IsGroupoid C] : Groupoid.{v} C

Full source

/-- Promote (noncomputably) an `IsGroupoid` to a `Groupoid` structure. -/
noncomputable def Groupoid.ofIsGroupoid [IsGroupoid C] :
    Groupoid.{v} C where
  inv := fun f => CategoryTheory.inv f

Groupoid structure from groupoid property

Informal description

Given a category $ C $ with the property that every morphism is an isomorphism (i.e., $ C $ is a groupoid), the structure `Groupoid.ofIsGroupoid` constructs a groupoid on $ C $. The inverse of any morphism $ f $ is defined to be the inverse morphism $ f^{-1} $ guaranteed by the `IsGroupoid` property.

CategoryTheory.Groupoid.ofIsIso definition

(all_is_iso : ∀ {X Y : C} (f : X ⟶ Y), IsIso f) : Groupoid.{v} C

Full source

/-- A category where every morphism `IsIso` is a groupoid. -/
noncomputable def Groupoid.ofIsIso (all_is_iso : ∀ {X Y : C} (f : X ⟶ Y), IsIso f) :
    Groupoid.{v} C where
  inv := fun f => CategoryTheory.inv f
  inv_comp := fun f => Classical.choose_spec (all_is_iso f).out|>.right

Groupoid from isomorphisms

Informal description

Given a category $ C $ where every morphism $ f : X \to Y $ is an isomorphism, the structure `Groupoid.ofIsIso` constructs a groupoid on $ C $. The inverse of any morphism $ f $ is defined to be the inverse morphism $ f^{-1} $ guaranteed by the `IsIso` property.

CategoryTheory.Groupoid.ofHomUnique definition

(all_unique : ∀ {X Y : C}, Unique (X ⟶ Y)) : Groupoid.{v} C

Full source

/-- A category with a unique morphism between any two objects is a groupoid -/
def Groupoid.ofHomUnique (all_unique : ∀ {X Y : C}, Unique (X ⟶ Y)) : Groupoid.{v} C where
  inv _ := all_unique.default

Groupoid from unique morphisms

Informal description

Given a category $C$ where for any two objects $X$ and $Y$ there exists a unique morphism $X \to Y$, the structure `Groupoid.ofHomUnique` constructs a groupoid on $C$ where every morphism is an isomorphism. The inverse of any morphism $f$ is defined to be the unique morphism in the opposite direction.

CategoryTheory.isGroupoid_of_reflects_iso theorem

{C D : Type*} [Category C] [Category D] (F : C ⥤ D) [F.ReflectsIsomorphisms] [IsGroupoid D] : IsGroupoid C

Full source

lemma isGroupoid_of_reflects_iso {C D : Type*} [Category C] [Category D]
    (F : C ⥤ D) [F.ReflectsIsomorphisms] [IsGroupoid D] :
    IsGroupoid C where
  all_isIso _ := isIso_of_reflects_iso _ F

Reflection of Groupoid Property via Isomorphism-Reflecting Functor

Informal description

Let $C$ and $D$ be categories, and let $F : C \to D$ be a functor that reflects isomorphisms. If $D$ is a groupoid (i.e., every morphism in $D$ is an isomorphism), then $C$ is also a groupoid.

CategoryTheory.Groupoid.ofFullyFaithfulToGroupoid definition

{C : Type*} [𝒞 : Category C] {D : Type u} [Groupoid.{v} D] (F : C ⥤ D) (h : F.FullyFaithful) : Groupoid C

Full source

/-- A category equipped with a fully faithful functor to a groupoid is fully faithful -/
def Groupoid.ofFullyFaithfulToGroupoid {C : Type*} [𝒞 : Category C] {D : Type u} [Groupoid.{v} D]
    (F : C ⥤ D) (h : F.FullyFaithful) : Groupoid C :=
  { 𝒞 with
    inv f := h.preimage <| Groupoid.inv (F.map f)
    inv_comp f := by
      apply h.map_injective
      simp
    comp_inv f := by
      apply h.map_injective
      simp }

Groupoid structure induced by a fully faithful functor to a groupoid

Informal description

Given a category $C$ and a fully faithful functor $F : C \to D$ to a groupoid $D$, the structure `Groupoid.ofFullyFaithfulToGroupoid` constructs a groupoid structure on $C$. The inverse of a morphism $f$ in $C$ is defined as the preimage under $F$ of the inverse of $F(f)$ in $D$. The groupoid axioms follow from the fully faithfulness of $F$ and the groupoid structure of $D$.

CategoryTheory.InducedCategory.groupoid instance

{C : Type u} (D : Type u₂) [Groupoid.{v} D] (F : C → D) : Groupoid.{v} (InducedCategory D F)

Full source

instance InducedCategory.groupoid {C : Type u} (D : Type u₂) [Groupoid.{v} D] (F : C → D) :
    Groupoid.{v} (InducedCategory D F) :=
  Groupoid.ofFullyFaithfulToGroupoid (inducedFunctor F) (fullyFaithfulInducedFunctor F)

Groupoid Structure on Induced Category

Informal description

Given a groupoid $\mathcal{D}$ and a function $F : C \to \mathcal{D}$ from a type $C$ to the objects of $\mathcal{D}$, the induced category structure on $C$ forms a groupoid where the morphisms between objects $X$ and $Y$ in $C$ are precisely the morphisms between $F(X)$ and $F(Y)$ in $\mathcal{D}$, and every such morphism has an inverse.

CategoryTheory.InducedCategory.isGroupoid instance

{C : Type u} (D : Type u₂) [Category.{v} D] [IsGroupoid D] (F : C → D) : IsGroupoid (InducedCategory D F)

Full source

instance InducedCategory.isGroupoid {C : Type u} (D : Type u₂)
    [Category.{v} D] [IsGroupoid D] (F : C → D) :
    IsGroupoid (InducedCategory D F) :=
  isGroupoid_of_reflects_iso (inducedFunctor F)

Induced Category from a Groupoid is a Groupoid

Informal description

Given a groupoid $\mathcal{D}$ and a function $F : C \to \mathcal{D}$ from a type $C$ to the objects of $\mathcal{D}$, the induced category structure on $C$ is also a groupoid. That is, every morphism in the induced category is an isomorphism.

CategoryTheory.groupoidPi instance

{I : Type u} {J : I → Type u₂} [∀ i, Groupoid.{v} (J i)] : Groupoid.{max u v} (∀ i : I, J i)

Full source

instance groupoidPi {I : Type u} {J : I → Type u₂} [∀ i, Groupoid.{v} (J i)] :
    Groupoid.{max u v} (∀ i : I, J i) where
  inv f := fun i : I => Groupoid.inv (f i)
  comp_inv := fun f => by funext i; apply Groupoid.comp_inv
  inv_comp := fun f => by funext i; apply Groupoid.inv_comp

Product of Groupoids is a Groupoid

Informal description

For any family of groupoids $\{J_i\}_{i \in I}$ indexed by a type $I$, the product category $\prod_{i \in I} J_i$ is also a groupoid.

CategoryTheory.groupoidProd instance

{α : Type u} {β : Type v} [Groupoid.{u₂} α] [Groupoid.{v₂} β] : Groupoid.{max u₂ v₂} (α × β)

Full source

instance groupoidProd {α : Type u} {β : Type v} [Groupoid.{u₂} α] [Groupoid.{v₂} β] :
    Groupoid.{max u₂ v₂} (α × β) where
  inv f := (Groupoid.inv f.1, Groupoid.inv f.2)

Product of Groupoids is a Groupoid

Informal description

For any groupoids $\alpha$ and $\beta$, the product category $\alpha \times \beta$ is also a groupoid.

CategoryTheory.isGroupoidPi instance

{I : Type u} {J : I → Type u₂} [∀ i, Category.{v} (J i)] [∀ i, IsGroupoid (J i)] : IsGroupoid (∀ i : I, J i)

Full source

instance isGroupoidPi {I : Type u} {J : I → Type u₂}
    [∀ i, Category.{v} (J i)] [∀ i, IsGroupoid (J i)] :
    IsGroupoid (∀ i : I, J i) where
  all_isIso f := (isIso_pi_iff f).mpr (fun _ ↦ inferInstance)

Product of Groupoids is a Groupoid

Informal description

For any family of categories $\{J_i\}_{i \in I}$ where each $J_i$ is a groupoid, the product category $\prod_{i \in I} J_i$ is also a groupoid.

CategoryTheory.isGroupoidProd instance

 {α : Type u} {β : Type u₂} [Category.{v} α] [Category.{v₂} β] [IsGroupoid α] [IsGroupoid β] : IsGroupoid (α × β)

Full source

instance isGroupoidProd {α : Type u} {β : Type u₂} [Category.{v} α] [Category.{v₂} β]
    [IsGroupoid α] [IsGroupoid β] :
    IsGroupoid (α × β) where
  all_isIso f := (isIso_prod_iff (f := f)).mpr ⟨inferInstance, inferInstance⟩

Product of Groupoids is a Groupoid

Informal description

For any categories $\alpha$ and $\beta$ that are groupoids, the product category $\alpha \times \beta$ is also a groupoid.

See also