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

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.ext {C : Type u} {inst✝ : CategoryTheory.Groupoid C} {x y : CategoryTheory.Subgroupoid C} (arrows : x.arrows = y.arrows) : x = y

theorem CategoryTheory.Subgroupoid.inv_mem_iff {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid 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 d 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 d 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

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

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

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

theorem CategoryTheory.Subgroupoid.id_mem_of_nonempty_isotropy {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) (c : C) : c ∈ S.objs → 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 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 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

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

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

The coercion of a subgroupoid as a groupoid

Equations

• S.coe = CategoryTheory.Groupoid.mk (fun {X Y : ↑S.objs} (p : X ⟶ Y) => ⟨CategoryTheory.Groupoid.inv ↑p, ⋯⟩) ⋯ ⋯

@[simp]

theorem CategoryTheory.Subgroupoid.coe_comp_coe {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {X✝ Y✝ Z✝ : ↑S.objs} (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✝ : ↑S.objs} (p : X✝ ⟶ Y✝) : ↑(CategoryTheory.Groupoid.inv p) = CategoryTheory.Groupoid.inv ↑p

@[simp]

theorem CategoryTheory.Subgroupoid.coe_inv_coe' {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c d : ↑S.objs} (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 (↑S.objs) C

The embedding of the coerced subgroupoid to its parent

Equations

• S.hom = { obj := fun (c : ↑S.objs) => ↑c, map := fun {X Y : ↑S.objs} (f : X ⟶ Y) => ↑f, map_id := ⋯, map_comp := ⋯ }

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

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

def CategoryTheory.Subgroupoid.vertexSubgroup {C : Type u} [CategoryTheory.Groupoid C] (S : CategoryTheory.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.vertexSubgroup hc = { 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.instSetLikeSigmaHom {C : Type u} [CategoryTheory.Groupoid C] : SetLike (CategoryTheory.Subgroupoid C) ((c : C) × (d : C) × (c ⟶ d))

Equations

• CategoryTheory.Subgroupoid.instSetLikeSigmaHom = { 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 T : CategoryTheory.Subgroupoid C) : S ≤ T ↔ ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d

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

Equations

• CategoryTheory.Subgroupoid.instTop = { top := { arrows := fun (x x_1 : C) => Set.univ, inv := ⋯, mul := ⋯ } }

theorem CategoryTheory.Subgroupoid.mem_top {C : Type u} [CategoryTheory.Groupoid 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 ∈ ⊤.objs

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

Equations

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

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

Equations

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

instance CategoryTheory.Subgroupoid.instMin {C : Type u} [CategoryTheory.Groupoid C] : Min (CategoryTheory.Subgroupoid C)

Equations

• CategoryTheory.Subgroupoid.instMin = { min := fun (S T : CategoryTheory.Subgroupoid C) => { arrows := fun (c d : C) => S.arrows c d ∩ T.arrows c d, inv := ⋯, mul := ⋯ } }

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

Equations

• CategoryTheory.Subgroupoid.instInfSet = { sInf := fun (s : Set (CategoryTheory.Subgroupoid C)) => { arrows := fun (c d : C) => ⋂ S ∈ s, S.arrows c d, inv := ⋯, mul := ⋯ } }

theorem CategoryTheory.Subgroupoid.mem_sInf_arrows {C : Type u} [CategoryTheory.Groupoid C] {s : Set (CategoryTheory.Subgroupoid 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.instCompleteLattice {C : Type u} [CategoryTheory.Groupoid C] : CompleteLattice (CategoryTheory.Subgroupoid C)

Equations

• CategoryTheory.Subgroupoid.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

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

The functor associated to the embedding of subgroupoids

Equations

• CategoryTheory.Subgroupoid.inclusion h = { obj := fun (s : ↑S.objs) => ⟨↑s, ⋯⟩, map := fun {X Y : ↑S.objs} (f : X ⟶ Y) => ⟨↑f, ⋯⟩, map_id := ⋯, map_comp := ⋯ }

theorem CategoryTheory.Subgroupoid.inclusion_inj_on_objects {C : Type u} [CategoryTheory.Groupoid C] {S 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 T : CategoryTheory.Subgroupoid C} (h : S ≤ T) (s t : ↑S.objs) : 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 ↑S.objs

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

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

inductive CategoryTheory.Subgroupoid.Discrete.Arrows {C : Type u} [CategoryTheory.Groupoid 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 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) : S.IsWide ↔ S.objs = Set.univ

theorem CategoryTheory.Subgroupoid.IsWide.id_mem {C : Type u} [CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C} (Sw : S.IsWide) (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 : S.IsWide) {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 S.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 : S.IsNormal) {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 : S.IsNormal) {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] : ⊤.IsNormal

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

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

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

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 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) ∧ S.IsNormal}

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.generatedNormal X).IsNormal

theorem CategoryTheory.Subgroupoid.IsNormal.generatedNormal_le {C : Type u} [CategoryTheory.Groupoid C] (X : (c d : C) → Set (c ⟶ d)) {S : CategoryTheory.Subgroupoid C} (Sn : S.IsNormal) : 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 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 : S.IsNormal) : (CategoryTheory.Subgroupoid.comap φ S).IsNormal

@[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 (φ.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 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.ker φ).IsNormal

@[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 (φ.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) : (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} (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} (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 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.map φ hφ S).objs ↔ ∃ c ∈ S.objs, φ.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.map φ hφ S).objs = φ.obj '' S.objs

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} (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.im φ hφ).objs ↔ ∃ (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 : S.IsNormal) : (CategoryTheory.Subgroupoid.map φ hφ S).IsNormal

@[reducible, inline]

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

• S.IsThin = Quiver.IsThin ↑S.objs

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

@[reducible, inline]

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

• S.IsTotallyDisconnected = CategoryTheory.Groupoid.IsTotallyDisconnected ↑S.objs

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

• S.disconnect = { 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) : S.disconnect ≤ S

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

@[simp]

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

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

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

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

@[simp]

theorem CategoryTheory.Subgroupoid.mem_full_iff {C : Type u} [CategoryTheory.Groupoid C] (D : Set 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.full D).objs ↔ 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 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 d : ↑(CategoryTheory.Subgroupoid.full D).objs} {f g : c ⟶ d} : f = g ↔ ↑f = ↑g