Mathlib Map

Theorems · Inductive type · group theory

CategoryTheory.Subgroupoid

(C : Type u) → [CategoryTheory.Groupoid C] → Type (max u u_1)

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

Defined in
Mathlib.CategoryTheory.Groupoid.Subgroupoid
Cited by
75 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Assumes
CategoryTheory.Groupoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.Subgroupoid.arrows · cited by 53Subgroupoid.arrowsCategoryTheory.Subgroupoid.objs · cited by 29Subgroupoid.objsCategoryTheory.Subgroupoid.IsNormal · cited by 15Subgroupoid.IsNormalCategoryTheory.Subgroupoid.map · cited by 10Subgroupoid.mapCategoryTheory.Subgroupoid.comap · cited by 8Subgroupoid.comapCategoryTheory.Subgroupoid.full · cited by 7Subgroupoid.fullCategoryTheory.Subgroupoid.IsNormal.conj · cited by 6IsNormal.conjCategoryTheory.Subgroupoid.IsWide.wide · cited by 6IsWide.wideCategoryTheory.Subgroupoid.inv · cited by 6Subgroupoid.invCategoryTheory.Subgroupoid.Map.Arrows · cited by 5Map.ArrowsCategoryTheory.Subgroupoid.IsWide · cited by 5Subgroupoid.IsWideCategoryTheory.Subgroupoid.disconnect · cited by 5Subgroupoid.disconnectCategoryTheory.Subgroupoid.inclusion · cited by 5Subgroupoid.inclusionCategoryTheory.Subgroupoid.mul · cited by 5Subgroupoid.mulCategoryTheory.Subgroupoid.IsNormal.toIsWide · cited by 4IsNormal.toIsWideCategoryTheory.Groupoid · cited by 182CategoryTheory.GroupoidCategoryTheory.SubgroupoidCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by108

Results whose statement or proof uses this declaration.