Subgroupoid #

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

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

containment of subgroupoids is a complete lattice;
images and preimages of subgroupoids under a functor;
the notion of normality of subgroupoids and its stability under intersection and preimage;
compatibility of the above with groupoid.vertex_group.

Main definitions #

Given a type C with associated groupoid C instance.

subgroupoid C is the type of subgroupoids of C
subgroupoid.is_normal is the property that the subgroupoid is stable under conjugation by arbitrary arrows, and that all identity arrows are contained in the subgroupoid.
subgroupoid.comap is the "preimage" map of subgroupoids along a functor.
subgroupoid.map is the "image" map of subgroupoids along a functor injective on objects.
subgroupoid.vertex_subgroup is the subgroup of the vertex group at a given vertex v, assuming v is contained in the subgroupoid (meaning, by definition, that the arrow 𝟙 v is contained in the subgroupoid).

Implementation details #

The structure of this file is copied from/inspired by group_theory.subgroup.basic and combinatorics.simple_graph.subgraph.

TODO #

Equivalent inductive characterization of generated (normal) subgroupoids.
Characterization of normal subgroupoids as kernels.
Prove that full and disconnect preserve intersections (and disconnect also unions)

Tags #

subgroupoid

source

@[ext]

structure category_theory.subgroupoid (C : Type u) [category_theory.groupoid C] :

Type (max u u_2)

arrows : Π (c d : C), set (c ⟶ d)
inv : ∀ {c d : C} {p : c ⟶ d}, p ∈ self.arrows c d → category_theory.groupoid.inv p ∈ self.arrows d c
mul : ∀ {c d e : C} {p : c ⟶ d}, p ∈ self.arrows c d → ∀ {q : d ⟶ e}, q ∈ self.arrows d e → p ≫ q ∈ self.arrows c e

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

category_theory.subgroupoid.has_sizeof_inst
category_theory.subgroupoid.sigma.set_like
category_theory.subgroupoid.has_top
category_theory.subgroupoid.has_bot
category_theory.subgroupoid.inhabited
category_theory.subgroupoid.has_inf
category_theory.subgroupoid.has_Inf
category_theory.subgroupoid.complete_lattice

source

theorem category_theory.subgroupoid.ext {C : Type u} {_inst_2 : category_theory.groupoid C} (x y : category_theory.subgroupoid C) (h : x.arrows = y.arrows) :

x = y

source

theorem category_theory.subgroupoid.ext_iff {C : Type u} {_inst_2 : category_theory.groupoid C} (x y : category_theory.subgroupoid C) :

x = y ↔ x.arrows = y.arrows

source

theorem category_theory.subgroupoid.inv_mem_iff {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) {c d : C} (f : c ⟶ d) :

category_theory.groupoid.inv f ∈ S.arrows d c ↔ f ∈ S.arrows c d

source

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

source

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

source

def category_theory.subgroupoid.objs {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) :

set C

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

Equations

S.objs = {c : C | (S.arrows c c).nonempty}

Instances for ↥category_theory.subgroupoid.objs

category_theory.subgroupoid.coe

source

theorem category_theory.subgroupoid.mem_objs_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.objs

source

theorem category_theory.subgroupoid.mem_objs_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.objs

source

theorem category_theory.subgroupoid.id_mem_of_nonempty_isotropy {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) (c : C) :

c ∈ S.objs → 𝟙 c ∈ S.arrows c c

source

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

source

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

source

def category_theory.subgroupoid.as_wide_quiver {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) :

quiver C

A subgroupoid seen as a quiver on vertex set C

Equations

S.as_wide_quiver = {hom := λ (c d : C), subtype (S.arrows c d)}

source

@[protected, instance]

def category_theory.subgroupoid.coe {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) :

category_theory.groupoid ↥(S.objs)

The coercion of a subgroupoid as a groupoid

Equations

