Structures · Category theory
CategoryTheory.IsGroupoid
A Prop-valued typeclass asserting that a given category is a groupoid.
- Defined in
- Mathlib.CategoryTheory.Groupoid
- Shape
- One type argument · adds all_isIso
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every CategoryTheory.IsGroupoid is also a
Concrete types that are instances4
- CategoryTheory.Discrete
- CategoryTheory.MorphismProperty.Localization
- CategoryTheory.InducedCategory
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by9
- CategoryTheory.InducedCategory.isGroupoid
- CategoryTheory.ObjectProperty.isCodetecting_bot_of_isGroupoid
- CategoryTheory.isGroupoidPi
- CategoryTheory.isGroupoidProd
- CategoryTheory.Groupoid.ofIsGroupoid
- CategoryTheory.ObjectProperty.isDetecting_bot_of_isGroupoid
- CategoryTheory.isGroupoid_of_reflects_iso
- CategoryTheory.IsGroupoid.all_isIso
- CategoryTheory.Limits.instPreservesLimitsOfShapeOppositeOfIsGroupoid
Ancestors18
- AlgebraicGeometry.IsAffineHom
- AlgebraicGeometry.IsClosedImmersion
- AlgebraicGeometry.IsDominant
- AlgebraicGeometry.IsFinite
- AlgebraicGeometry.IsImmersion
- AlgebraicGeometry.IsIntegralHom
- AlgebraicGeometry.IsPreimmersion
- AlgebraicGeometry.IsProper
- AlgebraicGeometry.IsSchemeTheoreticallyDominant
- AlgebraicGeometry.IsSeparated
- AlgebraicGeometry.LocallyOfFiniteType
- AlgebraicGeometry.LocallyQuasiFinite
- AlgebraicGeometry.QuasiCompact
- AlgebraicGeometry.QuasiSeparated
- AlgebraicGeometry.Surjective
- AlgebraicGeometry.SurjectiveOnStalks
- AlgebraicGeometry.UniversallyClosed
- CategoryTheory.IsIso