Subgroupoid

📁 Source: Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean

Statistics

Metric	Count
Definitions Subgroupoid, Arrows, IsThin, IsTotallyDisconnected, IsWide, Arrows, arrows, asWideQuiver, comap, disconnect, discrete, full, generated, generatedNormal, hom, im, inclusion, instBot, instCompleteLattice, instInfSet, instInhabited, instMin, instPartialOrder, instSetLikeSigmaHom, instTop, ker, map, objs, toSet, vertexSubgroup	30
Theorems conj, conj', conjugation_bij, generatedNormal_le, toIsWide, vertexSubgroup, eqToHom_mem, id_mem, wide, arrows_iff, coe_comp_coe, coe_inv_coe, coe_inv_coe', comap_comp, comap_mono, disconnect_isTotallyDisconnected, disconnect_le, disconnect_normal, disconnect_objs, discrete_isNormal, ext, ext_iff, full_arrow_eq_iff, full_empty, full_mono, full_objs, full_univ, galoisConnection_map_comap, generatedNormal_isNormal, generated_le_generatedNormal, faithful, inj_on_objects, id_mem_of_nonempty_isotropy, id_mem_of_src, id_mem_of_tgt, inclusion_comp_embedding, inclusion_faithful, inclusion_inj_on_objects, inclusion_refl, inclusion_trans, inv, inv_mem_iff, isNormal_comap, isNormal_map, isThin_iff, isTotallyDisconnected_iff, isWide_iff_objs_eq_univ, ker_comp, ker_isNormal, le_comap_map, le_iff, le_objs, map_comap_le, map_le_iff_le_comap, map_mono, map_objs_eq, mem_disconnect_objs_iff, mem_discrete_iff, mem_full_iff, mem_full_objs_iff, mem_iff, mem_im_iff, mem_im_objs_iff, mem_ker_iff, mem_map_iff, mem_map_objs_iff, mem_objs_of_src, mem_objs_of_tgt, mem_sInf, mem_sInf_arrows, mem_top, mem_top_objs, mul, mul_mem_cancel_left, mul_mem_cancel_right, obj_surjective_of_im_eq_top, sInf_isNormal, subset_generated, top_isNormal	79
Total	109

CategoryTheory

Definitions

Name	Category	Theorems
Subgroupoid 📖	CompData	20 math math: Subgroupoid.map_comap_le, Subgroupoid.full_empty, Subgroupoid.disconnect_le, Subgroupoid.le_iff, Subgroupoid.inclusion_refl, Subgroupoid.le_comap_map, Subgroupoid.IsNormal.generatedNormal_le, Subgroupoid.mem_sInf, Subgroupoid.generated_le_generatedNormal, Subgroupoid.comap_comp, Subgroupoid.full_univ, Subgroupoid.top_isNormal, Subgroupoid.mem_top_objs, Subgroupoid.mem_iff, Subgroupoid.mem_top, Subgroupoid.map_le_iff_le_comap, Subgroupoid.sInf_isNormal, Subgroupoid.mem_sInf_arrows, Subgroupoid.galoisConnection_map_comap, Subgroupoid.full_mono

CategoryTheory.Subgroupoid

Definitions

