English
Simplified associativity/identity lemmas for the Monoid structure on Hom(X,M) hold, i.e., standard monoid laws for the defined multiplication and unit coincide with category-theoretic constructions.
Русский
Упрощённые леммы ассоциативности и единичности для моноида на Hom(X,M) выполняются; стандартные законы моноида согласованы с конструциями из категории.
LaTeX
$$$\\text{(monoid laws)}$$$
Lean4
/-- If `M` is a monoid object, then `Hom(X, M)` has a monoid structure. -/
abbrev monoid : Monoid (X ⟶ M) where
mul f₁ f₂ := lift f₁ f₂ ≫ μ
mul_assoc f₁ f₂
f₃ := by
change lift (lift f₁ f₂ ≫ μ) f₃ ≫ μ = lift f₁ (lift f₂ f₃ ≫ μ) ≫ μ
trans lift (lift f₁ f₂) f₃ ≫ μ ▷ M ≫ μ
· rw [← tensorHom_id, lift_map_assoc, Category.comp_id]
trans lift f₁ (lift f₂ f₃) ≫ M ◁ μ ≫ μ
· rw [MonObj.mul_assoc]
simp_rw [← Category.assoc]
congr 2
ext <;> simp
· rw [← id_tensorHom, lift_map_assoc, Category.comp_id]
one := toUnit X ≫ η
one_mul
f := by
change lift (toUnit _ ≫ η) f ≫ μ = f
rw [← Category.comp_id f, ← lift_map_assoc, tensorHom_id, MonObj.one_mul, Category.comp_id, leftUnitor_hom]
exact lift_snd _ _
mul_one
f := by
change lift f (toUnit _ ≫ η) ≫ μ = f
rw [← Category.comp_id f, ← lift_map_assoc, id_tensorHom, MonObj.mul_one, Category.comp_id, rightUnitor_hom]
exact lift_fst _ _
