noncommPiCoprod — Mathlib

English

For a fixed index i, the noncommPiCoprod evaluated at the elementary element that is y at i and identity elsewhere equals ϕ_i(y).

Русский

Для фиксированного индекса i, noncommPiCoprod на элементе, в котором на позиции i стоит y, а в остальных единицы, даёт ϕ_i(y).

LaTeX

$$$\\text{noncommPiCoprod } ϕ hcomm (\\Pi\\text{mulSingle } i y) = ϕ(i)(y).$$$

Lean4

/-- The canonical homomorphism from a family of monoids. -/
@[to_additive /-- The canonical homomorphism from a family of additive monoids. See also
    `LinearMap.lsum` for a linear version without the commutativity assumption. -/
    ]
def noncommPiCoprod : (∀ i : ι, N i) →* M
    where
  toFun f := Finset.univ.noncommProd (fun i => ϕ i (f i)) fun _ _ _ _ h => hcomm h _ _
  map_one' := by
    apply (Finset.noncommProd_eq_pow_card _ _ _ _ _).trans (one_pow _)
    simp
  map_mul' f
    g := by
    classical
    convert @Finset.noncommProd_mul_distrib _ _ _ _ (fun i => ϕ i (f i)) (fun i => ϕ i (g i)) _ _ _
    · exact map_mul _ _ _
    · rintro i - j - h
      exact hcomm h _ _

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