Name	Category	Theorems
IsThin 📖	MathDef	1 math math: isThin_iff
IsTotallyDisconnected 📖	MathDef	2 math math: isTotallyDisconnected_iff, disconnect_isTotallyDisconnected
IsWide 📖	CompData	2 math math: IsNormal.toIsWide, isWide_iff_objs_eq_univ
arrows 📖	CompOp	23 math math: full_arrow_eq_iff, le_iff, IsWide.eqToHom_mem, coe_comp_coe, mem_discrete_iff, mem_map_iff, IsWide.wide, isThin_iff, IsNormal.generatedNormal_le, mem_ker_iff, IsWide.id_mem, ext_iff, IsNormal.conjugation_bij, coe_inv_coe', coe_inv_coe, inv_mem_iff, mem_full_iff, mem_iff, subset_generated, mem_im_iff, mem_top, id_mem_of_nonempty_isotropy, mem_sInf_arrows
asWideQuiver 📖	CompOp	—
comap 📖	CompOp	8 math math: map_comap_le, le_comap_map, comap_mono, comap_comp, isNormal_comap, map_le_iff_le_comap, ker_comp, galoisConnection_map_comap
disconnect 📖	CompOp	5 math math: disconnect_le, mem_disconnect_objs_iff, disconnect_isTotallyDisconnected, disconnect_objs, disconnect_normal
discrete 📖	CompOp	2 math math: mem_discrete_iff, discrete_isNormal
full 📖	CompOp	7 math math: full_empty, full_arrow_eq_iff, mem_full_objs_iff, full_univ, full_objs, mem_full_iff, full_mono
generated 📖	CompOp	2 math math: generated_le_generatedNormal, subset_generated
generatedNormal 📖	CompOp	3 math math: generatedNormal_isNormal, IsNormal.generatedNormal_le, generated_le_generatedNormal
hom 📖	CompOp	3 math math: hom.faithful, hom.inj_on_objects, inclusion_comp_embedding
im 📖	CompOp	2 math math: mem_im_iff, mem_im_objs_iff
inclusion 📖	CompOp	5 math math: inclusion_inj_on_objects, inclusion_refl, inclusion_trans, inclusion_faithful, inclusion_comp_embedding
instBot 📖	CompOp	1 math math: full_empty
instCompleteLattice 📖	CompOp	—
instInfSet 📖	CompOp	3 math math: mem_sInf, sInf_isNormal, mem_sInf_arrows
instInhabited 📖	CompOp	—
instMin 📖	CompOp	—
instPartialOrder 📖	CompOp	10 math math: map_comap_le, disconnect_le, le_iff, inclusion_refl, le_comap_map, IsNormal.generatedNormal_le, generated_le_generatedNormal, map_le_iff_le_comap, galoisConnection_map_comap, full_mono
instSetLikeSigmaHom 📖	CompOp	2 math math: mem_sInf, mem_iff
instTop 📖	CompOp	4 math math: full_univ, top_isNormal, mem_top_objs, mem_top
ker 📖	CompOp	3 math math: mem_ker_iff, ker_isNormal, ker_comp
map 📖	CompOp	9 math math: map_comap_le, map_mono, le_comap_map, mem_map_iff, isNormal_map, mem_map_objs_iff, map_le_iff_le_comap, galoisConnection_map_comap, map_objs_eq
objs 📖	CompOp	24 math math: full_arrow_eq_iff, inclusion_inj_on_objects, inclusion_refl, coe_comp_coe, isThin_iff, hom.faithful, mem_disconnect_objs_iff, isWide_iff_objs_eq_univ, mem_objs_of_src, mem_full_objs_iff, coe_inv_coe', full_objs, coe_inv_coe, mem_top_objs, mem_map_objs_iff, inclusion_trans, le_objs, mem_im_objs_iff, hom.inj_on_objects, disconnect_objs, inclusion_faithful, inclusion_comp_embedding, mem_objs_of_tgt, map_objs_eq
toSet 📖	CompOp	—
vertexSubgroup 📖	CompOp	1 math math: IsNormal.vertexSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp_coe 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership objs arrows CategoryTheory.CategoryStruct.comp Set.Elem coe	—	—
coe_inv_coe 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership objs arrows CategoryTheory.Groupoid.inv Set.Elem coe	—	—
coe_inv_coe' 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership objs arrows CategoryTheory.inv Set.Elem coe CategoryTheory.IsGroupoid.all_isIso CategoryTheory.instIsGroupoid	—	CategoryTheory.IsGroupoid.all_isIso CategoryTheory.instIsGroupoid
comap_comp 📖	mathematical	—	comap CategoryTheory.Functor.comp CategoryTheory.Groupoid.toCategory CategoryTheory.Subgroupoid	—	—
comap_mono 📖	mathematical	CategoryTheory.Subgroupoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	comap	—	—
disconnect_isTotallyDisconnected 📖	mathematical	—	IsTotallyDisconnected disconnect	—	isTotallyDisconnected_iff
disconnect_le 📖	mathematical	—	CategoryTheory.Subgroupoid Preorder.toLE PartialOrder.toPreorder instPartialOrder disconnect	—	le_iff
disconnect_normal 📖	mathematical	IsNormal	disconnect	—	IsWide.wide IsNormal.toIsWide IsNormal.conj
disconnect_objs 📖	mathematical	—	objs disconnect	—	Set.ext mem_disconnect_objs_iff
discrete_isNormal 📖	mathematical	—	IsNormal discrete	—	CategoryTheory.IsIso.of_groupoid CategoryTheory.Groupoid.inv_eq_inv CategoryTheory.Category.id_comp CategoryTheory.IsIso.inv_hom_id
ext 📖	—	arrows	—	—	—
ext_iff 📖	mathematical	—	arrows	—	ext
full_arrow_eq_iff 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership objs full arrows	—	—
full_empty 📖	mathematical	—	full Set Set.instEmptyCollection Bot.bot CategoryTheory.Subgroupoid instBot	—	ext Set.ext
full_mono 📖	mathematical	Set Set.instLE	CategoryTheory.Subgroupoid Preorder.toLE PartialOrder.toPreorder instPartialOrder full	—	le_iff
full_objs 📖	mathematical	—	objs full	—	Set.ext
full_univ 📖	mathematical	—	full Set.univ Top.top CategoryTheory.Subgroupoid instTop	—	ext Set.ext
galoisConnection_map_comap 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory	GaloisConnection CategoryTheory.Subgroupoid PartialOrder.toPreorder instPartialOrder map comap	—	—
generatedNormal_isNormal 📖	mathematical	—	IsNormal generatedNormal	—	sInf_isNormal
generated_le_generatedNormal 📖	mathematical	—	CategoryTheory.Subgroupoid Preorder.toLE PartialOrder.toPreorder instPartialOrder generated generatedNormal	—	sInf_le_sInf
id_mem_of_nonempty_isotropy 📖	mathematical	Set Set.instMembership objs	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory arrows CategoryTheory.CategoryStruct.id	—	CategoryTheory.IsIso.of_groupoid CategoryTheory.Groupoid.inv_eq_inv CategoryTheory.IsIso.hom_inv_id mul inv
id_mem_of_src 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership arrows	CategoryTheory.CategoryStruct.id	—	id_mem_of_nonempty_isotropy mem_objs_of_src
id_mem_of_tgt 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership arrows	CategoryTheory.CategoryStruct.id	—	id_mem_of_nonempty_isotropy mem_objs_of_tgt
inclusion_comp_embedding 📖	mathematical	CategoryTheory.Subgroupoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	CategoryTheory.Functor.comp Set.Elem objs CategoryTheory.Groupoid.toCategory coe inclusion hom	—	—
inclusion_faithful 📖	mathematical	CategoryTheory.Subgroupoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	Quiver.Hom Set.Elem objs CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory coe CategoryTheory.Functor.obj inclusion CategoryTheory.Functor.map	—	—
inclusion_inj_on_objects 📖	mathematical	CategoryTheory.Subgroupoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	Set.Elem objs CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory coe inclusion	—	—
inclusion_refl 📖	mathematical	—	inclusion le_refl CategoryTheory.Subgroupoid PartialOrder.toPreorder instPartialOrder CategoryTheory.Functor.id Set.Elem objs CategoryTheory.Groupoid.toCategory coe	—	CategoryTheory.Functor.hext le_refl
inclusion_trans 📖	mathematical	CategoryTheory.Subgroupoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	inclusion LE.le.trans CategoryTheory.Functor.comp Set.Elem objs CategoryTheory.Groupoid.toCategory coe	—	LE.le.trans
inv 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership arrows	CategoryTheory.Groupoid.inv	—	—
inv_mem_iff 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership arrows CategoryTheory.Groupoid.inv	—	CategoryTheory.IsIso.of_groupoid CategoryTheory.Groupoid.inv_eq_inv CategoryTheory.IsIso.inv_inv inv
isNormal_comap 📖	mathematical	IsNormal	comap	—	comap.eq_1 Set.mem_setOf CategoryTheory.Functor.map_id IsWide.wide IsNormal.toIsWide CategoryTheory.IsIso.of_groupoid CategoryTheory.Groupoid.inv_eq_inv CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_isIso CategoryTheory.Functor.map_inv IsNormal.conj
isNormal_map 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory im Top.top CategoryTheory.Subgroupoid instTop IsNormal	map	—	obj_surjective_of_im_eq_top CategoryTheory.Functor.map_id IsWide.wide IsNormal.toIsWide mem_map_iff mem_top_objs mem_im_objs_iff mem_im_iff CategoryTheory.IsIso.of_groupoid Map.Arrows.congr_simp CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Groupoid.inv_eq_inv IsNormal.conj CategoryTheory.Functor.map_isIso CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_inv
isThin_iff 📖	mathematical	—	IsThin Set.Elem Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership objs arrows	—	CategoryTheory.Groupoid.isThin_iff
isTotallyDisconnected_iff 📖	mathematical	—	IsTotallyDisconnected	—	mem_objs_of_src mem_objs_of_tgt
isWide_iff_objs_eq_univ 📖	mathematical	—	IsWide objs Set.univ	—	Set.ext mem_objs_of_src IsWide.wide le_of_eq Set.mem_univ id_mem_of_src
ker_comp 📖	mathematical	—	ker CategoryTheory.Functor.comp CategoryTheory.Groupoid.toCategory comap	—	—
ker_isNormal 📖	mathematical	—	IsNormal ker	—	isNormal_comap discrete_isNormal
le_comap_map 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory	CategoryTheory.Subgroupoid Preorder.toLE PartialOrder.toPreorder instPartialOrder comap map	—	GaloisConnection.le_u_l galoisConnection_map_comap
le_iff 📖	mathematical	—	CategoryTheory.Subgroupoid Preorder.toLE PartialOrder.toPreorder instPartialOrder Set Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set.instHasSubset arrows	—	SetLike.le_def instIsConcreteLE Sigma.forall
le_objs 📖	mathematical	CategoryTheory.Subgroupoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	Set Set.instHasSubset objs	—	—
map_comap_le 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory	CategoryTheory.Subgroupoid Preorder.toLE PartialOrder.toPreorder instPartialOrder map comap	—	GaloisConnection.l_u_le galoisConnection_map_comap
map_le_iff_le_comap 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory	CategoryTheory.Subgroupoid Preorder.toLE PartialOrder.toPreorder instPartialOrder map comap	—	GaloisConnection.le_iff_le galoisConnection_map_comap
map_mono 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory CategoryTheory.Subgroupoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	map	—	GaloisConnection.monotone_l galoisConnection_map_comap
map_objs_eq 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory	objs map Set.image	—	Set.ext mem_map_objs_iff
mem_disconnect_objs_iff 📖	mathematical	—	Set Set.instMembership objs disconnect	—	—
mem_discrete_iff 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership arrows discrete CategoryTheory.eqToHom	—	—
mem_full_iff 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership arrows full	—	—
mem_full_objs_iff 📖	mathematical	—	Set Set.instMembership objs full	—	full_objs
mem_iff 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory CategoryTheory.Subgroupoid SetLike.instMembership instSetLikeSigmaHom Set Set.instMembership arrows	—	—
mem_im_iff 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Set Set.instMembership arrows im CategoryTheory.CategoryStruct.comp CategoryTheory.eqToHom CategoryTheory.Functor.map	—	Map.arrows_iff
mem_im_objs_iff 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory	Set Set.instMembership objs im	—	—
mem_ker_iff 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership arrows ker CategoryTheory.Functor.map CategoryTheory.eqToHom CategoryTheory.Functor.obj	—	mem_discrete_iff
mem_map_iff 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Set Set.instMembership arrows map CategoryTheory.CategoryStruct.comp CategoryTheory.eqToHom CategoryTheory.Functor.map	—	Map.arrows_iff
mem_map_objs_iff 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory	Set Set.instMembership objs map	—	Map.arrows_iff mem_objs_of_src
mem_objs_of_src 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership arrows	objs	—	mul inv
mem_objs_of_tgt 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership arrows	objs	—	mul inv
mem_sInf 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory CategoryTheory.Subgroupoid SetLike.instMembership instSetLikeSigmaHom InfSet.sInf instInfSet	—	mem_sInf_arrows
mem_sInf_arrows 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership arrows InfSet.sInf CategoryTheory.Subgroupoid instInfSet	—	Set.mem_iInter₂
mem_top 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership arrows Top.top CategoryTheory.Subgroupoid instTop	—	—
mem_top_objs 📖	mathematical	—	Set Set.instMembership objs Top.top CategoryTheory.Subgroupoid instTop	—	One.instNonempty
mul 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership arrows	CategoryTheory.CategoryStruct.comp	—	—
mul_mem_cancel_left 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership arrows	CategoryTheory.CategoryStruct.comp	—	mul inv CategoryTheory.IsIso.of_groupoid CategoryTheory.Groupoid.inv_eq_inv CategoryTheory.IsIso.inv_hom_id_assoc
mul_mem_cancel_right 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership arrows	CategoryTheory.CategoryStruct.comp	—	mul inv CategoryTheory.IsIso.of_groupoid CategoryTheory.Groupoid.inv_eq_inv CategoryTheory.Category.assoc CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.comp_id
obj_surjective_of_im_eq_top 📖	—	CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory im Top.top CategoryTheory.Subgroupoid instTop	—	—	mem_im_objs_iff mem_top_objs
sInf_isNormal 📖	mathematical	IsNormal	InfSet.sInf CategoryTheory.Subgroupoid instInfSet	—	IsWide.wide IsNormal.toIsWide IsNormal.conj
subset_generated 📖	mathematical	—	Set Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set.instHasSubset arrows generated	—	—
top_isNormal 📖	mathematical	—	IsNormal Top.top CategoryTheory.Subgroupoid instTop	—	—

