Documentation

Mathlib.CategoryTheory.Groupoid.Subgroupoid

Subgroupoid #

This file defines subgroupoids as structures containing the subsets of arrows and their stability under composition and inversion. Also defined are:

Main definitions #

Given a type C with associated groupoid C instance.

Implementation details #

The structure of this file is copied from/inspired by Mathlib/GroupTheory/Subgroup/Basic.lean and Mathlib/Combinatorics/SimpleGraph/Subgraph.lean.

TODO #

Tags #

category theory, groupoid, subgroupoid

theorem CategoryTheory.Subgroupoid.ext {C : Type u} :
βˆ€ {inst : CategoryTheory.Groupoid C} (x y : CategoryTheory.Subgroupoid C), x.arrows = y.arrows β†’ x = y
theorem CategoryTheory.Subgroupoid.ext_iff {C : Type u} :
βˆ€ {inst : CategoryTheory.Groupoid C} (x y : CategoryTheory.Subgroupoid C), x = y ↔ x.arrows = y.arrows
structure CategoryTheory.Subgroupoid (C : Type u) [CategoryTheory.Groupoid C] :
Type (max u u_1)

A sugroupoid of C consists of a choice of arrows for each pair of vertices, closed under composition and inverses.

Instances For
    theorem CategoryTheory.Subgroupoid.mul_mem_cancel_left {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c : C} {d : C} {e : C} {f : c ⟢ d} {g : d ⟢ e} (hf : f ∈ S.arrows c d) :
    CategoryTheory.CategoryStruct.comp f g ∈ S.arrows c e ↔ g ∈ S.arrows d e
    theorem CategoryTheory.Subgroupoid.mul_mem_cancel_right {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c : C} {d : C} {e : C} {f : c ⟢ d} {g : d ⟢ e} (hg : g ∈ S.arrows d e) :
    CategoryTheory.CategoryStruct.comp f g ∈ S.arrows c e ↔ f ∈ S.arrows c d

    The vertices of C on which S has non-trivial isotropy

    Equations
    Instances For

      A subgroupoid seen as a quiver on vertex set C

      Equations
      Instances For

        The coercion of a subgroupoid as a groupoid

        Equations
        • One or more equations did not get rendered due to their size.

        The embedding of the coerced subgroupoid to its parent

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The subgroup of the vertex group at c given by the subgroupoid

          Equations
          Instances For
            def CategoryTheory.Subgroupoid.toSet {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) :
            Set ((c : C) Γ— (d : C) Γ— (c ⟢ d))

            The set of all arrows of a subgroupoid, as a set in Σ c d : C, c ⟢ d.

            Equations
            • ↑S = {F : (c : C) Γ— (d : C) Γ— (c ⟢ d) | F.snd.snd ∈ S.arrows F.fst F.snd.fst}
            Instances For
              Equations
              • CategoryTheory.Subgroupoid.instSetLikeSubgroupoidSigmaSigmaHomToQuiverToCategoryStructToCategory = { coe := CategoryTheory.Subgroupoid.toSet, coe_injective' := β‹― }
              theorem CategoryTheory.Subgroupoid.mem_iff {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) (F : (c : C) Γ— (d : C) Γ— (c ⟢ d)) :
              F ∈ S ↔ F.snd.snd ∈ S.arrows F.fst F.snd.fst
              theorem CategoryTheory.Subgroupoid.le_iff {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) (T : CategoryTheory.Subgroupoid C) :
              S ≀ T ↔ βˆ€ {c d : C}, S.arrows c d βŠ† T.arrows c d
              Equations
              • CategoryTheory.Subgroupoid.instTopSubgroupoid = { top := { arrows := fun (x x_1 : C) => Set.univ, inv := β‹―, mul := β‹― } }
              theorem CategoryTheory.Subgroupoid.mem_top {C : Type u} [CategoryTheory.Groupoid C] {c : C} {d : C} (f : c ⟢ d) :
              f ∈ ⊀.arrows c d
              Equations
              • CategoryTheory.Subgroupoid.instBotSubgroupoid = { bot := { arrows := fun (x x_1 : C) => βˆ…, inv := β‹―, mul := β‹― } }
              Equations
              • CategoryTheory.Subgroupoid.instInhabitedSubgroupoid = { default := ⊀ }
              Equations
              • CategoryTheory.Subgroupoid.instInfSubgroupoid = { inf := fun (S T : CategoryTheory.Subgroupoid C) => { arrows := fun (c d : C) => S.arrows c d ∩ T.arrows c d, inv := β‹―, mul := β‹― } }
              Equations
              • One or more equations did not get rendered due to their size.
              theorem CategoryTheory.Subgroupoid.mem_sInf_arrows {C : Type u} [CategoryTheory.Groupoid C] {s : Set (CategoryTheory.Subgroupoid C)} {c : C} {d : C} {p : c ⟢ d} :
              p ∈ (sInf s).arrows c d ↔ βˆ€ S ∈ s, p ∈ S.arrows c d
              theorem CategoryTheory.Subgroupoid.mem_sInf {C : Type u} [CategoryTheory.Groupoid C] {s : Set (CategoryTheory.Subgroupoid C)} {p : (c : C) Γ— (d : C) Γ— (c ⟢ d)} :
              p ∈ sInf s ↔ βˆ€ S ∈ s, p ∈ S
              Equations

              The functor associated to the embedding of subgroupoids

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                inductive CategoryTheory.Subgroupoid.Discrete.Arrows {C : Type u} [CategoryTheory.Groupoid C] (c : C) (d : C) :
                (c ⟢ d) β†’ Prop

                The family of arrows of the discrete groupoid

                Instances For

                  The only arrows of the discrete groupoid are the identity arrows.

                  Equations
                  Instances For
                    theorem CategoryTheory.Subgroupoid.mem_discrete_iff {C : Type u} [CategoryTheory.Groupoid C] {c : C} {d : C} (f : c ⟢ d) :
                    f ∈ CategoryTheory.Subgroupoid.discrete.arrows c d ↔ βˆƒ (h : c = d), f = CategoryTheory.eqToHom h

                    A subgroupoid is wide if its carrier set is all of C

                    Instances For

                      AΒ subgroupoid is normal if it is wide and satisfies the expected stability under conjugacy.

                      Instances For

                        The subgropoid generated by the set of arrows X

                        Equations
                        Instances For
                          theorem CategoryTheory.Subgroupoid.subset_generated {C : Type u} [CategoryTheory.Groupoid C] (X : (c d : C) β†’ Set (c ⟢ d)) (c : C) (d : C) :

                          The normal sugroupoid generated by the set of arrows X

                          Equations
                          Instances For

                            A functor between groupoid defines a map of subgroupoids in the reverse direction by taking preimages.

                            Equations
                            Instances For

                              The kernel of a functor between subgroupoid is the preimage.

                              Equations
                              Instances For
                                theorem CategoryTheory.Subgroupoid.mem_ker_iff {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (Ο† : CategoryTheory.Functor C D) {c : C} {d : C} (f : c ⟢ d) :
                                f ∈ (CategoryTheory.Subgroupoid.ker Ο†).arrows c d ↔ βˆƒ (h : Ο†.obj c = Ο†.obj d), Ο†.map f = CategoryTheory.eqToHom h
                                inductive CategoryTheory.Subgroupoid.Map.Arrows {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) (S : CategoryTheory.Subgroupoid C) (c : D) (d : D) :
                                (c ⟢ d) β†’ Prop

                                The family of arrows of the image of a subgroupoid under a functor injective on objects

                                Instances For
                                  theorem CategoryTheory.Subgroupoid.Map.arrows_iff {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (Ο† : CategoryTheory.Functor C D) (hΟ† : Function.Injective Ο†.obj) (S : CategoryTheory.Subgroupoid C) {c : D} {d : D} (f : c ⟢ d) :
                                  CategoryTheory.Subgroupoid.Map.Arrows Ο† hΟ† S c d f ↔ βˆƒ (a : C) (b : C) (g : a ⟢ b) (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))

                                  The "forward" image of a subgroupoid under a functor injective on objects

                                  Equations
                                  Instances For
                                    theorem CategoryTheory.Subgroupoid.mem_map_iff {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (Ο† : CategoryTheory.Functor C D) (hΟ† : Function.Injective Ο†.obj) (S : CategoryTheory.Subgroupoid C) {c : D} {d : D} (f : c ⟢ d) :
                                    f ∈ (CategoryTheory.Subgroupoid.map Ο† hΟ† S).arrows c d ↔ βˆƒ (a : C) (b : C) (g : a ⟢ b) (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))

                                    The image of a functor injective on objects

                                    Equations
                                    Instances For
                                      theorem CategoryTheory.Subgroupoid.mem_im_iff {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (Ο† : CategoryTheory.Functor C D) (hΟ† : Function.Injective Ο†.obj) {c : D} {d : D} (f : c ⟢ d) :
                                      f ∈ (CategoryTheory.Subgroupoid.im Ο† hΟ†).arrows c d ↔ βˆƒ (a : C) (b : C) (g : a ⟢ b) (ha : Ο†.obj a = c) (hb : Ο†.obj b = d), f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom β‹―) (CategoryTheory.CategoryStruct.comp (Ο†.map g) (CategoryTheory.eqToHom hb))
                                      @[inline, reducible]

                                      A subgroupoid is thin (CategoryTheory.Subgroupoid.IsThin) if it has at most one arrow between any two vertices.

                                      Equations
                                      Instances For

                                        The isotropy subgroupoid of S

                                        Equations
                                        Instances For

                                          The full subgroupoid on a set D : Set C

                                          Equations
                                          Instances For
                                            @[simp]