S.coe = {to_category := {to_category_struct := {to_quiver := {hom := λ (a b : ↥(S.objs)), ↥(S.arrows a.val b.val)}, id := λ (a : ↥(S.objs)), ⟨𝟙 a.val, _⟩, comp := λ (a b c : ↥(S.objs)) (p : a ⟶ b) (q : b ⟶ c), ⟨p.val ≫ q.val, _⟩}, id_comp' := _, comp_id' := _, assoc' := _}, inv := λ (a b : ↥(S.objs)) (p : a ⟶ b), ⟨category_theory.groupoid.inv p.val, _⟩, inv_comp' := _, comp_inv' := _}

source

theorem category_theory.subgroupoid.coe_inv_coe {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) (a b : ↥(S.objs)) (p : a ⟶ b) :

↑(category_theory.groupoid.inv p) = category_theory.groupoid.inv p.val

source

@[simp]

theorem category_theory.subgroupoid.coe_to_category_comp_coe {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) (a b c : ↥(S.objs)) (p : a ⟶ b) (q : b ⟶ c) :

↑(p ≫ q) = p.val ≫ q.val

source

@[simp]

theorem category_theory.subgroupoid.coe_inv_coe' {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) {c d : ↥(S.objs)} (p : c ⟶ d) :

(category_theory.inv p).val = category_theory.inv p.val

source

def category_theory.subgroupoid.hom {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) :

↥(S.objs) ⥤ C

The embedding of the coerced subgroupoid to its parent

Equations

S.hom = {obj := λ (c : ↥(S.objs)), c.val, map := λ (c d : ↥(S.objs)) (f : c ⟶ d), f.val, map_id' := _, map_comp' := _}

source

theorem category_theory.subgroupoid.hom.inj_on_objects {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) :

function.injective S.hom.obj

source

theorem category_theory.subgroupoid.hom.faithful {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) (c d : ↥(S.objs)) :

function.injective (λ (f : c ⟶ d), S.hom.map f)

source

def category_theory.subgroupoid.vertex_subgroup {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) {c : C} (hc : c ∈ S.objs) :

subgroup (c ⟶ c)

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

Equations

S.vertex_subgroup hc = {carrier := S.arrows c c, mul_mem' := _, one_mem' := _, inv_mem' := _}

source

@[protected, instance]

def category_theory.subgroupoid.sigma.set_like {C : Type u} [category_theory.groupoid C] :

set_like (category_theory.subgroupoid C) (Σ (c d : C), c ⟶ d)

Equations

category_theory.subgroupoid.sigma.set_like = {coe := λ (S : category_theory.subgroupoid C), {F : Σ (c d : C), c ⟶ d | F.snd.snd ∈ S.arrows F.fst F.snd.fst}, coe_injective' := _}

source

theorem category_theory.subgroupoid.mem_iff {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) (F : Σ (c d : C), c ⟶ d) :

F ∈ S ↔ F.snd.snd ∈ S.arrows F.fst F.snd.fst

source

theorem category_theory.subgroupoid.le_iff {C : Type u} [category_theory.groupoid C] (S T : category_theory.subgroupoid C) :

S ≤ T ↔ ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d

source

@[protected, instance]

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

has_top (category_theory.subgroupoid C)

Equations

category_theory.subgroupoid.has_top = {top := {arrows := λ (_x _x_1 : C), set.univ, inv := _, mul := _}}

source

theorem category_theory.subgroupoid.mem_top {C : Type u} [category_theory.groupoid C] {c d : C} (f : c ⟶ d) :

f ∈ ⊤.arrows c d

source

theorem category_theory.subgroupoid.mem_top_objs {C : Type u} [category_theory.groupoid C] (c : C) :

c ∈ ⊤.objs

source

@[protected, instance]

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

has_bot (category_theory.subgroupoid C)

Equations

category_theory.subgroupoid.has_bot = {bot := {arrows := λ (_x _x_1 : C), ∅, inv := _, mul := _}}

source

@[protected, instance]

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

inhabited (category_theory.subgroupoid C)

Equations

category_theory.subgroupoid.inhabited = {default := ⊤}

source

@[protected, instance]

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

has_inf (category_theory.subgroupoid C)

Equations

category_theory.subgroupoid.has_inf = {inf := λ (S T : category_theory.subgroupoid C), {arrows := λ (c d : C), S.arrows c d ∩ T.arrows c d, inv := _, mul := _}}

source

@[protected, instance]

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

has_Inf (category_theory.subgroupoid C)

Equations

category_theory.subgroupoid.has_Inf = {Inf := λ (s : set (category_theory.subgroupoid C)), {arrows := λ (c d : C), ⋂ (S : category_theory.subgroupoid C) (H : S ∈ s), S.arrows c d, inv := _, mul := _}}

source

@[protected, instance]

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

complete_lattice (category_theory.subgroupoid C)

Equations

category_theory.subgroupoid.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (category_theory.subgroupoid C) category_theory.subgroupoid.complete_lattice._proof_1), le := complete_lattice.le (complete_lattice_of_Inf (category_theory.subgroupoid C) category_theory.subgroupoid.complete_lattice._proof_1), lt := complete_lattice.lt (complete_lattice_of_Inf (category_theory.subgroupoid C) category_theory.subgroupoid.complete_lattice._proof_1), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf category_theory.subgroupoid.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (category_theory.subgroupoid C) category_theory.subgroupoid.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_Inf (category_theory.subgroupoid C) category_theory.subgroupoid.complete_lattice._proof_1), Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}

source

theorem category_theory.subgroupoid.le_objs {C : Type u} [category_theory.groupoid C] {S T : category_theory.subgroupoid C} (h : S ≤ T) :

S.objs ⊆ T.objs

source

def category_theory.subgroupoid.inclusion {C : Type u} [category_theory.groupoid C] {S T : category_theory.subgroupoid C} (h : S ≤ T) :

↥(S.objs) ⥤ ↥(T.objs)

The functor associated to the embedding of subgroupoids

Equations

category_theory.subgroupoid.inclusion h = {obj := λ (s : ↥(S.objs)), ⟨s.val, _⟩, map := λ (s t : ↥(S.objs)) (f : s ⟶ t), ⟨f.val, _⟩, map_id' := _, map_comp' := _}

source

theorem category_theory.subgroupoid.inclusion_inj_on_objects {C : Type u} [category_theory.groupoid C] {S T : category_theory.subgroupoid C} (h : S ≤ T) :

function.injective (category_theory.subgroupoid.inclusion h).obj

source

theorem category_theory.subgroupoid.inclusion_faithful {C : Type u} [category_theory.groupoid C] {S T : category_theory.subgroupoid C} (h : S ≤ T) (s t : ↥(S.objs)) :

function.injective (λ (f : s ⟶ t), (category_theory.subgroupoid.inclusion h).map f)

source

theorem category_theory.subgroupoid.inclusion_refl {C : Type u} [category_theory.groupoid C] {S : category_theory.subgroupoid C} :

category_theory.subgroupoid.inclusion _ = 𝟭 ↥(S.objs)

source

theorem category_theory.subgroupoid.inclusion_trans {C : Type u} [category_theory.groupoid C] {R S T : category_theory.subgroupoid C} (k : R ≤ S) (h : S ≤ T) :

category_theory.subgroupoid.inclusion _ = category_theory.subgroupoid.inclusion k ⋙ category_theory.subgroupoid.inclusion h

source

theorem category_theory.subgroupoid.inclusion_comp_embedding {C : Type u} [category_theory.groupoid C] {S T : category_theory.subgroupoid C} (h : S ≤ T) :

category_theory.subgroupoid.inclusion h ⋙ T.hom = S.hom

source

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

(c ⟶ d) → Prop

id : ∀ {C : Type u} [_inst_1 : category_theory.groupoid C] (c : C), category_theory.subgroupoid.discrete.arrows c c (𝟙 c)

The family of arrows of the discrete groupoid

source

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

category_theory.subgroupoid C

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

Equations

category_theory.subgroupoid.discrete = {arrows := category_theory.subgroupoid.discrete.arrows _inst_1, inv := _, mul := _}

source

theorem category_theory.subgroupoid.mem_discrete_iff {C : Type u} [category_theory.groupoid C] {c d : C} (f : c ⟶ d) :

f ∈ category_theory.subgroupoid.discrete.arrows c d ↔ ∃ (h : c = d), f = category_theory.eq_to_hom h

source

structure category_theory.subgroupoid.is_wide {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) :

Prop

wide : ∀ (c : C), 𝟙 c ∈ S.arrows c c

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

source

theorem category_theory.subgroupoid.is_wide_iff_objs_eq_univ {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) :

S.is_wide ↔ S.objs = set.univ

source

theorem category_theory.subgroupoid.is_wide.id_mem {C : Type u} [category_theory.groupoid C] {S : category_theory.subgroupoid C} (Sw : S.is_wide) (c : C) :

𝟙 c ∈ S.arrows c c

source

theorem category_theory.subgroupoid.is_wide.eq_to_hom_mem {C : Type u} [category_theory.groupoid C] {S : category_theory.subgroupoid C} (Sw : S.is_wide) {c d : C} (h : c = d) :

category_theory.eq_to_hom h ∈ S.arrows c d

source

structure category_theory.subgroupoid.is_normal {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) :

Prop

to_is_wide : S.is_wide
conj : ∀ {c d : C} (p : c ⟶ d) {γ : c ⟶ c}, γ ∈ S.arrows c c → category_theory.groupoid.inv p ≫ γ ≫ p ∈ S.arrows d d

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

source

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) :

