Theorems · Inductive type · category theory

CategoryTheory.IsAddMonHom.Normal

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {G H : C} → [CategoryTheory.AddGrpObj G] → [CategoryTheory.AddGrpObj H] → (H ⟶ G) → Prop

A morphism φ : H ⟶ G of additive group objects is a normal monoid homomorphism if it is a monoid homomorphism that is mono and such that the conjugation map (g, h) ↦ g + h - g factors through φ.

Defined in

Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Cited by

4 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.CartesianMonoidalCategoryCategoryTheory.AddGrpObjCategoryTheory.AddGrpObj