English
The associativity diagram of a group object is Cartesian; i.e., the relevant square is a pullback.
Русский
Диаграмма ассоциативности объекта группы является декартовой; соответствующий квадрат является вытяжкой.
LaTeX
$$$IsPullback (\mu \triangleright A) ((\alpha_A A A).hom \gg (A \triangleleft \mu)) \mu \mu$$$
Lean4
/-- Morphisms of group objects preserve inverses. -/
@[reassoc (attr := simp)]
theorem inv_hom [GrpObj A] [GrpObj B] (f : A ⟶ B) [IsMonHom f] : ι ≫ f = f ≫ ι :=
by
suffices lift (lift f (ι ≫ f)) f = lift (lift f (f ≫ ι)) f by simpa using (this =≫ fst _ _) =≫ snd _ _
apply (isPullback B).hom_ext <;> apply CartesianMonoidalCategory.hom_ext <;>
simp [lift_inv_comp_right, lift_inv_comp_left]