p ≫ γ ≫ category_theory.groupoid.inv p ∈ S.arrows d d

source

theorem category_theory.subgroupoid.is_normal.conjugation_bij {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) (Sn : S.is_normal) {c d : C} (p : c ⟶ d) :

set.bij_on (λ (γ : c ⟶ c), category_theory.groupoid.inv p ≫ γ ≫ p) (S.arrows c c) (S.arrows d d)

source

theorem category_theory.subgroupoid.top_is_normal {C : Type u} [category_theory.groupoid C] :

⊤.is_normal

source

theorem category_theory.subgroupoid.Inf_is_normal {C : Type u} [category_theory.groupoid C] (s : set (category_theory.subgroupoid C)) (sn : ∀ (S : category_theory.subgroupoid C), S ∈ s → S.is_normal) :

(has_Inf.Inf s).is_normal

source

theorem category_theory.subgroupoid.discrete_is_normal {C : Type u} [category_theory.groupoid C] :

category_theory.subgroupoid.discrete.is_normal

source

theorem category_theory.subgroupoid.is_normal.vertex_subgroup {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) (Sn : S.is_normal) (c : C) (cS : c ∈ S.objs) :

(S.vertex_subgroup cS).normal

source

def category_theory.subgroupoid.generated {C : Type u} [category_theory.groupoid C] (X : Π (c d : C), set (c ⟶ d)) :

