Theorems · Definition · category theory
GrpCat.ofHom
{X Y : Type u} → [inst : Group X] → [inst_1 : Group Y] → (X →* Y) → (GrpCat.of X ⟶ GrpCat.of Y)Typecheck a MonoidHom as a morphism in GrpCat.
- Defined in
- Mathlib.Algebra.Category.Grp.Basic
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement · cited by 32,603
- Groupstatement and proof · cited by 6,238
- MonoidHomstatement and proof · cited by 3,629
- GrpCatstatement · cited by 146
- GrpCat.ofstatement · cited by 32
- CategoryTheory.ConcreteCategory.ofHomproof · cited by 18
Cited by43
Results whose statement or proof uses this declaration.
- CategoryTheory.yonedaGrpproof · cited by 9
- CategoryTheory.yonedaGrpObjproof · cited by 9
- GrpCat.shrinkFunctorproof · cited by 6
- CategoryTheory.PreGaloisCategory.autGaloisSystemproof · cited by 6
- ProfiniteGrp.ProfiniteCompletion.etaproof · cited by 6
- AddGrpCat.toGrpproof · cited by 4
- MulEquiv.toGrpIsoproof · cited by 4
- MonCat.unitsproof · cited by 3
- GrpCat.shrinkFunctorMapproof · cited by 2
- GrpCat.uliftFunctorproof · cited by 2
- GrpCat.binaryProductLimitConeproof · cited by 2
- FiniteGrp.ofHomproof · cited by 1