Documentation

structure CategoryTheory.Subgroupoid (C : Type u) [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)
The arrow choice for each pair of vertices
inv {c d : C} {p : c ⟶ d} : p ∈ self.arrows c d → 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 → CategoryStruct.comp p q ∈ self.arrows c e

theorem CategoryTheory.Subgroupoid.ext_iff {C : Type u} {inst✝ : Groupoid C} {x y : Subgroupoid C} :

x = y ↔ x.arrows = y.arrows

theorem CategoryTheory.Subgroupoid.ext {C : Type u} {inst✝ : Groupoid C} {x y : Subgroupoid C} (arrows : x.arrows = y.arrows) :

x = y

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

Groupoid.inv f ∈ S.arrows d c ↔ f ∈ S.arrows c d

theorem CategoryTheory.Subgroupoid.mul_mem_cancel_left {C : Type u} [Groupoid C] (S : Subgroupoid C) {c d e : C} {f : c ⟶ d} {g : d ⟶ e} (hf : f ∈ S.arrows c d) :

CategoryStruct.comp f g ∈ S.arrows c e ↔ g ∈ S.arrows d e

theorem CategoryTheory.Subgroupoid.mul_mem_cancel_right {C : Type u} [Groupoid C] (S : Subgroupoid C) {c d e : C} {f : c ⟶ d} {g : d ⟶ e} (hg : g ∈ S.arrows d e) :

CategoryStruct.comp f g ∈ S.arrows c e ↔ f ∈ S.arrows c d

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

c ∈ S.objs → CategoryStruct.id c ∈ S.arrows c c

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

CategoryStruct.id c ∈ S.arrows c c

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

CategoryStruct.id d ∈ S.arrows d d

def CategoryTheory.Subgroupoid.asWideQuiver {C : Type u} [Groupoid C] (S : 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} [Groupoid C] (S : Subgroupoid C) :

Groupoid ↑S.objs

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_comp_coe {C : Type u} [Groupoid C] (S : Subgroupoid C) {X✝ Y✝ Z✝ : ↑S.objs} (p : ↑(S.arrows ↑X✝ ↑Y✝)) (q : ↑(S.arrows ↑Y✝ ↑Z✝)) :

↑(CategoryStruct.comp p q) = CategoryStruct.comp ↑p ↑q

theorem CategoryTheory.Subgroupoid.coe_inv_coe {C : Type u} [Groupoid C] (S : Subgroupoid C) {X✝ Y✝ : ↑S.objs} (p : ↑(S.arrows ↑X✝ ↑Y✝)) :

↑(Groupoid.inv p) = Groupoid.inv ↑p

@[simp]

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

↑(inv p) = inv ↑p

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

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} [Groupoid C] (S : Subgroupoid C) :

Function.Injective S.hom.obj

theorem CategoryTheory.Subgroupoid.hom.faithful {C : Type u} [Groupoid C] (S : Subgroupoid C) (c d : ↑S.objs) :

Function.Injective fun (f : c ⟶ d) => S.hom.map f

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

SetLike (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} [Groupoid C] (S : 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} [Groupoid C] (S T : Subgroupoid C) :

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

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

Top (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} [Groupoid C] {c d : C} (f : c ⟶ d) :

f ∈ ⊤.arrows c d

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

c ∈ ⊤.objs

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

Bot (Subgroupoid C)

Equations

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

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

Inhabited (Subgroupoid C)

Equations

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

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

Min (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} [Groupoid C] :

InfSet (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} [Groupoid C] {s : Set (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} [Groupoid C] {s : Set (Subgroupoid C)} {p : (c : C) × (d : C) × (c ⟶ d)} :

p ∈ sInf s ↔ ∀ S ∈ s, p ∈ S

instance CategoryTheory.Subgroupoid.instCompleteLattice {C : Type u} [Groupoid C] :

CompleteLattice (Subgroupoid C)

Equations

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

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

S.objs ⊆ T.objs

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

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} [Groupoid C] {S T : Subgroupoid C} (h : S ≤ T) :

Function.Injective (inclusion h).obj

theorem CategoryTheory.Subgroupoid.inclusion_faithful {C : Type u} [Groupoid C] {S T : Subgroupoid C} (h : S ≤ T) (s t : ↑S.objs) :

Function.Injective fun (f : s ⟶ t) => (inclusion h).map f

theorem CategoryTheory.Subgroupoid.inclusion_refl {C : Type u} [Groupoid C] {S : Subgroupoid C} :

inclusion ⋯ = Functor.id ↑S.objs

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

inclusion ⋯ = (inclusion k).comp (inclusion h)

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

(inclusion h).comp T.hom = S.hom

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

(c ⟶ d) → Prop

The family of arrows of the discrete groupoid

id {C : Type u} [Groupoid C] (c : C) : Arrows c c (CategoryStruct.id c)

def CategoryTheory.Subgroupoid.discrete {C : Type u} [Groupoid 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} [Groupoid C] {c d : C} (f : c ⟶ d) :

f ∈ discrete.arrows c d ↔ ∃ (h : c = d), f = eqToHom h

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

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

wide (c : C) : CategoryStruct.id c ∈ S.arrows c c

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

S.IsWide ↔ S.objs = Set.univ

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

CategoryStruct.id c ∈ S.arrows c c

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

eqToHom h ∈ S.arrows c d

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

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

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

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