category_theory.subgroupoid C

The subgropoid generated by the set of arrows X

Equations

category_theory.subgroupoid.generated X = has_Inf.Inf {S : category_theory.subgroupoid C | ∀ (c d : C), X c d ⊆ S.arrows c d}

source

theorem category_theory.subgroupoid.subset_generated {C : Type u} [category_theory.groupoid C] (X : Π (c d : C), set (c ⟶ d)) (c d : C) :

X c d ⊆ (category_theory.subgroupoid.generated X).arrows c d

source

def category_theory.subgroupoid.generated_normal {C : Type u} [category_theory.groupoid C] (X : Π (c d : C), set (c ⟶ d)) :

category_theory.subgroupoid C

The normal sugroupoid generated by the set of arrows X

Equations

category_theory.subgroupoid.generated_normal X = has_Inf.Inf {S : category_theory.subgroupoid C | (∀ (c d : C), X c d ⊆ S.arrows c d) ∧ S.is_normal}

source

theorem category_theory.subgroupoid.generated_le_generated_normal {C : Type u} [category_theory.groupoid C] (X : Π (c d : C), set (c ⟶ d)) :

category_theory.subgroupoid.generated X ≤ category_theory.subgroupoid.generated_normal X

source

theorem category_theory.subgroupoid.generated_normal_is_normal {C : Type u} [category_theory.groupoid C] (X : Π (c d : C), set (c ⟶ d)) :

