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)

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

• arrows : (c d : C) → Set (c ⟶ d)
• inv : ∀ {c d : C} {p : c ⟶ d}, p ∈ self.arrows c d → CategoryTheory.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 → CategoryTheory.CategoryStruct.comp p q ∈ self.arrows c e

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 ∈ S.arrows d c ↔ f ∈ S.arrows 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 ∈ 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

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

Equations

• CategoryTheory.Subgroupoid.objs S = {c : C | Set.Nonempty (S.arrows c c)}

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 ∈ S.arrows 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 ∈ S.arrows 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 ∈ S.arrows 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 ∈ S.arrows c d) : CategoryTheory.CategoryStruct.id c ∈ S.arrows 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 ∈ S.arrows c d) : CategoryTheory.CategoryStruct.id d ∈ S.arrows 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

Equations

• CategoryTheory.Subgroupoid.asWideQuiver S = { Hom := fun (c d : C) => Subtype (S.arrows c d) }

@[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

Equations

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

@[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

Equations

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

theorem CategoryTheory.Subgroupoid.hom.inj_on_objects {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : Function.Injective (CategoryTheory.Subgroupoid.hom S).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 : c ⟶ d) => (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

Equations

• CategoryTheory.Subgroupoid.vertexSubgroup S hc = { toSubmonoid := { toSubsemigroup := { carrier := S.arrows c c, mul_mem' := ⋯ }, one_mem' := ⋯ }, inv_mem' := ⋯ }

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}

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

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

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

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

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)

Equations

• CategoryTheory.Subgroupoid.instBotSubgroupoid = { bot := { arrows := fun (x x_1 : C) => ∅, inv := ⋯, mul := ⋯ } }

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

Equations

• CategoryTheory.Subgroupoid.instInhabitedSubgroupoid = { default := ⊤ }

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

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 := ⋯ } }

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

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

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

Equations

• CategoryTheory.Subgroupoid.instCompleteLatticeSubgroupoid = let __src := completeLatticeOfInf (CategoryTheory.Subgroupoid C) ⋯; CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

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

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).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 : s ⟶ t) => (CategoryTheory.Subgroupoid.inclusion h).map f

theorem CategoryTheory.Subgroupoid.inclusion_refl {C : Type u} [CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C} : CategoryTheory.Subgroupoid.inclusion ⋯ = 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 ⋯ = 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

The family of arrows of the discrete groupoid

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

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

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

Equations

• CategoryTheory.Subgroupoid.discrete = { arrows := fun (c d : C) => {p : c ⟶ d | CategoryTheory.Subgroupoid.Discrete.Arrows c d p}, inv := ⋯, mul := ⋯ }

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

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

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

• wide : ∀ (c : C), CategoryTheory.CategoryStruct.id c ∈ S.arrows c 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 ∈ S.arrows 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 ∈ S.arrows c d

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

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

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

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} : γ ∈ S.arrows c c → CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp γ (CategoryTheory.Groupoid.inv p)) ∈ S.arrows 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 (γ : c ⟶ c) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv p) (CategoryTheory.CategoryStruct.comp γ p)) (S.arrows c c) (S.arrows 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 ∈ 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

Equations

• CategoryTheory.Subgroupoid.generated X = sInf {S : CategoryTheory.Subgroupoid C | ∀ (c d : C), X c d ⊆ S.arrows c d}

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.generated X).arrows 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

Equations

• CategoryTheory.Subgroupoid.generatedNormal X = sInf {S : CategoryTheory.Subgroupoid C | (∀ (c d : C), X c d ⊆ S.arrows c d) ∧ CategoryTheory.Subgroupoid.IsNormal S}

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 ⊆ S.arrows 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.

Equations

• CategoryTheory.Subgroupoid.comap φ S = { arrows := fun (c d : C) => {f : c ⟶ d | φ.map f ∈ S.arrows (φ.obj c) (φ.obj d)}, inv := ⋯, mul := ⋯ }

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.

Equations

• CategoryTheory.Subgroupoid.ker φ = CategoryTheory.Subgroupoid.comap φ CategoryTheory.Subgroupoid.discrete

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

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

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

• 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 ∈ S.arrows c d, CategoryTheory.Subgroupoid.Map.Arrows φ hφ S (φ.obj c) (φ.obj d) (φ.map f)

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

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

Equations

• CategoryTheory.Subgroupoid.map φ hφ S = { arrows := fun (c d : D) => {x : c ⟶ d | CategoryTheory.Subgroupoid.Map.Arrows φ hφ S c d x}, inv := ⋯, mul := ⋯ }

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

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 ∈ 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

Equations

• CategoryTheory.Subgroupoid.im φ hφ = CategoryTheory.Subgroupoid.map φ hφ ⊤

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

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

Equations

• CategoryTheory.Subgroupoid.IsThin S = Quiver.IsThin ↑(CategoryTheory.Subgroupoid.objs S)

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 ↑(S.arrows ↑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.

Equations

• CategoryTheory.Subgroupoid.IsTotallyDisconnected S = CategoryTheory.Groupoid.IsTotallyDisconnected ↑(CategoryTheory.Subgroupoid.objs S)

theorem CategoryTheory.Subgroupoid.isTotallyDisconnected_iff {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) : CategoryTheory.Subgroupoid.IsTotallyDisconnected S ↔ ∀ (c d : C), Set.Nonempty (S.arrows 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

Equations

• CategoryTheory.Subgroupoid.disconnect S = { arrows := fun (c d : C) => {f : c ⟶ d | c = d ∧ f ∈ S.arrows c d}, inv := ⋯, mul := ⋯ }

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

Equations

• CategoryTheory.Subgroupoid.full D = { arrows := fun (c d : C) => {_f : c ⟶ d | c ∈ D ∧ d ∈ D}, inv := ⋯, mul := ⋯ }

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.full D).arrows 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