mathlib documentation

category_theory.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 group_theory.subgroup.basic and combinatorics.simple_graph.subgraph.

TODO #

Tags #

subgroupoid

@[ext]
structure category_theory.subgroupoid (C : Type u) [category_theory.groupoid C] :
Type (max u u_2)

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

Instances for category_theory.subgroupoid
theorem category_theory.subgroupoid.mul_mem_cancel_left {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) {c d e : C} {f : c d} {g : d e} (hf : f S.arrows c d) :
f g S.arrows c e g S.arrows d e
theorem category_theory.subgroupoid.mul_mem_cancel_right {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) {c d e : C} {f : c d} {g : d e} (hg : g S.arrows d e) :
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 category_theory.subgroupoid.objs
theorem category_theory.subgroupoid.id_mem_of_src {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) {c d : C} {f : c d} (h : f S.arrows c d) :
𝟙 c S.arrows c c
theorem category_theory.subgroupoid.id_mem_of_tgt {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) {c d : C} {f : c d} (h : f S.arrows c d) :
𝟙 d S.arrows d d

A subgroupoid seen as a quiver on vertex set C

Equations
@[protected, instance]

The coercion of a subgroupoid as a groupoid

Equations
@[simp]

The embedding of the coerced subgroupoid to its parent

Equations

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

Equations
theorem category_theory.subgroupoid.mem_top {C : Type u} [category_theory.groupoid C] {c d : C} (f : c d) :
f .arrows c d
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

The functor associated to the embedding of subgroupoids

Equations
inductive category_theory.subgroupoid.discrete.arrows {C : Type u} [category_theory.groupoid C] (c d : C) :
(c d) Prop

The family of arrows of the discrete groupoid

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

Equations

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

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

theorem category_theory.subgroupoid.is_normal.conj' {C : Type u} [category_theory.groupoid C] {S : category_theory.subgroupoid C} (Sn : S.is_normal) {c d : C} (p : d c) {γ : c c} (hs : γ S.arrows c c) :

The subgropoid generated by the set of arrows X

Equations

The normal sugroupoid generated by the set of arrows X

Equations

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

Equations
inductive category_theory.subgroupoid.map.arrows {C : Type u} [category_theory.groupoid C] {D : Type u_2} [category_theory.groupoid D] (φ : C D) (hφ : function.injective φ.obj) (S : category_theory.subgroupoid C) (c d : D) :
(c d) Prop

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

theorem category_theory.subgroupoid.map.arrows_iff {C : Type u} [category_theory.groupoid C] {D : Type u_2} [category_theory.groupoid D] (φ : C D) (hφ : function.injective φ.obj) (S : category_theory.subgroupoid C) {c d : D} (f : c d) :
category_theory.subgroupoid.map.arrows φ S c d f (a b : C) (g : a b) (ha : φ.obj a = c) (hb : φ.obj b = d) (hg : g S.arrows a b), f = category_theory.eq_to_hom _ φ.map g category_theory.eq_to_hom hb

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

Equations
theorem category_theory.subgroupoid.mem_map_iff {C : Type u} [category_theory.groupoid C] {D : Type u_2} [category_theory.groupoid D] (φ : C D) (hφ : function.injective φ.obj) (S : category_theory.subgroupoid C) {c d : D} (f : c d) :
f (category_theory.subgroupoid.map φ S).arrows c d (a b : C) (g : a b) (ha : φ.obj a = c) (hb : φ.obj b = d) (hg : g S.arrows a b), f = category_theory.eq_to_hom _ φ.map g category_theory.eq_to_hom hb

The image of a functor injective on objects

Equations
theorem category_theory.subgroupoid.mem_im_iff {C : Type u} [category_theory.groupoid C] {D : Type u_2} [category_theory.groupoid D] (φ : C D) (hφ : function.injective φ.obj) {c d : D} (f : c d) :
f (category_theory.subgroupoid.im φ hφ).arrows c d (a b : C) (g : a b) (ha : φ.obj a = c) (hb : φ.obj b = d), f = category_theory.eq_to_hom _ φ.map g category_theory.eq_to_hom hb
@[reducible]

A subgroupoid is_thin if it has at most one arrow between any two vertices.

@[reducible]

A subgroupoid is_totally_disconnected if it has only isotropy arrows.

The isotropy subgroupoid of S

Equations

The full subgroupoid on a set D : set C

Equations
@[simp]