(category_theory.subgroupoid.generated_normal X).is_normal

source

theorem category_theory.subgroupoid.is_normal.generated_normal_le {C : Type u} [category_theory.groupoid C] (X : Π (c d : C), set (c ⟶ d)) {S : category_theory.subgroupoid C} (Sn : S.is_normal) :

category_theory.subgroupoid.generated_normal X ≤ S ↔ ∀ (c d : C), X c d ⊆ S.arrows c d

source

def category_theory.subgroupoid.comap {C : Type u} [category_theory.groupoid C] {D : Type u_2} [category_theory.groupoid D] (φ : C ⥤ D) (S : category_theory.subgroupoid D) :

category_theory.subgroupoid C

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

Equations

category_theory.subgroupoid.comap φ S = {arrows := λ (c d : C), {f : c ⟶ d | φ.map f ∈ S.arrows (φ.obj c) (φ.obj d)}, inv := _, mul := _}

source

theorem category_theory.subgroupoid.comap_mono {C : Type u} [category_theory.groupoid C] {D : Type u_2} [category_theory.groupoid D] (φ : C ⥤ D) (S T : category_theory.subgroupoid D) :

S ≤ T → category_theory.subgroupoid.comap φ S ≤ category_theory.subgroupoid.comap φ T

source

theorem category_theory.subgroupoid.is_normal_comap {C : Type u} [category_theory.groupoid C] {D : Type u_2} [category_theory.groupoid D] (φ : C ⥤ D) {S : category_theory.subgroupoid D} (Sn : S.is_normal) :

(category_theory.subgroupoid.comap φ S).is_normal

source

@[simp]

theorem category_theory.subgroupoid.comap_comp {C : Type u} [category_theory.groupoid C] {D : Type u_2} [category_theory.groupoid D] (φ : C ⥤ D) {E : Type u_4} [category_theory.groupoid E] (ψ : D ⥤ E) :

category_theory.subgroupoid.comap (φ ⋙ ψ) = category_theory.subgroupoid.comap φ ∘ category_theory.subgroupoid.comap ψ

source

def category_theory.subgroupoid.ker {C : Type u} [category_theory.groupoid C] {D : Type u_2} [category_theory.groupoid D] (φ : C ⥤ D) :

category_theory.subgroupoid C

The kernel of a functor between subgroupoid is the preimage.

Equations

category_theory.subgroupoid.ker φ = category_theory.subgroupoid.comap φ category_theory.subgroupoid.discrete

source

theorem category_theory.subgroupoid.mem_ker_iff {C : Type u} [category_theory.groupoid C] {D : Type u_2} [category_theory.groupoid D] (φ : C ⥤ D) {c d : C} (f : c ⟶ d) :

f ∈ (category_theory.subgroupoid.ker φ).arrows c d ↔ ∃ (h : φ.obj c = φ.obj d), φ.map f = category_theory.eq_to_hom h

source

theorem category_theory.subgroupoid.ker_is_normal {C : Type u} [category_theory.groupoid C] {D : Type u_2} [category_theory.groupoid D] (φ : C ⥤ D) :

(category_theory.subgroupoid.ker φ).is_normal

source

@[simp]

theorem category_theory.subgroupoid.ker_comp {C : Type u} [category_theory.groupoid C] {D : Type u_2} [category_theory.groupoid D] (φ : C ⥤ D) {E : Type u_4} [category_theory.groupoid E] (ψ : D ⥤ E) :

category_theory.subgroupoid.ker (φ ⋙ ψ) = category_theory.subgroupoid.comap φ (category_theory.subgroupoid.ker ψ)

source

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