CategoryTheory.Subgroupoid.Discrete

Definitions

Name	Category	Theorems
Arrows 📖	CompData	—

CategoryTheory.Subgroupoid.IsNormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conj 📖	mathematical	CategoryTheory.Subgroupoid.IsNormal Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership CategoryTheory.Subgroupoid.arrows	CategoryTheory.CategoryStruct.comp CategoryTheory.Groupoid.inv	—	—
conj' 📖	mathematical	CategoryTheory.Subgroupoid.IsNormal Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership CategoryTheory.Subgroupoid.arrows	CategoryTheory.CategoryStruct.comp CategoryTheory.Groupoid.inv	—	CategoryTheory.IsIso.of_groupoid CategoryTheory.Groupoid.inv_eq_inv CategoryTheory.IsIso.inv_inv conj
conjugation_bij 📖	mathematical	CategoryTheory.Subgroupoid.IsNormal	Set.BijOn Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Groupoid.inv CategoryTheory.Subgroupoid.arrows	—	conj CategoryTheory.IsGroupoid.all_isIso CategoryTheory.instIsGroupoid CategoryTheory.IsIso.of_groupoid CategoryTheory.Groupoid.inv_eq_inv CategoryTheory.Category.assoc CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.IsIso.hom_inv_id_assoc CategoryTheory.whisker_eq CategoryTheory.eq_whisker conj' CategoryTheory.IsIso.inv_hom_id CategoryTheory.IsIso.inv_hom_id_assoc
generatedNormal_le 📖	mathematical	CategoryTheory.Subgroupoid.IsNormal	CategoryTheory.Subgroupoid Preorder.toLE PartialOrder.toPreorder CategoryTheory.Subgroupoid.instPartialOrder CategoryTheory.Subgroupoid.generatedNormal Set Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set.instHasSubset CategoryTheory.Subgroupoid.arrows	—	CategoryTheory.Subgroupoid.generated_le_generatedNormal HasSubset.Subset.trans Set.instIsTransSubset CategoryTheory.Subgroupoid.subset_generated CategoryTheory.Subgroupoid.le_iff sInf_le
toIsWide 📖	mathematical	CategoryTheory.Subgroupoid.IsNormal	CategoryTheory.Subgroupoid.IsWide	—	—
vertexSubgroup 📖	mathematical	CategoryTheory.Subgroupoid.IsNormal Set Set.instMembership CategoryTheory.Subgroupoid.objs	Subgroup.Normal Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory CategoryTheory.Groupoid.vertexGroup CategoryTheory.Subgroupoid.vertexSubgroup	—	mul_assoc conj'

