English
The forgetful functor forget₂Mon C is full: it surjects on hom-sets from group objects to monoid objects.
Русский
Потеряющий функтор forget₂Mon C является полнотой: отображает все множества гомоморфизмов между группоподобными объектами на моноидальные.
LaTeX
$$$\text{forget}_{2\mathrm{Mon}}(C) \text{ is full}$$$
Lean4
/-- The associativity diagram of a group object is Cartesian.
In fact, any monoid object whose associativity diagram is Cartesian can be made into a group object
(we do not prove this in this file), so we should expect that many properties of group objects
follow from this result. -/
theorem isPullback (A : C) [GrpObj A] : IsPullback (μ ▷ A) ((α_ A A A).hom ≫ (A ◁ μ)) μ μ
where
w := by simp
isLimit' :=
Nonempty.intro <|
PullbackCone.IsLimit.mk _
(fun s => lift (lift (s.snd ≫ fst _ _) (lift (s.snd ≫ fst _ _ ≫ ι) (s.fst ≫ fst _ _) ≫ μ)) (s.fst ≫ snd _ _))
(by
refine fun s => CartesianMonoidalCategory.hom_ext _ _ ?_ (by simp)
simp only [lift_whiskerRight, lift_fst]
rw [← lift_lift_assoc, ← assoc, lift_comp_inv_right, lift_comp_one_left])
(by
refine fun s => CartesianMonoidalCategory.hom_ext _ _ (by simp) ?_
simp only [lift_lift_associator_hom_assoc, lift_whiskerLeft, lift_snd]
have : lift (s.snd ≫ fst _ _ ≫ ι) (s.fst ≫ fst _ _) ≫ μ = lift (s.snd ≫ snd _ _) (s.fst ≫ snd _ _ ≫ ι) ≫ μ :=
by
rw [← assoc s.fst, eq_lift_inv_right, lift_lift_assoc, ← assoc s.snd, lift_inv_left_eq, lift_comp_fst_snd,
lift_comp_fst_snd, s.condition]
rw [this, lift_lift_assoc, ← assoc, lift_comp_inv_left, lift_comp_one_right])
(by
intro s m hm₁ hm₂
refine CartesianMonoidalCategory.hom_ext _ _ (CartesianMonoidalCategory.hom_ext _ _ ?_ ?_) ?_
· simpa using hm₂ =≫ fst _ _
· have h : m ≫ fst _ _ ≫ fst _ _ = s.snd ≫ fst _ _ := by simpa using hm₂ =≫ fst _ _
have := hm₁ =≫ fst _ _
simp only [assoc, whiskerRight_fst, lift_fst, lift_snd] at this ⊢
rw [← assoc, ← lift_comp_fst_snd (m ≫ _), assoc, assoc, h] at this
rwa [← assoc s.snd, eq_lift_inv_left]
· simpa using hm₁ =≫ snd _ _)