im : ∀ {C : Type u} [_inst_1 : category_theory.groupoid C] {D : Type u_2} [_inst_2 : category_theory.groupoid D] {φ : C ⥤ D} {hφ : function.injective φ.obj} {S : category_theory.subgroupoid C} {c d : C} (f : c ⟶ d), f ∈ S.arrows c d → category_theory.subgroupoid.map.arrows φ hφ S (φ.obj c) (φ.obj d) (φ.map f)

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

source

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 φ hφ 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

source

def category_theory.subgroupoid.map {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) :

category_theory.subgroupoid D

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

Equations

category_theory.subgroupoid.map φ hφ S = {arrows := category_theory.subgroupoid.map.arrows φ hφ S, inv := _, mul := _}

source

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 φ hφ 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

source

theorem category_theory.subgroupoid.galois_connection_map_comap {C : Type u} [category_theory.groupoid C] {D : Type u_2} [category_theory.groupoid D] (φ : C ⥤ D) (hφ : function.injective φ.obj) :

galois_connection (category_theory.subgroupoid.map φ hφ) (category_theory.subgroupoid.comap φ)

source

theorem category_theory.subgroupoid.map_mono {C : Type u} [category_theory.groupoid C] {D : Type u_2} [category_theory.groupoid D] (φ : C ⥤ D) (hφ : function.injective φ.obj) (S T : category_theory.subgroupoid C) :

S ≤ T → category_theory.subgroupoid.map φ hφ S ≤ category_theory.subgroupoid.map φ hφ T

source

theorem category_theory.subgroupoid.le_comap_map {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) :

S ≤ category_theory.subgroupoid.comap φ (category_theory.subgroupoid.map φ hφ S)

source

theorem category_theory.subgroupoid.map_comap_le {C : Type u} [category_theory.groupoid C] {D : Type u_2} [category_theory.groupoid D] (φ : C ⥤ D) (hφ : function.injective φ.obj) (T : category_theory.subgroupoid D) :

category_theory.subgroupoid.map φ hφ (category_theory.subgroupoid.comap φ T) ≤ T

source

theorem category_theory.subgroupoid.map_le_iff_le_comap {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) (T : category_theory.subgroupoid D) :

category_theory.subgroupoid.map φ hφ S ≤ T ↔ S ≤ category_theory.subgroupoid.comap φ T

source

theorem category_theory.subgroupoid.mem_map_objs_iff {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) {D : Type u_2} [category_theory.groupoid D] (φ : C ⥤ D) (hφ : function.injective φ.obj) (d : D) :

d ∈ (category_theory.subgroupoid.map φ hφ S).objs ↔ ∃ (c : C) (H : c ∈ S.objs), φ.obj c = d

source

@[simp]

theorem category_theory.subgroupoid.map_objs_eq {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) {D : Type u_2} [category_theory.groupoid D] (φ : C ⥤ D) (hφ : function.injective φ.obj) :

(category_theory.subgroupoid.map φ hφ S).objs = φ.obj '' S.objs

source

def category_theory.subgroupoid.im {C : Type u} [category_theory.groupoid C] {D : Type u_2} [category_theory.groupoid D] (φ : C ⥤ D) (hφ : function.injective φ.obj) :

category_theory.subgroupoid D

The image of a functor injective on objects

Equations

category_theory.subgroupoid.im φ hφ = category_theory.subgroupoid.map φ hφ ⊤

source

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

source

theorem category_theory.subgroupoid.mem_im_objs_iff {C : Type u} [category_theory.groupoid C] {D : Type u_2} [category_theory.groupoid D] (φ : C ⥤ D) (hφ : function.injective φ.obj) (d : D) :

d ∈ (category_theory.subgroupoid.im φ hφ).objs ↔ ∃ (c : C), φ.obj c = d

source

