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

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

    Instances For

      A subgroupoid seen as a quiver on vertex set C

      Instances For

        The embedding of the coerced subgroupoid to its parent

        Instances For

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

          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.

            Instances For
              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 ∈ CategoryTheory.Subgroupoid.arrows S F.fst F.snd.fst
              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 : CategoryTheory.Subgroupoid C), S ∈ s β†’ p ∈ S
              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.

                Instances For
                  theorem CategoryTheory.Subgroupoid.mem_discrete_iff {C : Type u} [CategoryTheory.Groupoid C] {c : C} {d : C} (f : c ⟢ d) :
                  f ∈ CategoryTheory.Subgroupoid.arrows CategoryTheory.Subgroupoid.discrete c d ↔ βˆƒ h, 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

                      Instances For

                        The normal sugroupoid generated by the set of arrows X

                        Instances For

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

                          Instances For

                            The kernel of a functor between subgroupoid is the preimage.

                            Instances For
                              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

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

                                Instances For

                                  The image of a functor injective on objects

                                  Instances For
                                    @[inline, reducible]

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

                                    Instances For
                                      @[inline, reducible]

                                      A subgroupoid IsTotallyDisconnected if it has only isotropy arrows.

                                      Instances For

                                        The full subgroupoid on a set D : Set C

                                        Instances For