Theorems · Definition · category theory
CategoryTheory.Grp.homMk
{C : Type u₁} →
[inst : CategoryTheory.Category.{v₁, u₁} C] →
[inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
{A B : CategoryTheory.Grp C} → (f : A.X ⟶ B.X) → [CategoryTheory.IsMonHom f] → A ⟶ BConstruct a morphism A ⟶ B of Grp C from a map f : A.X ⟶ A.X and a IsMonHom f
instance.
- Defined in
- Mathlib.CategoryTheory.Monoidal.Grp
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.CartesianMonoidalCategorystatement and proof · cited by 947
- CategoryTheory.Grpstatement and proof · cited by 144
- CategoryTheory.Grp.Xstatement and proof · cited by 99
- CategoryTheory.IsMonHomstatement and proof · cited by 56
- CategoryTheory.Grp.homMk'proof · cited by 2
Cited by6
Results whose statement or proof uses this declaration.
- CategoryTheory.Grp.homMk''proof · cited by 4
- CategoryTheory.Grp.ofHomproof · cited by 1
- CategoryTheory.GrpObj.div_compproof · cited by 1
- CategoryTheory.GrpObj.zpow_compproof · cited by 1
- CategoryTheory.Grp.homMk_hom_homstatement and proof · cited by 0
- CategoryTheory.Grp.homMk.congr_simpstatement and proof · cited by 0