theorem category_theory.subgroupoid.obj_surjective_of_im_eq_top {C : Type u} [category_theory.groupoid C] {D : Type u_2} [category_theory.groupoid D] (φ : C ⥤ D) (hφ : function.injective φ.obj) (hφ' : category_theory.subgroupoid.im φ hφ = ⊤) :

function.surjective φ.obj

source

theorem category_theory.subgroupoid.is_normal_map {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) {D : Type u_2} [category_theory.groupoid D] (φ : C ⥤ D) (hφ : function.injective φ.obj) (hφ' : category_theory.subgroupoid.im φ hφ = ⊤) (Sn : S.is_normal) :

(category_theory.subgroupoid.map φ hφ S).is_normal

source

@[reducible]

def category_theory.subgroupoid.is_thin {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) :

Prop

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

source

theorem category_theory.subgroupoid.is_thin_iff {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) :

S.is_thin ↔ ∀ (c : ↥(S.objs)), subsingleton ↥(S.arrows ↑c ↑c)

source

@[reducible]

def category_theory.subgroupoid.is_totally_disconnected {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) :

Prop

A subgroupoid is_totally_disconnected if it has only isotropy arrows.

source

theorem category_theory.subgroupoid.is_totally_disconnected_iff {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) :

S.is_totally_disconnected ↔ ∀ (c d : C), (S.arrows c d).nonempty → c = d

source

def category_theory.subgroupoid.disconnect {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) :

category_theory.subgroupoid C

The isotropy subgroupoid of S

Equations

S.disconnect = {arrows := λ (c d : C) (f : c ⟶ d), c = d ∧ f ∈ S.arrows c d, inv := _, mul := _}

source

theorem category_theory.subgroupoid.disconnect_le {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) :

S.disconnect ≤ S

source

theorem category_theory.subgroupoid.disconnect_normal {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) (Sn : S.is_normal) :

S.disconnect.is_normal

source

@[simp]

theorem category_theory.subgroupoid.mem_disconnect_objs_iff {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) {c : C} :

c ∈ S.disconnect.objs ↔ c ∈ S.objs

source

theorem category_theory.subgroupoid.disconnect_objs {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) :

S.disconnect.objs = S.objs

source

theorem category_theory.subgroupoid.disconnect_is_totally_disconnected {C : Type u} [category_theory.groupoid C] (S : category_theory.subgroupoid C) :

S.disconnect.is_totally_disconnected

source

def category_theory.subgroupoid.full {C : Type u} [category_theory.groupoid C] (D : set C) :

category_theory.subgroupoid C

The full subgroupoid on a set D : set C

Equations

category_theory.subgroupoid.full D = {arrows := λ (c d : C) (_x : c ⟶ d), c ∈ D ∧ d ∈ D, inv := _, mul := _}

source

theorem category_theory.subgroupoid.full_objs {C : Type u} [category_theory.groupoid C] (D : set C) :

(category_theory.subgroupoid.full D).objs = D

source

@[simp]

theorem category_theory.subgroupoid.mem_full_iff {C : Type u} [category_theory.groupoid C] (D : set C) {c d : C} {f : c ⟶ d} :

f ∈ (category_theory.subgroupoid.full D).arrows c d ↔ c ∈ D ∧ d ∈ D

source

@[simp]

theorem category_theory.subgroupoid.mem_full_objs_iff {C : Type u} [category_theory.groupoid C] (D : set C) {c : C} :

c ∈ (category_theory.subgroupoid.full D).objs ↔ c ∈ D

source

@[simp]

theorem category_theory.subgroupoid.full_empty {C : Type u} [category_theory.groupoid C] :

category_theory.subgroupoid.full ∅ = ⊥

source

@[simp]

theorem category_theory.subgroupoid.full_univ {C : Type u} [category_theory.groupoid C] :

category_theory.subgroupoid.full set.univ = ⊤

source

theorem category_theory.subgroupoid.full_mono {C : Type u} [category_theory.groupoid C] {D E : set C} (h : D ≤ E) :

category_theory.subgroupoid.full D ≤ category_theory.subgroupoid.full E

source

theorem category_theory.subgroupoid.full_arrow_eq_iff {C : Type u} [category_theory.groupoid C] (D : set C) {c d : ↥((category_theory.subgroupoid.full D).objs)} {f g : c ⟶ d} :

f = g ↔ ↑f = ↑g