Subgroupoid

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 CategoryTheory.Groupoid.vertexGroup.

Main definitions

Given a type C with associated groupoid C instance.

• CategoryTheory.Subgroupoid C is the type of subgroupoids of C
• CategoryTheory.Subgroupoid.IsNormal is the property that the subgroupoid is stable under conjugation by arbitrary arrows, and that all identity arrows are contained in the subgroupoid.
• CategoryTheory.Subgroupoid.comap is the "preimage" map of subgroupoids along a functor.
• CategoryTheory.Subgroupoid.map is the "image" map of subgroupoids along a functor injective on objects.
• CategoryTheory.Subgroupoid.vertexSubgroup is the subgroup of the vertex group at a given vertex v, assuming v is contained in the CategoryTheory.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 Mathlib/GroupTheory/Subgroup/Basic.lean and Mathlib/Combinatorics/SimpleGraph/Subgraph.lean.

TODO

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

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)

• arrows : (c d : C) → Set (c ⟶ d)
• inv : ∀ {c d : C} {p : c ⟶ d}, p ∈ CategoryTheory.Subgroupoid.arrows s c d → CategoryTheory.Groupoid.inv p ∈ CategoryTheory.Subgroupoid.arrows s d c
• mul : ∀ {c d e : C} {p : c ⟶ d}, p ∈ CategoryTheory.Subgroupoid.arrows s c d → ∀ {q : d ⟶ e}, q ∈ CategoryTheory.Subgroupoid.arrows s d e → CategoryTheory.CategoryStruct.comp p q ∈ CategoryTheory.Subgroupoid.arrows s c e

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

theorem CategoryTheory.Subgroupoid.inv_mem_iff {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c : C} {d : C} (f : c ⟶ d) : CategoryTheory.Groupoid.inv f ∈ CategoryTheory.Subgroupoid.arrows S d c ↔ f ∈ CategoryTheory.Subgroupoid.arrows S c d

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 ∈ CategoryTheory.Subgroupoid.arrows S c d) : CategoryTheory.CategoryStruct.comp f g ∈ CategoryTheory.Subgroupoid.arrows S c e ↔ g ∈ CategoryTheory.Subgroupoid.arrows S 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 ∈ CategoryTheory.Subgroupoid.arrows S d e) : CategoryTheory.CategoryStruct.comp f g ∈ CategoryTheory.Subgroupoid.arrows S c e ↔ f ∈ CategoryTheory.Subgroupoid.arrows S c d