CategoryTheory.Subgroupoid.IsWide

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqToHom_mem 📖	mathematical	CategoryTheory.Subgroupoid.IsWide	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership CategoryTheory.Subgroupoid.arrows CategoryTheory.eqToHom	—	id_mem
id_mem 📖	mathematical	CategoryTheory.Subgroupoid.IsWide	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership CategoryTheory.Subgroupoid.arrows CategoryTheory.CategoryStruct.id	—	wide
wide 📖	mathematical	CategoryTheory.Subgroupoid.IsWide	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory Set Set.instMembership CategoryTheory.Subgroupoid.arrows CategoryTheory.CategoryStruct.id	—	—

CategoryTheory.Subgroupoid.Map

Definitions

Name	Category	Theorems
Arrows 📖	CompData	1 math math: arrows_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arrows_iff 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory	Arrows CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom CategoryTheory.Functor.map	—	CategoryTheory.eq_conj_eqToHom

CategoryTheory.Subgroupoid.hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithful 📖	mathematical	—	Quiver.Hom Set.Elem CategoryTheory.Subgroupoid.objs CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory CategoryTheory.Subgroupoid.coe CategoryTheory.Functor.obj CategoryTheory.Subgroupoid.hom CategoryTheory.Functor.map	—	—
inj_on_objects 📖	mathematical	—	Set.Elem CategoryTheory.Subgroupoid.objs CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory CategoryTheory.Subgroupoid.coe CategoryTheory.Subgroupoid.hom	—	—

---

← Back to Index