γ ∈ S.arrows c c → CategoryStruct.comp p (CategoryStruct.comp γ (Groupoid.inv p)) ∈ S.arrows d d

theorem CategoryTheory.Subgroupoid.IsNormal.conjugation_bij {C : Type u} [Groupoid C] (S : Subgroupoid C) (Sn : S.IsNormal) {c d : C} (p : c ⟶ d) :

Set.BijOn (fun (γ : c ⟶ c) => CategoryStruct.comp (Groupoid.inv p) (CategoryStruct.comp γ p)) (S.arrows c c) (S.arrows d d)

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

⊤.IsNormal

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

(sInf s).IsNormal

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

discrete.IsNormal

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

(S.vertexSubgroup cS).Normal

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

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} [Groupoid C] (X : (c d : C) → Set (c ⟶ d)) (c d : C) :

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

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

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} [Groupoid C] (X : (c d : C) → Set (c ⟶ d)) :

generated X ≤ generatedNormal X

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

(generatedNormal X).IsNormal

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

generatedNormal X ≤ S ↔ ∀ (c d : C), X c d ⊆ S.arrows c d

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

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} [Groupoid C] {D : Type u_1} [Groupoid D] (φ : Functor C D) (S T : Subgroupoid D) :

S ≤ T → comap φ S ≤ comap φ T

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

(comap φ S).IsNormal

@[simp]

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

comap (φ.comp ψ) = comap φ ∘ comap ψ

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

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} [Groupoid C] {D : Type u_1} [Groupoid D] (φ : Functor C D) {c d : C} (f : c ⟶ d) :

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

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

(ker φ).IsNormal

@[simp]

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

ker (φ.comp ψ) = comap φ (ker ψ)

inductive CategoryTheory.Subgroupoid.Map.Arrows {C : Type u} [Groupoid C] {D : Type u_1} [Groupoid D] (φ : Functor C D) (hφ : Function.Injective φ.obj) (S : 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} [Groupoid C] {D : Type u_1} [Groupoid D] {φ : Functor C D} {hφ : Function.Injective φ.obj} {S : Subgroupoid C} {c d : C} (f : c ⟶ d) (hf : f ∈ S.arrows c d) : Arrows φ hφ S (φ.obj c) (φ.obj d) (φ.map f)

theorem CategoryTheory.Subgroupoid.Map.arrows_iff {C : Type u} [Groupoid C] {D : Type u_1} [Groupoid D] (φ : Functor C D) (hφ : Function.Injective φ.obj) (S : Subgroupoid C) {c d : D} (f : c ⟶ d) :

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 = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (φ.map g) (eqToHom hb))

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

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} [Groupoid C] {D : Type u_1} [Groupoid D] (φ : Functor C D) (hφ : Function.Injective φ.obj) (S : Subgroupoid C) {c d : D} (f : c ⟶ d) :

f ∈ (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 = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (φ.map g) (eqToHom hb))

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

GaloisConnection (map φ hφ) (comap φ)

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

S ≤ T → map φ hφ S ≤ map φ hφ T

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

S ≤ comap φ (map φ hφ S)

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

map φ hφ (comap φ T) ≤ T

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

map φ hφ S ≤ T ↔ S ≤ comap φ T

theorem CategoryTheory.Subgroupoid.mem_map_objs_iff {C : Type u} [Groupoid C] (S : Subgroupoid C) {D : Type u_1} [Groupoid D] (φ : Functor C D) (hφ : Function.Injective φ.obj) (d : D) :

d ∈ (map φ hφ S).objs ↔ ∃ c ∈ S.objs, φ.obj c = d

@[simp]

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

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

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

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} [Groupoid C] {D : Type u_1} [Groupoid D] (φ : Functor C D) (hφ : Function.Injective φ.obj) {c d : D} (f : c ⟶ d) :

f ∈ (im φ hφ).arrows c d ↔ ∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d), f = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (φ.map g) (eqToHom hb))

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

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

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

Function.Surjective φ.obj

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

(map φ hφ S).IsNormal

@[reducible, inline]

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

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} [Groupoid C] (S : Subgroupoid C) :

S.IsThin ↔ ∀ (c : ↑S.objs), Subsingleton ↑(S.arrows ↑c ↑c)

@[reducible, inline]

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

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} [Groupoid C] (S : Subgroupoid C) :

S.IsTotallyDisconnected ↔ ∀ (c d : C), (S.arrows c d).Nonempty → c = d

def CategoryTheory.Subgroupoid.disconnect {C : Type u} [Groupoid C] (S : 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} [Groupoid C] (S : Subgroupoid C) :

S.disconnect ≤ S

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

S.disconnect.IsNormal

@[simp]

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

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

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

S.disconnect.objs = S.objs

S.disconnect.IsTotallyDisconnected

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

def CategoryTheory.Subgroupoid.full {C : Type u} [Groupoid C] (D : Set 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} [Groupoid C] (D : Set C) :

(full D).objs = D

@[simp]

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

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

@[simp]

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

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

@[simp]

theorem CategoryTheory.Subgroupoid.full_empty {C : Type u} [Groupoid C] :

full ∅ = ⊥

@[simp]

theorem CategoryTheory.Subgroupoid.full_univ {C : Type u} [Groupoid C] :

full Set.univ = ⊤

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

full D ≤ full E