def CategoryTheory.Subgroupoid.objs {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : Set C

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

theorem CategoryTheory.Subgroupoid.mem_objs_of_src {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c : C} {d : C} {f : c ⟶ d} (h : f ∈ CategoryTheory.Subgroupoid.arrows S c d) : c ∈ CategoryTheory.Subgroupoid.objs S

theorem CategoryTheory.Subgroupoid.mem_objs_of_tgt {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c : C} {d : C} {f : c ⟶ d} (h : f ∈ CategoryTheory.Subgroupoid.arrows S c d) : d ∈ CategoryTheory.Subgroupoid.objs S

theorem CategoryTheory.Subgroupoid.id_mem_of_nonempty_isotropy {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) (c : C) : c ∈ CategoryTheory.Subgroupoid.objs S → CategoryTheory.CategoryStruct.id c ∈ CategoryTheory.Subgroupoid.arrows S c c

theorem CategoryTheory.Subgroupoid.id_mem_of_src {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c : C} {d : C} {f : c ⟶ d} (h : f ∈ CategoryTheory.Subgroupoid.arrows S c d) : CategoryTheory.CategoryStruct.id c ∈ CategoryTheory.Subgroupoid.arrows S c c

theorem CategoryTheory.Subgroupoid.id_mem_of_tgt {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c : C} {d : C} {f : c ⟶ d} (h : f ∈ CategoryTheory.Subgroupoid.arrows S c d) : CategoryTheory.CategoryStruct.id d ∈ CategoryTheory.Subgroupoid.arrows S d d

def CategoryTheory.Subgroupoid.asWideQuiver {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : Quiver C

A subgroupoid seen as a quiver on vertex set C

@[simp]

theorem CategoryTheory.Subgroupoid.coe_comp_coe {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : ∀ {X Y Z : ↑(CategoryTheory.Subgroupoid.objs S)} (p : X ⟶ Y) (q : Y ⟶ Z), ↑(CategoryTheory.CategoryStruct.comp p q) = CategoryTheory.CategoryStruct.comp ↑p ↑q

theorem CategoryTheory.Subgroupoid.coe_inv_coe {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : ∀ {X Y : ↑(CategoryTheory.Subgroupoid.objs S)} (p : X ⟶ Y), ↑(CategoryTheory.Groupoid.inv p) = CategoryTheory.Groupoid.inv ↑p

instance CategoryTheory.Subgroupoid.coe {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : CategoryTheory.Groupoid ↑(CategoryTheory.Subgroupoid.objs S)

The coercion of a subgroupoid as a groupoid

@[simp]

theorem CategoryTheory.Subgroupoid.coe_inv_coe' {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c : ↑(CategoryTheory.Subgroupoid.objs S)} {d : ↑(CategoryTheory.Subgroupoid.objs S)} (p : c ⟶ d) : ↑(CategoryTheory.inv p) = CategoryTheory.inv ↑p

def CategoryTheory.Subgroupoid.hom {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : CategoryTheory.Functor (↑(CategoryTheory.Subgroupoid.objs S)) C

The embedding of the coerced subgroupoid to its parent

theorem CategoryTheory.Subgroupoid.hom.inj_on_objects {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : Function.Injective (CategoryTheory.Subgroupoid.hom S).toPrefunctor.obj

theorem CategoryTheory.Subgroupoid.hom.faithful {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) (c : ↑(CategoryTheory.Subgroupoid.objs S)) (d : ↑(CategoryTheory.Subgroupoid.objs S)) : Function.Injective fun f => (CategoryTheory.Subgroupoid.hom S).map f

def CategoryTheory.Subgroupoid.vertexSubgroup {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c : C} (hc : c ∈ CategoryTheory.Subgroupoid.objs S) : Subgroup (c ⟶ c)

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

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.

instance CategoryTheory.Subgroupoid.instSetLikeSubgroupoidSigmaSigmaHomToQuiverToCategoryStructToCategory {C : Type u} [CategoryTheory.Groupoid C] : SetLike (CategoryTheory.Subgroupoid C) ((c : C) × (d : C) × (c ⟶ d))

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.le_iff {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) (T : CategoryTheory.Subgroupoid C) : S ≤ T ↔ ∀ {c d : C}, CategoryTheory.Subgroupoid.arrows S c d ⊆ CategoryTheory.Subgroupoid.arrows T c d

instance CategoryTheory.Subgroupoid.instTopSubgroupoid {C : Type u} [CategoryTheory.Groupoid C] : Top (CategoryTheory.Subgroupoid C)

theorem CategoryTheory.Subgroupoid.mem_top {C : Type u} [CategoryTheory.Groupoid C] {c : C} {d : C} (f : c ⟶ d) : f ∈ CategoryTheory.Subgroupoid.arrows ⊤ c d

theorem CategoryTheory.Subgroupoid.mem_top_objs {C : Type u} [CategoryTheory.Groupoid C] (c : C) : c ∈ CategoryTheory.Subgroupoid.objs ⊤

instance CategoryTheory.Subgroupoid.instBotSubgroupoid {C : Type u} [CategoryTheory.Groupoid C] : Bot (CategoryTheory.Subgroupoid C)

instance CategoryTheory.Subgroupoid.instInhabitedSubgroupoid {C : Type u} [CategoryTheory.Groupoid C] : Inhabited (CategoryTheory.Subgroupoid C)

instance CategoryTheory.Subgroupoid.instInfSubgroupoid {C : Type u} [CategoryTheory.Groupoid C] : Inf (CategoryTheory.Subgroupoid C)

instance CategoryTheory.Subgroupoid.instInfSetSubgroupoid {C : Type u} [CategoryTheory.Groupoid C] : InfSet (CategoryTheory.Subgroupoid C)

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 ∈ CategoryTheory.Subgroupoid.arrows (sInf s) c d ↔ ∀ (S : CategoryTheory.Subgroupoid C), S ∈ s → p ∈ CategoryTheory.Subgroupoid.arrows S 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 : CategoryTheory.Subgroupoid C), S ∈ s → p ∈ S

instance CategoryTheory.Subgroupoid.instCompleteLatticeSubgroupoid {C : Type u} [CategoryTheory.Groupoid C] : CompleteLattice (CategoryTheory.Subgroupoid C)

theorem CategoryTheory.Subgroupoid.le_objs {C : Type u} [CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C} {T : CategoryTheory.Subgroupoid C} (h : S ≤ T) : CategoryTheory.Subgroupoid.objs S ⊆ CategoryTheory.Subgroupoid.objs T

def CategoryTheory.Subgroupoid.inclusion {C : Type u} [CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C} {T : CategoryTheory.Subgroupoid C} (h : S ≤ T) : CategoryTheory.Functor ↑(CategoryTheory.Subgroupoid.objs S) ↑(CategoryTheory.Subgroupoid.objs T)

The functor associated to the embedding of subgroupoids

theorem CategoryTheory.Subgroupoid.inclusion_inj_on_objects {C : Type u} [CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C} {T : CategoryTheory.Subgroupoid C} (h : S ≤ T) : Function.Injective (CategoryTheory.Subgroupoid.inclusion h).toPrefunctor.obj

theorem CategoryTheory.Subgroupoid.inclusion_faithful {C : Type u} [CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C} {T : CategoryTheory.Subgroupoid C} (h : S ≤ T) (s : ↑(CategoryTheory.Subgroupoid.objs S)) (t : ↑(CategoryTheory.Subgroupoid.objs S)) : Function.Injective fun f => (CategoryTheory.Subgroupoid.inclusion h).map f

theorem CategoryTheory.Subgroupoid.inclusion_refl {C : Type u} [CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C} : CategoryTheory.Subgroupoid.inclusion (_ : S ≤ S) = CategoryTheory.Functor.id ↑(CategoryTheory.Subgroupoid.objs S)

theorem CategoryTheory.Subgroupoid.inclusion_trans {C : Type u} [CategoryTheory.Groupoid C] {R : CategoryTheory.Subgroupoid C} {S : CategoryTheory.Subgroupoid C} {T : CategoryTheory.Subgroupoid C} (k : R ≤ S) (h : S ≤ T) : CategoryTheory.Subgroupoid.inclusion (_ : R ≤ T) = CategoryTheory.Functor.comp (CategoryTheory.Subgroupoid.inclusion k) (CategoryTheory.Subgroupoid.inclusion h)

theorem CategoryTheory.Subgroupoid.inclusion_comp_embedding {C : Type u} [CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C} {T : CategoryTheory.Subgroupoid C} (h : S ≤ T) : CategoryTheory.Functor.comp (CategoryTheory.Subgroupoid.inclusion h) (CategoryTheory.Subgroupoid.hom T) = CategoryTheory.Subgroupoid.hom S

inductive CategoryTheory.Subgroupoid.Discrete.Arrows {C : Type u} [CategoryTheory.Groupoid C] (c : C) (d : C) : (c ⟶ d) → Prop

• id: ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (c : C), CategoryTheory.Subgroupoid.Discrete.Arrows c c (CategoryTheory.CategoryStruct.id c)

The family of arrows of the discrete groupoid

def CategoryTheory.Subgroupoid.discrete {C : Type u} [CategoryTheory.Groupoid C] : CategoryTheory.Subgroupoid C

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

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

structure CategoryTheory.Subgroupoid.IsWide {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : Prop

• wide : ∀ (c : C), CategoryTheory.CategoryStruct.id c ∈ CategoryTheory.Subgroupoid.arrows S c c

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

theorem CategoryTheory.Subgroupoid.isWide_iff_objs_eq_univ {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : CategoryTheory.Subgroupoid.IsWide S ↔ CategoryTheory.Subgroupoid.objs S = Set.univ

theorem CategoryTheory.Subgroupoid.IsWide.id_mem {C : Type u} [CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C} (Sw : CategoryTheory.Subgroupoid.IsWide S) (c : C) : CategoryTheory.CategoryStruct.id c ∈ CategoryTheory.Subgroupoid.arrows S c c

theorem CategoryTheory.Subgroupoid.IsWide.eqToHom_mem {C : Type u} [CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C} (Sw : CategoryTheory.Subgroupoid.IsWide S) {c : C} {d : C} (h : c = d) : CategoryTheory.eqToHom h ∈ CategoryTheory.Subgroupoid.arrows S c d

structure CategoryTheory.Subgroupoid.IsNormal {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) extends CategoryTheory.Subgroupoid.IsWide : Prop

• wide : ∀ (c : C), CategoryTheory.CategoryStruct.id c ∈ CategoryTheory.Subgroupoid.arrows S c c
• conj : ∀ {c d : C} (p : c ⟶ d) {γ : c ⟶ c}, γ ∈ CategoryTheory.Subgroupoid.arrows S c c → CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv p) (CategoryTheory.CategoryStruct.comp γ p) ∈ CategoryTheory.Subgroupoid.arrows S d d

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

theorem CategoryTheory.Subgroupoid.IsNormal.conj' {C : Type u} [CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C} (Sn : CategoryTheory.Subgroupoid.IsNormal S) {c : C} {d : C} (p : d ⟶ c) {γ : c ⟶ c} : γ ∈ CategoryTheory.Subgroupoid.arrows S c c → CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp γ (CategoryTheory.Groupoid.inv p)) ∈ CategoryTheory.Subgroupoid.arrows S d d

theorem CategoryTheory.Subgroupoid.IsNormal.conjugation_bij {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) (Sn : CategoryTheory.Subgroupoid.IsNormal S) {c : C} {d : C} (p : c ⟶ d) : Set.BijOn (fun γ => CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv p) (CategoryTheory.CategoryStruct.comp γ p)) (CategoryTheory.Subgroupoid.arrows S c c) (CategoryTheory.Subgroupoid.arrows S d d)

theorem CategoryTheory.Subgroupoid.top_isNormal {C : Type u} [CategoryTheory.Groupoid C] : CategoryTheory.Subgroupoid.IsNormal ⊤

theorem CategoryTheory.Subgroupoid.sInf_isNormal {C : Type u} [CategoryTheory.Groupoid C] (s : Set (CategoryTheory.Subgroupoid C)) (sn : ∀ (S : CategoryTheory.Subgroupoid C), S ∈ s → CategoryTheory.Subgroupoid.IsNormal S) : CategoryTheory.Subgroupoid.IsNormal (sInf s)

theorem CategoryTheory.Subgroupoid.discrete_isNormal {C : Type u} [CategoryTheory.Groupoid C] : CategoryTheory.Subgroupoid.IsNormal CategoryTheory.Subgroupoid.discrete

theorem CategoryTheory.Subgroupoid.IsNormal.vertexSubgroup {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) (Sn : CategoryTheory.Subgroupoid.IsNormal S) (c : C) (cS : c ∈ CategoryTheory.Subgroupoid.objs S) : Subgroup.Normal (CategoryTheory.Subgroupoid.vertexSubgroup S cS)

def CategoryTheory.Subgroupoid.generated {C : Type u} [CategoryTheory.Groupoid C] (X : (c d : C) → Set (c ⟶ d)) : CategoryTheory.Subgroupoid C

The subgropoid generated by the set of arrows X

theorem CategoryTheory.Subgroupoid.subset_generated {C : Type u} [CategoryTheory.Groupoid C] (X : (c d : C) → Set (c ⟶ d)) (c : C) (d : C) : X c d ⊆ CategoryTheory.Subgroupoid.arrows (CategoryTheory.Subgroupoid.generated X) c d

def CategoryTheory.Subgroupoid.generatedNormal {C : Type u} [CategoryTheory.Groupoid C] (X : (c d : C) → Set (c ⟶ d)) : CategoryTheory.Subgroupoid C

The normal sugroupoid generated by the set of arrows X

theorem CategoryTheory.Subgroupoid.generated_le_generatedNormal {C : Type u} [CategoryTheory.Groupoid C] (X : (c d : C) → Set (c ⟶ d)) : CategoryTheory.Subgroupoid.generated X ≤ CategoryTheory.Subgroupoid.generatedNormal X

theorem CategoryTheory.Subgroupoid.generatedNormal_isNormal {C : Type u} [CategoryTheory.Groupoid C] (X : (c d : C) → Set (c ⟶ d)) : CategoryTheory.Subgroupoid.IsNormal (CategoryTheory.Subgroupoid.generatedNormal X)

theorem CategoryTheory.Subgroupoid.IsNormal.generatedNormal_le {C : Type u} [CategoryTheory.Groupoid C] (X : (c d : C) → Set (c ⟶ d)) {S : CategoryTheory.Subgroupoid C} (Sn : CategoryTheory.Subgroupoid.IsNormal S) : CategoryTheory.Subgroupoid.generatedNormal X ≤ S ↔ ∀ (c d : C), X c d ⊆ CategoryTheory.Subgroupoid.arrows S c d

def CategoryTheory.Subgroupoid.comap {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) (S : CategoryTheory.Subgroupoid D) : CategoryTheory.Subgroupoid C

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

theorem CategoryTheory.Subgroupoid.comap_mono {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) (S : CategoryTheory.Subgroupoid D) (T : CategoryTheory.Subgroupoid D) : S ≤ T → CategoryTheory.Subgroupoid.comap φ S ≤ CategoryTheory.Subgroupoid.comap φ T

theorem CategoryTheory.Subgroupoid.isNormal_comap {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) {S : CategoryTheory.Subgroupoid D} (Sn : CategoryTheory.Subgroupoid.IsNormal S) : CategoryTheory.Subgroupoid.IsNormal (CategoryTheory.Subgroupoid.comap φ S)

@[simp]

theorem CategoryTheory.Subgroupoid.comap_comp {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) {E : Type u_2} [CategoryTheory.Groupoid E] (ψ : CategoryTheory.Functor D E) : CategoryTheory.Subgroupoid.comap (CategoryTheory.Functor.comp φ ψ) = CategoryTheory.Subgroupoid.comap φ ∘ CategoryTheory.Subgroupoid.comap ψ

def CategoryTheory.Subgroupoid.ker {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) : CategoryTheory.Subgroupoid C

The kernel of a functor between subgroupoid is the preimage.

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.arrows (CategoryTheory.Subgroupoid.ker φ) c d ↔ ∃ h, φ.map f = CategoryTheory.eqToHom h

theorem CategoryTheory.Subgroupoid.ker_isNormal {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) : CategoryTheory.Subgroupoid.IsNormal (CategoryTheory.Subgroupoid.ker φ)

@[simp]

theorem CategoryTheory.Subgroupoid.ker_comp {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) {E : Type u_2} [CategoryTheory.Groupoid E] (ψ : CategoryTheory.Functor D E) : CategoryTheory.Subgroupoid.ker (CategoryTheory.Functor.comp φ ψ) = CategoryTheory.Subgroupoid.comap φ (CategoryTheory.Subgroupoid.ker ψ)

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

• im: ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D] {φ : CategoryTheory.Functor C D} {hφ : Function.Injective φ.obj} {S : CategoryTheory.Subgroupoid C} {c d : C} (f : c ⟶ d), f ∈ CategoryTheory.Subgroupoid.arrows S c d → CategoryTheory.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

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 b g ha hb _hg, f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : c = φ.obj a)) (CategoryTheory.CategoryStruct.comp (φ.map g) (CategoryTheory.eqToHom hb))

def CategoryTheory.Subgroupoid.map {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) : CategoryTheory.Subgroupoid D

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

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.arrows (CategoryTheory.Subgroupoid.map φ hφ S) c d ↔ ∃ a b g ha hb _hg, f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : c = φ.obj a)) (CategoryTheory.CategoryStruct.comp (φ.map g) (CategoryTheory.eqToHom hb))

theorem CategoryTheory.Subgroupoid.galoisConnection_map_comap {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) : GaloisConnection (CategoryTheory.Subgroupoid.map φ hφ) (CategoryTheory.Subgroupoid.comap φ)

theorem CategoryTheory.Subgroupoid.map_mono {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) (T : CategoryTheory.Subgroupoid C) : S ≤ T → CategoryTheory.Subgroupoid.map φ hφ S ≤ CategoryTheory.Subgroupoid.map φ hφ T

theorem CategoryTheory.Subgroupoid.le_comap_map {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) : S ≤ CategoryTheory.Subgroupoid.comap φ (CategoryTheory.Subgroupoid.map φ hφ S)

theorem CategoryTheory.Subgroupoid.map_comap_le {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) (T : CategoryTheory.Subgroupoid D) : CategoryTheory.Subgroupoid.map φ hφ (CategoryTheory.Subgroupoid.comap φ T) ≤ T

theorem CategoryTheory.Subgroupoid.map_le_iff_le_comap {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) (T : CategoryTheory.Subgroupoid D) : CategoryTheory.Subgroupoid.map φ hφ S ≤ T ↔ S ≤ CategoryTheory.Subgroupoid.comap φ T

theorem CategoryTheory.Subgroupoid.mem_map_objs_iff {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {D : Type u_1} [CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) (d : D) : d ∈ CategoryTheory.Subgroupoid.objs (CategoryTheory.Subgroupoid.map φ hφ S) ↔ ∃ c, c ∈ CategoryTheory.Subgroupoid.objs S ∧ φ.obj c = d

@[simp]

theorem CategoryTheory.Subgroupoid.map_objs_eq {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {D : Type u_1} [CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) : CategoryTheory.Subgroupoid.objs (CategoryTheory.Subgroupoid.map φ hφ S) = φ.obj '' CategoryTheory.Subgroupoid.objs S

def CategoryTheory.Subgroupoid.im {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) : CategoryTheory.Subgroupoid D

The image of a functor injective on objects

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.arrows (CategoryTheory.Subgroupoid.im φ hφ) c d ↔ ∃ a b g ha hb, f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : c = φ.obj a)) (CategoryTheory.CategoryStruct.comp (φ.map g) (CategoryTheory.eqToHom hb))

theorem CategoryTheory.Subgroupoid.mem_im_objs_iff {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) (d : D) : d ∈ CategoryTheory.Subgroupoid.objs (CategoryTheory.Subgroupoid.im φ hφ) ↔ ∃ c, φ.obj c = d

theorem CategoryTheory.Subgroupoid.obj_surjective_of_im_eq_top {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) (hφ' : CategoryTheory.Subgroupoid.im φ hφ = ⊤) : Function.Surjective φ.obj

theorem CategoryTheory.Subgroupoid.isNormal_map {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {D : Type u_1} [CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) (hφ' : CategoryTheory.Subgroupoid.im φ hφ = ⊤) (Sn : CategoryTheory.Subgroupoid.IsNormal S) : CategoryTheory.Subgroupoid.IsNormal (CategoryTheory.Subgroupoid.map φ hφ S)

@[inline, reducible]

abbrev CategoryTheory.Subgroupoid.IsThin {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : Prop

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

theorem CategoryTheory.Subgroupoid.isThin_iff {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : CategoryTheory.Subgroupoid.IsThin S ↔ ∀ (c : ↑(CategoryTheory.Subgroupoid.objs S)), Subsingleton ↑(CategoryTheory.Subgroupoid.arrows S ↑c ↑c)

@[inline, reducible]

abbrev CategoryTheory.Subgroupoid.IsTotallyDisconnected {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : Prop

A subgroupoid IsTotallyDisconnected if it has only isotropy arrows.

theorem CategoryTheory.Subgroupoid.isTotallyDisconnected_iff {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : CategoryTheory.Subgroupoid.IsTotallyDisconnected S ↔ ∀ (c d : C), Set.Nonempty (CategoryTheory.Subgroupoid.arrows S c d) → c = d

def CategoryTheory.Subgroupoid.disconnect {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : CategoryTheory.Subgroupoid C

The isotropy subgroupoid of S

theorem CategoryTheory.Subgroupoid.disconnect_le {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : CategoryTheory.Subgroupoid.disconnect S ≤ S

theorem CategoryTheory.Subgroupoid.disconnect_normal {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) (Sn : CategoryTheory.Subgroupoid.IsNormal S) : CategoryTheory.Subgroupoid.IsNormal (CategoryTheory.Subgroupoid.disconnect S)

@[simp]

theorem CategoryTheory.Subgroupoid.mem_disconnect_objs_iff {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c : C} : c ∈ CategoryTheory.Subgroupoid.objs (CategoryTheory.Subgroupoid.disconnect S) ↔ c ∈ CategoryTheory.Subgroupoid.objs S

theorem CategoryTheory.Subgroupoid.disconnect_objs {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : CategoryTheory.Subgroupoid.objs (CategoryTheory.Subgroupoid.disconnect S) = CategoryTheory.Subgroupoid.objs S

theorem CategoryTheory.Subgroupoid.disconnect_isTotallyDisconnected {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : CategoryTheory.Subgroupoid.IsTotallyDisconnected (CategoryTheory.Subgroupoid.disconnect S)

def CategoryTheory.Subgroupoid.full {C : Type u} [CategoryTheory.Groupoid C] (D : Set C) : CategoryTheory.Subgroupoid C

The full subgroupoid on a set D : Set C

theorem CategoryTheory.Subgroupoid.full_objs {C : Type u} [CategoryTheory.Groupoid C] (D : Set C) : CategoryTheory.Subgroupoid.objs (CategoryTheory.Subgroupoid.full D) = D

@[simp]

theorem CategoryTheory.Subgroupoid.mem_full_iff {C : Type u} [CategoryTheory.Groupoid C] (D : Set C) {c : C} {d : C} {f : c ⟶ d} : f ∈ CategoryTheory.Subgroupoid.arrows (CategoryTheory.Subgroupoid.full D) c d ↔ c ∈ D ∧ d ∈ D

@[simp]

theorem CategoryTheory.Subgroupoid.mem_full_objs_iff {C : Type u} [CategoryTheory.Groupoid C] (D : Set C) {c : C} : c ∈ CategoryTheory.Subgroupoid.objs (CategoryTheory.Subgroupoid.full D) ↔ c ∈ D

@[simp]

theorem CategoryTheory.Subgroupoid.full_empty {C : Type u} [CategoryTheory.Groupoid C] : CategoryTheory.Subgroupoid.full ∅ = ⊥

@[simp]

theorem CategoryTheory.Subgroupoid.full_univ {C : Type u} [CategoryTheory.Groupoid C] : CategoryTheory.Subgroupoid.full Set.univ = ⊤

theorem CategoryTheory.Subgroupoid.full_mono {C : Type u} [CategoryTheory.Groupoid C] {D : Set C} {E : Set C} (h : D ≤ E) : CategoryTheory.Subgroupoid.full D ≤ CategoryTheory.Subgroupoid.full E

theorem CategoryTheory.Subgroupoid.full_arrow_eq_iff {C : Type u} [CategoryTheory.Groupoid C] (D : Set C) {c : ↑(CategoryTheory.Subgroupoid.objs (CategoryTheory.Subgroupoid.full D))} {d : ↑(CategoryTheory.Subgroupoid.objs (CategoryTheory.Subgroupoid.full D))} {f : c ⟶ d} {g : c ⟶ d} : f = g ↔ ↑f = ↑g