μ_forget_apply — Mathlib

English

The μ-map for forget AddCommGrpCat is the identity on pairs: μ forget (p,q) = (p,q).

Русский

μ-функция забывания AddCommGrpCat действует как тождественный отображение на пары.

LaTeX

$$μ_{forget AddCommGrpCat}(G,H)(p,q) = (p,q)$$

Lean4

@[simp]
theorem μ_forget_apply {G H : AddCommGrpCat.{u}} (p : G) (q : H) :
    Functor.LaxMonoidal.μ (forget AddCommGrpCat.{u}) G H (p, q) = (p, q) :=
  by
  apply Prod.ext
  · exact congrFun (Functor.Monoidal.μ_fst (forget AddCommGrpCat.{u}) G H) (p, q)
  · exact congrFun (Functor.Monoidal.μ_snd (forget AddCommGrpCat.{u}) G H) (p, q)

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