isMonHom_preimage — Mathlib

English

Under a fully faithful functor, preimages of Mon morphisms are Mon morphisms.

Русский

Под полностью верным функтором предобраз моноидного гомоморфизма является моноидный гомоморфизм.

LaTeX

$$$\\text{F.F.}.isMonHom\\_preimage$$$

Lean4

instance isMonHom_preimage (hF : F.FullyFaithful) {X Y : C} [MonObj X] [MonObj Y] (f : F.obj X ⟶ F.obj Y) [IsMonHom f] :
    IsMonHom (hF.preimage f)
    where
  one_hom := hF.map_injective <| by simp [← obj.η_def_assoc, ← obj.η_def, ← cancel_epi (ε F)]
  mul_hom :=
    hF.map_injective <| by simp [← obj.μ_def_assoc, ← obj.μ_def, ← μ_natural_assoc, ← cancel_epi (LaxMonoidal.μ F ..)]

Похожие утверждения